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:

AB =_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 → (AB), B → (AB)	-Introduction
7.	((A → B) & (A → B)) → (A → (B & C))	& -Introduction
8.	((AB) → C)↔((A → B) & (A → C))	-Elimination
9.	(A & (BC)) → ((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