In the usual axiomatization of propositional logic with the $\to$ and $\lnot$ connectives, we have the modus ponens inference rule (from $p$ and $p \to q$ infer $q$) and the axiom schemes:
- $p \to (q \to p)$
- $(p \to (q \to r)) \to ((p \to q) \to (p \to r))$
- $(\lnot p \to \lnot q) \to (q \to p)$
Of these, only the second axiom scheme uses three meta-variables. I am wondering whether there is a way to replace this axiom scheme with one or more axiom schemes using at most two meta-variables.
The axioms systems listed here all seem to need at least one axiom schemes with three or more meta-variables, even for different sets of logical connectives.