9
$\begingroup$

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?

Lucas

$\endgroup$
6
  • 1
    $\begingroup$ A related question: mathoverflow.net/questions/48365/… $\endgroup$ Mar 2, 2014 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$ Mar 2, 2014 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$ Mar 3, 2014 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$ Mar 3, 2014 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$ Mar 3, 2014 at 17:02

1 Answer 1

10
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ Those are the more obvious ones. But can you also drop unnecessary nesting of quantifyers? $\endgroup$
    – Lucas K.
    Mar 2, 2014 at 21:18
  • $\begingroup$ @LucasK. Not really, see KP: en.wikipedia.org/wiki/Kripke%E2%80%93Platek_set_theory $\endgroup$ Mar 2, 2014 at 21:37
  • 5
    $\begingroup$ @LucasK. : $\:$ If you can't drop them, then they're not unnecessary. $\;\;\;\;$ $\endgroup$
    – user5810
    Mar 3, 2014 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, 2014 at 21:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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