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:
- (first k-incompleteness) Which $T$s are k-incomplete for every $k$?
(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$ ?
(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?
Are there theories that become eventually $k$-incomplete for a sufficiently large $k$ ?
- (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?