3
$\begingroup$

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.)

$\endgroup$

0

You must log in to answer this question.

Browse other questions tagged .