% -*- TeX:EN -*-
%%% ====================================================================
%%% @LaTeX-file    qedeq_formal_logic_v1
%%% Generated from http://www.qedeq.org/0_04_03/doc/math/qedeq_formal_logic_v1.xml
%%% Generated at   2011-06-13 11:43:38.220
%%% ====================================================================

%%% Permission is granted to copy, distribute and/or modify this document
%%% under the terms of the GNU Free Documentation License, Version 1.2
%%% or any later version published by the Free Software Foundation;
%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.

\documentclass[a4paper,german,10pt,twoside]{book}
\usepackage[english]{babel}
\usepackage{makeidx}
\usepackage{amsmath,amsthm,amssymb}
\usepackage{color}
\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,
   colorlinks,linkcolor=webgreen,pagebackref]{hyperref}
\definecolor{webgreen}{rgb}{0,.5,0}
\usepackage{graphicx}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{tabularx}

\newtheorem{thm}{Theorem}
\newtheorem{cor}[thm]{Corollary}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{ax}{Axiom}
\newtheorem{rul}{Rule}

\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{idefn}[defn]{Initial Definition}

\theoremstyle{remark}
\newtheorem{rem}[thm]{Remark}
\newtheorem*{notation}{Notation}

\addtolength{\textheight}{7\baselineskip}
\addtolength{\topmargin}{-5\baselineskip}

\setlength{\parindent}{0pt}

\frenchspacing \sloppy

\makeindex


\title{Predicate Calculus}
\author{
Michael Meyling
}

\begin{document}

\maketitle

\setlength{\parskip}{5pt plus 2pt minus 1pt}
\mbox{}
\vfill

