The Coq mailing list

[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?

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