Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Let $S$ be a "rich enough" theory such as Peano arithmetic or ZFC ; assume that we have a complete formalization of the theory of $S$ so that we may talk about Godel numbers and the length of a proof.

Godel's sentence is constructed so that it says "I am not provable from S". Now let $n$ be a fixed integer, and consider a sentence $\phi_n$ formed likewise that says "I am not provable in at most $n$ steps from S". Then $\phi_n$ is a true statement, and if $\phi_n$ has a proof from $S$ this proof has length at least $n$. What is not clear is whether $\phi_n$ is provable from $S$. Does the answer to that question depend on the formalization we initially choose ?

share|improve this question
add comment

2 Answers

up vote 5 down vote accepted

Every true statement of the form "Such-and-such $\phi$ is not provable by a proof that contains at most $n$ symbols" is in fact provable -- the proof can consist of simply listing all strings of $n$ symbols or less and noting that neither of them is a valid proof of $\phi$.

I am fairly sure that the same holds for "at most $n$ steps" instead of "at most $n$ symbols", in any reasonable deductive system (even though the most straightforward way to represent a single "step" can often be arbitrarily long). But I can't think of a simple generic argument for this right away.

share|improve this answer
add comment

I suppose that $\phi_n$ is always provable, unless I am making some basic mistake. Given a string of length at most $n$, you can determine if it happens to be a proof for $\phi_n$. Now, just brute-seach all possible strings of length at most $n$ to see that none of them is a proof of $\phi_n$ (none can be, since $\phi_n$ is true), and you have proved $\phi_n$.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.