The late Elliot Mendelson's system in his Introduction to Mathematical Logic had an set of axiom schema for classical propositional which corresponds to the following set of axiom schema:

M1: (B -> (C -> B))

M2: ((B -> (C -> D)) -> ((B -> C) -> (B -> D)))

M3: (((~C) -> (~B)) -> (((~C) -> B) -> C))

The above are not axioms, but rather axiom schema.  The only rule of inference is modus ponens: L is a direct consequence of B and (B -> C)...

What direct consequence means I find a bit hard to state, but the general idea seems that any wff deduced must get produced must using M1, M2, or M3 or use a direct consequence of one of a previous theorem produced using M1, M2, or M3 when using modus ponens.  An indirect consequence such as making substitutions in a produced theorem is disallowed.  For doing logic and writing formal proofs this has strong disadvantages, but it has the advantage of relative simplicity for metalogical theory. 

After describing a definition of a statement letter, which I don't believe has relevance here, the following definition of a wff gets described:

2. (a) All statement letters are wfs.
    (b) If B and C are wfs, then so are (~B) and (B -> C).

Now for the following meta-theorem we will need to check the abstract form for all consequences in this system.  Basically as follows:

Case 1: Suppose that M1 gets used in a formal proof as the major premiss (the one having form... at a more abstract level, b).  Then, at a more abstract level it will have form D1: (c -> b).  I hasten to note that b here carries over from how B got instantiated as a wf in the first place.  But, in this case, what gets produced has the form of a conditional.

Case 2: Suppose that M2 gets used in a formal proof as the major premiss.  Then at a more abstract level, we infer to D2: ((b -> c) -> (b -> d)) with b, c, and d all having forms instantiated from how B, C, and D, got instantiated as wfs.  This also has the form of a conditional.

Case 3: Suppose that M3 gets used in a formal proof as the major premiss.  Then at a more abstract level, we infer to D3: (((~c) -> b) -> c) with c and b having forms instantiated from how C and B got instantiated as a wfs.  This also has the form of a conditional.

Case 4: Suppose that D1: (c -> b) gets used in a formal proof as the major premiss, with b carrying over from how B got used to formally deduce a wf of the form D1: (c -> b).  Then, we deduce D4: b.  Since b carries over from how B got used, b must qualify as following the original plan of for the above three schema.  b will thus qualify as a theorem directly instantiable from M1, M2, or M3.  Each of those is a conditional.  The minor premiss c qualifies as a theorem.  By soundness, proposition 1.12 of Mendelson's book it qualifies as a tautology.  Suppose that it consists of a statement letter.  Now all tautologies can get checked by two values for their variables, and thus two truth values suffice for this logic.  All statement letters may represent either the value of truth arbitrarily or the value of false arbitrary.  Thus, for any statement letter we may select it's truth value at will.  So, let us suppose that this b has the form of a statement letter.  We thus can choose that b is not a tautology, contradicting soundness.  Thus, b does not have the form of a statement letter.  Checking the definition of a wf again thus implies that b either has form (~x) or (x -> y).

Suppose we selected a finite-valued or infinite-valued logic to model such a formal system.  Then, we have many more choices to show that b either has form (~x) or (x -> y) similar to the above contradicting soundness.

Case 5: Suppose that D2: ((b -> c) -> (b -> d)) gets used in a formal proof as the major premiss, with b, c, and d all carrying over from B, C, and D how got used in a formal proof falling under case 2 following the original plan for wfs, and D5: (b -> c) corresponding to a substitution instance of M1, M2, or M3 following the original plan for wfs, or (b -> c) is one of the consequences of what has got produced by a formal theorem previously formally proved in the proof sequence.  Then a meaningful expression with the form D5: (b -> d)  follows, with b and d following the original plan for wfs corresponding to B and D in the formal deduction which used M2 as the major premiss to deduce ((b -> c) -> (b -> d)).  D5 has the form of a conditional.
Case 6: Suppose that D3: (((~c) -> b) -> c) gets used in a formal proof as a premiss, with c and b carrying over from how C and B when M3 got used when M3 got used to deduce (((~c) -> b) -> c) in case 3, or ((~c) -> b) has the form of one of the consequences directly produced by the definition of a formal proof or is a substitution instance of M1, M2, or M3 following the original plan for wfs.  Thus, a meaningful expression with the form D6: c would get proved.

