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$?

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?