Supplement to Relevance Logic
The Logic E
Here is a Hilbert-style axiomatisation of the logic E of relevant entailment.
Our language contains propositional variables, parentheses, negation, conjunction, and implication. In addition, we use the following defined connectives:
A∨B =df ¬(¬A & ¬B)
A ↔ B =df (A → B) & (B → A)
| Axiom Scheme | Axiom Name | |
| 1. | A → A | Identity |
| 2. | ((A → A) → B) → B | EntT |
| 3. | (A → B) → ((B → C) → (A → C)) | Suffixing |
| 4. | (A → (A → B)) → (A → B) | Contraction |
| 5. | (A & B) → A,(A & B) → B | & -Elimination |
| 6. | A → (A∨B), B → (A∨B) | ∨-Introduction |
| 7. | ((A → B) & (A → C)) → (A → (B & C)) | & -Introduction |
| 8. | ((A∨B) → C)↔((A → C) & (B → C)) | ∨-Elimination |
| 9. | (A & (B∨C)) → ((A & B)∨(A & C)) | Distribution |
| 10. | (A → ¬B) → (B → ¬A) | Contraposition |
| 11. | ¬¬A → A | Double Negation |
| Rule | Name |
| A → B, A⊢ B | Modus Ponens |
| A, B⊢ A & B | Adjunction |
