Finite versions of Godel' s incompleteness

Question

Assume you have some notion of proof complexity: for instance, at the basic level, the length of a proof, or the number of symbols used, take your pick (there are more involved measures, but for sake of simplicity I will limit myself to the above).

Now, start from some ground arithmetical theory $T$, and say that $T\vdash_k \phi$ if there is a proof of $\phi$ from $T$ of complexity $\leq k$.

I call a sentence $\phi$ $k$-godelian iff it is $k$-undecidable (i.e. neither $T\vdash_k \phi$ nor $T\vdash_k \neg\phi$ , but provable in the standard sense in the theory $T$ (and so true in $N$, for those fortunate and seemingly numerous mortals who believe in such a creature).

$T$ is $k$-incomplete if there is such a $\phi$.

Now the two questions:

1. (first k-incompleteness) Which $T$s are k-incomplete for every $k$?

   Are there theories that become eventually $k$-incomplete for a sufficiently large $k$ ?

2. (second k-incompleteness). Does any $k$-incomplete theory also satisfy the $k$-version of Godel 's second incompleteness? That is, is it true that $T$ is such that it $k$-proves its $k$-consistency only if it is $k$-inconsistent?

Answer 1

Nice questions!

For the first question, I claim that every theory $T$ is $k$-incomplete in your sense for every finite $k$. This is because every statement appears explicitly as a part of any proof of it, and when $\phi$ is any very long theorem of $T$ in comparison with $k$, then any proof of $\phi$ has at least as many symbols in it as $\phi$ does, and so by your measures $\phi$ has no proof of size $k$ and hence is $k$-Goedelian by your definition. Thus, for any given $k$, the theory $T$ is $k$-incomplete. In particular, every theory becomes $k$-incomplete.

For the second question, it seems that any decent consistent theory will prove its own $k$-consistency for any particular $k$. For example, if $T$ is consistent and extends $PA$, and probably even extending $Q$ suffices, then since $T$ really does not have any proofs of contradictions, it has none of size $k$, and since there are only finitely many proofs of this size, which can be enumerated and known to be an exhaustive list within the theory $T$, it follows that $T$ will prove that there is no proof of a contradiction in $T$ of size at most $k$. That is, for each $k$ separately, $T$ proves its own $k$-consistency.

But since this is not a $k$-proof of its own consistency, it doesn't quite answer your second question. But it shows that you have to pay attention to the precise measure of $k$-provability. For example, it isn't even clear that a $k$-inconsistent theory will necessarily $k$-prove much, since perhaps the $k$-proof of a contradiction already uses up most of the $k$ symbols, leaving little room for further deductions from that contradiction.

In light of this, we can make a negative answer to your second question as follows. Let $T$ be the theory PA + $0=1$, which is $k$-inconsistent for a very small value of $k$, perhaps $25$ or so, since the extra axiom directly contradicts an axiom of PA. But this $k$ is much too small to even state the $k$-consistency of $T$, and so $T$ will not $k$-prove its own $k$-consistency. So it violates the second $k$-incompleteness theorem, because this is a theory that is $k$-inconsistent but does not $k$-prove its own $k$-consistency, contrary to the proposed equivalence in your question.

Answer 2

The answer to the second question is negative. Consider a (first-order) theory of PA without the successor axiom like fpa. Then T is consistent and proves its own consistency. Let k be the complexity of this proof of consistency. Then trivially T is k-consistent and k-proves its k-consistency.

[the following is added in an edit] As my comment indicated, the previous remarks are not completely correct. Instead: Let T be a (first-order) theory of PA without the successor axiom like fpa. Then T is consistent and proves its own consistency. In fact, T proves:

(x)(there does not exist an x-proof of a contradiction in T). (*)

Let this proof have complexity z. Then T can prove - call this sentence S(y) -

"there does not exist a y-proof of a contradiction in T" for any y,

but its proof may have greater complexity than z; indeed, if the proof uses (*), then it will have greater complexity, by say f(y). That is, T proves S(y) with a proof of complexity no greater than z + f(y). Suppose there exists a k such that k <= z + f(k). Then T k-proves S(k), i.e. T k-proves the k-consistency of T. Since T is k-consistent, the answer to the question would therefore be negative.

Is there likely to exist k <= z + f(k)? The important step is to find k which can be referred to with complexity much less than k. If complexity is defined to be say the length of the proof, then this should be possible by defining an exponential operator and defining k to be a power of two reasonably large numbers.

Answer 3

It is important to include the axioms as well, since there is a theorem of logic that an axiom system can be changed equivalently so that any given proof can be made arbitrarily sorter, or on the contrary, longer.