\par
The source for this document can be found here:
\par
\url{http://www.qedeq.org/0_04_03/doc/math/qedeq_formal_logic_v1.xml}

\par
Copyright by the authors. All rights reserved.
\par
If you have any questions, suggestions or want to add something to the list of modules that use this one, please send an email to the address \href{mailto:mime@qedeq.org}{mime@qedeq.org}

\par
The authors of this document are:
Michael Meyling \href{mailto:michael@meyling.com}{michael@meyling.com}

\setlength{\parskip}{0pt}
\tableofcontents

\setlength{\parskip}{5pt plus 2pt minus 1pt}

\chapter*{Summary\index{summary}} \label{chapter0} \hypertarget{chapter0}{}
\addcontentsline{toc}{chapter}{Summary\index{summary}}

In this text we present the development of predicate calculus in axiomatic form.
The language of our calculus bases on the formalizations of \emph{D.~Hilbert}, \emph{W.~Ackermann}\cite{hilback}, \emph{P.~S.~Novikov}\cite{novikov}, \emph{V.~Detlovs} and \emph{K.~Podnieks}\cite{detnieks}. New rules can be derived from the herein presented logical axioms and basic inference rules. Only these meta rules lead to a smooth flowing logical argumentation.
For background informations see under \url{http://www.ltn.lv/~podnieks/mlog/ml.htm}
and \url{http://en.wikipedia.org/wiki/Propositional_calculus}.

%% end of chapter Summary\index{summary}

\chapter{Language} \label{chapter1} \hypertarget{chapter1}{}

In this chapter we define a formal language to express mathematical propositions in a very precise way. Although this document describes a very formal approach to express mathematical content it is not sufficent to serve as a definition for an computer readable document format. Therefore such an extensive specification has to be done elsewhere. The choosen format is the \emph{Extensible Markup Language} abbreviated \emph{XML}. XML is a set of rules for encoding documents electronically.\footnote{See \url{http://www.w3.org/XML/} for more information.}
The according formal syntax specification can be found at \url{http://www.qedeq.org/current/xml/qedeq.xsd}.
It specifies a complete mathematical document format that enables the generation of \LaTeX books and makes automatic proof checking possible. 
Further syntax restrictions and some explanations can be found at \url{http://www.qedeq.org/current/doc/project/qedeq_logic_language_en.pdf}.
%%% TODO explain XSD, XML etc.

\par          
Even this document is (or was generated) from an XML file that can be found here: \url{http://wwww.qedeq.org/0_04_03/doc/math/qedeq_logic_v1.xml}.
But now we just follow the traditional mathematical way to present the elements of mathematical logic.

\section{Terms\index{term} and Formulas\index{formula}} \label{chapter1_section0} \hypertarget{chapter1_section0}{}
We use the \emph{logical symbols} 
$L = \{$ \mbox{`$\neg$'}, \mbox{`$\vee$'}, \mbox{`$\wedge$'}, \mbox{`$\leftrightarrow$'}, \mbox{`$\rightarrow$'}, \mbox{`$\forall$'}, \mbox{`$\exists$'} $\}$, the \emph{predicate constants}\index{predicate constant}\index{constant!predicate} $C = \{c^k_i~|~i, k \in \omega\}$, the \emph{function variables}\index{function variable}\index{variable!function}\footnote{Function variables are used for a shorter notation. For example writing an identity proposition $x = y \rightarrow f(x) = f(y)$. Also this introduction prepares for the syntax extension for functional classes.} $F = \{f^k_i~|~i, k \in \omega \land k > 0\}$, the \emph{function constants}\index{function constant}\index{constant!function}\footnote{Function constants are also introduced for convenience and are used for direct defined class functions. For example to define building of the power class operator, the union and intersection operator and the successor function. All these function constants can be interpreted as abbreviations.} $H = \{h^k_i~|~i, k \in \omega\}$, the \emph{subject variables}\index{subject variable}\index{variable!subject} $V = \{v_i~|~i \in \omega\}$, as well as
\emph{predicate variables}\index{predicate variable}\index{variable!predicate} $P = \{p^k_i~|~i, k \in \omega\}$.\footnote{By $\omega$ we understand the natural numbers including zero. All involved symbols are pairwise disjoint. 
Therefore we can conclude for example: $f^k_i = f^{k'}_{i'} \rightarrow (k = k' \land i = i')$ and $h^k_i \neq v_j$.} 
For the \emph{arity}\index{arity} or \emph{rank}\index{rank} of an operator we take the upper index. The set of predicate variables with zero arity is also called set of \emph{proposition variables}\index{proposition variable}\index{variable!proposition} or \emph{sentence letters}\index{sentence letters}: $A := \{p_i^0~|~i \in \omega \}$.
For subject variables we write short hand certain lower letters: \mbox{$v_1 = $ `$u$'}, \mbox{$v_2 = $ `$v$'}, 
\mbox{$v_3 = $ `$w$'}, \mbox{$v_4 = $ `$x$'}, \mbox{$v_5 = $ `$y$'}, \mbox{$v_5 = $ `$z$'}.
Furthermore we use the following short notations: for the predicate variables $p^n_1 = $ `$\phi$' und $p^n_2 = $ `$\psi$', where the appropriate arity $n$ is calculated by counting the subsequent parameters, for the proposition variables
$a_1 = $ `$A$', $a_2 = $ `$B$' and $a_3 = $ `$C$', for the function variables: $f^n_1 = $ `$f$' und $f^n_2 = $ `$g$', where again the appropriate arity $n$ is calculated by counting the subsequent parameters.  All binary propositional operators are written in infix notation. Parentheses surrounding groups of operands and operators are necessary to indicate the 
intended order in which operations are to be performed. E.~g. for the operator $\land$ with the parameters $A$ and $B$ we write $(A \land B)$.


In the absence of parentheses the usual precedence rules determine the order of operations. Especially outermost parentheses are omitted. Also empty parentheses are stripped.

\par
The operators have the order of precedence described below (starting with the highest).
$$
\begin{array}{c}
  \neg, \forall, \exists  \\
  \land \\
  \lor \\
  \rightarrow, \leftrightarrow \\
\end{array}
$$

\par
The term \emph{term\index{term}} is defined recursively as follows:

\begin{enumerate}
\item Every subject variable is a term. 
\item Let $i, k \in \omega$ and let $t_1$, \ldots, $t_k$ be terms. Then $h^k_i(t_1, \ldots, t_k)$ is a term and if $k > 0$, so $f^k_i(t_1, \ldots, t_k)$ is a term too.
\end{enumerate}

Therefore all zero arity function constants $\{h^0_i~|~i \in \omega\}$ are terms. They are called \emph{individual constants}\index{individual constant}\index{constant!individual}.\footnote{In an analogous manner subject variables might be defined as function variables of zero arity. Because subject variables play an important role they have their own notation.}

\par
We define a \emph{formula\index{formula}} and the relations \emph{free}\index{bound subject variable}\index{subject variable!free} and \emph{bound}\index{bound subject variable}\index{subject variable!bound} subject variable recursivly as follows:

\begin{enumerate}

\item Every proposition variable is a formula. Such formulas contain no free or bound subject variables.

\item If $p^k$ is a predicate variable with arity $k$ and $c^k$ is a predicate constant with arity $k$ and $t_1, t_2, \ldots, t_k$ are terms, then $p^k(t_1, t_2, \ldots t_k)$ and $c^k(t_1, t_2, \ldots, t_k)$ are formulas. All subject variables that occur at least in one of $t_1, t_2, \ldots, t_k$ are free subject variables. Bound subject variables does not occur.\footnote{This second item includes the first one, which is only listed for clarity.} 

\item Let $\alpha, \beta$ be formulas in which no subject variables occur bound in one formula and free in the other. Then $\neg \alpha$, $(\alpha \land \beta)$, $(\alpha \lor \beta)$, $(\alpha \rightarrow \beta)$ and $(\alpha \leftrightarrow \beta)$ are also formulas. Subject variables which occur free (respectively bound) in $\alpha$ or $\beta$ stay free (respectively bound).

\item If in the formula $\alpha$ the subject variable $x_1$ occurs not bound\footnote{This means that $x_1$ is free in the formula or does not occur at all.}, then also $\forall x_1~\alpha$ and $\exists x_1~\alpha$ are formulas. The symbol $\forall$ is called \emph{universal quantifier}\index{universal quantifier}\index{quantifier!universal} and $\exists$ as
\emph{existential quantifier}\index{existential quantifier}\index{quantifier!existential}.

Except for $x_1$ all free subject variables of $\alpha$ stay free. All bound subject variables are still bound and additionally $x_1$ is bound too.

\end{enumerate}

All formulas that are only built by usage of 1. and 3. are called formulas of the \emph{propositional calculus}\index{propositional calculus}\index{calculus!propositional}.

\par
For each formula $\alpha$ the following proposition holds: the set of free subject variables is disjoint with the set of bound subject variables..\footnote{Other formalizations allow for example $\forall x_1~\alpha$ also if $x_1$ occurs already bound within $\alpha$. Also propositions like $\alpha(x_1)~\land~(\forall~x_1~\beta)$ are allowed. In this formalizations
free and bound are defined for a single occurrence of a variable.}

\par
If a formula has the form $\forall x_1 ~ \alpha$ respectively $\exists x_1 ~ \alpha$ then the formula $\alpha$ is called the
\emph{scope}\index{scope}\index{quantifier!scope} of the quantifier $\forall$ respectively $\exists$.

\par
All formulas that are used to build up a formula by 1. to 4. are called \emph{part formulas}\index{part formula}\index{formula!part}.


%% end of chapter Language

\chapter{Axioms and Rules of Inference} \label{chapter2} \hypertarget{chapter2}{}

We now state the system of axioms for the propositional calculus and present the rules for obtaining new formulas from them.

\section{Axioms\index{axioms}} \label{chapter2_section0} \hypertarget{chapter2_section0}{}
Here we just list the axioms without further explanations.

\par


\begin{ax}[Implication Introduction\index{implication introduction}]
\label{axiom:THEN-1} \hypertarget{axiom:THEN-1}{}
{\tt \tiny [\verb]axiom:THEN-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ (B\ \rightarrow\ A)$
\end{longtable}

\end{ax}




\par


\begin{ax}[Distribute Hypothesis over Implication\index{hypothesis distribution}]
\label{axiom:THEN-2} \hypertarget{axiom:THEN-2}{}
{\tt \tiny [\verb]axiom:THEN-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))$
\end{longtable}

\end{ax}




\par


\begin{ax}[Eliminate Conjunction Right\index{conjunction!elimination}]
\label{axiom:AND-1} \hypertarget{axiom:AND-1}{}
{\tt \tiny [\verb]axiom:AND-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \land\ B)\ \rightarrow\ A$
\end{longtable}

\end{ax}




\par


\begin{ax}[Eliminate Conjunction Left\index{conjunction!elimination}]
\label{axiom:AND-2} \hypertarget{axiom:AND-2}{}
{\tt \tiny [\verb]axiom:AND-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \land\ B)\ \rightarrow\ B$
\end{longtable}

\end{ax}




\par


\begin{ax}[Conjunction Introduction\index{conjunction!introduction}]
\label{axiom:AND-3} \hypertarget{axiom:AND-3}{}
{\tt \tiny [\verb]axiom:AND-3]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$
\end{longtable}

\end{ax}




\par


\begin{ax}[Disjunction Introduction Right\index{disjunction!introduction}]
\label{axiom:OR-1} \hypertarget{axiom:OR-1}{}
{\tt \tiny [\verb]axiom:OR-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ (A\ \lor\ B)$
\end{longtable}

\end{ax}




\par


\begin{ax}[Disjunction Introduction Left\index{disjunction!introduction}]
\label{axiom:OR-2} \hypertarget{axiom:OR-2}{}
{\tt \tiny [\verb]axiom:OR-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ (B\ \lor\ A)$
\end{longtable}

\end{ax}




\par


\begin{ax}[Disjunction Elimination\index{disjunction!elimination}]
\label{axiom:OR-3} \hypertarget{axiom:OR-3}{}
{\tt \tiny [\verb]axiom:OR-3]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$
\end{longtable}

\end{ax}




\par


\begin{ax}[Negation Introduction\index{negation!introduction}]
\label{axiom:NOT-1} \hypertarget{axiom:NOT-1}{}
{\tt \tiny [\verb]axiom:NOT-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$
\end{longtable}

\end{ax}




\par


\begin{ax}[Negation Elimination\index{negation!elimination}]
\label{axiom:NOT-2} \hypertarget{axiom:NOT-2}{}
{\tt \tiny [\verb]axiom:NOT-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\neg A\ \rightarrow\ (A\ \rightarrow\ B)$
\end{longtable}

\end{ax}




\par


\begin{ax}[Excluded Middle\index{negation!excluded middle}]
\label{axiom:NOT-3} \hypertarget{axiom:NOT-3}{}
{\tt \tiny [\verb]axiom:NOT-3]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \lor\ \neg A$
\end{longtable}

\end{ax}




\par


\begin{ax}[Equivalence Elimination right\index{equivalence!elimination}]
\label{axiom:IFF-1} \hypertarget{axiom:IFF-1}{}
{\tt \tiny [\verb]axiom:IFF-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \leftrightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ B)$
\end{longtable}

\end{ax}




\par


\begin{ax}[Equivalence Elimination left\index{equivalence!elimination}]
\label{axiom:IFF-2} \hypertarget{axiom:IFF-2}{}
{\tt \tiny [\verb]axiom:IFF-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \leftrightarrow\ B)\ \rightarrow\ (B\ \rightarrow\ A)$
\end{longtable}

\end{ax}




\par


\begin{ax}[Equivalence Introduction\index{equivalence!introduction}]
\label{axiom:IFF-3} \hypertarget{axiom:IFF-3}{}
{\tt \tiny [\verb]axiom:IFF-3]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((B\ \rightarrow\ A)\ \rightarrow\ (A\ \leftrightarrow\ B))$
\end{longtable}

\end{ax}




\par
If something is true for all $x$, it is true for any specific $y$.

\begin{ax}[Universal Instantiation\index{axiom!of universal instantiation}]
\label{axiom:universalInstantiation} \hypertarget{axiom:universalInstantiation}{}
{\tt \tiny [\verb]axiom:universalInstantiation]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\forall x\ \phi(x)\ \rightarrow\ \phi(y)$
\end{longtable}

\end{ax}




\par
If a predicate holds for some particular $y$, then there is an $x$ for which the predicate holds.

\begin{ax}[Existential Generalization\index{axiom!of existential generalization}]
\label{axiom:existencialGeneralization} \hypertarget{axiom:existencialGeneralization}{}
{\tt \tiny [\verb]axiom:existencialGeneralization]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\phi(y)\ \rightarrow\ \exists x\ \phi(x)$
\end{longtable}

\end{ax}




\section{Rules of Inference\index{rules!of predicate calculus}\index{rules!of inference}} \label{chapter2_section1} \hypertarget{chapter2_section1}{}
The following rules of inference enable us to obtain new true formulas from the axioms that are assumed to be true. From these new formulas we derive further formulas. So we can successively extend the set of true formulas.

\par


\begin{rul}[Modus Ponens\index{Modus Ponens}]
\label{rule:modusPonens} \hypertarget{rule:modusPonens}{}
{\tt \tiny [\verb]rule:modusPonens]]}
If both formulas $\alpha$ and $\alpha \rightarrow \beta$ are true, then we can conclude that $\beta$ is true as well.
\end{rul}




\par


\begin{rul}[Replace Free Subject Variable]
\label{rule:replaceFree} \hypertarget{rule:replaceFree}{}
{\tt \tiny [\verb]rule:replaceFree]]}
We start with a true formula.
A free subject variable may be replaced by an arbitrary term, provided that the substituted term contains no subject variable that have a bound occurrence in the original formula. All occurrences of the free variable must be simultaneously replaced.
\end{rul}

The prohibition to use subject variables within the term that occur bound in the original formula has two reasons. First it ensures that the resulting formula is well-formed. Secondly it preserves the validity of the formula. Let us look at the following derivation.

\par
\begin{tabularx}{\linewidth}{rclX}
  $\forall x \ \exists y \ \phi(x, y)$ & $\rightarrow$ & $\exists y \ \phi(z,y)$ 
    & with \hyperref[axiom:universalInstantiation]{axiom~15} \\
  $\forall x \ \exists y \ \phi(x, y)$ & $\rightarrow$ & $\exists y \ \phi(y,y)$ 
    & forbidden replacement: $z$ in $y$, despite $y$ is already bound \\
  $\forall x \ \exists y \ x \neq y$ & $\rightarrow$ & $\exists y \ \neq y$ 
    & replace $\neq$ for $\phi$
\end{tabularx}

\par
This last proposition is not valid in many models.


\par


\begin{rul}[Rename Bound Subject Variable]
\label{rule:renameBound} \hypertarget{rule:renameBound}{}
{\tt \tiny [\verb]rule:renameBound]]}
We may replace a bound subject variable occurring in a formula by any other subject variable, provided that the new variable occurs not free in the original formula. If the variable to be replaced occurs in more than one scope, then the replacement needs to be made in one scope only.
\end{rul}




\par


\begin{rul}[Replace Predicate Variable]
\label{rule:replacePred} \hypertarget{rule:replacePred}{}
{\tt \tiny [\verb]rule:replacePred]]}
Let $\alpha$ be a true formula that contains a predicate variable $p$ of arity $n$, let $x_1$, \ldots, $x_n$ be pairwise different subject variables and let $\beta(x_1, \ldots, x_n)$ be a formula where $x_1$, \ldots, $x_n$ are not bound. The formula $\beta(x_1, \ldots, x_n)$ must not contain all $x_1$, \ldots, $x_n$ as free subject variables. Furthermore it can also have other subject variables either free or bound.

If the following conditions are fulfilled, then a replacement of all occurrences of $p(t_1, \ldots, t_n)$ each with appropriate terms $t_1$, \ldots, $t_n$ in $\alpha$ by $\beta(t_1, \ldots, t_n)$ results in another true formula.

\begin{itemize}

\item
the free variables of $\beta(x_1, \ldots, x_n)$ without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$ 

\item 
each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains no bound variable of $\beta(x_1, \ldots, x_n)$ 

\item
the result of the substitution is a well-formed formula

\end{itemize}
\end{rul}

See III \S 5 in \cite{hilback}.

\par
The prohibition to use additional subject variables within the replacement formula that occur bound in the original formula assurs that the resulting formula is well-formed. Furthermore it preserves the validity of the formla. Take a look at the following derivation.

\par
\begin{tabularx}{\linewidth}{rclX}
  $ \phi(x)$                             & $\rightarrow$ & $\exists y \ \phi(y)$  
    & with \hyperref[axiom:existencialGeneralization]{axiom~16} \\
  $ (\exists y \ y = y) \land \phi(x)$   & $\rightarrow$ & $\exists y \ \phi(y)$  
    &  \\
  $ \exists y \ (y = y \land \phi(x))$   & $\rightarrow$ & $\exists y \ \phi(y)$  
    &  \\
  $ \exists y \ (y = y \land x \neq y)$  & $\rightarrow$ & $\exists y \ y \neq y$  
    & forbidden replacment: $\phi(x)$ by $x \neq y$, despite $y$ is already bound \\
  $ \exists y \  x \neq y$  & $\rightarrow$ & $\exists y \ y \neq y$  
    &
\end{tabularx}

\par
The last proposition is not valid in many models.


\par
Analogous to \hyperref[rule:replacePred]{rule~4} we can replace function variables too.

\begin{rul}[Replace Function Variable]
\label{rule:replaceFunct} \hypertarget{rule:replaceFunct}{}
{\tt \tiny [\verb]rule:replaceFunct]]}
Let $\alpha$ be an already proved formula that contains a function variable $\sigma$ of arity $n$, let $x_1$, \ldots, $x_n$ be pairwise different subject variables and let $\tau(x_1, \ldots, x_n)$ be an arbitrary term where $x_1$, \ldots, $x_n$ are not bound. 
The term $\tau(x_1, \ldots, x_n)$ must not contain all $x_1$, \ldots, $x_n$ as free subject variables. Furthermore it can also have other subject variables either free or bound. 

If the following conditions are fulfilled we can obtain a new true formula by replacing each occurrence of $\sigma(t_1, \ldots, t_n)$ with appropriate terms $t_1$, \ldots, $t_n$ in $\alpha$ by $\tau(t_1, \ldots, t_n)$.

\begin{itemize}

\item 
the free variables of $\tau(x_1, \ldots, x_n)$ without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$

\item
each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$ contains no bound variable of $\tau(x_1, \ldots, x_n)$

\item
the result of the substitution is a well-formed formula
                  
\end{itemize}
\end{rul}




\par


\begin{rul}[Universal Generalization]
\label{rule:universalGeneralization} \hypertarget{rule:universalGeneralization}{}
{\tt \tiny [\verb]rule:universalGeneralization]]}
If $\alpha \rightarrow \beta(x_1)$ is a true formula and $\alpha$ does not contain the subject variable $x_1$, then $\alpha \rightarrow (\forall x_1~(\beta(x_1)))$ is a true 
formula too.
\end{rul}




\par


\begin{rul}[Existential Generalization]
\label{rule:existentialGeneralization} \hypertarget{rule:existentialGeneralization}{}
{\tt \tiny [\verb]rule:existentialGeneralization]]}
If $\alpha(x_1) \rightarrow \beta$ is already proved to be true and $\beta$ does not contain the subject variable $x_1$, then $(\exists x_1~\alpha(x_1)) \rightarrow \beta$ is also a true formula.
\end{rul}




