How Does the Number of Lines of a Proof Change If Expanding a Condensed Detachment Proof into a Simultaneous Substitution and Detachment Proof?

For every condensed detachment proof, there exists a substitution and detachment proof.

If both the antecedent of the major premise, e. g. one having form C$\alpha$$\beta or (p \rightarrow q) or (p) \rightarrow (q) or pqC or C(p, q), or (p, q)i, etc., and the minor premise \gamma qualify as equiform, then a condensed detachment proof corresponds to a single step substitution and detachment proof. We just make a detachment. If the antecedent of the major premise \alpha and the minor premise \gamma both require substitutions to transform them into equiform forms, then we need to make two substitutions, and one detachment to expand the condensed detachment proof into a substitution and detachment proof. Examples of such a case: Let CCzCNxNyCzCyx consist of the major premise and CCNyyCNyx as the minor, which after condensed detachment yields CCNyyCxy or any formula having the same relative positions of the variables in the formula after condensed detachment, such as CCNxxCyx or CCNaaCba, or if the major and minor premise looked differently and appropriately so ((\lnotf \rightarrow f) \rightarrow (u \rightarrow f)) etc. Or take two copies of CCCCqrCprsCCpqs and then reproduce the condensed detachment of those two copies. Often enough though, we only need to make one substitution in exclusively the major or the minor premise to expand the condensed detachment proof into a substitution and detachment proof. Thus, we require only two steps for an expansion of the condensed detachment proof into a corresponding substitution and detachment proof; a simultaneous substitution and a detachment. Meta-Theorem 1: If exclusively the antecedent of the major premise or the minor premise have exactly one instance of any propositional variable throughout the antecedent of the major premise or throughout the entire minor premise, then for any condensed detachment proof from those two premises, there exists a two line substitution and detachment proof. Meta-Proof: A most general unifier can get found simply by substituting each variable in the antecedent of the major premise or throughout the minor premise. Consequently, the substitution and detachment proof will only need one simultaneous substitution to make a detachment. Since the detachment qualifies as a step also, that makes for a two line proof as was to get metalogically demonstrated. Meta-Corollary 1: Systems with formulas of any of the following: CpCqp, CCCpqrCqr, CCCpqqCCqpp, CCCpqrCCprr, CCCpqrCCrpp, CCpqCCqrCpr, CCpqCCrpCrq, CCpCqrCqCpr, CpCCpqq, CCpqCCCprqq, CpCCNqNpq and possibly many more do not have a last theorem under condensed detachment. Discussion: This size of the question space is a bit small to contain much of a meta-proof. But, to see how this works fix the formula selected under condensed detachment and call it a. For formulas which have only a propositional variable in the antecedent, the meta-corollary follows by substituting the minor premise in the fixed formula a for every use of condensed detachment. For some others, the antecedent of a has bracket type C\alpha$$\beta$, while any detached formula from a and any minor premise also has bracket type C$\alpha$$\beta$. For another set, the bracket type of the formula gets preserved under condensed detachment.

Given a condensed detachment proof, let us call the number of steps (lines in a proof) in any of the shortest corresponding substitution and detachment proofs, the condensed detachment expansion number, CoDEN, of a condensed detachment proof of a formula $\delta$ from a fixed major premise C($\alpha$, $\beta$) and a fixed minor premise $\gamma$, CoDEN({C($\alpha$, $\beta$), $\gamma$} $\vdash$ $\delta$), or just CoDEN for short.

Now, suppose we had a large number of condensed detachment proofs in classical propositional calculi... I don't know maybe a million or a billion or maybe just a hundred, or even just a few proofs. What is the mean value of CoDEN over all of those proofs? If we took the limit of all formal proofs as n gets larger and larger, would the mean value of CoDEN converge to a rational number or transcendental number? What would make for a suitable upper estimate and a lower estimate for the mean value of CoDEN if using it to predict the length of a minimal substitution and detachment proof from a condensed detachment proof? I'll guess between 2.0 and 2.5. Does it matter which set of formal proofs we select? Does selecting sub-theories which have their formal theorems properly contained in classical propositional logic substantially alter the mean value of CoDEN? Using a program that I wrote, and the mean value of CoDEN for the proof here is 2.25.

Related paper.

• There exist more cases when CoDEN equals two than suggested above. Exclusively, either we can substitute the variables in the antecedent of the major premise with formulas beginning with a connective symbol in the minor premise and obtain a most general unifier, or we can substitute those in the minor premise with formulas beginning with a connective symbol in the major premise. Examples, if CCpCqrCCpqCpr is the major and CpCqp the minor, then we substitute r with p in the major premise. If CCpCppCCppCpp is the major and CpCqp the minor, then we substitute q with p in the minor. – Doug Spoonwood Aug 30 '16 at 0:21