% -*- TeX:EN -*-
%%% ====================================================================
%%% $RCSfile: Module2Latex.java,v $
%%% $Revision: 1.28 $
%%% ====================================================================
%%%
%%% Generated by class com.meyling.principia.latex.Module2Latex
%%% at 2004-09-26T23:33:11+0200.
%%%
%%% Project Hilbert II - http://www.qedeq.org
%%% Copyright 2001, 2002, 2003, 2004 Michael Meyling (mime@qedeq.org)
%%%
%%% This file is part of *Principia Mathematica II*, the prototype of
%%% Hilbert II.
%%%
%%% 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]{article}

\usepackage{amsmath,amsthm,amsfonts}
\usepackage[]{color}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{varioref}
\usepackage[bookmarksnumbered,colorlinks,breaklinks,plainpages,backref,bookmarksopen=true,pdfpagemode=None]{hyperref}

\oddsidemargin       8mm
\evensidemargin      9mm
\topmargin           0mm
\headsep             10mm
\marginparsep        2.5mm
\marginparwidth      25mm
\textwidth           160mm
\textheight          220mm


\newtheorem{axm}{Axiom}[section]
\newtheorem{abr}{Abbreviation}[section]
\newtheorem{thm}{Theorem}[section]
\newtheorem{dec}{Rule Declaration}[section]
\newtheorem{cor}[thm]{Corollary}
\newtheorem{prop}{Proposition}
\newtheorem{lem}[thm]{Lemma}
\theoremstyle{remark}
\newtheorem*{rmk}{Remark}

\makeindex
\makeatletter
\externaldocument{proptheo2_1.00.00_1.00.00.qedeq}
\hyperbaseurl{proptheo2_1.00.00_1.00.00.qedeq}
\makeatother

\setlength{\LTleft}{0pt}
\setlength{\LTright}{0pt}

\setlength{\parindent}{0pt}
\frenchspacing \sloppy
\pagestyle{headings}

\title{The Axioms of the Whitehead Russell Calculus}
\author{Michael Meyling}
\date{\tt <module@qedeq.org>}


\begin{document}

\maketitle

\setlongtables



