# Starting Hilbert's Program on the other end

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?

Lucas

-
A related question: mathoverflow.net/questions/48365/… – Emil Jeřábek Mar 2 '14 at 21:09
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. – Christoph-Simon Senjak Mar 2 '14 at 21:53
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. – Thomas Klimpel Mar 3 '14 at 8:21
@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. – Emil Jeřábek Mar 3 '14 at 14:41
@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.) – Thomas Klimpel Mar 3 '14 at 17:02

@LucasK. : $\:$ If you can't drop them, then they're not unnecessary. $\;\;\;\;$ – Ricky Demer Mar 3 '14 at 0:26