The Logic E

Here is a Hilbert-style axiomatisation of the logic \(\mathbf{E}\) of relevant entailment.

Our language contains propositional variables, parentheses, negation, conjunction, and implication. In addition, we use the following defined connectives:

\[\begin{align} A\vee B &=_{df} \neg(\neg A \amp \neg B) \\ A \leftrightarrow B &=_{df} (A \rightarrow B) \amp(B \rightarrow A) \end{align}\]

	Axiom Scheme	Axiom Name
1.	\(A \rightarrow A\)	Identity
2.	\(((A \rightarrow A) \rightarrow B) \rightarrow B\)	EntT
3.	\((A \rightarrow B) \rightarrow((B \rightarrow C) \rightarrow(A \rightarrow C))\)	Suffixing
4.	\((A \rightarrow(A \rightarrow B)) \rightarrow(A \rightarrow B)\)	Contraction
5.	\((A \amp B) \rightarrow A,(A \amp B) \rightarrow B\)	& -Elimination
6.	\(A \rightarrow(A\vee B), B \rightarrow(A\vee B)\)	\(\vee\)-Introduction
7.	\(((A \rightarrow B) \amp(A \rightarrow C)) \rightarrow(A \rightarrow(B \amp C))\)	& -Introduction
8.	\(((A\vee B) \rightarrow C)\leftrightarrow((A \rightarrow C) \amp(B \rightarrow C))\)	\(\vee\)-Elimination
9.	\((A \amp(B\vee C)) \rightarrow((A \amp B)\vee(A \amp C))\)	Distribution
10.	\((A \rightarrow \neg B) \rightarrow(B \rightarrow \neg A)\)	Contraposition
11.	\(\neg \neg A \rightarrow A\)	Double Negation

	Rule	Name
1.	\(A \rightarrow B, A\vdash B\)	Modus Ponens
2.	\(A, B\vdash A \amp B\)	Adjunction