On the relative consistency of the Axiom of Extensionality

Question

Who proved the relative consistency of the Axiom of Extensionality?

Answer 1

Perhaps surprisingly, the situation is a bit complicated!

Let's start with a pair of results, one positive and one negative, from the same paper. Scott showed that $\mathsf{Z-Ext}$ is equiconsistent with $\mathsf{Z}$, but $\mathsf{ZF-Ext}$ is in fact equiconsistent with ... $\mathsf{Z}$ again! So adding extensionality to $\mathsf{ZF-Ext}$ results in a huge increase in consistency strength, but adding it to $\mathsf{Z-Ext}$ doesn't change consistency strength at all.

Focusing on the $\mathsf{ZF}$-flavored situation, Scott's result relies on the exact way the $\mathsf{ZF}$ axioms are posed; specifically, it assumes that we're using replacement instead of collection. If we use collection instead, we do get equiconsistency: $\mathsf{ZF_{coll}-Ext}$ is equiconsistent with $\mathsf{ZF}$, where $\mathsf{ZF_{coll}}$ is $\mathsf{ZF}$ with the collection scheme instead of the replacement scheme. In fact, full $\mathsf{ZF}$ can be "embedded" into even intuitionistic $\mathsf{ZF_{coll}-Ext}$ in a precise sense; this was shown by Friedman. So between the Scott and Friedman results it's clear that there is a high degree of detail-sensitivity here.

Incidentally, note that the replacement/collection issue is also crucial in making sense of "$\mathsf{ZF(C)}$ without powerset" - see Gitman/Hamkins/Johnstone.

Separately, Gandy gave equiconsistency proofs for extensionality over non-extensional versions of simple type theory and NBG. Specker's proof that $\mathsf{NF+AC}$ is inconsistent, in light of the low consistency strength of $\mathsf{NFU+AC}$, can be construed as another negative observation. And finally, Enayat mentions a paper of Robinson as being relevant, but I can't get a hold of it at the moment.