\section{First Propositions} \label{chapter2_section2} \hypertarget{chapter2_section2}{}
Here we draw the first conclusions.

\par


\begin{prop}
\label{proposition:implicationReflexive1} \hypertarget{proposition:implicationReflexive1}{}
{\tt \tiny [\verb]proposition:implicationReflexive1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implicationReflexive1:1} \hypertarget{proposition:implicationReflexive1:1}{} \mbox{(1)}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny Add \hyperref[axiom:THEN-1]{axiom~1}} \\ 
\label{proposition:implicationReflexive1:2} \hypertarget{proposition:implicationReflexive1:2}{} \mbox{(2)}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny Add \hyperref[axiom:THEN-2]{axiom~2}} \\ 
\label{proposition:implicationReflexive1:3} \hypertarget{proposition:implicationReflexive1:3}{} \mbox{(3)}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny Add \hyperref[axiom:OR-2]{axiom~7}} \\ 
\label{proposition:implicationReflexive1:4} \hypertarget{proposition:implicationReflexive1:4}{} \mbox{(4)}  \ &  \ $A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ A)$ \ &  \ {\tiny SubstPred $B$ by $B\ \lor\ A$ in \hyperref[proposition:implicationReflexive1/1]{(1)}} \\ 
\label{proposition:implicationReflexive1:5} \hypertarget{proposition:implicationReflexive1:5}{} \mbox{(5)}  \ &  \ $(A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ C))\ \rightarrow\ ((A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny SubstPred $B$ by $B\ \lor\ A$ in \hyperref[proposition:implicationReflexive1/2]{(2)}} \\ 
\label{proposition:implicationReflexive1:6} \hypertarget{proposition:implicationReflexive1:6}{} \mbox{(6)}  \ &  \ $(A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ A))\ \rightarrow\ ((A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ A))$ \ &  \ {\tiny SubstPred $C$ by $A$ in \hyperref[proposition:implicationReflexive1/5]{(5)}} \\ 
\label{proposition:implicationReflexive1:7} \hypertarget{proposition:implicationReflexive1:7}{} \mbox{(7)}  \ &  \ $(A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ A)$ \ &  \ {\tiny MP \hyperref[proposition:implicationReflexive1/6]{(6)}, \hyperref[proposition:implicationReflexive1/4]{(4)}} \\ 
\label{proposition:implicationReflexive1:8} \hypertarget{proposition:implicationReflexive1:8}{} \mbox{(8)}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny MP \hyperref[proposition:implicationReflexive1/7]{(7)}, \hyperref[proposition:implicationReflexive1/3]{(3)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication19} \hypertarget{proposition:implication19}{}
{\tt \tiny [\verb]proposition:implication19]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication19:1} \hypertarget{proposition:implication19:1}{} \mbox{(1)}  \ &  \ $A\ \rightarrow\ (A\ \lor\ B)$ \ &  \ {\tiny Add \hyperref[axiom:OR-1]{axiom~6}} \\ 
\label{proposition:implication19:2} \hypertarget{proposition:implication19:2}{} \mbox{(2)}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny Add \hyperref[axiom:OR-2]{axiom~7}} \\ 
\label{proposition:implication19:3} \hypertarget{proposition:implication19:3}{} \mbox{(3)}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny Add \hyperref[axiom:OR-3]{axiom~8}} \\ 
\label{proposition:implication19:4} \hypertarget{proposition:implication19:4}{} \mbox{(4)}  \ &  \ $D\ \rightarrow\ (D\ \lor\ B)$ \ &  \ {\tiny SubstPred $A$ by $D$ in \hyperref[proposition:implication19/1]{(1)}} \\ 
\label{proposition:implication19:5} \hypertarget{proposition:implication19:5}{} \mbox{(5)}  \ &  \ $(A\ \rightarrow\ (C\ \lor\ A))\ \rightarrow\ ((B\ \rightarrow\ (C\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (C\ \lor\ A)))$ \ &  \ {\tiny SubstPred $C$ by $C\ \lor\ A$ in \hyperref[proposition:implication19/3]{(3)}} \\ 
\label{proposition:implication19:6} \hypertarget{proposition:implication19:6}{} \mbox{(6)}  \ &  \ $D\ \rightarrow\ (D\ \lor\ A)$ \ &  \ {\tiny SubstPred $B$ by $A$ in \hyperref[proposition:implication19/4]{(4)}} \\ 
\label{proposition:implication19:7} \hypertarget{proposition:implication19:7}{} \mbox{(7)}  \ &  \ $(A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((B\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A)))$ \ &  \ {\tiny SubstPred $C$ by $B$ in \hyperref[proposition:implication19/5]{(5)}} \\ 
\label{proposition:implication19:8} \hypertarget{proposition:implication19:8}{} \mbox{(8)}  \ &  \ $(B\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A))$ \ &  \ {\tiny MP \hyperref[proposition:implication19/7]{(7)}, \hyperref[proposition:implication19/2]{(2)}} \\ 
\label{proposition:implication19:9} \hypertarget{proposition:implication19:9}{} \mbox{(9)}  \ &  \ $B\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny SubstPred $D$ by $B$ in \hyperref[proposition:implication19/6]{(6)}} \\ 
\label{proposition:implication19:10} \hypertarget{proposition:implication19:10}{} \mbox{(10)}  \ &  \ $(A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny MP \hyperref[proposition:implication19/8]{(8)}, \hyperref[proposition:implication19/9]{(9)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication23} \hypertarget{proposition:implication23}{}
{\tt \tiny [\verb]proposition:implication23]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\neg (A\ \land\ \neg A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication23:1} \hypertarget{proposition:implication23:1}{} \mbox{(1)}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny Add \hyperref[axiom:AND-1]{axiom~3}} \\ 
\label{proposition:implication23:2} \hypertarget{proposition:implication23:2}{} \mbox{(2)}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny Add \hyperref[axiom:AND-2]{axiom~4}} \\ 
\label{proposition:implication23:3} \hypertarget{proposition:implication23:3}{} \mbox{(3)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny Add \hyperref[axiom:NOT-1]{axiom~9}} \\ 
\label{proposition:implication23:4} \hypertarget{proposition:implication23:4}{} \mbox{(4)}  \ &  \ $(A\ \land\ \neg A)\ \rightarrow\ A$ \ &  \ {\tiny SubstPred $B$ by $\neg A$ in \hyperref[proposition:implication23/1]{(1)}} \\ 
\label{proposition:implication23:5} \hypertarget{proposition:implication23:5}{} \mbox{(5)}  \ &  \ $(A\ \land\ \neg A)\ \rightarrow\ \neg A$ \ &  \ {\tiny SubstPred $B$ by $\neg A$ in \hyperref[proposition:implication23/2]{(2)}} \\ 
\label{proposition:implication23:6} \hypertarget{proposition:implication23:6}{} \mbox{(6)}  \ &  \ $((A\ \land\ \neg A)\ \rightarrow\ B)\ \rightarrow\ (((A\ \land\ \neg A)\ \rightarrow\ \neg B)\ \rightarrow\ \neg (A\ \land\ \neg A))$ \ &  \ {\tiny SubstPred $A$ by $A\ \land\ \neg A$ in \hyperref[proposition:implication23/3]{(3)}} \\ 
\label{proposition:implication23:7} \hypertarget{proposition:implication23:7}{} \mbox{(7)}  \ &  \ $((A\ \land\ \neg A)\ \rightarrow\ A)\ \rightarrow\ (((A\ \land\ \neg A)\ \rightarrow\ \neg A)\ \rightarrow\ \neg (A\ \land\ \neg A))$ \ &  \ {\tiny SubstPred $B$ by $A$ in \hyperref[proposition:implication23/6]{(6)}} \\ 
\label{proposition:implication23:8} \hypertarget{proposition:implication23:8}{} \mbox{(8)}  \ &  \ $((A\ \land\ \neg A)\ \rightarrow\ \neg A)\ \rightarrow\ \neg (A\ \land\ \neg A)$ \ &  \ {\tiny MP \hyperref[proposition:implication23/7]{(7)}, \hyperref[proposition:implication23/4]{(4)}} \\ 
\label{proposition:implication23:9} \hypertarget{proposition:implication23:9}{} \mbox{(9)}  \ &  \ $\neg (A\ \land\ \neg A)$ \ &  \ {\tiny MP \hyperref[proposition:implication23/8]{(8)}, \hyperref[proposition:implication23/5]{(5)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\section{Deduction Theorem\index{deduction theorem}} \label{chapter2_section3} \hypertarget{chapter2_section3}{}
We prove the deduction theorem. This leads to the new rule \emph{Conditional Proof}.

\par
If we can prove $B$ by assuming $A$ as a hypothesis then we have proved $A \rightarrow B$. This reasoning is justified by the so-called \emph{deduction theorem}. The deduction theorem holds for all first-order theories with the usual deductive systems for first-order logic. However our use of proposition variables and substitution rules make difficulties. We have to restrict the allowed inference rules to get a simular result.

\begin{rul}
\label{rule:CP} \hypertarget{rule:CP}{}
{\tt \tiny [\verb]rule:CP]]}
We have the well-formed formula $\alpha$ and add it as a new proof line. Now we modify the existing inference rules. We can add a further proof line $\beta$ if $\alpha \rightarrow \beta$ is a well-formed formula and the usage of a previous inference rule with the following restrictions justifies the addition:
for \hyperref[rule:replaceFree]{rule~2} occurs the replaced free variable not in $\alpha$, for \hyperref[rule:replacePred]{rule~4} occurs the replaced predicate variable not in $\alpha$, for \hyperref[rule:replaceFunct]{rule~5} occurs the replaced function variable not in $\alpha$.
\end{rul}
\begin{proof}

