Supplement to Relevance Logic
The Logic S
Here is a Hilbert-style axiomatisation of the logic S (for “syllogism”).
Our language contains propositional variables, parentheses and one connective: implication.
| Axiom Scheme | Axiom Name | |
| 1. | (B→C) →((A→B) →(A→C)) | Prefixing |
| 2. | (A→B) →((B→C) →(A→C)) | Suffixing |
| Rule | Name |
| A → B, A ⊢ B | Modus Ponens |
The logic T-W is S with the addition of the identity axiom (A→A). Martin's theorem is that no instance of the identity axiom is a theorem of S. It is a corollary of Martin's theorem that in T-W if both A→B and B→A are provable, then A and B are the same formula (see Anderson, Belnap, and Dunn (1992) §66).