%%% ====================================================================
%%% @LaTeX-file generated by com.meyling.principia.latex.Module2Latex
%%% ====================================================================

\documentclass{amsart}

\usepackage{amsmath,amsthm,amsfonts}
\usepackage[]{color}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{varioref}
\usepackage[a4paper,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

\makeatletter
\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn\fi
\chapter*{List of Figures}
{\let\\ \ \markboth{Title}{List of Figures}}
\addcontentsline{toc}{chapter}{\protect
\numberline{LIST OF FIGURES\string\hss}}
\@starttoc{lof}\if@restonecol \twocolumn\fi}
\makeatother
\def\boldindex#1{\textbf{\hyperpage{#1}}}

\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{proptheo1_1.00.00_1.00.00.qedeq}
\hyperbaseurl{proptheo1_1.00.00_1.00.00.qedeq}
\makeatother

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

\sloppy

\begin{document}

\title{First theorems of Propositional Calculus}
\author{Michael Meyling}
\email{principa@meyling.com}
\date{2002-07-27T20:51:18}

\begin{abstract}
This module includes first proofs of propositional calculus theorems.
\end{abstract}

\makeatletter
\long\def\hyper@section@backref#1#2#3{%
\typeout{BACK REF #1 / #2 / #3}%
\hyperlink{#3}{#2}}
\makeatother
\pdfbookmark{Title}{tit}
\setlongtables
\maketitle
\tableofcontents


\section*{module specification}

Author of this module: 
\begin{longtable}[h!]{l@{\extracolsep{\fill}}l}
Michael Meyling & michael@meyling.com \\
\end{longtable}


\medskip
This module has the following specification:

\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & proptheo1 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{http://www.meyling.com/principia/0_00_51/proptheo1_1.00.00_1.00.00.qedeq} \\
\end{longtable}


\medskip
The following modules were used:

\mbox{}
\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}



First we prove a well known tautology:




\begin{thm}
\hypertarget{theo1}{}
\begin{displaymath}
(\neg P\ \vee \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{theo1: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{theo1:2}
  $2$ & $(((P\ \vee \  P)\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \vee \  (P\ \vee \  P))\ \Rightarrow \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $(P\ \vee \  P)$ in \hyperref[theo1:1]{$1$}
} \\
\label{theo1:3}
  $3$ & $(((P\ \vee \  P)\ \Rightarrow \  P)\ \Rightarrow \  ((A\ \vee \  (P\ \vee \  P))\ \Rightarrow \  (A\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[theo1:2]{$2$}
} \\
\label{theo1:4}
  $4$ & $(((P\ \vee \  P)\ \Rightarrow \  P)\ \Rightarrow \  ((\neg P\ \vee \  (P\ \vee \  P))\ \Rightarrow \  (\neg P\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $\neg P$ in \hyperref[theo1:3]{$3$}
} \\
\label{theo1:5}
  $5$ & $((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{theo1:6}
  $6$ & $((\neg P\ \vee \  (P\ \vee \  P))\ \Rightarrow \  (\neg P\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theo1:5]{$5$}, \hyperref[theo1:4]{$4$}} \\
\label{theo1:7}
  $7$ & $((P\ \Rightarrow \  (P\ \vee \  P))\ \Rightarrow \  (\neg P\ \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[theo1:6]{$6$} at occurence $1$
} \\
\label{theo1:8}
  $8$ & $(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{theo1:9}
  $9$ & $(P\ \Rightarrow \  (P\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[theo1:8]{$8$}
} \\
\label{theo1:10}
  $10$ & $(\neg P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theo1:9]{$9$}, \hyperref[theo1:7]{$7$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



We just use our first sentence to get the second theorem:




\begin{thm}
\hypertarget{theo2}{}
\begin{displaymath}
(P\ \Rightarrow \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{theo2:1}
  $1$ & $(\neg P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{theo1}{theo1} } \\
\label{theo2:2}
  $2$ & $(P\ \Rightarrow \  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[theo2:1]{$1$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



And another use of the first theorem, to get the law of the excluded middle (tertium non datur):




\begin{thm}
\hypertarget{theo3}{}
\begin{displaymath}
(P\ \vee \  \neg P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{theo3:1}
  $1$ & $(\neg P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{theo1}{theo1} } \\
\label{theo3:2}
  $2$ & $((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{theo3:3}
  $3$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $\neg P$ in \hyperref[theo3:2]{$2$}
} \\
\label{theo3:4}
  $4$ & $((\neg P\ \vee \  P)\ \Rightarrow \  (P\ \vee \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[theo3:3]{$3$}
} \\
\label{theo3:5}
  $5$ & $(P\ \vee \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theo3:1]{$1$}, \hyperref[theo3:4]{$4$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Also trivial is:




\begin{thm}
\hypertarget{theo4}{}
\begin{displaymath}
(P\ \Rightarrow \  \neg \neg P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{theo4:1}
  $1$ & $(P\ \vee \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{theo3}{theo3} } \\
\label{theo4:2}
  $2$ & $(\neg P\ \vee \  \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $\neg P$ in \hyperref[theo4:1]{$1$}
} \\
\label{theo4:3}
  $3$ & $(P\ \Rightarrow \  \neg \neg 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[theo4:2]{$2$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Three negations:




\begin{thm}
\hypertarget{theo5}{}
\begin{displaymath}
(P\ \vee \  \neg \neg \neg P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{theo5:1}
  $1$ & $(P\ \Rightarrow \  \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{theo4}{theo4} } \\
\label{theo5:2}
  $2$ & $((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{theo5:3}
  $3$ & $((P\ \Rightarrow \  \neg \neg P)\ \Rightarrow \  ((A\ \vee \  P)\ \Rightarrow \  (A\ \vee \  \neg \neg P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $\neg \neg P$ in \hyperref[theo5:2]{$2$}
} \\
\label{theo5:4}
  $4$ & $((A\ \vee \  P)\ \Rightarrow \  (A\ \vee \  \neg \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theo5:1]{$1$}, \hyperref[theo5:3]{$3$}} \\
\label{theo5:5}
  $5$ & $((A\ \vee \  \neg P)\ \Rightarrow \  (A\ \vee \  \neg \neg \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $\neg P$ in \hyperref[theo5:4]{$4$}
} \\
\label{theo5:6}
  $6$ & $((P\ \vee \  \neg P)\ \Rightarrow \  (P\ \vee \  \neg \neg \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P$ in \hyperref[theo5:5]{$5$}
} \\
\label{theo5:7}
  $7$ & $(P\ \vee \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{theo3}{theo3} } \\
\label{theo5:8}
  $8$ & $(P\ \vee \  \neg \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theo5:7]{$7$}, \hyperref[theo5:6]{$6$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Now we could prove the reverse of Proposition 4:




\begin{thm}
\hypertarget{theo6}{}
\begin{displaymath}
(\neg \neg P\ \Rightarrow \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{theo6:1}
  $1$ & $(P\ \vee \  \neg \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{theo5}{theo5} } \\
\label{theo6:2}
  $2$ & $((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{theo6:3}
  $3$ & $((P\ \vee \  \neg \neg \neg P)\ \Rightarrow \  (\neg \neg \neg P\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $\neg \neg \neg P$ in \hyperref[theo6:2]{$2$}
} \\
\label{theo6:4}
  $4$ & $(\neg \neg \neg P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theo6:1]{$1$}, \hyperref[theo6:3]{$3$}} \\
\label{theo6:5}
  $5$ & $(\neg \neg P\ \Rightarrow \  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[theo6:4]{$4$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}

\section*{}

\end{document}