The Logic S

Here is a Hilbert-style axiomatisation of the logic $\mathbf{S}$ (for “syllogism”).

Our language contains propositional variables, parentheses and one connective: implication.

The logic T-W is $\mathbf{S}$ with the addition of the identity axiom $(A\rightarrow A)$. Martin’s theorem is that no instance of the identity axiom is a theorem of $\mathbf{S}$. It is a corollary of Martin’s theorem that in T-W if both $A\rightarrow B$ and $B\rightarrow A$ are provable, then $A$ and $B$ are the same formula (see Anderson, Belnap, and Dunn (1992) §66).