The Logic NR

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

Our language contains propositional variables, parentheses, necessity, 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 B) \rightarrow((B \rightarrow C) \rightarrow(A \rightarrow C))\)	Suffixing
3.	\(A \rightarrow((A \rightarrow B) \rightarrow B)\)	Assertion
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
12.	\(\Box(A \rightarrow B) \rightarrow(\Box A \rightarrow \Box B)\)	K
13.	\((\Box A \amp \Box B) \rightarrow \Box(A \amp B)\)	K&

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