# Set theory based on different logic

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?

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.