2

From my current understanding these 2 theorems are talking about different things.

  1. Gödel proved that arithmetic cannot demonstrate its own consistency.
  2. Gentzen proved that arithmetic is consistent but we need additional separate system (without contradictions) for this proof.

Do I understand correctly?

Oleg Dats
  • 425

1 Answers1

2

Basically yes.

Godel's incompleteness theorem suggests the following program:

Given a theory of interest $T$, what other theories can prove $\mathit{Con}(T)$?

In particular, it would be great if we had some "strength hierarchy" for comparing different theories. In particular, it would be very nice if we could somehow measure the difficulty of proving the consistency of a given theory by an ordinal (ordinals are great things to measure with - not only are they linearly ordered, they're well-ordered, which has some nice consequences).

Gentzen's theorem demonstrates one way this program can be realized: roughly speaking, it shows that over a very weak base theory $\mathsf{PRA}$ there is a principle $\mathit{Ind}(\epsilon_0)$ related to the ordinal $\epsilon_0$ which suffices to prove $\mathit{Con}(\mathsf{PA})$. (Of course by Godel since $\mathsf{PRA}\subseteq\mathsf{PA}$ we know $\mathsf{PA}$ can't prove $\mathit{Ind}(\epsilon_0)$; meanwhile, this is optimal in the sense that $\mathsf{PA}$ does prove $\mathit{Ind}(\alpha)$ for every $\alpha<\epsilon_0$ and so $\mathsf{PRA}+\mathit{Ind}(\alpha)$ can't prove $\mathit{Con}(\mathsf{PA})$ if $\alpha<\epsilon_0$). This suggests the following refinement to the vague program immediately suggested by Godel:

Given a theory of interest $T$, what ordinal-based principle $\mathit{Ind}(\alpha)$ corresponds to $\mathit{Con}(T)$?

This is known as ordinal analysis.

Noah Schweber
  • 245,398