Are all proofs “short enough” to be computed?

The Completness Theorem in Propositional Logic says that a tautological statement has a derivation.

Does this existence imply that this derivation consists of a finite formation sequence?

I don't know if there is a conclusion, which would require infinite steps though (except for when there is an induction rule), i.e. in this sense an unexecutable proof. But I don't know why it would be excluded. If not, where is this constraint used?

And are there proofs, which can be "found", but not be done? In the sense that their idea can be seen explicitly, but they can't be executed in finite time $-$ even in prinicple.

-

Proofs/derivations are by definition finite. So yes, every tautology has a finite derivations.

Allowing proofs to be infinite would lead to absurdities such as this proof of $1=0$ in a system where $\mathscr P\to\mathscr P$ is a logical axiom:

$$\begin{array}{rll} 1.&1=0\to 1=0 & \text{Ax}\\ 2.&1=0\to 1=0 & \text{Ax}\\ 3.&1=0\to 1=0 & \text{Ax}\\ 4.&1=0\to 1=0 & \text{Ax}\\ \vdots&\vdots\\ (\infty-3).&1=0 & \text{MP}, 1, (\infty-4) \\ (\infty-2).&1=0 & \text{MP}, 1, (\infty-3) \\ (\infty-1).&1=0 & \text{MP}, 1, (\infty-2) \\ \infty.&1=0 & \text{MP}, 1, (\infty-1) \\ \end{array}$$ You can check that each line follows by a valid application of the indicated rule from lines earlier in the derivation.

In order to prove that the formal system with infinite derivations is sound, one would need to require at least that the ordering of the lines in a derivation is a well-order -- and if that is the case and every rule of inference has finitely many premises, then it can be shown that everything that has a derivation also has a finite derivation. So there's no point in considering even this kind of infinite derivations.

However, depending on the details of how you set up your formal system, it is quite possible that there are short(ish) provable statements whose derivations (though finite) must be too long to be written down anywhere inside the observable universe. Sometimes this can be helped by using more powerful rules (for example, considering the Deduction Theorem a primitive rule of inference rather than a meta-result helps tremendously in getting many proofs down in size); sometimes it cannot.

-
In any formal system to which Godel's Theorem applies there are short provable statements which require extremely long proofs, in the following sense: there is no recursive function $f(n)$ such that every provable statement of length $\le n$ has a proof of length $\le f(n)$. Otherwise we could have a decision procedure: search through all possible proofs of length $\le f(n)$. But for propositional logic you can use a truth table: there are only $O(2^n)$ cases. – Robert Israel Feb 13 '12 at 22:44
I am not sure whether infinitary logic can that easily be dismissed. Check out this wikipedia article en.wikipedia.org/wiki/Infinitary_logic – corto Feb 14 '12 at 12:05
Ordinary proof theory is full of infinite deductions, which as you say usually take the form of well-founded trees with the conclusion at the root. For example, the proof-theoretic consistency proof of Peano arithmetic begins with a finite deduction in PA and transforms it into an infinite deduction of a certain sort ending with the same conclusion. The structure of these particular infinite deductions prevents them from ending with 0=1, so that conclusion is not provable in PA either. – Carl Mummert Feb 14 '12 at 18:31

Yes, every proof in propositional logic consists of a finite formation sequence.

Yes, "proofs" can get found which can't get done in terms of real-world computing power/hand-writing. Ultimately, we have a finite amount of computing power before all of our computers cease to exist, and we as a species do also. A proof consists of a finite sequence of formulas (wffs) which ends with a theorem, where each formula gets inferred validly by a rule of inference or qualifies as an axiom. Nothing says proofs can't stupidly repeat sequences which go nowhere that the proof hasn't gone already. For example, here's a proof (in Polish notation and in a natural deduction system) of the weak law of identity:

1 | p assumption
2 | App 1 disjunction introduction
3 | KpApp 1, 2 conjunction introduction
4 | p 3 conjunction elimination
5 | App 4 disjunction introduction
6 | KpApp 4, 5 conjunction introduction
7 | p 6 conjunction elimination
8 Cpp 1-7 conditional introduction


Now, of course, there exists little point in steps 5-7 in terms of proving the theorem (and even steps 2-4, but I digress). But, proofs "exist" (in principle), which repeat the subsequence of formulas from steps 2-4 over and over again seemingly without end immediately starting after step 4, and end with Cpp after the last subsequence. So, say all the computing power in the multiverse/universe could only write 10$^{1,000,000}$ of those subsequences in any sequence of formulas. Well, a sequence of formulas with 10$^{2,000,000}$ of those subsequences, and then Cpp after that last subsequence still qualifies as a proof, even though by hypothesis the material resources to actually write such a proof don't exist (let alone any sort of being that would ever read it!).

So, yes, there exist proofs which can get "found" but not done.

-