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.