In HoTT book it is written that,

We note that a set-theoretic foundation has two “layers”: the deductive system of first-order logic, and, formulated inside this system, the axioms of a particular theory, such as $\sf{ZFC}$. Thus, set theory is not only about sets, but rather about the interplay between sets (the objects of the second layer) and propositions (the objects of the first layer).

This seems to suggest that if we somehow change the objects of the first layer we may expect to get a different set theory. So my questions are,

  • Does there exist any set theory such that if the underlying logic is changed (i.e., if the first layer is changed) keeping the second layer unchanged (i.e., keeping the non-logical axioms unchanged) such that the set of theorems provable are different for these different systems (assuming both of them are consistent)?

  • What is an example of such a theorem?


Such set theories do exist, for example Myhill's intuitionistic Zermelo–Fraenkel set theory (IZF) is formulated inside intuitionistic first-order logic, leaving the ZF axioms 'unchanged'.

The reason for the quotes in 'unchanged' is that it's not clear what it means for an axiom to be unchanged if you change the underlying logical system. Two classically equivalent forms of a non-logical axiom might not be equivalent in a different logical system.

In IZF, this manifests itself in that the law of excluded middle can be derived in intuitionistic first-order logic from the axiom of foundation (in its usual form)—shock horror! But classically, ZF–Foundation proves that the axiom of foundation is equivalent to $\in$-induction, and $\in$-induction does not imply the law of excluded middle under intuitionistic logic. So IZF is really ZF with the axiom of foundation replaced by $\in$-induction (and a slightly weaker form of separation is used, too). Clasically, the latter 'is' ZF, but intuitionistically it is not.

So to answer your first question, the answer is yes: IZF is an example. The axiom of foundation is an example of a theorem provable from IZF with classical logic but not provably from IZF with intuitionistic logic.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.