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

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ A related question: mathoverflow.net/questions/48365/… $\endgroup$
    – Emil Jeřábek
    Commented 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$
    – Christoph-Simon Senjak
    Commented 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$
    – Thomas Klimpel
    Commented 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$
    – Emil Jeřábek
    Commented 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$
    – Thomas Klimpel
    Commented Mar 3, 2014 at 17:02

1 Answer 1

Reset to default
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.

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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .