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.

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.

share|improve this question

2 Answers 2

up vote 8 down vote accepted

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.

share|improve this answer
4  
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.

share|improve this answer

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.