The fundamental S-theorem - A corollary (Q793001)

The relevant logic S is given by the following schemata. \[ Axioms:\quad(B)\quad B\to(C).\quad A\to B\to.\quad A\to C\quad(B^ 1)\quad A\to B\to.\quad B\to(C)\to.A\to C \] \[ Rules:\quad(B)\quad B\to C\Rightarrow A\to B\to.\quad A\to C\quad(B^ 1)\quad A\to B\Rightarrow B\to C\to.\quad A\to C\quad(BB)\quad B\to C,\quad A\to B\Rightarrow A\to C. \] The logic P-W is given by S \(+\) the axiom schema \(A\to A\). It was conjectured by Belnap that both \(A\to B\) and \(B\to A\) are theorems of P-W only if A is B. This was proved equivalent by Powers to the proposition that no formula of the form \(A\to A\) is a theorem of S. A number of other equivalents were known. The problem remained unsolved for a long time, until answered in the positive by Martin. This paper proves another two equivalents: let \(\Delta A=_{df}A\to A.\) Then (1) \(\Delta\) \(A\to \Delta B\) is a theorem of P-W iff A is a subformula of B, and (2) \(\Delta\) \(A\to \Delta B\) is a theorem of S iff A is a proper subformula of B. The authors intend these results to reinforce their thesis that Aristotelian Syllogistic is basic logic and that S is the correct propositional expression of it.