The Coq mailing list

[Victor Porton <porton AT narod.ru>]

23.12.2012, 01:22, "Victor Porton" 
<porton AT narod.ru>:
> There is an implementation of ZFC set theory in Coq called GAIA.
>
> I have the following thought (either smart or stupid one) for formalizing 
> set theory in Coq:
>
> In GAIA axioms are defined for type Set.
>
> What if we will exclude all axioms which lead to Russell paradox or similar 
> paradox and define the remaining axioms for a parametrized type T (where T 
> may be set or ANY other Coq type)?
>
> Then we would have a more general theory and the theory for type Set as a 
> specialized case (with additional axioms).
>
> I thought about this, considering how binary relations (Set->Set->Prop) are 
> related with sets (Set) and whether I should represent a relation as 
> Set->Set->Prop or as a special case of Set.
>
> This is my (either smart or stupid one) thoughts what a future version of 
> GAIA (or similar theories) may be. Any comments?

Sorry for polluting this Coq mailing list with my wrong idea.

I should have think more. I see that it does not work for instance with 
boolean type.

Well, maybe somebody may have a similar idea to mine, but not wrong like mine.

-- 
Victor Porton - http://portonvictor.org