11
$\begingroup$

I am not a logician or set theorist, so hopefully this makes sense. Let $T$ be a theory which is expressive enough to make statements like "Statement $A$ has a proof in $T$"; for example, $T$ might be capable of expressing elementary arithmetic and proving certain basic arithmetic facts.

Let $\Pi^0(T)$ consist of those statements $A$ in $T$ such that either $A$ or $\neg A$ admits a proof in $T$. In general, for $i\in \mathbb{N}$ let $\Pi^i(T)$ consist of those statements $A$ such that the statement "Con(T) implies that there does not exist a proof of $A$, or a proof of $\neg A$, in $T$" is in $\Pi^{i-1}(T)$. Intuitively, $\Pi^1$ should consist of those statements $A$ for which one can prove in $T$ that neither $A$ nor $\neg A$ admits a proof in $T$, $\Pi^2$ should consist of those statements $A$ such that one can prove in $T$ that one cannot tell whether or not they admit a proof, but where one knows this fact, and so on.

Godel's first incompleteness theorem implies that $\Pi^0(T)$ does not contain every sentence of $T$; in particular, the proof amounts to constructing a sentence in $\Pi^1(T)$.

Now I'm sure that if this hierarchy is not nonsense for some reason that I'm missing, then it must be well-studied. So here goes:

  1. If this set-up is studied, what is it called?
  1. In standard theories, e.g. ZFC, is every sentence contained in $\bigcup_{i\in \mathbb{N}} \Pi^i(T)$? It seems to me that any ZFC proof that this is not the case must be non-constructive, and so would be pretty interesting.
  1. Are there any standard theories $T$ of finite (known) depth in this hierarchy, i.e. every sentence is contained in $\Pi^i(T)$ for some fixed $i>0$? If so, can this be proven in $T$?
  1. One can also define this hierarchy in a relative setting; e.g. one can take two theories $T\subset S$ and ask about $S$-proofs of statements about the existence of proofs in $T$. Is this studied? Are answers to the above questions known in these cases?

Motivation: I recently watched this talk by Voevodsky, and ever since I've been wondering about how much we actually know about what we can prove. One might hope that even if we can't prove every "true" statement, then we can at least always prove that a statement does not admit a proof in our theory, if that is indeed the case. That seems unlikely, and amounts to the claim that all statements in our theory are in $\Pi^1(T)$, but I think that it is the best situation one can hope for (at least naively) given Godel's theorems. So, is the situation hopeless? Give it to me straight, doc.

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ First, note that the usual theories (like PA or ZFC) don't literally say "Statement $A$ has a proof in $T$"; what they actually do is code such statements in some way such that, in the standard model, these codes correspond in some well-understood way to actual proofs. Usually this is a minor point, but I bring it up because when you talk about a $\Pi^\alpha(T)$ hierarchy for arbitrary ordinals $\alpha$, this coding suddenly becomes problematic. As soon as $\alpha$ is infinite, you have to start worrying about how you're going to express $\Pi^\alpha(T)$ inside the theory $T$. $\endgroup$
    – Henry Towsner
    Commented Oct 29, 2010 at 22:50
  • 1
    $\begingroup$ I eliminated the ordinal claim, altered the definitions in response to your comment. Hopefully this works now? I do think the ordinal encoding does work for the relative situation I describe in (4), however. $\endgroup$
    – Daniel Litt
    Commented Oct 30, 2010 at 0:03

2 Answers 2

Reset to default
11
$\begingroup$

I believe the concept you are looking for is that of "iterated consistency extension." A very nice treatment is given by Torkel Franzén in his book Inexhaustibility: a non-exhaustive treatment. See also this related question and this blog article by Mike O'Connor.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Thanks! Since it took me a second to realize the connection between these two notions, I'll spell it out here. The consistency extension of the theory $T$ is "$T$+Con($T$)"; so $\Pi^0("$T$+Con($T$)")=\Pi^1(T)$ and so on. So $\Pi^i(T)$ are exactly the set of statements $A$ such that $A$ or $\neg A$ have proofs in the $i$-th iterated consistency extension of $T$. I haven't looked for the answers to my questions in this book yet--I'll update the question if some of them are not answered. $\endgroup$
    – Daniel Litt
    Commented Oct 30, 2010 at 21:37
  • $\begingroup$ I don't believe it's true that $\Pi^0(T+Con(T))=\Pi^1(T)$. For instance, $\Pi^0(T)\subseteq\Pi^0(T+Con(T))$ while $\Pi^1(T)\cap\Pi^0(T)=\emptyset$ for reasonable theories. $\endgroup$
    – Henry Towsner
    Commented Oct 31, 2010 at 0:31
  • $\begingroup$ Henry, I agree. Nevertheless, I think "iterated consistency extensions" is what Daniel was really aiming for... $\endgroup$
    – François G. Dorais
    Commented Oct 31, 2010 at 13:15
4
$\begingroup$

I think you'll have to at least tweak the definition of your hierarchy, since a (strong enough) consistent theory can't prove that it doesn't prove something: $T$ can prove "$\neg Con(T)$ implies that $T$ proves every formula" (where $T$ is, say, a strong enough fragment of $PA$), so $T$ proves that "if $T$ does not prove $A$ then $T$ is consistent". And of course, if $T$ proves that it is consistent, then it isn't.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Fixed, I think. $\endgroup$
    – Daniel Litt
    Commented Oct 30, 2010 at 21:34

You must log in to answer this question.

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