Natural Deduction
Muhammad Haris Rao
Trees
Definition: A (strict) partially ordered set is a pair $(S, <)$ where $S$ is a set and $<$ a binary relation on $S$ such that
- If $x \in S$, then not $x < x$
- If $x, y \in S$ are such that $x < y$, then not $y < x$
- If $x, y, z \in S$ are such that $x < y$ and $y < z$, then $x < z$
A tree is a partially ordered set $(T, <)$ such that if $x \in S$, then $\{ y \in T \mid y < x \}$ is well-ordered with respect to $<$. For $x \in T$, we define $o(x)$ to be the order type of $\{ y \in T \mid y < x \}$. For ordinal number $\alpha$, the $\alpha$th level of $S$ is the set of elements $x$ of $T$ such that $\{ y \in T \mid y < x \}$ has order type $\alpha$. The elements of the 0th level are called the roots of $T$. The height of $T$ is
$$
h(T) = \sup \{ o(x) + 1 \mid x \in T \}
$$
If $\{ \left( \Pi_k, \text{<}_k \right) \}_{k = 1}^n$ are trees where $n \in \mathbb{Z}_{> 0}$ with $\{ \Pi_k \}_{k = 1}^n$ mutually disjoint, and $\varphi$ an arbitrary set, we define a new tree $(\Pi, < )$ with $\Pi = \bigcup_{k = 1}^n \Pi_k \cup \{ \varphi \}$ and denoted
\begin{prooftree}
\AxiomC{$\Pi_1 \,\,\,\,\,\,\,\,\,\, \Pi_2 \,\,\,\,\,\,\,\,\,\, \Pi_3 \,\,\,\,\,\,\,\,\,\, \cdots \,\,\,\,\,\,\,\,\,\, \Pi_n$}
\UnaryInfC{$\varphi$}
\end{prooftree}
The order $<$ is defined so that $\varphi < x$ for all $x \in \bigcup_{k = 1}^n \Pi_k$, and for $x, y \in \bigcup_{k = 1}^n \Pi_k$, $x < y$ if and only if there is $k \in \{ 1, 2, \cdots, n \}$ such that $x, y \in \Pi_k$ and $x \text{<}_k y$. It is not hard to check that this will be a tree as has been claimed
While it really is necessary that the $\{ \Pi_k \}_{k = 1}^n$ be disjoint so that the above constrcution yields a tree, we will not shy away from applying this construction to arbitrary collections of trees. For this, simply make each of the trees disjoint by, for example, replacing each $x$ element of $\Pi_k$ by the ordered pair $(k, x)$ and reinterpret the order in the obvious way. This is analogous to the explicit construction of the disjoint union of sets.
Natural Deduction Using Proof Trees
We now move onto defining a proof tree. For the sequel, fix a first-order language $\mathcal{L}$. A proof tree $\Pi$ of height $n \in \omega_{> 0}$ is given by three pieces of information: a tree of height $n$, a set of $\mathcal{L}$-formulas called the premises of $\Pi$, and an $\mathcal{L}$-formula called the conclusion of $\Pi$.
A proof tree in the language $\mathcal{L}$ of height 1 is a triple determined consisting of a tree $( \{ \varphi \} , \emptyset )$, a set of premises $\{ \varphi \}$ and a conclusion $\varphi$ for some $\mathcal{L}$-formula $\varphi \in \tt{Form}(\mathcal{L})$. Such a tree is denoted
\begin{prooftree}
\AxiomC{$\varphi$}
\end{prooftree}
Given a proof tree $\Pi$ of some height $n \in \omega_{> 0}$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\varphi \in \tt{Form}(\mathcal{L})$, we write it as
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$\varphi$}
\end{prooftree}
to make the premises and conclusion clear.
After having defined proof trees of height at most $n \in \omega_{> 0}$, the proof trees of height $n + 1$ are defined in the following way:
-
Falsum Elimination: Given that
$\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conlcusion $(\bot)$
$\,\,\,\,\,\,\,\,$$\varphi \in \tt{Form}(\mathcal{L})$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$(\bot)$}
\RightLabel{$\scriptsize{\bot E}$}
\UnaryInfC{$\varphi$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma$ and conclusion $\varphi$.
-
Double Negation Elimination: Given that
$\,\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conlcusion $(\neg (\neg \varphi))$ for some $\varphi \in \tt{Form}(\mathcal{L})$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$(\neg (\neg \varphi))$}
\RightLabel{$\scriptsize{DNE}$}
\UnaryInfC{$\varphi$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma$ and conclusion $\varphi$.
-
Negation Eliminiation: Given that
$\,\,\,\,\,\,\,\,$$\Pi_1$ is a proof tree of height at most $n$ with premises $\Sigma_1 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\varphi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$\Pi_2$ is a proof tree of height at most $n$ with premises $\Sigma_2 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $(\neg \varphi)$
$\,\,\,\,\,\,\,\,$At least one of $\Pi_1, \Pi_2$ is of height $n$
Then,
\begin{prooftree}
\AxiomC{$\Sigma_1$}
\noLine
\UnaryInfC{$\Pi_1$}
\noLine
\UnaryInfC{$\varphi$}
\AxiomC{$\Sigma_2$}
\noLine
\UnaryInfC{$\Pi_2$}
\noLine
\UnaryInfC{$(\neg \varphi)$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$(\bot)$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma_1 \cup \Sigma_2$ and conclusion $(\bot)$.
-
Negation Introduction: Given that
$\,\,\,\,\,\,\,\,$$\Pi_1$ is a proof tree of height $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conlusion $(\bot)$
$\,\,\,\,\,\,\,\,$$\varphi \in \Sigma$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I}$}
\UnaryInfC{$(\neg \varphi)$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma \backslash \{ \varphi \}$ and conclusion $(\neg \varphi)$.
-
Conditional Eliminiation: Given that
$\,\,\,\,\,\,\,\,$$\Pi_1$ is a proof tree of height at most $n$ with premises $\Sigma_1 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $(\varphi \to \psi)$ for some $\varphi, \psi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$\Pi_2$ is a proof tree of height at most $n$ with premises $\Sigma_2 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\varphi$
$\,\,\,\,\,\,\,\,$At least one of $\Pi_1, \Pi_2$ is of height $n$
Then,
\begin{prooftree}
\AxiomC{$\Sigma_1$}
\noLine
\UnaryInfC{$\Pi_1$}
\noLine
\UnaryInfC{$(\varphi \to \psi)$}
\AxiomC{$\Sigma_2$}
\noLine
\UnaryInfC{$\Pi_2$}
\noLine
\UnaryInfC{$\varphi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\end{prooftree}
is a proof tree of height $n$ with premises $\Sigma_1 \cup \Sigma_2$ and conslusion $\psi$.
-
Conditional Introduction: Given that
$\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height $n$ with premises $\Sigma_1 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\psi \in \tt{Form}(\mathcal{L})$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$\psi$}
\RightLabel{$\scriptsize{\to I}$}
\UnaryInfC{$(\varphi \to \psi)$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma \backslash \{ \varphi \}$ and conclusion $(\varphi \to \psi)$.
-
Conjunction Elimination: Given that
$\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conclusion $(\varphi \wedge \psi)$ for some $\varphi, \psi \in \tt{Form}(\mathcal{L})$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$(\varphi \wedge \psi)$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\varphi$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$(\varphi \wedge \psi)$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\psi$}
\end{prooftree}
are proof trees of height $n + 1$ with premises $\Sigma$ and conclusions $\varphi$ and $\psi$ respectively.
-
Conjunction Introduction: Given that
$\,\,\,\,\,\,\,\,$$\Pi_1$ is a proof tree of height at most $n$ with premises $\Sigma_1 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\varphi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$\Pi_2$ is a proof tree of height at most $n$ with premises $\Sigma_2 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\psi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$At least one of $\Pi_1, \Pi_2$ has height $n$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi_1$}
\noLine
\UnaryInfC{$\varphi$}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi_1$}
\noLine
\UnaryInfC{$\psi$}
\RightLabel{$\scriptsize{\wedge I}$}
\BinaryInfC{$(\varphi \wedge \psi)$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma_1 \cup \Sigma_2$ and conclusion $(\varphi \wedge \psi)$.
-
Disjunction Elimination: Given that
$\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height at most $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conclusion $(\varphi \vee \psi)$ for some $\varphi, \psi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$\Pi_1$ is a proof tree of height at most $n$ with premises $\Sigma_1 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\chi$
$\,\,\,\,\,\,\,\,$$\Pi_2$ is a proof tree of height at most $n$ with premises $\Sigma_2 \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\chi$
$\,\,\,\,\,\,\,\,$At least one of $\Pi, \Pi_1, \Pi_2$ has height $n$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$(\varphi \vee \psi)$}
\AxiomC{$\Sigma_1$}
\noLine
\UnaryInfC{$\Pi_1$}
\noLine
\UnaryInfC{$\chi$}
\AxiomC{$\Sigma_2$}
\noLine
\UnaryInfC{$\Pi_2$}
\noLine
\UnaryInfC{$\chi$}
\RightLabel{$\scriptsize{\vee E}$}
\TrinaryInfC{$\chi$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma \cup \left( \Sigma_1 \backslash \{ \varphi \} \right) \cup \left( \Sigma_2 \backslash \{ \psi \} \right)$ and conclusion $\chi$.
-
Disjunction Introduction: Given that
$\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\varphi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$\psi \in \tt{Form}(\mathcal{L})$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$\varphi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$(\varphi \vee \psi)$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$\varphi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$(\varphi \vee \psi)$}
\end{prooftree}
are proof trees of height $n + 1$ with premises $\Sigma$ and conclusions $(\varphi \vee \psi)$ and $(\psi \vee \varphi)$ respectively.
-
Universal Elimination: Given that
$\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conclusion $(\forall x \, \varphi)$ for some $x \in \tt{Var}$ and $\varphi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$t \in \tt{Term}(\mathcal{L})$ and $t$ is free for $x$ in $\varphi$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$(\forall x \, \varphi)$}
\RightLabel{$\scriptsize{\forall E}$}
\UnaryInfC{$\varphi [ x / t]$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma$ and conclusion $\varphi[x/t]$.
-
Universal Introduction: Given that
$\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\varphi[x/y]$ for some $x, y \in \tt{Var}$ and $\varphi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$y$ is not free in $(\forall x \, \varphi)$ nor in $\psi$ for any $\psi \in \Sigma$
$\,\,\,\,\,\,\,\,$$y$ is free for $x$ in $\varphi$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$\varphi[x/y]$}
\RightLabel{$\scriptsize{\forall I}$}
\UnaryInfC{$(\forall x \, \varphi)$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma$ and conclusion $(\forall x \, \varphi)$.
-
Existential Elimination: Given that
$\,\,\,\,\,\,\,\,$$\Pi_1$ is a proof tree of height at most $n$ with premises $\Sigma_1$ and conclusion $(\exists x \, \varphi)$ for some $x \in \tt{Var}$ and $\varphi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$\Pi_2$ is a proof tree of height at most $n$ with premises $\Sigma_2$ and conclusion $\psi$ for some $\psi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$There is $y \in \texttt{Var}$ is not free in $(\exists x \, \varphi)$, nor in $\psi$, nor in $\chi$ for any $\chi \in \Sigma_2 \backslash \{ \varphi[x/y] \}$
$\,\,\,\,\,\,\,\,$$y$ is free for $x$ in $\varphi$
$\,\,\,\,\,\,\,\,$At least one of $\Pi_1, \Pi_2$ is of height $n$
Then,
\begin{prooftree}
\AxiomC{$\Sigma_1$}
\noLine
\UnaryInfC{$\Pi_1$}
\noLine
\UnaryInfC{$(\exists x \, \varphi)$}
\AxiomC{$\Sigma_2$}
\noLine
\UnaryInfC{$\Pi_2$}
\noLine
\UnaryInfC{$\psi$}
\RightLabel{$\scriptsize{\exists E}$}
\BinaryInfC{$\psi$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma_1 \cup \left( \Sigma_2 \backslash \{ \varphi[x/y] \} \right)$ and conlcusion $\psi$.
-
Existential Introduction: Given that
$\,\,\,\,\,\,\,\,$$\Pi$ is a proof tree of height $n$ with premises $\Sigma \subseteq \tt{Form}(\mathcal{L})$ and conclusion $\varphi[x/t]$ for some $x \in \tt{Var}$, $t \in \tt{Term}(\mathcal{L})$ and $\varphi \in \tt{Form}(\mathcal{L})$
$\,\,\,\,\,\,\,\,$$t \in \tt{Term}(\mathcal{L})$ and $t$ is free for $x$ in $\varphi$
Then,
\begin{prooftree}
\AxiomC{$\Sigma$}
\noLine
\UnaryInfC{$\Pi$}
\noLine
\UnaryInfC{$\varphi[x/t]$}
\RightLabel{$\scriptsize{\exists I}$}
\UnaryInfC{$(\exists x \, \varphi)$}
\end{prooftree}
is a proof tree of height $n + 1$ with premises $\Sigma$ and conclusion $(\exists x \, \varphi)$.
Proofs of Common Argument Forms
-
Modus Ponens: $\varphi, \varphi \to \psi \vdash \psi$
\begin{prooftree}
\AxiomC{$\varphi$}
\AxiomC{$(\varphi \to \psi)$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\end{prooftree}
-
Modus Tollens: $\neg \psi, \varphi \to \psi \vdash \neg\varphi$
\begin{prooftree}
\AxiomC{$[\varphi]^1$}
\AxiomC{$\varphi \to \psi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\AxiomC{$\neg \psi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg \varphi$}
\end{prooftree}
-
Hypothetical Syllogism: $\varphi \to \psi, \psi \to \chi \vdash \varphi \to \chi$
\begin{prooftree}
\AxiomC{$[\varphi]^1$}
\AxiomC{$\varphi \to \psi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\AxiomC{$\psi \to \chi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\chi$}
\RightLabel{$\scriptsize{\to I^1}$}
\UnaryInfC{$\varphi \to \chi$}
\end{prooftree}
-
Disjunctive Syllogism: $\varphi \vee \psi, \neg \varphi \vdash \psi$
\begin{prooftree}
\AxiomC{$\varphi \vee \psi$}
\AxiomC{$[\varphi]^1$}
\AxiomC{$\neg \varphi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\bot E}$}
\UnaryInfC{$\psi$}
\AxiomC{$[\psi]^2$}
\RightLabel{$\scriptsize{\vee E^{1, 2}}$}
\TrinaryInfC{$\psi$}
\end{prooftree}
-
Constructive Dilemma: $\varphi \to \psi, \chi \to \vartheta, \varphi \vee \chi \vdash \psi \vee \vartheta$
\begin{prooftree}
\AxiomC{$\varphi \vee \chi$}
\AxiomC{$[\varphi]^1$}
\AxiomC{$\varphi \to \psi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\psi \vee \vartheta$}
\AxiomC{$[\chi]^2$}
\AxiomC{$\chi \to \vartheta$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\vartheta$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\psi \vee \vartheta$}
\RightLabel{$\scriptsize{\vee E^{1, 2}}$}
\TrinaryInfC{$\psi \vee \vartheta$}
\end{prooftree}
-
Destructive Dilemma: $\varphi \to \psi, \chi \to \vartheta, \neg \psi \vee \neg \vartheta \vdash \neg \varphi \vee \neg \chi$
\begin{prooftree}
\AxiomC{$\neg\psi \vee \neg\vartheta$}
\AxiomC{$[\neg \psi]^3$}
\AxiomC{$[\varphi]^1$}
\AxiomC{$\varphi \to \psi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg \varphi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\neg \varphi \vee \neg \psi$}
\AxiomC{$[\neg \vartheta]^4$}
\AxiomC{$[\chi]^2$}
\AxiomC{$\chi \to \vartheta$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\vartheta$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^2}$}
\UnaryInfC{$\neg \chi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\neg \psi \vee \neg \psi$}
\RightLabel{$\scriptsize{\vee E^{3, 4}}$}
\TrinaryInfC{$\neg \varphi \vee \neg \chi$}
\end{prooftree}
-
Simplification: $\varphi \wedge \psi \vdash \varphi$
\begin{prooftree}
\AxiomC{$\varphi \wedge \psi$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\varphi$}
\end{prooftree}
-
Addition: $\varphi \vdash \varphi \vee \psi$
\begin{prooftree}
\AxiomC{$\varphi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\varphi \vee \psi$}
\end{prooftree}
-
Composition: $\varphi \to \psi, \varphi \to \chi \vdash \varphi \to (\psi \wedge \chi)$
\begin{prooftree}
\AxiomC{$[\varphi]^1$}
\AxiomC{$\varphi \to \psi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\AxiomC{$[\varphi]^1$}
\AxiomC{$\varphi \to \chi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\chi$}
\RightLabel{$\scriptsize{\wedge I}$}
\BinaryInfC{$\psi \wedge \chi$}
\RightLabel{$\scriptsize{\to I^1}$}
\UnaryInfC{$\varphi \to (\psi \wedge \chi)$}
\end{prooftree}
-
De Morgan's Law I: $\neg (\varphi \wedge \psi) \vdash \neg \varphi \vee \neg \psi$
\begin{prooftree}
\AxiomC{$[\neg (\neg \varphi \vee \neg \psi)]^3$}
\AxiomC{$[\varphi]^1$}
\AxiomC{$[\psi]^2$}
\RightLabel{$\scriptsize{\wedge I}$}
\BinaryInfC{$\varphi \wedge \psi$}
\AxiomC{$\neg(\varphi \wedge \psi)$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg \varphi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\neg \varphi \vee \neg \psi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^2}$}
\UnaryInfC{$\neg \psi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\neg \varphi \vee \neg \psi$}
\AxiomC{$[\neg (\neg \varphi \vee \neg \psi)]^3$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^3}$}
\UnaryInfC{$\neg \neg (\neg \varphi \vee \neg \psi)$}
\RightLabel{$\scriptsize{DNE}$}
\UnaryInfC{$\neg \varphi \vee \neg \psi$}
\end{prooftree}
-
De Morgan's Law II: $\neg (\varphi \vee \psi) \vdash \neg \varphi \wedge \neg \psi$
\begin{prooftree}
\AxiomC{$\neg (\varphi \vee \psi)$}
\AxiomC{$[\varphi]^1$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\varphi \vee \psi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg \varphi$}
\AxiomC{$\neg (\varphi \vee \psi)$}
\AxiomC{$[\psi]^2$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\varphi \vee \psi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^2}$}
\UnaryInfC{$\neg \psi$}
\RightLabel{$\scriptsize{\wedge I}$}
\BinaryInfC{$\neg \varphi \wedge \neg \psi$}
\end{prooftree}
-
Commutation I: $\varphi \vee \psi \vdash \psi \vee \varphi$
\begin{prooftree}
\AxiomC{$\varphi \vee \psi$}
\AxiomC{$[\varphi]^1$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\psi \vee \varphi$}
\AxiomC{$[\psi]^2$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\psi \vee \varphi$}
\RightLabel{$\scriptsize{\vee E^{1, 2}}$}
\TrinaryInfC{$\psi \vee \varphi$}
\end{prooftree}
-
Commutation II: $\varphi \wedge \psi \vdash \psi \wedge \varphi$
\begin{prooftree}
\AxiomC{$\varphi \wedge \psi$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\psi$}
\AxiomC{$\varphi \wedge \psi$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\varphi$}
\RightLabel{$\scriptsize{\wedge I}$}
\BinaryInfC{$\psi \wedge \varphi$}
\end{prooftree}
-
Association I: $\varphi \vee (\psi \vee \chi) \vdash (\varphi \vee \psi) \vee \chi$
\begin{prooftree}
\AxiomC{$\varphi \vee (\psi \vee \chi)$}
\AxiomC{$[\varphi]^3$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\varphi \vee \psi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$(\varphi \vee \psi) \vee \chi$}
\AxiomC{$[\psi \vee \chi]^4$}
\AxiomC{$[\psi]^1$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\varphi \vee \psi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$(\varphi \vee \psi) \vee \chi$}
\AxiomC{$[\chi]^2$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$(\varphi \vee \psi) \vee \chi$}
\RightLabel{$\scriptsize{\vee E^{1, 2}}$}
\TrinaryInfC{$(\varphi \vee \psi) \vee \chi$}
\RightLabel{$\scriptsize{\vee E^{3, 4}}$}
\TrinaryInfC{$(\varphi \vee \psi) \vee \chi$}
\end{prooftree}
-
Association II: $\varphi \wedge (\psi \wedge \chi) \vdash (\varphi \wedge \psi) \wedge \chi$
\begin{prooftree}
\AxiomC{$\varphi \wedge (\psi \wedge \chi)$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\varphi$}
\AxiomC{$\varphi \wedge (\psi \wedge \chi)$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\psi \wedge \chi$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\psi$}
\RightLabel{$\scriptsize{\wedge I}$}
\BinaryInfC{$\varphi \wedge \psi$}
\AxiomC{$\varphi \wedge (\psi \wedge \chi)$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\psi \wedge \chi$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\chi$}
\RightLabel{$\scriptsize{\wedge I}$}
\BinaryInfC{$(\varphi \wedge \psi) \wedge \chi$}
\end{prooftree}
-
Double Negation: $\varphi \vdash \neg \neg \varphi$
\begin{prooftree}
\AxiomC{$\varphi$}
\AxiomC{$[\neg \varphi]^1$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg \neg \varphi$}
\end{prooftree}
-
Double Negation Elimination: $\neg \neg \varphi \vdash \varphi$
\begin{prooftree}
\AxiomC{$\neg \neg \varphi$}
\RightLabel{$\scriptsize{DNE}$}
\UnaryInfC{$\varphi$}
\end{prooftree}
-
Transpotition: $\varphi \to \psi \vdash \neg \psi \to \neg \varphi$
\begin{prooftree}
\AxiomC{$\varphi \to \psi$}
\AxiomC{$[\varphi]^1$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\AxiomC{$[\neg \psi]^2$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg \varphi$}
\RightLabel{$\scriptsize{\to I^2}$}
\UnaryInfC{$\neg \psi \to \neg \varphi$}
\end{prooftree}
-
Material Implication: $\varphi \to \psi \vdash \neg \varphi \vee \psi$
\begin{prooftree}
\AxiomC{$[\neg (\neg \varphi \vee \psi)]^2$}
\AxiomC{$\varphi \to \psi$}
\AxiomC{$[\varphi]^1$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\neg \varphi \vee \psi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg \varphi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\neg \varphi \vee \psi$}
\AxiomC{$[\neg (\neg \varphi \vee \psi)]^2$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^2}$}
\UnaryInfC{$\neg \neg (\neg \varphi \vee \psi)$}
\RightLabel{$\scriptsize{DNE}$}
\UnaryInfC{$\neg \varphi \vee \psi$}
\end{prooftree}
-
Exportation: $(\varphi \wedge \psi) \to \chi \vdash \varphi \to (\psi \to \chi)$
\begin{prooftree}
\AxiomC{$(\varphi \wedge \psi) \to \chi$}
\AxiomC{$[\varphi]^2$}
\AxiomC{$[\psi]^1$}
\RightLabel{$\scriptsize{\wedge I}$}
\BinaryInfC{$\varphi \wedge \psi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\chi$}
\RightLabel{$\scriptsize{\to I^1}$}
\UnaryInfC{$\psi \to \chi$}
\RightLabel{$\scriptsize{\to I^2}$}
\UnaryInfC{$\varphi \to (\psi \to \chi)$}
\end{prooftree}
-
Importation: $\varphi \to (\psi \to \chi) \vdash (\varphi \wedge \psi) \to \chi$
\begin{prooftree}
\AxiomC{$\varphi \to (\psi \to \chi)$}
\AxiomC{$[\varphi \wedge \psi]^1$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\varphi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\psi \to \chi$}
\AxiomC{$[\varphi \wedge \psi]^1$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\psi$}
\RightLabel{$\scriptsize{\to E}$}
\BinaryInfC{$\chi$}
\RightLabel{$\scriptsize{\to I^1}$}
\UnaryInfC{$(\varphi \wedge \psi) \to \chi$}
\end{prooftree}
-
Law of the Excluded Middle: $\vdash \varphi \vee \neg \varphi$
\begin{prooftree}
\AxiomC{$[\neg (\varphi \vee \neg \varphi)]^2$}
\AxiomC{$[\neg (\varphi \vee \neg \varphi)]^2$}
\AxiomC{$[\varphi]^1$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\varphi \vee \neg \varphi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg \varphi$}
\RightLabel{$\scriptsize{\vee I}$}
\UnaryInfC{$\varphi \vee \neg \varphi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^2}$}
\UnaryInfC{$\neg \neg (\varphi \vee \neg \varphi)$}
\RightLabel{$\scriptsize{DNE}$}
\UnaryInfC{$\varphi \vee \neg \varphi$}
\end{prooftree}
-
Law of Non Contradiction: $\vdash \neg (\varphi \wedge \neg \varphi)$
\begin{prooftree}
\AxiomC{$[\varphi \wedge \neg \varphi]^1$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\varphi$}
\AxiomC{$[\varphi \wedge \neg \varphi]^1$}
\RightLabel{$\scriptsize{\wedge E}$}
\UnaryInfC{$\neg \varphi$}
\RightLabel{$\scriptsize{\neg E}$}
\BinaryInfC{$\bot$}
\RightLabel{$\scriptsize{\neg I^1}$}
\UnaryInfC{$\neg (\varphi \wedge \neg \varphi)$}
\end{prooftree}
Set Theoretic Examples
Theorem (Russel's Paradox): Let $\mathcal{L}$ be a first-order language. If $R$ is a relation symbol of $\mathcal{L}$ with arity $n_R = 2$ and $x, y \in \texttt{Var}$ are distinct variables, then
$$
\exists x \forall y \left( \left( Ryx \to \neg Ryy \right) \wedge \left( \neg Ryy \to Ryx \right) \right) \vdash \bot
$$
Proof.
$\space$$\blacksquare$
Let $\mathcal{L}_{\text{Set}}$ be the language of set theory consisting of a single relation symbol $\in$ with arity $n_\in = 2$. If $\varphi \in \texttt{Form}\left(\mathcal{L}_{\text{Set}} \right)$ with $\text{fv}(\varphi) = \{ y \}$ and $x \in \texttt{Var}$ is distinct from $y$, then the naïve comprehension principle allows us to take as an axiom
$$
\exists x \forall y \left( (y \in x \to \varphi) \wedge (\varphi \to y \in x) \right)
$$
Russel's paradox says that this leads to contradictions. For if we take $\varphi$ to be the formula $y \notin y$, then the theorem above tells us that
$$
\exists x \forall y \left( (y \in x \to y \notin y) \wedge (y \notin y \to y \in x) \right) \vdash \bot
$$
Therefore, accepting the naïve comprehension principle leads to an inconsistent set of axioms.
The $ZF$ axioms of set theory contains the sentance
$$\forall x \exists z \forall y \left( \left( y \in z \to \left( y \in x \wedge y \notin y \right) \right) \wedge \left( \left( y \in x \wedge y \notin y \right) \to y \in z \right) \right)$$
Theorem: There is no set of all sets. That is,
$$
ZF \vdash \neg \exists x \forall y \left( y \in x \right)
$$
Proof.
$\space$$\blacksquare$