The Coq mailing list

[Pierre Courtieu <pierrecourtieu AT gmail.com>]

Hi. answering the question although not an expert on these subjects.

AFAIU it is not completely accurate to say that "Set theory and type
theory can be defined in one another" as it would imply that Set
theory can be defined in itself, which would violate Gödel's second
incompleteness theorem.
It is commonly said (although quite imprecise) to say that both set
theory and type theory have comparable expressivity.
I guess a more precise statement AFAICT would be: "Any set theory S
can be define in *some* type theory T, strictly more expressive that
S, and in turn T can be defined in *another* set theory S', strictly
more expressive than T and S, etc".
So this is not exactly a "loop".

Cross-encodings between type and set theory have been extensively
studied indeed. On set theory encoded in type theory this may be a
starting point:
https://proofassistants.stackexchange.com/questions/1525/is-there-a-standard-encoding-or-model-of-material-set-theory-in-type-theory

Best regards

Pierre


Le lun. 12 mai 2025 à 09:09, Iaroslav Baranov <kciray8 AT gmail.com> a écrit :
>
> Hi!
>
> I know that all math can be reduced to type theory (calculus of 
> constructions). Type theory rules can then be implemented using Turing 
> Machine so we can have perfect math machine which decices the correctness 
> of any mathwork. This seems astonishing and I love it. It seems to be the 
> lowest level of foundation of everything.
>
> Hovewer, the turing machine and the type theory can be expressed inside 
> themselves using set theory and logic. It seems like some kind of loop. 
> When I think about it, it seems very interesting. Has anyone thought about 
> it? Have any researchers tried to pin down this loop, extract it out and 
> formalize?
>
> Best regards,
>
> Iaroslav Baranov, Java Software Engineer
>
> kciray8 AT gmail.comtyp