About theorem's proof length in propositional calculus

Question

In PC(propositional calculus) system, how long will a formula's proof be?

That is to say if there exists a computable function $f$ such that for any formula $A$, if $\vdash_{\mathrm{PC}}A$ then $A$ has a proof with length less than $f(A)$.

Answer 1

In propositional logic, a formula is provable if and only if it is a tautology, and the set of tautologies is decidable. Moreover, for any complete and effective proof system, if we know a formula is a tautology, we can simply enumerate proofs until we find a proof of the formula. Therefore, given a formula $\phi$, we can compute the following function: if $\phi$ is not a tautology, return $1$. Otherwise, search for the first proof of $\phi$ that you find, and return the length of that proof. This function will be computable and give an affirmative answer to the question. Notice that this answer is also independent of how the "length" of a proof is defined; the answer works for any definition of "length" as long as the length of the proof is computable from the proof itself.

The situation would be very different in first-order logic. In that context, the set of provable formulas is no longer decidable, and the definition of "length" becomes very important.

Answer 2

Which formal system of the propositional calculus is in question?

There's a familiar, perfectly good formal deductive, system $S$ which has every tautology as an axiom, so in this system, if $\vdash_S A$, then there is a one-line proof of $A$!

There are other familiar, perfectly good, formal deductive systems -- say, tableaux systems -- where the notion of the "length" of a proof can't be taken for granted without any explanation (are we talking about the depth of the tree, the number of nodes, or what?).

But suppose you have in mind, say, a standard Hilbert-style system (e.g. as in Mendelson's classic text), so proofs have lengths in a straightforward sense, and there is a non-trivial question about the length of proofs. Then have a look at how you prove the completeness of such a system by Kalmar's method (as in Mendelson). This method gives in effect an algorithm for taking a tautology $\varphi$ and producing a proof of $\varphi$ -- and if you look at the details you can evidently in principle read off a computable upper bound for the length of the proof from the complexity of $\varphi$ (though details would get boringly messy).