\end{proof}
Based on: 
 \ref{axiom:THEN-1} \ref{axiom:THEN-2}
\begin{proof}

\end{proof}




\section{Further Theorems} \label{chapter2_section4} \hypertarget{chapter2_section4}{}
The deduction theorem enables us to prove more propopsitions.

\par


\begin{prop}
\label{proposition:implication10} \hypertarget{proposition:implication10}{}
{\tt \tiny [\verb]proposition:implication10]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (A\ \rightarrow\ B))\ \rightarrow\ (A\ \rightarrow\ B)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication10:1} \hypertarget{proposition:implication10:1}{} \mbox{(1)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication10:2} \hypertarget{proposition:implication10:2}{} \mbox{(2)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication10:3} \hypertarget{proposition:implication10:3}{} \mbox{(3)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny MP \hyperref[proposition:implication10/1]{(1)}, \hyperref[proposition:implication10/2]{(2)}} \\ 
\label{proposition:implication10:4} \hypertarget{proposition:implication10:4}{} \mbox{(4)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny MP \hyperref[proposition:implication10/3]{(3)}, \hyperref[proposition:implication10/2]{(2)}} \\ 
\label{proposition:implication10:5} \hypertarget{proposition:implication10:5}{} \mbox{(5)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication10:6} \hypertarget{proposition:implication10:6}{} \mbox{(6)}  \ &  \ $(A\ \rightarrow\ (A\ \rightarrow\ B))\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication11} \hypertarget{proposition:implication11}{}
{\tt \tiny [\verb]proposition:implication11]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication11:1} \hypertarget{proposition:implication11:1}{} \mbox{(1)}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny Add \hyperref[axiom:THEN-1]{axiom~1}} \\ 
\label{proposition:implication11:2} \hypertarget{proposition:implication11:2}{} \mbox{(2)}  \ &  \ $D\ \rightarrow\ (B\ \rightarrow\ D)$ \ &  \ {\tiny SubstPred $A$ by $D$ in \hyperref[proposition:implication11/1]{(1)}} \\ 
\label{proposition:implication11:3} \hypertarget{proposition:implication11:3}{} \mbox{(3)}  \ &  \ $D\ \rightarrow\ (A\ \rightarrow\ D)$ \ &  \ {\tiny SubstPred $B$ by $A$ in \hyperref[proposition:implication11/2]{(2)}} \\ 
\label{proposition:implication11:4} \hypertarget{proposition:implication11:4}{} \mbox{(4)}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny SubstPred $D$ by $B$ in \hyperref[proposition:implication11/3]{(3)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication11:5} \hypertarget{proposition:implication11:5}{} \mbox{(5)}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication11:6} \hypertarget{proposition:implication11:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication11:7} \hypertarget{proposition:implication11:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication11:8} \hypertarget{proposition:implication11:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny MP \hyperref[proposition:implication11/4]{(4)}, \hyperref[proposition:implication11/7]{(7)}} \\ 
\label{proposition:implication11:9} \hypertarget{proposition:implication11:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny MP \hyperref[proposition:implication11/5]{(5)}, \hyperref[proposition:implication11/8]{(8)}} \\ 
\label{proposition:implication11:10} \hypertarget{proposition:implication11:10}{} \mbox{(10)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny MP \hyperref[proposition:implication11/9]{(9)}, \hyperref[proposition:implication11/6]{(6)}} \\ 
\label{proposition:implication11:11} \hypertarget{proposition:implication11:11}{} \mbox{(11)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication11:12} \hypertarget{proposition:implication11:12}{} \mbox{(12)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication11:13} \hypertarget{proposition:implication11:13}{} \mbox{(13)}  \ &  \ $((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication12} \hypertarget{proposition:implication12}{}
{\tt \tiny [\verb]proposition:implication12]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication12:1} \hypertarget{proposition:implication12:1}{} \mbox{(1)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication12:2} \hypertarget{proposition:implication12:2}{} \mbox{(2)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication12:3} \hypertarget{proposition:implication12:3}{} \mbox{(3)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication12:4} \hypertarget{proposition:implication12:4}{} \mbox{(4)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny MP \hyperref[proposition:implication12/1]{(1)}, \hyperref[proposition:implication12/3]{(3)}} \\ 
\label{proposition:implication12:5} \hypertarget{proposition:implication12:5}{} \mbox{(5)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny MP \hyperref[proposition:implication12/2]{(2)}, \hyperref[proposition:implication12/4]{(4)}} \\ 
\label{proposition:implication12:6} \hypertarget{proposition:implication12:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication12:7} \hypertarget{proposition:implication12:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}$(B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication12:8} \hypertarget{proposition:implication12:8}{} \mbox{(8)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication13} \hypertarget{proposition:implication13}{}
{\tt \tiny [\verb]proposition:implication13]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ (A\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication13:1} \hypertarget{proposition:implication13:1}{} \mbox{(1)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication13:2} \hypertarget{proposition:implication13:2}{} \mbox{(2)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication13:3} \hypertarget{proposition:implication13:3}{} \mbox{(3)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication13:4} \hypertarget{proposition:implication13:4}{} \mbox{(4)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny MP \hyperref[proposition:implication13/1]{(1)}, \hyperref[proposition:implication13/3]{(3)}} \\ 
\label{proposition:implication13:5} \hypertarget{proposition:implication13:5}{} \mbox{(5)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny MP \hyperref[proposition:implication13/4]{(4)}, \hyperref[proposition:implication13/2]{(2)}} \\ 
\label{proposition:implication13:6} \hypertarget{proposition:implication13:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication13:7} \hypertarget{proposition:implication13:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication13:8} \hypertarget{proposition:implication13:8}{} \mbox{(8)}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication15} \hypertarget{proposition:implication15}{}
{\tt \tiny [\verb]proposition:implication15]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ C)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication15:1} \hypertarget{proposition:implication15:1}{} \mbox{(1)}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny Add \hyperref[axiom:AND-1]{axiom~3}} \\ 
\label{proposition:implication15:2} \hypertarget{proposition:implication15:2}{} \mbox{(2)}  \ &  \ $(A\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ A$ \ &  \ {\tiny SubstPred $B$ by $B\ \rightarrow\ C$ in \hyperref[proposition:implication15/1]{(1)}} \\ 
\label{proposition:implication15:3} \hypertarget{proposition:implication15:3}{} \mbox{(3)}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny SubstPred $A$ by $A\ \rightarrow\ B$ in \hyperref[proposition:implication15/2]{(2)}} \\ 
\label{proposition:implication15:4} \hypertarget{proposition:implication15:4}{} \mbox{(4)}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny Add \hyperref[axiom:AND-2]{axiom~4}} \\ 
\label{proposition:implication15:5} \hypertarget{proposition:implication15:5}{} \mbox{(5)}  \ &  \ $(A\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny SubstPred $B$ by $B\ \rightarrow\ C$ in \hyperref[proposition:implication15/4]{(4)}} \\ 
\label{proposition:implication15:6} \hypertarget{proposition:implication15:6}{} \mbox{(6)}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny SubstPred $A$ by $A\ \rightarrow\ B$ in \hyperref[proposition:implication15/5]{(5)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication15:7} \hypertarget{proposition:implication15:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication15:8} \hypertarget{proposition:implication15:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny MP \hyperref[proposition:implication15/3]{(3)}, \hyperref[proposition:implication15/7]{(7)}} \\ 
\label{proposition:implication15:9} \hypertarget{proposition:implication15:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny MP \hyperref[proposition:implication15/6]{(6)}, \hyperref[proposition:implication15/7]{(7)}} \\ 
\label{proposition:implication15:10} \hypertarget{proposition:implication15:10}{} \mbox{(10)}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny Add \hyperref[proposition:implication12]{proposition~6}} \\ 
\label{proposition:implication15:11} \hypertarget{proposition:implication15:11}{} \mbox{(11)}  \ &  \ \mbox{\qquad}$(B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny MP \hyperref[proposition:implication15/10]{(10)}, \hyperref[proposition:implication15/8]{(8)}} \\ 
\label{proposition:implication15:12} \hypertarget{proposition:implication15:12}{} \mbox{(12)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny MP \hyperref[proposition:implication15/11]{(11)}, \hyperref[proposition:implication15/9]{(9)}} \\ 
\label{proposition:implication15:13} \hypertarget{proposition:implication15:13}{} \mbox{(13)}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication17} \hypertarget{proposition:implication17}{}
{\tt \tiny [\verb]proposition:implication17]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C)))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication17:1} \hypertarget{proposition:implication17:1}{} \mbox{(1)}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny Add \hyperref[axiom:AND-3]{axiom~5}} \\ 
\label{proposition:implication17:2} \hypertarget{proposition:implication17:2}{} \mbox{(2)}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny SubstPred $B$ by $C$ in \hyperref[proposition:implication17/1]{(1)}} \\ 
\label{proposition:implication17:3} \hypertarget{proposition:implication17:3}{} \mbox{(3)}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny SubstPred $A$ by $B$ in \hyperref[proposition:implication17/2]{(2)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication17:4} \hypertarget{proposition:implication17:4}{} \mbox{(4)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication17:5} \hypertarget{proposition:implication17:5}{} \mbox{(5)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication17:6} \hypertarget{proposition:implication17:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication17:7} \hypertarget{proposition:implication17:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny MP \hyperref[proposition:implication17/5]{(5)}, \hyperref[proposition:implication17/6]{(6)}} \\ 
\label{proposition:implication17:8} \hypertarget{proposition:implication17:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny MP \hyperref[proposition:implication17/3]{(3)}, \hyperref[proposition:implication17/7]{(7)}} \\ 
\label{proposition:implication17:9} \hypertarget{proposition:implication17:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny MP \hyperref[proposition:implication17/4]{(4)}, \hyperref[proposition:implication17/6]{(6)}} \\ 
\label{proposition:implication17:10} \hypertarget{proposition:implication17:10}{} \mbox{(10)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ &  \ {\tiny MP \hyperref[proposition:implication17/8]{(8)}, \hyperref[proposition:implication17/9]{(9)}} \\ 
\label{proposition:implication17:11} \hypertarget{proposition:implication17:11}{} \mbox{(11)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication17:12} \hypertarget{proposition:implication17:12}{} \mbox{(12)}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication17:13} \hypertarget{proposition:implication17:13}{} \mbox{(13)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C)))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication18} \hypertarget{proposition:implication18}{}
{\tt \tiny [\verb]proposition:implication18]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \land\ B)\ \rightarrow\ (B\ \land\ A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication18:1} \hypertarget{proposition:implication18:1}{} \mbox{(1)}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny Add \hyperref[axiom:AND-3]{axiom~5}} \\ 
\label{proposition:implication18:2} \hypertarget{proposition:implication18:2}{} \mbox{(2)}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny SubstPred $B$ by $C$ in \hyperref[proposition:implication18/1]{(1)}} \\ 
\label{proposition:implication18:3} \hypertarget{proposition:implication18:3}{} \mbox{(3)}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny SubstPred $A$ by $B$ in \hyperref[proposition:implication18/2]{(2)}} \\ 
\label{proposition:implication18:4} \hypertarget{proposition:implication18:4}{} \mbox{(4)}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ A))$ \ &  \ {\tiny SubstPred $C$ by $A$ in \hyperref[proposition:implication18/3]{(3)}} \\ 
\label{proposition:implication18:5} \hypertarget{proposition:implication18:5}{} \mbox{(5)}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny Add \hyperref[axiom:AND-1]{axiom~3}} \\ 
\label{proposition:implication18:6} \hypertarget{proposition:implication18:6}{} \mbox{(6)}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny Add \hyperref[axiom:AND-2]{axiom~4}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication18:7} \hypertarget{proposition:implication18:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}$A\ \land\ B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication18:8} \hypertarget{proposition:implication18:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny MP \hyperref[proposition:implication18/5]{(5)}, \hyperref[proposition:implication18/7]{(7)}} \\ 
\label{proposition:implication18:9} \hypertarget{proposition:implication18:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ (B\ \land\ A)$ \ &  \ {\tiny MP \hyperref[proposition:implication18/4]{(4)}, \hyperref[proposition:implication18/8]{(8)}} \\ 
\label{proposition:implication18:10} \hypertarget{proposition:implication18:10}{} \mbox{(10)}  \ &  \ \mbox{\qquad}$B$ \ &  \ {\tiny MP \hyperref[proposition:implication18/6]{(6)}, \hyperref[proposition:implication18/7]{(7)}} \\ 
\label{proposition:implication18:11} \hypertarget{proposition:implication18:11}{} \mbox{(11)}  \ &  \ \mbox{\qquad}$B\ \land\ A$ \ &  \ {\tiny MP \hyperref[proposition:implication18/9]{(9)}, \hyperref[proposition:implication18/10]{(10)}} \\ 
\label{proposition:implication18:12} \hypertarget{proposition:implication18:12}{} \mbox{(12)}  \ &  \ $(A\ \land\ B)\ \rightarrow\ (B\ \land\ A)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication20} \hypertarget{proposition:implication20}{}
{\tt \tiny [\verb]proposition:implication20]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ \neg \neg A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication20:1} \hypertarget{proposition:implication20:1}{} \mbox{(1)}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny Add \hyperref[axiom:THEN-1]{axiom~1}} \\ 
\label{proposition:implication20:2} \hypertarget{proposition:implication20:2}{} \mbox{(2)}  \ &  \ $A\ \rightarrow\ (\neg A\ \rightarrow\ A)$ \ &  \ {\tiny SubstPred $B$ by $\neg A$ in \hyperref[proposition:implication20/1]{(1)}} \\ 
\label{proposition:implication20:3} \hypertarget{proposition:implication20:3}{} \mbox{(3)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny Add \hyperref[axiom:NOT-1]{axiom~9}} \\ 
\label{proposition:implication20:4} \hypertarget{proposition:implication20:4}{} \mbox{(4)}  \ &  \ $(\neg A\ \rightarrow\ B)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg B)\ \rightarrow\ \neg \neg A)$ \ &  \ {\tiny SubstPred $A$ by $\neg A$ in \hyperref[proposition:implication20/3]{(3)}} \\ 
\label{proposition:implication20:5} \hypertarget{proposition:implication20:5}{} \mbox{(5)}  \ &  \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A)$ \ &  \ {\tiny SubstPred $B$ by $A$ in \hyperref[proposition:implication20/4]{(4)}} \\ 
\label{proposition:implication20:6} \hypertarget{proposition:implication20:6}{} \mbox{(6)}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny Add \hyperref[proposition:implicationReflexive1]{proposition~1}} \\ 
\label{proposition:implication20:7} \hypertarget{proposition:implication20:7}{} \mbox{(7)}  \ &  \ $\neg A\ \rightarrow\ \neg A$ \ &  \ {\tiny SubstPred $A$ by $\neg A$ in \hyperref[proposition:implication20/6]{(6)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication20:8} \hypertarget{proposition:implication20:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication20:9} \hypertarget{proposition:implication20:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ &  \ {\tiny MP \hyperref[proposition:implication20/2]{(2)}, \hyperref[proposition:implication20/8]{(8)}} \\ 
\label{proposition:implication20:10} \hypertarget{proposition:implication20:10}{} \mbox{(10)}  \ &  \ \mbox{\qquad}$(\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication20/5]{(5)}, \hyperref[proposition:implication20/9]{(9)}} \\ 
\label{proposition:implication20:11} \hypertarget{proposition:implication20:11}{} \mbox{(11)}  \ &  \ \mbox{\qquad}$\neg \neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication20/10]{(10)}, \hyperref[proposition:implication20/7]{(7)}} \\ 
\label{proposition:implication20:12} \hypertarget{proposition:implication20:12}{} \mbox{(12)}  \ &  \ $A\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication21} \hypertarget{proposition:implication21}{}
{\tt \tiny [\verb]proposition:implication21]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication21:1} \hypertarget{proposition:implication21:1}{} \mbox{(1)}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny Add \hyperref[axiom:THEN-1]{axiom~1}} \\ 
\label{proposition:implication21:2} \hypertarget{proposition:implication21:2}{} \mbox{(2)}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny SubstPred $A$ by $C$ in \hyperref[proposition:implication21/1]{(1)}} \\ 
\label{proposition:implication21:3} \hypertarget{proposition:implication21:3}{} \mbox{(3)}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny SubstPred $B$ by $A$ in \hyperref[proposition:implication21/2]{(2)}} \\ 
\label{proposition:implication21:4} \hypertarget{proposition:implication21:4}{} \mbox{(4)}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny SubstPred $C$ by $B$ in \hyperref[proposition:implication21/3]{(3)}} \\ 
\label{proposition:implication21:5} \hypertarget{proposition:implication21:5}{} \mbox{(5)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny Add \hyperref[axiom:NOT-1]{axiom~9}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication21:6} \hypertarget{proposition:implication21:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ \neg B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication21:7} \hypertarget{proposition:implication21:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication21:8} \hypertarget{proposition:implication21:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny MP \hyperref[proposition:implication21/4]{(4)}, \hyperref[proposition:implication21/7]{(7)}} \\ 
\label{proposition:implication21:9} \hypertarget{proposition:implication21:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$(A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication21/5]{(5)}, \hyperref[proposition:implication21/8]{(8)}} \\ 
\label{proposition:implication21:10} \hypertarget{proposition:implication21:10}{} \mbox{(10)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$\neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication21/9]{(9)}, \hyperref[proposition:implication21/6]{(6)}} \\ 
\label{proposition:implication21:11} \hypertarget{proposition:implication21:11}{} \mbox{(11)}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ \neg A$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication21:12} \hypertarget{proposition:implication21:12}{} \mbox{(12)}  \ &  \ $(A\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg A)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication22} \hypertarget{proposition:implication22}{}
{\tt \tiny [\verb]proposition:implication22]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ (\neg B\ \rightarrow\ \neg A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication22:1} \hypertarget{proposition:implication22:1}{} \mbox{(1)}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny Add \hyperref[axiom:THEN-1]{axiom~1}} \\ 
\label{proposition:implication22:2} \hypertarget{proposition:implication22:2}{} \mbox{(2)}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny SubstPred $A$ by $C$ in \hyperref[proposition:implication22/1]{(1)}} \\ 
\label{proposition:implication22:3} \hypertarget{proposition:implication22:3}{} \mbox{(3)}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny SubstPred $B$ by $A$ in \hyperref[proposition:implication22/2]{(2)}} \\ 
\label{proposition:implication22:4} \hypertarget{proposition:implication22:4}{} \mbox{(4)}  \ &  \ $\neg B\ \rightarrow\ (A\ \rightarrow\ \neg B)$ \ &  \ {\tiny SubstPred $C$ by $\neg B$ in \hyperref[proposition:implication22/3]{(3)}} \\ 
\label{proposition:implication22:5} \hypertarget{proposition:implication22:5}{} \mbox{(5)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny Add \hyperref[axiom:NOT-1]{axiom~9}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication22:6} \hypertarget{proposition:implication22:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication22:7} \hypertarget{proposition:implication22:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication22/5]{(5)}, \hyperref[proposition:implication22/6]{(6)}} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication22:8} \hypertarget{proposition:implication22:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$\neg B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication22:9} \hypertarget{proposition:implication22:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ \neg B$ \ &  \ {\tiny MP \hyperref[proposition:implication22/4]{(4)}, \hyperref[proposition:implication22/8]{(8)}} \\ 
\label{proposition:implication22:10} \hypertarget{proposition:implication22:10}{} \mbox{(10)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$\neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication22/7]{(7)}, \hyperref[proposition:implication22/9]{(9)}} \\ 
\label{proposition:implication22:11} \hypertarget{proposition:implication22:11}{} \mbox{(11)}  \ &  \ \mbox{\qquad}$\neg B\ \rightarrow\ \neg A$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication22:12} \hypertarget{proposition:implication22:12}{} \mbox{(12)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ (\neg B\ \rightarrow\ \neg A)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication31} \hypertarget{proposition:implication31}{}
{\tt \tiny [\verb]proposition:implication31]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\neg \neg \neg A\ \rightarrow\ \neg A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication31:1} \hypertarget{proposition:implication31:1}{} \mbox{(1)}  \ &  \ $A\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny Add \hyperref[proposition:implication20]{proposition~11}} \\ 
\label{proposition:implication31:2} \hypertarget{proposition:implication31:2}{} \mbox{(2)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ (\neg B\ \rightarrow\ \neg A)$ \ &  \ {\tiny Add \hyperref[proposition:implication22]{proposition~13}} \\ 
\label{proposition:implication31:3} \hypertarget{proposition:implication31:3}{} \mbox{(3)}  \ &  \ $(A\ \rightarrow\ \neg \neg A)\ \rightarrow\ (\neg \neg \neg A\ \rightarrow\ \neg A)$ \ &  \ {\tiny SubstPred $B$ by $\neg \neg A$ in \hyperref[proposition:implication31/2]{(2)}} \\ 
\label{proposition:implication31:4} \hypertarget{proposition:implication31:4}{} \mbox{(4)}  \ &  \ $\neg \neg \neg A\ \rightarrow\ \neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication31/3]{(3)}, \hyperref[proposition:implication31/1]{(1)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication33} \hypertarget{proposition:implication33}{}
{\tt \tiny [\verb]proposition:implication33]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(\neg A\ \rightarrow\ A)\ \rightarrow\ \neg \neg A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication33:1} \hypertarget{proposition:implication33:1}{} \mbox{(1)}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny Add \hyperref[proposition:implicationReflexive1]{proposition~1}} \\ 
\label{proposition:implication33:2} \hypertarget{proposition:implication33:2}{} \mbox{(2)}  \ &  \ $\neg A\ \rightarrow\ \neg A$ \ &  \ {\tiny SubstPred $A$ by $\neg A$ in \hyperref[proposition:implication33/1]{(1)}} \\ 
\label{proposition:implication33:3} \hypertarget{proposition:implication33:3}{} \mbox{(3)}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny Add \hyperref[axiom:NOT-1]{axiom~9}} \\ 
\label{proposition:implication33:4} \hypertarget{proposition:implication33:4}{} \mbox{(4)}  \ &  \ $(\neg A\ \rightarrow\ B)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg B)\ \rightarrow\ \neg \neg A)$ \ &  \ {\tiny SubstPred $A$ by $\neg A$ in \hyperref[proposition:implication33/3]{(3)}} \\ 
\label{proposition:implication33:5} \hypertarget{proposition:implication33:5}{} \mbox{(5)}  \ &  \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A)$ \ &  \ {\tiny SubstPred $B$ by $A$ in \hyperref[proposition:implication33/4]{(4)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication33:6} \hypertarget{proposition:implication33:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication33:7} \hypertarget{proposition:implication33:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}$(\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication33/5]{(5)}, \hyperref[proposition:implication33/6]{(6)}} \\ 
\label{proposition:implication33:8} \hypertarget{proposition:implication33:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}$\neg \neg A$ \ &  \ {\tiny MP \hyperref[proposition:implication33/7]{(7)}, \hyperref[proposition:implication33/2]{(2)}} \\ 
\label{proposition:implication33:9} \hypertarget{proposition:implication33:9}{} \mbox{(9)}  \ &  \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication35} \hypertarget{proposition:implication35}{}
{\tt \tiny [\verb]proposition:implication35]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\neg \neg A\ \rightarrow\ A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication35:1} \hypertarget{proposition:implication35:1}{} \mbox{(1)}  \ &  \ $A\ \lor\ \neg A$ \ &  \ {\tiny Add \hyperref[axiom:NOT-3]{axiom~11}} \\ 
\label{proposition:implication35:2} \hypertarget{proposition:implication35:2}{} \mbox{(2)}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny Add \hyperref[axiom:OR-3]{axiom~8}} \\ 
\label{proposition:implication35:3} \hypertarget{proposition:implication35:3}{} \mbox{(3)}  \ &  \ $(A\ \rightarrow\ A)\ \rightarrow\ ((B\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ A))$ \ &  \ {\tiny SubstPred $C$ by $A$ in \hyperref[proposition:implication35/2]{(2)}} \\ 
\label{proposition:implication35:4} \hypertarget{proposition:implication35:4}{} \mbox{(4)}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny Add \hyperref[proposition:implicationReflexive1]{proposition~1}} \\ 
\label{proposition:implication35:5} \hypertarget{proposition:implication35:5}{} \mbox{(5)}  \ &  \ $(B\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ A)$ \ &  \ {\tiny MP \hyperref[proposition:implication35/3]{(3)}, \hyperref[proposition:implication35/4]{(4)}} \\ 
\label{proposition:implication35:6} \hypertarget{proposition:implication35:6}{} \mbox{(6)}  \ &  \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ \neg A)\ \rightarrow\ A)$ \ &  \ {\tiny SubstPred $B$ by $\neg A$ in \hyperref[proposition:implication35/5]{(5)}} \\ 
\label{proposition:implication35:7} \hypertarget{proposition:implication35:7}{} \mbox{(7)}  \ &  \ $\neg A\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny Add \hyperref[axiom:NOT-2]{axiom~10}} \\ 
\label{proposition:implication35:8} \hypertarget{proposition:implication35:8}{} \mbox{(8)}  \ &  \ $\neg \neg A\ \rightarrow\ (\neg A\ \rightarrow\ B)$ \ &  \ {\tiny SubstPred $A$ by $\neg A$ in \hyperref[proposition:implication35/7]{(7)}} \\ 
\label{proposition:implication35:9} \hypertarget{proposition:implication35:9}{} \mbox{(9)}  \ &  \ $\neg \neg A\ \rightarrow\ (\neg A\ \rightarrow\ A)$ \ &  \ {\tiny SubstPred $B$ by $A$ in \hyperref[proposition:implication35/8]{(8)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication35:10} \hypertarget{proposition:implication35:10}{} \mbox{(10)}  \ &  \ \mbox{\qquad}$\neg \neg A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication35:11} \hypertarget{proposition:implication35:11}{} \mbox{(11)}  \ &  \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ &  \ {\tiny MP \hyperref[proposition:implication35/9]{(9)}, \hyperref[proposition:implication35/10]{(10)}} \\ 
\label{proposition:implication35:12} \hypertarget{proposition:implication35:12}{} \mbox{(12)}  \ &  \ \mbox{\qquad}$(A\ \lor\ \neg A)\ \rightarrow\ A$ \ &  \ {\tiny MP \hyperref[proposition:implication35/6]{(6)}, \hyperref[proposition:implication35/11]{(11)}} \\ 
\label{proposition:implication35:13} \hypertarget{proposition:implication35:13}{} \mbox{(13)}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny MP \hyperref[proposition:implication35/12]{(12)}, \hyperref[proposition:implication35/1]{(1)}} \\ 
\label{proposition:implication35:14} \hypertarget{proposition:implication35:14}{} \mbox{(14)}  \ &  \ $\neg \neg A\ \rightarrow\ A$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication43} \hypertarget{proposition:implication43}{}
{\tt \tiny [\verb]proposition:implication43]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ C)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication43:1} \hypertarget{proposition:implication43:1}{} \mbox{(1)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication43:2} \hypertarget{proposition:implication43:2}{} \mbox{(2)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \land\ B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication43:3} \hypertarget{proposition:implication43:3}{} \mbox{(3)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny Add \hyperref[axiom:AND-1]{axiom~3}} \\ 
\label{proposition:implication43:4} \hypertarget{proposition:implication43:4}{} \mbox{(4)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny MP \hyperref[proposition:implication43/3]{(3)}, \hyperref[proposition:implication43/2]{(2)}} \\ 
\label{proposition:implication43:5} \hypertarget{proposition:implication43:5}{} \mbox{(5)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny Add \hyperref[axiom:AND-2]{axiom~4}} \\ 
\label{proposition:implication43:6} \hypertarget{proposition:implication43:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny MP \hyperref[proposition:implication43/5]{(5)}, \hyperref[proposition:implication43/2]{(2)}} \\ 
\label{proposition:implication43:7} \hypertarget{proposition:implication43:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny MP \hyperref[proposition:implication43/1]{(1)}, \hyperref[proposition:implication43/4]{(4)}} \\ 
\label{proposition:implication43:8} \hypertarget{proposition:implication43:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny MP \hyperref[proposition:implication43/7]{(7)}, \hyperref[proposition:implication43/6]{(6)}} \\ 
\label{proposition:implication43:9} \hypertarget{proposition:implication43:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication43:10} \hypertarget{proposition:implication43:10}{} \mbox{(10)}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


