#### 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 |