Now, c is a formally produced theorem following the definition of a formal proof carrying over from how M3 got used above.  By soundness of the system, proposition 1.12 of Mendelson's book, it follows that this c is a tautology.  Now, similar to the above, all tautologies can get checked by two values for their variables, and thus two truth values suffice for this logic.  All statement letters may represent either the value of truth arbitrarily or the value of falsity arbitrarily.  Thus, for any statement letter we may select it's truth value at will.  So, let us suppose that this c has the form of a statement letter.  We thus choose that c takes on the value F.  But, then c is not a tautology, contradicting soundness.  But, soundness holds.  Therefore, c has the form (~x) or the form (x -> y). 

Meta-Corollary Interlude 1: If M3 gets used to produce D3, and then D3 once detached gets used to produce D6, then the antecedent of M3 has a proper subformula s (it's shorter in length than the antecedent) which also qualifies as a substitution instance of a formally provable theorem in the above system.  So does the antecedent of D3.  The antecedent of M3 is also inorganic, and so is the antecedent of D3.

Meta-Proof: By the above s and c qualify as the same formula.  Since c got substituted or instantiated as some wf from C corresponding to c also, then s has shorter length (number of symbols) than the antecedent having form ((~b) -> (~c)).  c having length 1 is shorter than ((~b) -> (~c)).  Thus, c is a proper subformula.  I would call such a formal proof, an extraction of a formula.  The soundness meta-theorem holds.  Thus, c is also a tautology.  Inorganic (a term due to Wajsberg who noticed this property about Nicod's single axiom or what it would formally get property recast as) means that a formula has a proper subformula which is also a tautology.  So, the antecedent of M3 is also inorganic.

Case 7:  Suppose that D5: (b -> d) gets used in a formal proof as a premiss, with b and d carrying over from B and D in how M2 got used according to the plan for wfs for the first detachment from an instance of M2.  Then, by a similar argument to the above concerning soundness, D7: b qualifies as a formal theorem.  I note that it could have gotten produced as in the proof sequence and thus not qualify as an instance of M1, M2, or M3.  By a similar argument to the above argument concerning soundness also, d qualifies as a formal theorem also and does not qualify as a variable.  Consequently:

Meta-Corollary Interlude 2: If the original plan for axiom schema involves M2 getting used such that an instance of D2 gets produced, and then used as a major premiss, and then an instance of D5 gets produced and then used as a major premiss, then the original antecedent F1: (B -> (C -> *D*)) has a proper subformula which is a formal theorem, and thus is inorganic.

Meta-Proof: *D* is a subformula of F1.  F1 has *D* inside of it.  Thus, *D* is a proper subformula.  By hypothesis it qualifies as provable.  By soundness, it follows that F1 is inorganic.

General Meta-Claim: For Any Schematic Axiomatic Propositional Calculus Such That a Formal Proof Can Get Carried Out to the Last Place in Polish Notation Meaningful Expressions (if the only axiom were CpCNpq, still an unlimited system, the condition fails), Then If the Formal Theory is Sound Also and Has At Least A Two-Valued Model, Then That Last Schematic Variable for Well-Formed Formulas Will Have an Equiform Variable Somewhere Else In the Plan for Formulas (this isn't new, and probably the content of much, if not all of the above isn't either):

Argument: The last place in all Polish notation meaningful expressions are propositional variables.  The soundness meta-theorem holds.  Thus, if a formal proof gets carried out to the last place, and that variable doesn't appear anywhere else in the meaningful expression for the axiom schemata, then no substitutions for that last variable were required to carry out the formal proof.  Thus, a formal proof using that axiom schemata could get changed to have no other place in the proof where that last variable appears.  That is, no substitutions came as required in the last variable to carry out the formal proof.  The soundness meta-theorem holds for the above, so the variable can get substituted by any truth value.  We select falsity.  Since the deduction gets carried out to that last point, we have a contradiction.  Therefore, that variable will appear in at least one other place in the original axiom schemata.

Corollary: The Same Applies for the Last Propositional Variable in Mendelson's System Or In Reverse Polish Notation

Argument: Rewriting definitions of so that we have something in Mendelson's system or in reverse polish or many others preserves the sequence of propositional variables in the formula.  Consequently, if the above argument qualifies as adequate, so does the corollary.

Now check the definition of a wff in Mendelson's book.  For any formal proof, case 1. got ruled out by the analysis of cases 1-7 above.  Now, I will note that the above might accurately get strongly criticized in some respects.  I might need to have several different logical alphabets for formulas for this meta-proof to work out.  They all look somewhat like this (a -> b) or like this (~a).  But, notice that they got notated D1, D2, ..., D7.  None of those symbols represent cardinal numbers.  They aren't integers.  They represent what can get thought of as the first logical order, the second logical order, and so on.  So under at least one interpretation, they can get thought of as representing different logical alphabets.

I note that I believe that all forms of possible cases has to get analyzed for this meta-proof to go through.  This indicates how a single axiom schemata can work out as simpler for some metalogical purposes, because then we have less cases to check.  E. G. if we picked CCCpqrCCrpCsp, C0p as our axiom set, we would only need to stipulate that 0 models falsity in the semantics of the logic.  Thus, 0 showing up somehow probably indicates that we had some string which wasn't a meaningful expression in the first place.  So, we go check that and almost surely learn there wasn't a well-formed formula somewhere.  We would also only need to check forms like CCabc, Cca, and s, which makes for three cases instead of seven.  Three logical orders is simpler than seven logical orders, isn't it?  Sure, there exist other disadvantages, but oh well.

The above implies the following:

Meta-Theorem on Mendelson's Formal System: There Do Not Exist Any Formal Proofs Which Yield A Statement Letter.

Consequently, all strings deduced in that system fall under the forms (~a) and (b -> c).  Each of these forms has has a left parenthesis '(' and a right parenthesis ')'. 

Therefore:

Meta-Theorem: Every formal theorem in Mendelson's formal axiomatic system begins with a left parenthesis '(' and ends with a right parenthesis ')'.

Also, string 1. on p. 28 is not an instance of axiom schema (A2).  String 2. doesn't have a left parenthesis.  So, the inference to 3. isn't in the formal system M.  And 4. and 5. don't have a left parenthesis either.  So, no step of his so-called, self-proclaimed "proof" in Lemma 1.8 belongs to L.  And the rest of his talk about propositional calculi is plagued by the same sort of syntactical problem.  When doing reasoning in formal systems, they have deep relevance.  Strangely, Mendelson seems better with writing meaningful expressions when talking about matters of semantics.

Did any of Mendelson's students even challenge him and point out that his book didn't stick to his own definitions?  If they did, did Mendelson just brush them off?

And how in the world could Kleene not have a definition of a well-formed formula or statement form or meaningful expression or some other term in his Mathematical Logic for beginners who may need clarity about syntax most *after* having written his Introduction to MetaMathematics where he at least has such a definition and even called his postulates "dramatis personae" which might suggest that he wasn't sticking to his definitions?  But that is another matter.

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α
β or (p → q) or (p) → (q) or pqC or C(p, q), or (p, q)i, etc., and the minor premise γ 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 α
and the minor premise γ 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 would consist of taking CCzCNxNyCzCyx as 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 ((¬f→ f) → (u →f)) etc. Or taking two copies of CCCCqrCprsCCpqs and then reproducing 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 the 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 or the major premise respectively, then for any condensed detachment proof, 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 in the minor premise whichever satisfies the hypothesis. 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 a in the antecedent, the meta-corollary follows directly from Meta-Theorem 1. For some others, the antecedent of a has bracket type Cαβ, while any detached formula from a also has bracket type Cαβ. 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 P, CoDEN(⊢P), 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 proof. What is the value of CoDEN over all of those proofs? If we took the limit of all formal proofs as n gets larger and larger, would CoDEN converge to a rational number or transcendental number? What would make for a suitable upper estimate and a lower estimate for CoDEN if using it to predicate 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 theories which have their formal theorems contained in classical propositional logic substantially alter the value of CoDEN? Using a program that I wrote, and perhaps I'll analyze some other proofs, the value of CoDEN for the proof here is 2.25.

Related paper