\begin{prop}
\label{proposition:implication44} \hypertarget{proposition:implication44}{}
{\tt \tiny [\verb]proposition:implication44]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \land\ B)\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication44:1} \hypertarget{proposition:implication44:1}{} \mbox{(1)}  \ &  \ \mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ C$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication44:2} \hypertarget{proposition:implication44:2}{} \mbox{(2)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication44:3} \hypertarget{proposition:implication44:3}{} \mbox{(3)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny Add \hyperref[axiom:AND-3]{axiom~5}} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication44:4} \hypertarget{proposition:implication44:4}{} \mbox{(4)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication44:5} \hypertarget{proposition:implication44:5}{} \mbox{(5)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ (A\ \land\ B)$ \ &  \ {\tiny MP \hyperref[proposition:implication44/3]{(3)}, \hyperref[proposition:implication44/4]{(4)}} \\ 
\label{proposition:implication44:6} \hypertarget{proposition:implication44:6}{} \mbox{(6)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \land\ B$ \ &  \ {\tiny MP \hyperref[proposition:implication44/5]{(5)}, \hyperref[proposition:implication44/2]{(2)}} \\ 
\label{proposition:implication44:7} \hypertarget{proposition:implication44:7}{} \mbox{(7)}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny MP \hyperref[proposition:implication44/1]{(1)}, \hyperref[proposition:implication44/6]{(6)}} \\ 
\label{proposition:implication44:8} \hypertarget{proposition:implication44:8}{} \mbox{(8)}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication44:9} \hypertarget{proposition:implication44:9}{} \mbox{(9)}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication44:10} \hypertarget{proposition:implication44:10}{} \mbox{(10)}  \ &  \ $((A\ \land\ B)\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}