{\small
This document is part of the project ``Hilbert II''.
To get more information about this project look at:\\
\mbox{\url{http://www.qedeq.org}}.


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. See also under \url{http://www.gnu.org/copyleft/}
}


\section*{Abstract}

This module notates the original axioms of the Whitehead-Russell calculus, the so called `primitive propositions'. These five primitive propositions could be deduced by our four axioms.


\section*{Specification}

This document has the following specification:

\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & proptheo2 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{http://www.qedeq.org/0_00_53/proptheo2_1.00.00_1.00.00.qedeq} \\
\end{longtable}

\medskip

Author of this module: 
\begin{longtable}[h!]{l@{\extracolsep{\fill}}l}
Michael Meyling & mime@qedeq.org \\
\end{longtable}




\section*{References}

This document uses the results of the following documents:

\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & propaxiom \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{propaxiom_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{propaxiom_1.00.00_1.00.00.pdf}  \\
\end{longtable}


\section*{Content}




At first we show a little proposition to demonstrate the basic proof methods of propositional calculus:




\begin{thm}[lem1]
\hypertarget{lem1}{}
\begin{displaymath}
P\ \rightarrow \  (Q\ \vee \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{lem1:1}
  $1$ & $(P\ \rightarrow \  Q)\ \rightarrow \  ((A\ \vee \  P)\ \rightarrow \  (A\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{lem1:2}
  $2$ & $(B\ \rightarrow \  Q)\ \rightarrow \  ((A\ \vee \  B)\ \rightarrow \  (A\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[lem1:1]{$1$}
} \\
\label{lem1:3}
  $3$ & $(B\ \rightarrow \  (Q\ \vee \  P))\ \rightarrow \  ((A\ \vee \  B)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $Q\ \vee \  P$ in \hyperref[lem1:2]{$2$}
} \\
\label{lem1:4}
  $4$ & $((P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P))\ \rightarrow \  ((A\ \vee \  (P\ \vee \  Q))\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P\ \vee \  Q$ in \hyperref[lem1:3]{$3$}
} \\
\label{lem1:5}
  $5$ & $((P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P))\ \rightarrow \  ((\neg P\ \vee \  (P\ \vee \  Q))\ \rightarrow \  (\neg P\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $\neg P$ in \hyperref[lem1:4]{$4$}
} \\
\label{lem1:6}
  $6$ & $((P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P))\ \rightarrow \  ((P\ \rightarrow \  (P\ \vee \  Q))\ \rightarrow \  (\neg P\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[lem1:5]{$5$} at occurence $1$
} \\
\label{lem1:7}
  $7$ & $((P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P))\ \rightarrow \  ((P\ \rightarrow \  (P\ \vee \  Q))\ \rightarrow \  (P\ \rightarrow \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[lem1:6]{$6$} at occurence $1$
} \\
\label{lem1:8}
  $8$ & $(P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{lem1:9}
  $9$ & $(P\ \rightarrow \  (P\ \vee \  Q))\ \rightarrow \  (P\ \rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[lem1:8]{$8$}, \hyperref[lem1:7]{$7$}} \\
\label{lem1:10}
  $10$ & $P\ \rightarrow \  (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{lem1:11}
  $11$ & $P\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[lem1:10]{$10$}, \hyperref[lem1:9]{$9$}} \\
 & & \qedhere
\end{longtable}
\end{proof}



This is the first primitive proposition, its equal to our first axiom:




\begin{thm}[prin1]
\hypertarget{prin1}{}
\begin{displaymath}
(P\ \vee \  P)\ \rightarrow \  P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{prin1:1}
  $1$ & $(P\ \vee \  P)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom1}{axiom1} } \\
 & & \qedhere
\end{longtable}
\end{proof}



Now comes the second primitive proposition. It looks simular to our second axiom, but we have to use our first proposition to prove it:




\begin{thm}[prin2]
\hypertarget{prin2}{}
\begin{displaymath}
Q\ \rightarrow \  (P\ \vee \  Q)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{prin2:1}
  $1$ & $P\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{lem1}{lem1} } \\
\label{prin2:2}
  $2$ & $P\ \rightarrow \  (A\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[prin2:1]{$1$}
} \\
\label{prin2:3}
  $3$ & $Q\ \rightarrow \  (A\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[prin2:2]{$2$}
} \\
\label{prin2:4}
  $4$ & $Q\ \rightarrow \  (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P$ in \hyperref[prin2:3]{$3$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The third primitive proposition:




\begin{thm}[prin3]
\hypertarget{prin3}{}
\begin{displaymath}
(P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{prin3:1}
  $1$ & $(P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
 & & \qedhere
\end{longtable}
\end{proof}



The fourth primitive proposition was proved with the other primitve propositions by P. Bernays. Here comes the sledgehammer:




\begin{thm}[prin4]
\hypertarget{prin4}{}
\begin{displaymath}
(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{prin4:1}
  $1$ & $(P\ \rightarrow \  Q)\ \rightarrow \  ((A\ \vee \  P)\ \rightarrow \  (A\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{prin4:2}
  $2$ & $(P_{7}\ \rightarrow \  Q)\ \rightarrow \  ((A\ \vee \  P_{7})\ \rightarrow \  (A\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $P_{7}$ in \hyperref[prin4:1]{$1$}
} \\
\label{prin4:3}
  $3$ & $(P_{7}\ \rightarrow \  P_{8})\ \rightarrow \  ((A\ \vee \  P_{7})\ \rightarrow \  (A\ \vee \  P_{8}))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P_{8}$ in \hyperref[prin4:2]{$2$}
} \\
\label{prin4:4}
  $4$ & $(P_{7}\ \rightarrow \  P_{8})\ \rightarrow \  ((P_{9}\ \vee \  P_{7})\ \rightarrow \  (P_{9}\ \vee \  P_{8}))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P_{9}$ in \hyperref[prin4:3]{$3$}
} \\
\label{prin4:5}
  $5$ & $P\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{lem1}{lem1} } \\
\label{prin4:6}
  $6$ & $(P\ \rightarrow \  (Q\ \vee \  P))\ \rightarrow \  ((A\ \vee \  P)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $Q\ \vee \  P$ in \hyperref[prin4:1]{$1$}
} \\
\label{prin4:7}
  $7$ & $(A\ \vee \  P)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:5]{$5$}, \hyperref[prin4:6]{$6$}} \\
\label{prin4:8}
  $8$ & $((A\ \vee \  P)\ \rightarrow \  P_{8})\ \rightarrow \  ((P_{9}\ \vee \  (A\ \vee \  P))\ \rightarrow \  (P_{9}\ \vee \  P_{8}))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{7}$ by $A\ \vee \  P$ in \hyperref[prin4:4]{$4$}
} \\
\label{prin4:9}
  $9$ & $((A\ \vee \  P)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  ((P_{9}\ \vee \  (A\ \vee \  P))\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{8}$ by $A\ \vee \  (Q\ \vee \  P)$ in \hyperref[prin4:8]{$8$}
} \\
\label{prin4:10}
  $10$ & $(P_{9}\ \vee \  (A\ \vee \  P))\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:7]{$7$}, \hyperref[prin4:9]{$9$}} \\
\label{prin4:11}
  $11$ & $(Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  (Q\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{9}$ by $Q$ in \hyperref[prin4:10]{$10$}
} \\
\label{prin4:12}
  $12$ & $(P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{prin4:13}
  $13$ & $(D\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  D)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[prin4:12]{$12$}
} \\
\label{prin4:14}
  $14$ & $(D\ \vee \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  D)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A\ \vee \  (Q\ \vee \  P)$ in \hyperref[prin4:13]{$13$}
} \\
\label{prin4:15}
  $15$ & $(Q\ \vee \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $Q$ in \hyperref[prin4:14]{$14$}
} \\
\label{prin4:16}
  $16$ & $((Q\ \vee \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  P_{8})\ \rightarrow \  ((P_{9}\ \vee \  (Q\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (P_{9}\ \vee \  P_{8}))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{7}$ by $Q\ \vee \  (A\ \vee \  (Q\ \vee \  P))$ in \hyperref[prin4:4]{$4$}
} \\
\label{prin4:17}
  $17$ & $((Q\ \vee \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))\ \rightarrow \  ((P_{9}\ \vee \  (Q\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (P_{9}\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{8}$ by $(A\ \vee \  (Q\ \vee \  P))\ \vee \  Q$ in \hyperref[prin4:16]{$16$}
} \\
\label{prin4:18}
  $18$ & $(P_{9}\ \vee \  (Q\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (P_{9}\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:15]{$15$}, \hyperref[prin4:17]{$17$}} \\
\label{prin4:19}
  $19$ & $(\neg (Q\ \vee \  (A\ \vee \  P))\ \vee \  (Q\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (\neg (Q\ \vee \  (A\ \vee \  P))\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{9}$ by $\neg (Q\ \vee \  (A\ \vee \  P))$ in \hyperref[prin4:18]{$18$}
} \\
\label{prin4:20}
  $20$ & $((Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  (Q\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (\neg (Q\ \vee \  (A\ \vee \  P))\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[prin4:19]{$19$} at occurence $1$
} \\
\label{prin4:21}
  $21$ & $((Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  (Q\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  ((Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[prin4:20]{$20$} at occurence $1$
} \\
\label{prin4:22}
  $22$ & $(Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:11]{$11$}, \hyperref[prin4:21]{$21$}} \\
\label{prin4:23}
  $23$ & $P\ \rightarrow \  (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{prin4:24}
  $24$ & $A\ \rightarrow \  (A\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A$ in \hyperref[prin4:23]{$23$}
} \\
\label{prin4:25}
  $25$ & $A\ \rightarrow \  (A\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[prin4:24]{$24$}
} \\
\label{prin4:26}
  $26$ & $Q\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $Q$ in \hyperref[prin4:25]{$25$}
} \\
\label{prin4:27}
  $27$ & $P\ \rightarrow \  (A\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[prin4:5]{$5$}
} \\
\label{prin4:28}
  $28$ & $(Q\ \vee \  P)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q\ \vee \  P$ in \hyperref[prin4:27]{$27$}
} \\
\label{prin4:29}
  $29$ & $((Q\ \vee \  P)\ \rightarrow \  P_{8})\ \rightarrow \  ((P_{9}\ \vee \  (Q\ \vee \  P))\ \rightarrow \  (P_{9}\ \vee \  P_{8}))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{7}$ by $Q\ \vee \  P$ in \hyperref[prin4:4]{$4$}
} \\
\label{prin4:30}
  $30$ & $((Q\ \vee \  P)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  ((P_{9}\ \vee \  (Q\ \vee \  P))\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{8}$ by $A\ \vee \  (Q\ \vee \  P)$ in \hyperref[prin4:29]{$29$}
} \\
\label{prin4:31}
  $31$ & $(P_{9}\ \vee \  (Q\ \vee \  P))\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:28]{$28$}, \hyperref[prin4:30]{$30$}} \\
\label{prin4:32}
  $32$ & $(\neg Q\ \vee \  (Q\ \vee \  P))\ \rightarrow \  (\neg Q\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{9}$ by $\neg Q$ in \hyperref[prin4:31]{$31$}
} \\
\label{prin4:33}
  $33$ & $(Q\ \rightarrow \  (Q\ \vee \  P))\ \rightarrow \  (\neg Q\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[prin4:32]{$32$} at occurence $1$
} \\
\label{prin4:34}
  $34$ & $(Q\ \rightarrow \  (Q\ \vee \  P))\ \rightarrow \  (Q\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[prin4:33]{$33$} at occurence $1$
} \\
\label{prin4:35}
  $35$ & $Q\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:26]{$26$}, \hyperref[prin4:34]{$34$}} \\
\label{prin4:36}
  $36$ & $(Q\ \rightarrow \  P_{8})\ \rightarrow \  ((P_{9}\ \vee \  Q)\ \rightarrow \  (P_{9}\ \vee \  P_{8}))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{7}$ by $Q$ in \hyperref[prin4:4]{$4$}
} \\
\label{prin4:37}
  $37$ & $(Q\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  ((P_{9}\ \vee \  Q)\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{8}$ by $A\ \vee \  (Q\ \vee \  P)$ in \hyperref[prin4:36]{$36$}
} \\
\label{prin4:38}
  $38$ & $(P_{9}\ \vee \  Q)\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:35]{$35$}, \hyperref[prin4:37]{$37$}} \\
\label{prin4:39}
  $39$ & $((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{9}$ by $A\ \vee \  (Q\ \vee \  P)$ in \hyperref[prin4:38]{$38$}
} \\
\label{prin4:40}
  $40$ & $(P\ \vee \  P)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom1}{axiom1} } \\
\label{prin4:41}
  $41$ & $((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A\ \vee \  (Q\ \vee \  P)$ in \hyperref[prin4:40]{$40$}
} \\
\label{prin4:42}
  $42$ & $(((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  P_{8})\ \rightarrow \  ((P_{9}\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (P_{9}\ \vee \  P_{8}))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{7}$ by $(A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P))$ in \hyperref[prin4:4]{$4$}
} \\
\label{prin4:43}
  $43$ & $(((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  ((P_{9}\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{8}$ by $A\ \vee \  (Q\ \vee \  P)$ in \hyperref[prin4:42]{$42$}
} \\
\label{prin4:44}
  $44$ & $(P_{9}\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:41]{$41$}, \hyperref[prin4:43]{$43$}} \\
\label{prin4:45}
  $45$ & $(\neg ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (\neg ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{9}$ by $\neg ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)$ in \hyperref[prin4:44]{$44$}
} \\
\label{prin4:46}
  $46$ & $(((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (\neg ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[prin4:45]{$45$} at occurence $1$
} \\
\label{prin4:47}
  $47$ & $(((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P))))\ \rightarrow \  (((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[prin4:46]{$46$} at occurence $1$
} \\
\label{prin4:48}
  $48$ & $((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:39]{$39$}, \hyperref[prin4:47]{$47$}} \\
\label{prin4:49}
  $49$ & $(((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \rightarrow \  P_{8})\ \rightarrow \  ((P_{9}\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))\ \rightarrow \  (P_{9}\ \vee \  P_{8}))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{7}$ by $(A\ \vee \  (Q\ \vee \  P))\ \vee \  Q$ in \hyperref[prin4:4]{$4$}
} \\
\label{prin4:50}
  $50$ & $(((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q)\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \rightarrow \  ((P_{9}\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{8}$ by $A\ \vee \  (Q\ \vee \  P)$ in \hyperref[prin4:49]{$49$}
} \\
\label{prin4:51}
  $51$ & $(P_{9}\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))\ \rightarrow \  (P_{9}\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:48]{$48$}, \hyperref[prin4:50]{$50$}} \\
\label{prin4:52}
  $52$ & $(\neg (Q\ \vee \  (A\ \vee \  P))\ \vee \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))\ \rightarrow \  (\neg (Q\ \vee \  (A\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{9}$ by $\neg (Q\ \vee \  (A\ \vee \  P))$ in \hyperref[prin4:51]{$51$}
} \\
\label{prin4:53}
  $53$ & $((Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))\ \rightarrow \  (\neg (Q\ \vee \  (A\ \vee \  P))\ \vee \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[prin4:52]{$52$} at occurence $1$
} \\
\label{prin4:54}
  $54$ & $((Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  ((A\ \vee \  (Q\ \vee \  P))\ \vee \  Q))\ \rightarrow \  ((Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[prin4:53]{$53$} at occurence $1$
} \\
\label{prin4:55}
  $55$ & $(Q\ \vee \  (A\ \vee \  P))\ \rightarrow \  (A\ \vee \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[prin4:22]{$22$}, \hyperref[prin4:54]{$54$}} \\
\label{prin4:56}
  $56$ & $(P_{7}\ \vee \  (A\ \vee \  P))\ \rightarrow \  (A\ \vee \  (P_{7}\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P_{7}$ in \hyperref[prin4:55]{$55$}
} \\
\label{prin4:57}
  $57$ & $(P_{7}\ \vee \  (Q\ \vee \  P))\ \rightarrow \  (Q\ \vee \  (P_{7}\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $Q$ in \hyperref[prin4:56]{$56$}
} \\
\label{prin4:58}
  $58$ & $(P_{7}\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (Q\ \vee \  (P_{7}\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A$ in \hyperref[prin4:57]{$57$}
} \\
\label{prin4:59}
  $59$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P_{7}$ by $P$ in \hyperref[prin4:58]{$58$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The fifth primitive proposition is our fourth axiom:




\begin{thm}[prin5]
\hypertarget{prin5}{}
\begin{displaymath}
(P\ \rightarrow \  Q)\ \rightarrow \  ((A\ \vee \  P)\ \rightarrow \  (A\ \vee \  Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{prin5:1}
  $1$ & $(P\ \rightarrow \  Q)\ \rightarrow \  ((A\ \vee \  P)\ \rightarrow \  (A\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
 & & \qedhere
\end{longtable}
\end{proof}


\end{document}