% -*- TeX:EN -*-
%%% ====================================================================
%%% $RCSfile: Module2Latex.java,v $
%%% $Revision: 1.28 $
%%% ====================================================================
%%%
%%% Generated by class com.meyling.principia.latex.Module2Latex
%%% at 2004-09-26T23:33:09+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{luktheo1_1.00.00_1.00.00.qedeq}
\hyperbaseurl{luktheo1_1.00.00_1.00.00.qedeq}
\makeatother

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

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

\title{First theorems of Propositional Calculus}
\author{Franz Fritsche}
\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 includes first proofs of propositional calculus theorems.


\section*{Specification}

This document has the following specification:

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

\medskip

Authors of this module: 
\begin{longtable}[h!]{l@{\extracolsep{\fill}}l}
Franz Fritsche & ff@qedeq.org \\
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: & lukaxiom \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{lukaxiom_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{lukaxiom_1.00.00_1.00.00.pdf}  \\
\end{longtable}


\section*{Content}




First we prove a theorem known as {\emph identity}:




\begin{thm}[theorem1]
\hypertarget{theorem1}{}
\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{theorem1:1}
  $1$ & $P\ \rightarrow \  (Q\ \rightarrow \  P)$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{axiom1}{axiom1} } \\
\label{theorem1:2}
  $2$ & $P\ \rightarrow \  ((P\ \rightarrow \  P)\ \rightarrow \  P)$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P\ \rightarrow \  P$ in \hyperref[theorem1:1]{$1$}
} \\
\label{theorem1:3}
  $3$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{theorem1:4}
  $4$ & $(P\ \rightarrow \  ((P\ \rightarrow \  P)\ \rightarrow \  A))\ \rightarrow \  ((P\ \rightarrow \  (P\ \rightarrow \  P))\ \rightarrow \  (P\ \rightarrow \  A))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P\ \rightarrow \  P$ in \hyperref[theorem1:3]{$3$}
} \\
\label{theorem1:5}
  $5$ & $(P\ \rightarrow \  ((P\ \rightarrow \  P)\ \rightarrow \  P))\ \rightarrow \  ((P\ \rightarrow \  (P\ \rightarrow \  P))\ \rightarrow \  (P\ \rightarrow \  P))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P$ in \hyperref[theorem1:4]{$4$}
} \\
\label{theorem1:6}
  $6$ & $(P\ \rightarrow \  (P\ \rightarrow \  P))\ \rightarrow \  (P\ \rightarrow \  P)$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theorem1:2]{$2$}, \hyperref[theorem1:5]{$5$}} \\
\label{theorem1:7}
  $7$ & $P\ \rightarrow \  (P\ \rightarrow \  P)$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[theorem1:1]{$1$}
} \\
\label{theorem1:8}
  $8$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theorem1:7]{$7$}, \hyperref[theorem1:6]{$6$}} \\
 & & \qedhere
\end{longtable}
\end{proof}



Now we prove a theorem  known as (one form of) {\emph hypothetical syllogism}:




\begin{thm}[theorem2]
\hypertarget{theorem2}{}
\begin{displaymath}
(Q\ \rightarrow \  A)\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{theorem2:1}
  $1$ & $P\ \rightarrow \  (Q\ \rightarrow \  P)$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{axiom1}{axiom1} } \\
\label{theorem2:2}
  $2$ & $P\ \rightarrow \  ((Q\ \rightarrow \  A)\ \rightarrow \  P)$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $Q\ \rightarrow \  A$ in \hyperref[theorem2:1]{$1$}
} \\
\label{theorem2:3}
  $3$ & $((P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A)))\ \rightarrow \  ((Q\ \rightarrow \  A)\ \rightarrow \  ((P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A))))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A))$ in \hyperref[theorem2:2]{$2$}
} \\
\label{theorem2:4}
  $4$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{theorem2:5}
  $5$ & $(Q\ \rightarrow \  A)\ \rightarrow \  ((P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A)))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theorem2:4]{$4$}, \hyperref[theorem2:3]{$3$}} \\
\label{theorem2:6}
  $6$ & $(B\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((B\ \rightarrow \  Q)\ \rightarrow \  (B\ \rightarrow \  A))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[theorem2:4]{$4$}
} \\
\label{theorem2:7}
  $7$ & $(B\ \rightarrow \  (C\ \rightarrow \  A))\ \rightarrow \  ((B\ \rightarrow \  C)\ \rightarrow \  (B\ \rightarrow \  A))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[theorem2:6]{$6$}
} \\
\label{theorem2:8}
  $8$ & $(B\ \rightarrow \  (C\ \rightarrow \  D))\ \rightarrow \  ((B\ \rightarrow \  C)\ \rightarrow \  (B\ \rightarrow \  D))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $D$ in \hyperref[theorem2:7]{$7$}
} \\
\label{theorem2:9}
  $9$ & $((Q\ \rightarrow \  A)\ \rightarrow \  (C\ \rightarrow \  D))\ \rightarrow \  (((Q\ \rightarrow \  A)\ \rightarrow \  C)\ \rightarrow \  ((Q\ \rightarrow \  A)\ \rightarrow \  D))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q\ \rightarrow \  A$ in \hyperref[theorem2:8]{$8$}
} \\
\label{theorem2:10}
  $10$ & $((Q\ \rightarrow \  A)\ \rightarrow \  ((P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  D))\ \rightarrow \  (((Q\ \rightarrow \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A)))\ \rightarrow \  ((Q\ \rightarrow \  A)\ \rightarrow \  D))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $P\ \rightarrow \  (Q\ \rightarrow \  A)$ in \hyperref[theorem2:9]{$9$}
} \\
\label{theorem2:11}
  $11$ & $((Q\ \rightarrow \  A)\ \rightarrow \  ((P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A))))\ \rightarrow \  (((Q\ \rightarrow \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A)))\ \rightarrow \  ((Q\ \rightarrow \  A)\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A))))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A)$ in \hyperref[theorem2:10]{$10$}
} \\
\label{theorem2:12}
  $12$ & $((Q\ \rightarrow \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A)))\ \rightarrow \  ((Q\ \rightarrow \  A)\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A)))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theorem2:5]{$5$}, \hyperref[theorem2:11]{$11$}} \\
\label{theorem2:13}
  $13$ & $P\ \rightarrow \  (B\ \rightarrow \  P)$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[theorem2:1]{$1$}
} \\
\label{theorem2:14}
  $14$ & $(Q\ \rightarrow \  A)\ \rightarrow \  (B\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q\ \rightarrow \  A$ in \hyperref[theorem2:13]{$13$}
} \\
\label{theorem2:15}
  $15$ & $(Q\ \rightarrow \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[theorem2:14]{$14$}
} \\
\label{theorem2:16}
  $16$ & $(Q\ \rightarrow \  A)\ \rightarrow \  ((P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  A))$
  & {\tiny \hyperref{lukaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[theorem2:15]{$15$}, \hyperref[theorem2:12]{$12$}} \\
 & & \qedhere
\end{longtable}
\end{proof}


\end{document}