I am interested in minimal length proofs of tautologies in propositional logic. For concreteness, let's fix a particular Frege system $F$ (i.e., sound and complete set of axioms and deduction rules for propositional such as the ones here which has three axioms and modus ponens as the only deduction rule).
Given a tautology $\tau$, let $s(\tau)$ denote the minimal number of steps needed to prove $\tau$ in $F$. Here is a warm-up to my actual questions that I already do not know how to answer:
Is there some explicit sequence of tautologies $\{\tau_n\}$ with $s(\tau)$ exactly computable by some explicit nice formula (I leave that to your interpretation - an example of "nice" being say a polynomial) and with $s(\tau_n) \to \infty$?
On a related note, I'm interested in what can be said about the possible forms of minimal number of step proofs. For a proof $\pi$, let me denote by $a(\pi)$ and $m(\pi)$ the number of axiom lines in $\pi$ and modus ponens lines in $\pi$, respectively. We must have $a(\pi) \leq m(\pi) - 1$ for $\pi$ a minimal-step-number proof of some tautology.
Is there some explicit sequence of tautologies $\{\tau_n\}$ with $s(\tau_n) \to \infty$ and $a(\pi_n) = m(\pi_n) - 1$ for $\pi_n$ a minimal-step-number proof of $\tau_n$ (so these all require the minimal amount of invocations of modus ponens)?
On the opposite extreme, is there some explicit sequence of tautologies $\{\tau_n\}$ with $s(\tau_n) \to \infty$ and $a(\pi_n) = 2$ for $\pi_n$ a minimal-step-number proof of $\tau_n$ (so these require the maximal ration of modus ponens to other axioms)?
(I'm happy to hear about answers to similar questions for other Frege systems or related proof systems.)
