The idea of Hilbert's program was to start with a simple finitary logic and proof the consistency of more complex systems in this system. Of course, this turned out to be problematic. Even when absolute consistency is replaced by relative consistency.

But I just wondered, if someone attempted to tried it the other way. So, what is the simplest logical system X, such that X can prove the consistency of ZFC relative to X?

In other words, are there things in ZFC that can be dropped from foundational point of view?

Is there any scientific article about this?


  • 1
    $\begingroup$ A related question: mathoverflow.net/questions/48365/… $\endgroup$ – Emil Jeřábek Mar 2 '14 at 21:09
  • $\begingroup$ What do you mean by "Simple"? You can drop the axiom of choice, you can drop classical logic, as others have already said. On the other hand, why are these systems "simpler"? In theory, you could just use omega-Heiting-Arithmetic with the additional axiom that in some reasonable syntactic embedding, ZFC is consistent. $\endgroup$ – Christoph-Simon Senjak Mar 2 '14 at 21:53
  • $\begingroup$ I'm not sure whether PA is really able to prove the consistency of PA relative to PA. You probably mean "relative to the consistency of X" instead of "relative to X". Or maybe you didn't even think about what it means to talk about the consistency of ZFC within X. Note that you probably need to be able to talk about the consistency of ZFC within X if you want to prove it within X. $\endgroup$ – Thomas Klimpel Mar 3 '14 at 8:21
  • 3
    $\begingroup$ @ThomasKlimpel: The phrase “$T$ proves the consistency of $S$ relative to $U$” means $T\vdash\mathrm{Con}_U\to\mathrm{Con}_S$. I don’t understand what else could it be mistaken for. $\endgroup$ – Emil Jeřábek Mar 3 '14 at 14:41
  • $\begingroup$ @EmilJeřábek Neither the question nor the answer indicate to me that your interpretation was the intended one. As many people are confused about the true meaning of Gentzen's consistency proof of PA, already the point that "T" and "U" need not be the same theory seems to be missed. The statement might simply be assumed to have some meaning, and an independence result is taken to be a proof of equiconsistency. (There might be a theorem that this actually works in case of ZF like theories, but independence results are also available for theories that can't even talk about consistency.) $\endgroup$ – Thomas Klimpel Mar 3 '14 at 17:02

You can drop choice: ZF proves that ZFC and ZF are equiconsistent.

You can also drop excluded middle from your logic, in various ways, e.g.:

IZF proves that IZF and ZF are equiconsistent. See here.

| cite | improve this answer | |
  • 1
    $\begingroup$ Those are the more obvious ones. But can you also drop unnecessary nesting of quantifyers? $\endgroup$ – Lucas K. Mar 2 '14 at 21:18
  • $\begingroup$ @LucasK. Not really, see KP: en.wikipedia.org/wiki/Kripke%E2%80%93Platek_set_theory $\endgroup$ – François G. Dorais Mar 2 '14 at 21:37
  • 3
    $\begingroup$ @LucasK. : $\:$ If you can't drop them, then they're not unnecessary. $\;\;\;\;$ $\endgroup$ – user5810 Mar 3 '14 at 0:26
  • $\begingroup$ One way to prove that they are not necessary is to show that ZFC can prove the absolute consistency of such simplified system. Has such proof been given? I am not convinced that further simplifications are not possible. $\endgroup$ – Lucas K. Mar 4 '14 at 21:00

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.