0
$\begingroup$

What is the relation between the number of lines (or we could say steps) in a Frege style derivation of a propositional tautology, and its length in the number of symbols?

Obviously you can always add junk axioms of wathever length, but assuming an optimal proof $\pi$ in $m$ lines, for a tautology of length $n$, what can we say about the length of $\pi$?

$\endgroup$
1
$\begingroup$

Every tautology is more than one symbol long given that any variable and a connective is counted at least once. Suppose the contrary, that there exists some tautology that is just one symbol long. Then there would exist some tautology which would be a variable. But, a tautology could be false and true simultaneously, contradicting the definition of tautology. So, every tautology is more than one symbol long.

A proof is a list of tautologies, with each line of a proof as one tautology. Thus, the total number of symbols of a proof of a tautology is always greater than the number of lines of the proof.

For more precise information I think we would need to answer the shortest possible proof question such that we could predict (one of) the shortest possible proof(s) for the axioms and the tautology. However, resolving that question doesn't appear at all tractable since finding the shortest possible proofs requires an exhaustive search in some general sense, since exhaustively searching for the shortest possible proof becomes too computationally expensive for enough tautologies under some axiom sets. Even with more computing power, once another tautology gets proved, the set of provable tautologies in just one more step tends to grow very fast, even with a control rule like condensed detachment and other control rules like subsumption or others used in automated reasoning. Also, there might not be much of a pattern there, since any given the degree of variance between (one of) the shortest possible proof(s) and axioms and tautologies might have some exceptions.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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