%% end of chapter Axioms and Rules of Inference

\backmatter

\begin{thebibliography}{99}
\addcontentsline{toc}{chapter}{Bibliography}
\bibitem{novikov} \emph{P.S. Novikov}, Elements of Mathematical Logic, Edinburgh: Oliver and Boyd, 1964.

\bibitem{detnieks} \emph{V.~Detlovs, K.~Podnieks}, Introduction to Mathematical Logic, 
           \url{http://www.ltn.lv/~podnieks/mlog/ml.htm}.

\bibitem{hilback} \emph{D.~Hilbert, W.~Ackermann}, Grundz{\"u}ge der theoretischen Logik, 2nd ed., Berlin: Springer, 1938. English version: Principles of Mathematical Logic, Chelsea, New York 1950, ed. by R.~E.~Luce.
           See also \url{http://www.math.uwaterloo.ca/~snburris/htdocs/scav/hilbert/hilbert.html}

\bibitem{mendelson} \emph{E.~Mendelson}, Introduction to Mathematical Logic, 3rd. ed., Belmont, CA: Wadsworth, 1987.



%% QEDEQ modules that use this one:
\bibitem{qedeq_logic_v1} qedeq\_logic\_v1 \url{http://www.qedeq.org/0_04_03/doc/math/qedeq_logic_v1.xml}


\end{thebibliography}
\addcontentsline{toc}{chapter}{\indexname} \printindex

\end{document}