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, B → C ⊢ A → C | Transitivity |
| A → B ⊢ (B → C) → (A → C) | Rule Suffixing |
| B → C ⊢ (A → B) → (A → C) | Rule Prefixing |
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).