% -*- TeX:EN -*-
%%% ====================================================================
%%% @LaTeX-file    qedeq_propositional_v1
%%% Generated from http://www.qedeq.org/0_04_02/doc/math/qedeq_propositional_v1.xml
%%% Generated at   2011-05-01 07:49:31.729
%%% ====================================================================

%%% 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{Propositional 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_02/doc/math/qedeq_propositional_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 propositional calculus in axiomatic form.
For background informations see under \url{http://en.wikipedia.org/wiki/Propositional_calculus}
and \url{http://www.ltn.lv/~podnieks/mlog/ml1.htm#axioms}.

%% end of chapter Summary\index{summary}

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

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{chapter1_section0} \hypertarget{chapter1_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\ B)\ \rightarrow\ ((C\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ B))$
\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}




\section{First Propositions} \label{chapter1_section1} \hypertarget{chapter1_section1}{}
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{\emph{(1)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny Add \hyperref[axiom:THEN-1]{axiom~1}} \\ 
\label{proposition:implicationReflexive1:2} \hypertarget{proposition:implicationReflexive1:2}{} \mbox{\emph{(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{\emph{(3)}}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny Add \hyperref[axiom:OR-2]{axiom~7}} \\ 
\label{proposition:implicationReflexive1:4} \hypertarget{proposition:implicationReflexive1:4}{} \mbox{\emph{(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{\emph{(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{\emph{(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{\emph{(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{\emph{(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:implication12} \hypertarget{proposition:implication12}{}
{\tt \tiny [\verb]proposition:implication12]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ C)$
\end{longtable}

\end{prop}




\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\ ((B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C))$
\end{longtable}

\end{prop}




\par


\begin{prop}
\label{proposition:implication14} \hypertarget{proposition:implication14}{}
{\tt \tiny [\verb]proposition:implication14]]}
\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}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}





%% end of chapter Axioms and Rules of Inference

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

\end{document}

