% -*- TeX:DE -*- %%% ==================================================================== %%% @LaTeX-file qedeq_formal_logic_v1 %%% Generated from http://www.qedeq.org/0_04_04/doc/math/qedeq_formal_logic_v1.xml %%% Generated at 2011-07-30 01:42:49.511 %%% ==================================================================== %%% 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[german]{babel} \usepackage{makeidx} \usepackage{amsmath,amsthm,amssymb} \usepackage{color} \usepackage{xr} \usepackage{tabularx} \usepackage[bookmarks=true,bookmarksnumbered,bookmarksopen, unicode=true,colorlinks=true,linkcolor=webgreen, pagebackref=true,pdfnewwindow=true,pdfstartview=FitH]{hyperref} \definecolor{webgreen}{rgb}{0,.5,0} \usepackage{epsfig,longtable} \usepackage{graphicx} \usepackage[all]{hypcap} \newtheorem{thm}{Theorem} \newtheorem{cor}[thm]{Korollar} \newtheorem{lem}[thm]{Lemma} \newtheorem{prop}[thm]{Proposition} \newtheorem{ax}{Axiom} \newtheorem{rul}{Regel} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{idefn}[defn]{Initiale Definition} \theoremstyle{remark} \newtheorem{rem}[thm]{Bemerkung} \newtheorem*{notation}{Notation} \addtolength{\textheight}{7\baselineskip} \addtolength{\topmargin}{-5\baselineskip} \setlength{\parindent}{0pt} \frenchspacing \sloppy \makeindex \title{Formale Pr{\"a}dikatenlogik} \author{ Michael Meyling } \begin{document} \maketitle \setlength{\parskip}{5pt plus 2pt minus 1pt} \mbox{} \vfill \par Die Quelle f{"ur} dieses Dokument ist hier zu finden: \par \url{http://www.qedeq.org/0_04_04/doc/math/qedeq_formal_logic_v1.xml} \par Die vorliegende Publikation ist urheberrechtlich gesch{"u}tzt. \par Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der abh{"a}ngigen Module schicken Sie bitte eine EMail an die Adresse \href{mailto:mime@qedeq.org}{mime@qedeq.org} \par Die Autoren dieses Dokuments sind: Michael Meyling \href{mailto:michael@meyling.com}{michael@meyling.com} \setlength{\parskip}{0pt} \tableofcontents \setlength{\parskip}{5pt plus 2pt minus 1pt} \chapter*{Zusammenfassung\index{Zusammenfassung}} \label{chapter1} \hypertarget{chapter1}{} \addcontentsline{toc}{chapter}{Zusammenfassung\index{Zusammenfassung}} In diesem Text wird die Pr{\"a}dikatenlogik in axiomatischer Weise entwickelt. Die folgende Kalk{\"u}lsprache und ihre Axiome basieren auf den Formulierungen von \emph{D.~Hilbert}, \emph{W.~Ackermann}\cite{hilback}, \emph{P.~S.~Novikov}\cite{novikov}, \emph{V.~Detlovs} und \emph{K.~Podnieks}\cite{detnieks}. Aus den hier angegebenen logischen Axiomen und den elementaren Schlussregeln k{\"o}nnen weitere Gesetzm{\"a}{\ss}igkeiten abgeleitet werden. Erst diese neuen Metaregeln f{\"u}hren zu einer komfortablen logischen Argumentation. Hintergrundinformationen stehen unter \url{http://www.ltn.lv/~podnieks/mlog/ml.htm} und \url{http://en.wikipedia.org/wiki/Propositional_calculus}. %% end of chapter Zusammenfassung\index{Zusammenfassung} \chapter{Sprache} \label{chapter2} \hypertarget{chapter2}{} Um mathematische Aussagen pr{\"a}zise formulieren zu k{\"o}nnen, wird in diesem Kapitel eine formale Sprache definiert. Obgleich dieses Dokument mathematischen Inhalt sehr formal beschreibt, reicht es nicht aus um als Definition f{\"u}r ein computerlesbares Dokumentformat zu dienen. Daher muss eine solch extensive Spezifikation an anderer Stelle erfolgen. Das daf{\"u}r ausgew{\"a}hlte Format ist die \emph{Extensible Markup Language} abgek{\"u}rzt \emph{XML}. XML beschreibt eine Menge von Regeln f{\"u}r den Aufbau elektronischer Dokumente.\footnote{Siehe \url{http://www.w3.org/XML/} f{\"u}r weitere Informationen.} Die daran ausgerichtete formale Syntaxspezifikation kann hier gelesen werden: \url{http://www.qedeq.org/current/xml/qedeq.xsd}. Damit wird ein mathematisches Dokumentenformat festgelegt, das die Erzeugung von \LaTeX B{\"u}chern und eine automatische Beweis{\"u}berpr{\"u}fung erm{\"o}glicht. Weitere Syntaxbeschr{\"a}nkungen und einige Erkl{\"a}rungen werden beschrieben in \url{http://www.qedeq.org/current/doc/project/qedeq_logic_language_en.pdf}. \par Auch dieses Dokument ist eine (oder wurde erzeugt aus einer) XML-Datei, die hier zu finden ist \url{http://wwww.qedeq.org/0_04_04/doc/math/qedeq_logic_v1.xml}. Aber nun folgen wir einfach dem traditionellen mathematischen Weg, die Anfangsg{\"u}nde der mathematischen Logik vorzustellen. \section{Terme\index{Term} und Formeln\index{Formel}} \label{chapter2_section1} \hypertarget{chapter2_section1}{} Als Symbole kommen die \emph{logischen Symbole} $L = \{$ \mbox{`$\neg$'}, \mbox{`$\vee$'}, \mbox{`$\wedge$'}, \mbox{`$\leftrightarrow$'}, \mbox{`$\rightarrow$'}, \mbox{`$\forall$'}, \mbox{`$\exists$'} $\}$, die \emph{Pr{\"a}dikatenkonstanten}\index{Pr{\"a}dikatenkonstante}\index{Konstante!Pr{\"a}dikaten-} $C = \{c^k_i~|~i, k \in \omega\}$, die \emph{Funktionsvariablen}\index{Funktionsvariablen}\index{Variable!Funktions-}\footnote{Funktionsvariablen dienen der einfacheren Notation und werden beispielsweise zur Formulierung eines identit{\"a}tslogischen Satzes ben{\"o}tigt: $x = y \rightarrow f(x) = f(y)$. Ausserdem bereitet ihre Einf{\"u}hrung die sp{\"a}tere Syntaxerweiterung zur Anwendung von funktionalen Klassen vor.} $F = \{f^k_i~|~i, k \in \omega \land k > 0\}$, die \emph{Funktionskonstanten}\index{Funktionskonstanten}\index{Konstante!Funktions-}\footnote{Funktionskonstanten dienen ebenfalls der Bequemlichkeit und werden sp{\"a}ter f{\"u}r direkt definierte Klassenfunktionen verwendet. So zum Beispiel zur Potenzklassenbildung, zur Vereinigungsklassenbildung und f{\"u}r die Nachfolgerfunktion. All diese Funktionskonstanten k{\"o}nnen auch als Abk{\"u}rzungen verstanden werden.} $H = \{h^k_i~|~i, k \in \omega\}$, die \emph{Subjektvariablen}\index{Subjektvariable}\index{Variable!Subjekt-} $V = \{v_i~|~i \in \omega\}$, sowie die \emph{Pr{\"a}dikatenvariablen}\index{Pr{\"a}dikatenvariable}\index{Variable!Pr{\"a}dikaten-} $P = \{p^k_i~|~i, k \in \omega\}$ vor.\footnote{Unter $\omega$ werden die nat{\"u}rlichen Zahlen, die Null eingeschlossen, verstanden. Alle bei den Mengenbildungen beteiligten Symbole werden als paarweise verschieden vorausgesetzt. Das bedeutet z.~B.: $f^k_i = f^{k'}_{i'} \rightarrow (k = k' \land i = i')$ und $h^k_i \neq v_j$.} Unter der \emph{Stellenzahl} eines Operators wird der obere Index verstanden. Die Menge der nullstelligen Pr{\"a}dikatenvariablen wird auch als Menge der \emph{Aussagenvariablen}\index{Aussagenvariable}\index{Variable!Aussagen-} bezeichnet: $A := \{p_i^0~|~i \in \omega \}$. F{\"u}r die Subjektvariablen werden abk{\"u}rzend auch bestimmte Kleinbuchstaben geschrieben. Die Kleinbuchstaben stehen f{\"u}r verschiedene Subjektvariablen: \mbox{$v_1 = $ `$u$'}, \mbox{$v_2 = $ `$v$'}, \mbox{$v_3 = $ `$w$'}, \mbox{$v_4 = $ `$x$'}, \mbox{$v_5 = $ `$y$'}, \mbox{$v_5 = $ `$z$'}. Weiter werden als Abk{\"u}rzungen verwendet: f{\"u}r die Pr{\"a}dikatenvariablen $p^n_1 = $ `$\phi$' und $p^n_2 = $ `$\psi$', wobei die jeweilige Stellenanzahl $n$ aus der Anzahl der nachfolgenden Parameter ermittelt wird, f{\"u}r die Aussagenvariablen $a_1 = $ `$A$', $a_2 = $ `$B$' und $a_3 = $ `$C$'. Als Abk{\"u}rzungen f{\"u}r Funktionsvariablen wird festgelegt $f^n_1 = $ `$f$' und $f^n_2 = $ `$g$', wobei wiederum die jeweilige Stellenanzahl $n$ aus der Anzahl der nachfolgenden Parameter ermittelt wird. Bei allen aussagenlogischen zwei\-stelligen Operatoren wird der leichteren Lesbarkeit wegen die Infixschreibweise benutzt, dabei werden die Symbole `(' und `)' verwandt. D.~h. f{\"u}r den Operator $\land$ mit den Argumenten $A$ und $B$ wird $(A \land B)$ geschrieben. Es gelten die {\"u}blichen Operatorpriorit{\"a}ten und die dazugeh{\"o}rigen Klammerregeln. Insbesondere die {\"a}u{\ss}eren Klammern werden in der Regel weggelassen. Auch werden leere Klammern nicht geschrieben. \par Nachfolgend werden die Operatoren mit absteigender Priorit{\"a}t aufgelistet. $$ \begin{array}{c} \neg, \forall, \exists \\ \land \\ \lor \\ \rightarrow, \leftrightarrow \\ \end{array} $$ \par Der Begriff \emph{Term\index{Term}} wird im Folgenden rekursiv definiert: \begin{enumerate} \item Jede Subjektvariable ist ein Term. \item Seien $i, k \in \omega$ und $t_1$, \ldots, $t_k$ Terme. Dann ist auch $h^k_i(t_1, \ldots, t_k)$ und falls $k > 0$, so auch $f^k_i(t_1, \ldots, t_k)$ ein Term. \end{enumerate} Alle nullstelligen Funktionskonstanten $\{h^0_i~|~i, \in \omega\}$ sind demzufolge Terme, sie werden auch \emph{Individuenkonstanten}\index{Individuenkonstante}\index{Konstante!Individuen-} genannt.\footnote{Analog dazu k{\"o}nnten Subjektvariablen auch als nullstellige Funktionsvariablen definiert werden. Da die Subjektvariablen jedoch eine hervorgehobene Rolle spielen, werden sie auch gesondert bezeichnet.} \par Die Begriffe \emph{Formel\index{Formel}}, \emph{freie\index{freie Subjektvariable}\index{Subjektvariable!freie}} und \emph{gebundene\index{gebundene Subjektvariable}\index{Subjektvariable!gebundene}} Subjektvariable werden rekursiv wie folgt definiert: \begin{enumerate} \item Jede Aussagenvariable ist eine Formel, solche Formeln enthalten keine freien oder gebundenen Subjektvariablen. \item Ist $p^k$ eine $k$-stellige Pr{\"a}dikatenvariable und $c^k$ eine $k$-stellige Pr{\"a}dikatenkonstante und sind $t_1, t_2, \ldots, t_k$ Terme, so sind $p^k(t_1, t_2, \ldots t_k)$ und $c^k(t_1, t_2, \ldots, t_k)$ Formeln. Dabei gelten alle in $t_1, t_2, \ldots, t_k$ vorkommenden Subjektvariablen als freie Subjektvariablen, gebundene Subjektvariablen kommen nicht vor.\footnote{Dieser zweite Punkt umfasst den ersten, welcher nur der Anschaulichkeit wegen extra aufgef{\"u}hrt ist.} \item Es seien $\alpha, \beta$ Formeln, in denen keine Subjektvariablen vorkommen, die in einer Formel gebunden und in der anderen frei sind. Dann sind auch $\neg \alpha$, $(\alpha \land \beta)$, $(\alpha \lor \beta)$, $(\alpha \rightarrow \beta)$, $(\alpha \leftrightarrow \beta)$ Formeln. Subjektvariablen, welche in $\alpha$ oder $\beta$ frei (bzw. gebunden) vorkommen, bleiben frei (bzw. gebunden). \item Falls in der Formel $\alpha$ die Subjektvariable $x_1$ nicht gebunden vorkommt\footnote{D.~h. $x_1$ kommt h{\"o}chstens frei vor.}, dann sind auch $\forall x_1~\alpha$ und $\exists x_1~\alpha$ Formeln. Dabei wird $\forall$ als \emph{Allquantor}\index{Allquantor}\index{Quantor!All-} und $\exists$ als \emph{Existenzquantor}\index{Existenzquantor}\index{Quantor!Existenz-} bezeichnet. Bis auf $x_1$ bleiben alle freien Subjektvariablen von $\alpha$ auch frei, und zu den gebundenen Subjektvariablen von $\alpha$ kommt $x_1$ hinzu. \end{enumerate} Alle Formeln die nur durch Anwendung von 1. und 3. gebildet werden, hei{\ss}en Formeln der \emph{Aussagenalgebra}. \par Es gilt f{\"u}r jede Formel $\alpha$: die Menge der freien und der gebundenen Subjektvariablen von $\alpha$ sind disjunkt.\footnote{Andere Formalisierungen erlauben z.~B. $\forall x_1~\alpha$ auch dann, wenn $x_1$ schon in $\alpha$ gebunden vorkommt. Auch Ausdr{\"u}cke wie $\alpha(x_1)~\land~(\forall~x_1~\beta)$ sind erlaubt. Es wird dann f{\"u}r ein einzelnes Vorkommen einer Variablen definiert, ob es sich um ein freies oder gebundenes Vorkommen handelt.} \par Falls eine Formel die Gestalt $\forall x_1 ~ \alpha$ bzw. $\exists x_1 ~ \alpha$ besitzt, dann hei{\ss}t die Formel $\alpha$ der \emph{Wirkungsbereich} des Quantors $\forall$ bzw. $\exists$. \par Alle Formeln, die beim Aufbau einer Formel mittels 1. bis 4. ben{\"o}tigt werden, hei{\ss}en \emph{Teilformeln}. %% end of chapter Sprache \chapter{Axiome und Schlussregeln} \label{chapter3} \hypertarget{chapter3}{} Nun geben wir das Axiomensystem f{\"u}r die Aussagenlogik an und formulieren die Regeln um daraus neue Formeln zu gewinnen. \section{Axiome\index{Axiome}} \label{chapter3_section1} \hypertarget{chapter3_section1}{} Nun listen wir einfach alle Axiome ohne weitere Erl{\"a}uterungen auf. \begin{ax}[Hypotheseineinf{\"u}hrung\index{Hypotheseneinf{\"u}hrung}] \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} \begin{ax}[Verteilung einer Hypothese {\"u}ber Implikation\index{Hypothesenverteilung}] \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} \begin{ax}[Konjunktionsk{\"u}rzung rechts\index{Konjunktion!K{\"u}rzung}] \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} \begin{ax}[Konjunktionsk{\"u}rzung links\index{Konjunktion!K{\"u}rzung}] \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} \begin{ax}[Konjunktionseinf{\"u}hrung\index{Konjunktion!Einf{\"u}hrung}] \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} \begin{ax}[Konjunktionseinf{\"u}hrung rechts\index{Disjunktion!Einf{\"u}hrung}] \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} \begin{ax}[Konjunktionseinf{\"u}hrung links\index{Disjunktion!Einf{\"u}hrung}] \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} \begin{ax}[Konjunktionsk{\"u}rzung\index{Disjunktion!K{\"u}rzung}] \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} \begin{ax}[Negationseinf{\"u}hrung\index{Negation!Einf{\"u}hrung}] \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} \begin{ax}[Negationsk{\"u}rzung\index{Negation!K{\"u}rzung}] \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} \begin{ax}[Ausgeschlossenes Drittes\index{Negation!ausgeschlossenes Drittes}] \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} \begin{ax}[{\"A}quivalenzk{\"u}rzung rechts\index{{\"A}quivalenz!K{\"u}rzung}] \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} \begin{ax}[{\"A}quivalenzk{\"u}rzung links\index{{\"A}quivalenz!K{\"u}rzung}] \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} \begin{ax}[{\"A}quivalenzeinf{\"u}hrung\index{{\"A}quivalenz!Einf{\"u}hrung}] \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 Wenn ein Pr{\"a}dikat auf alle $x$ zutrifft, so trifft es auch auf ein beliebiges $y$ zu. \begin{ax}[Spezialisierung\index{Axiom!der Spezialisierung}] \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 Wenn ein Pr{\"a}dikat auf irgend ein $y$ zutrifft, so gibt es ein $x$, auf das es zutrifft. \begin{ax}[Existenz\index{Axiom!der Existenz}] \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{Ableitungsregeln\index{Regeln!predikatenlogische}} \label{chapter3_section2} \hypertarget{chapter3_section2}{} Die im folgenden angegebenen Regeln erm{\"o}glichen uns aus den wahr angesehenen Axiomen neue wahre Formeln zu gewinnen. Aus diesen k{\"o}nnen wiederum weitere Formeln abgeleitet werden, so dass sich die Menge der wahren Formeln sukzessive erweitern l{\"a}sst. \begin{rul}[Hinzuf{\"u}gung einer wahren Formel] \label{rule:addProvenFormula} \hypertarget{rule:addProvenFormula}{} {\tt \tiny [\verb]rule:addProvenFormula]]} \par {\em Name: \verb]Add] - Version: \verb]0.01.00]} Hinzuf{\"u}gen eines Axioms, einer Definition oder einer bereits bewiesenen Proposition. Wir m{\"u}ssen den Ort der Formel angeben. \end{rul} \begin{rul}[Abtrennung, Modus Ponens\index{Modus Ponens}\index{Abtrennungsregel}] \label{rule:modusPonens} \hypertarget{rule:modusPonens}{} {\tt \tiny [\verb]rule:modusPonens]]} \par {\em Name: \verb]MP] - Version: \verb]0.01.00]} Wenn $\alpha$ und $\alpha \rightarrow \beta$ wahre Formeln sind, dann ist auch $\beta$ eine wahre Formel. \end{rul} \begin{rul}[Ersetzung f{\"u}r freie Subjektvariable] \label{rule:replaceFree} \hypertarget{rule:replaceFree}{} {\tt \tiny [\verb]rule:replaceFree]]} \par {\em Name: \verb]SubstFree] - Version: \verb]0.01.00]} Ausgehend von einer wahren Formel kann jede freie Subjektvariable durch einen Term ersetzt werden, der keine in der Formel bereits gebundenen Subjektvariablen enth{\"a}lt. Die Ersetzung muss durchg{\"a}ngig in der gesamten Formel erfolgen. \end{rul} Das Verbot in dem Term Subjektvariablen zu verwenden, welche in der Originalformel gebunden vorkommen, dient nicht nur der Absicherung der Wohlgeformtheit, sondern besitzt auch eine inhaltliche Bedeutung. Dazu betrachten wir die folgende Ableitung. \par \begin{tabularx}{\linewidth}{rclX} $\forall x \ \exists y \ \phi(x, y)$ & $\rightarrow$ & $\exists y \ \phi(z,y)$ & mit \hyperlink{axiom:universalInstantiation}{Axiom~15} \\ $\forall x \ \exists y \ \phi(x, y)$ & $\rightarrow$ & $\exists y \ \phi(y,y)$ & verbotene Ersetzung: $z$ durch $y$, obwohl $y$ bereits gebunden \\ $\forall x \ \exists y \ x \neq y$ & $\rightarrow$ & $\exists y \ \neq y$ & Einsetzung von $\neq$ f{\"u}r $\phi$ \end{tabularx} \par Diese letzte Aussage ist in vielen Modellen nicht g{\"u}ltig. \begin{rul}[Umbenennung f{\"u}r gebundene Subjektvariable] \label{rule:renameBound} \hypertarget{rule:renameBound}{} {\tt \tiny [\verb]rule:renameBound]]} \par {\em Name: \verb]Rename] - Version: \verb]0.01.00]} Jede gebundene Subjektvariable kann in eine andere, nicht bereits frei vorkommende, Subjektvariable umbenannt werden. Falls {\"u}ber umzubenennende Variable mehrfach quantifiziert wird, dann braucht die Umbenennung nur im Wirkungsbereich eines bestimmten Quantors zu erfolgen. \end{rul} \begin{rul}[Einsetzung f{\"u}r Pr{\"a}dikatenvariable] \label{rule:replacePred} \hypertarget{rule:replacePred}{} {\tt \tiny [\verb]rule:replacePred]]} \par {\em Name: \verb]SubstPred] - Version: \verb]0.01.00]} Es sei $\alpha$ eine wahre Formel, die die $n$-stellige Pr{\"a}dikatenvariable $p$ enth{\"a}lt, $x_1$, \ldots, $x_n$ seien paarweise verschiedene Subjektvariable und $\beta(x_1, \ldots, x_n)$ eine beliebige Formel in der die Variablen $x_1$, \ldots, $x_n$ nicht gebunden sind. In der Formel $\beta(x_1, \ldots, x_n)$ m{\"u}ssen jedoch nicht alle $x_1$, \ldots, $x_n$ als freie Subjektvariable vorkommen. Weiterhin k{\"o}nnen auch noch weitere Variable frei oder gebunden vorkommen. Wenn die folgenden Bedingungen erf{\"u}llt sind, dann kann durch die Ersetzung jedes Vorkommens von $p(t_1, \ldots, t_n)$ mit jeweils passenden Termen $t_1$, \ldots, $t_n$ in $\alpha$ durch $\beta(t_1, \ldots, t_n)$ eine weitere wahre Formel gewonnen werden. \begin{itemize} \item die freien Variablen von $\beta(x_1, \ldots, x_n)$ ohne $x_1$, \ldots, $x_n$ kommen nicht in $\alpha$ als gebundene Variablen vor \item jedes Vorkommen von $p(t_1, \ldots, t_n)$ in $\alpha$ enth{\"a}lt keine gebundene Variable von $\beta(x_1, \ldots, x_n)$ \item das Ergebnis der Substitution ist eine wohlgeformte Formel \end{itemize} \end{rul} Siehe III \S 5 in \cite{hilback}. \par Das Verbot in der Ersetzungsformel keine zus{\"a}tzliche Subjektvariable zu verwenden, welche in der Originalformel gebunden vorkommt, hat nicht nur die Absicherung der Wohlgeformtheit zum Zweck. Es bewahrt auch die inhaltliche G{\"u}ltigkeit. Dazu betrachten wir die folgende Ableitung. \par \begin{tabularx}{\linewidth}{rclX} $ \phi(x)$ & $\rightarrow$ & $\exists y \ \phi(y)$ & mit \hyperlink{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$ & verbotene Ersetzung: $\phi(x)$ durch $x \neq y$, obwohl $y$ bereits gebunden \\ $ \exists y \ x \neq y$ & $\rightarrow$ & $\exists y \ y \neq y$ & \end{tabularx} \par Diese letzte Aussage ist in vielen Modellen nicht g{\"u}ltig. \par Analog zu Regel~\hyperlink{rule:replacePred}{Regel~5} k{\"o}nnen wir auch Funktionsvariablen ersetzen. \begin{rul}[Einsetzung f{\"u}r Funktionsvariable] \label{rule:replaceFunct} \hypertarget{rule:replaceFunct}{} {\tt \tiny [\verb]rule:replaceFunct]]} \par {\em Name: \verb]SubstFun] - Version: \verb]0.01.00]} Es sei $\alpha$ eine bereits bewiesene Formel, die die $n$-stellige Funktionsvariable $\sigma$ enth{\"a}lt, $x_1$, \ldots, $x_n$ seien paarweise verschiedene Subjektvariable und $\tau(x_1, \ldots, x_n)$ ein beliebiger Term in dem die Subjektvariablen $x_1$, \ldots, $x_n$ nicht gebunden sind. In dem Term $\tau(x_1, \ldots, x_n)$ m{\"u}ssen nicht alle $x_1$, \ldots, $x_n$ als freie Subjektvariable vorkommen. Weiterhin k{\"o}nnen auch noch noch weitere Variable frei oder gebunden vorkommen. Wenn die folgenden Bedingungen erf{\"u}llt sind, dann kann durch die Ersetzung jedes Vorkommens von $\sigma(t_1, \ldots, t_n)$ mit jeweils passenden Termen $t_1$, \ldots, $t_n$ in $\alpha$ durch $\tau(t_1, \ldots, t_n)$ eine weitere wahre Formel gewonnen werden. \begin{itemize} \item die freien Variablen von $\tau(x_1, \ldots, x_n)$ ohne $x_1$, \ldots, $x_n$ kommen in $\alpha$ nicht als gebundene Variablen vor \item jedes Vorkommen von $\sigma(t_1, \ldots, t_n)$ in $\alpha$ enth{\"a}lt keine gebundene Variable von $\tau(x_1, \ldots, x_n)$ \item das Ergebnis der Substitution ist eine wohlgeformte Formel \end{itemize} \end{rul} \begin{rul}[Hintere Generalisierung\index{Generalisierung!hintere}] \label{rule:universalGeneralization} \hypertarget{rule:universalGeneralization}{} {\tt \tiny [\verb]rule:universalGeneralization]]} \par {\em Name: \verb]Universal] - Version: \verb]0.01.00]} Wenn $\alpha \rightarrow \beta(x_1)$ eine wahre Formel ist und $\alpha$ die Subjektvariable $x_1$ nicht enth{\"a}lt, dann ist auch $\alpha \rightarrow (\forall x_1~(\beta(x_1)))$ eine wahre Formel. \end{rul} \begin{rul}[Vordere Partikularisierung\index{Partikularisierung!vordere}] \label{rule:existentialGeneralization} \hypertarget{rule:existentialGeneralization}{} {\tt \tiny [\verb]rule:existentialGeneralization]]} \par {\em Name: \verb]Existential] - Version: \verb]0.01.00]} Wenn $\alpha(x_1) \rightarrow \beta$ eine wahre Formel ist und $\beta$ die Subjektvariable $x_1$ nicht enth{\"a}lt, dann ist auch $(\exists x_1~\alpha(x_1)) \rightarrow \beta$ eine wahre Formel. \end{rul} %% end of chapter Axiome und Schlussregeln \chapter{Aussagenlogik} \label{chapter4} \hypertarget{chapter4}{} In diesem Kapitel stellen wir eine wichtige neue Ableitungsregel vor und entwickeln die {\"u}blichen S{\"a}tze der Aussagenlogik. \section{First Propositions} \label{chapter4_section1} \hypertarget{chapter4_section1}{} Hier nehmen wir die ersten Ableitungen vor. \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 \hyperlink{rule:addProvenFormula}{Add} \hyperlink{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 \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:THEN-2}{Axiom~2}} \\ \label{proposition:implicationReflexive1!3} \hypertarget{proposition:implicationReflexive1!3}{\mbox{(3)}} \ & \ $A\ \rightarrow\ (B\ \lor\ A)$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-2}{Axiom~7}} \\ \label{proposition:implicationReflexive1!4} \hypertarget{proposition:implicationReflexive1!4}{\mbox{(4)}} \ & \ $A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $B\ \lor\ A$ in \hyperlink{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 \hyperlink{rule:replacePred}{SubstPred} $B$ by $B\ \lor\ A$ in \hyperlink{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 \hyperlink{rule:replacePred}{SubstPred} $C$ by $A$ in \hyperlink{proposition:implicationReflexive1!5}{(5)}} \\ \label{proposition:implicationReflexive1!7} \hypertarget{proposition:implicationReflexive1!7}{\mbox{(7)}} \ & \ $(A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implicationReflexive1!6}{(6)}, \hyperlink{proposition:implicationReflexive1!4}{(4)}} \\ \label{proposition:implicationReflexive1!8} \hypertarget{proposition:implicationReflexive1!8}{\mbox{(8)}} \ & \ $A\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implicationReflexive1!7}{(7)}, \hyperlink{proposition:implicationReflexive1!3}{(3)}} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication2} \hypertarget{proposition:implication2}{} {\tt \tiny [\verb]proposition:implication2]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(A\ \lor\ A)\ \rightarrow\ A$ \end{longtable} \end{prop} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{proposition:implication2!1} \hypertarget{proposition:implication2!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{proposition:implicationReflexive1}{Proposition~1}} \\ \label{proposition:implication2!2} \hypertarget{proposition:implication2!2}{\mbox{(2)}} \ & \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-3}{Axiom~8}} \\ \label{proposition:implication2!3} \hypertarget{proposition:implication2!3}{\mbox{(3)}} \ & \ $(A\ \rightarrow\ C)\ \rightarrow\ ((A\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ A)\ \rightarrow\ C))$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication2!2}{(2)}} \\ \label{proposition:implication2!4} \hypertarget{proposition:implication2!4}{\mbox{(4)}} \ & \ $(A\ \rightarrow\ A)\ \rightarrow\ ((A\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ A)\ \rightarrow\ A))$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $C$ by $A$ in \hyperlink{proposition:implication2!3}{(3)}} \\ \label{proposition:implication2!5} \hypertarget{proposition:implication2!5}{\mbox{(5)}} \ & \ $(A\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ A)\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication2!4}{(4)}, \hyperlink{proposition:implication2!1}{(1)}} \\ \label{proposition:implication2!6} \hypertarget{proposition:implication2!6}{\mbox{(6)}} \ & \ $(A\ \lor\ A)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication2!5}{(5)}, \hyperlink{proposition:implication2!1}{(1)}} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication03} \hypertarget{proposition:implication03}{} {\tt \tiny [\verb]proposition:implication03]]} \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:implication03!1} \hypertarget{proposition:implication03!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ (A\ \lor\ B)$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-1}{Axiom~6}} \\ \label{proposition:implication03!2} \hypertarget{proposition:implication03!2}{\mbox{(2)}} \ & \ $A\ \rightarrow\ (B\ \lor\ A)$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-2}{Axiom~7}} \\ \label{proposition:implication03!3} \hypertarget{proposition:implication03!3}{\mbox{(3)}} \ & \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-3}{Axiom~8}} \\ \label{proposition:implication03!4} \hypertarget{proposition:implication03!4}{\mbox{(4)}} \ & \ $D\ \rightarrow\ (D\ \lor\ B)$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $A$ by $D$ in \hyperlink{proposition:implication03!1}{(1)}} \\ \label{proposition:implication03!5} \hypertarget{proposition:implication03!5}{\mbox{(5)}} \ & \ $(A\ \rightarrow\ (C\ \lor\ A))\ \rightarrow\ ((B\ \rightarrow\ (C\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (C\ \lor\ A)))$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $C$ by $C\ \lor\ A$ in \hyperlink{proposition:implication03!3}{(3)}} \\ \label{proposition:implication03!6} \hypertarget{proposition:implication03!6}{\mbox{(6)}} \ & \ $D\ \rightarrow\ (D\ \lor\ A)$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication03!4}{(4)}} \\ \label{proposition:implication03!7} \hypertarget{proposition:implication03!7}{\mbox{(7)}} \ & \ $(A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((B\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A)))$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $C$ by $B$ in \hyperlink{proposition:implication03!5}{(5)}} \\ \label{proposition:implication03!8} \hypertarget{proposition:implication03!8}{\mbox{(8)}} \ & \ $(B\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A))$ \ & \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication03!7}{(7)}, \hyperlink{proposition:implication03!2}{(2)}} \\ \label{proposition:implication03!9} \hypertarget{proposition:implication03!9}{\mbox{(9)}} \ & \ $B\ \rightarrow\ (B\ \lor\ A)$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $D$ by $B$ in \hyperlink{proposition:implication03!6}{(6)}} \\ \label{proposition:implication03!10} \hypertarget{proposition:implication03!10}{\mbox{(10)}} \ & \ $(A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A)$ \ & \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication03!8}{(8)}, \hyperlink{proposition:implication03!9}{(9)}} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication04} \hypertarget{proposition:implication04}{} {\tt \tiny [\verb]proposition:implication04]]} \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:implication04!1} \hypertarget{proposition:implication04!1}{\mbox{(1)}} \ & \ $(A\ \land\ B)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication04!2} \hypertarget{proposition:implication04!2}{\mbox{(2)}} \ & \ $(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:AND-2}{Axiom~4}} \\ \label{proposition:implication04!3} \hypertarget{proposition:implication04!3}{\mbox{(3)}} \ & \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ & \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:NOT-1}{Axiom~9}} \\ \label{proposition:implication04!4} \hypertarget{proposition:implication04!4}{\mbox{(4)}} \ & \ $(A\ \land\ \neg A)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $\neg A$ in \hyperlink{proposition:implication04!1}{(1)}} \\ \label{proposition:implication04!5} \hypertarget{proposition:implication04!5}{\mbox{(5)}} \ & \ $(A\ \land\ \neg A)\ \rightarrow\ \neg A$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $\neg A$ in \hyperlink{proposition:implication04!2}{(2)}} \\ \label{proposition:implication04!6} \hypertarget{proposition:implication04!6}{\mbox{(6)}} \ & \ $((A\ \land\ \neg A)\ \rightarrow\ B)\ \rightarrow\ (((A\ \land\ \neg A)\ \rightarrow\ \neg B)\ \rightarrow\ \neg (A\ \land\ \neg A))$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $A$ by $A\ \land\ \neg A$ in \hyperlink{proposition:implication04!3}{(3)}} \\ \label{proposition:implication04!7} \hypertarget{proposition:implication04!7}{\mbox{(7)}} \ & \ $((A\ \land\ \neg A)\ \rightarrow\ A)\ \rightarrow\ (((A\ \land\ \neg A)\ \rightarrow\ \neg A)\ \rightarrow\ \neg (A\ \land\ \neg A))$ \ & \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication04!6}{(6)}} \\ \label{proposition:implication04!8} \hypertarget{proposition:implication04!8}{\mbox{(8)}} \ & \ $((A\ \land\ \neg A)\ \rightarrow\ \neg A)\ \rightarrow\ \neg (A\ \land\ \neg A)$ \ & \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication04!7}{(7)}, \hyperlink{proposition:implication04!4}{(4)}} \\ \label{proposition:implication04!9} \hypertarget{proposition:implication04!9}{\mbox{(9)}} \ & \ $\neg (A\ \land\ \neg A)$ \ & \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication04!8}{(8)}, \hyperlink{proposition:implication04!5}{(5)}} \\ & & \qedhere \end{longtable} \end{proof} \section{Deduktionstheorem\index{Deduktionstheorem}} \label{chapter4_section2} \hypertarget{chapter4_section2}{} Wir leiten das Deduktionstheorem her. Dies erm{\"o}glicht die neue Regel \emph{Conditional Proof}. \par Wenn wir $B$ beweisen k{\"o}nnen, indem wir $A$ als Hypothese annehmen, dann haben wir $A \rightarrow B$ bewiesen. Diese Argumentation wir durch das sogenannte \emph{Deduktionstheorem} gerechtfertigt. Das Deduktionstheorem gilt f{\"u}r alle {\"u}blichen Ableitungssysteme der Pr{\"a}dikatenlogik der ersten Stufe. Leider macht unsere Verwendung von Pr{\"a}dikatsvariablen und Ersetzungsregeln hier Schwierigkeiten. Wir m{\"u}ssen die Verwendung von Ableitungsregeln einschr{\"a}nken um ein entsprechendes Resultat zu erhalten. \begin{rul} \label{rule:CP} \hypertarget{rule:CP}{} {\tt \tiny [\verb]rule:CP]]} \par {\em Name: \verb]CP] - Version: \verb]0.02.00]} Wir haben die wohlgeformte Formel $\alpha$ und f{\"u}gen sie als neue Beweiszeile hinzu. Nun modifizieren wir die existierenden Ableitungsregeln. Wir k{\"o}nnen eine weitere Beweiszeile anf{\"u}gen, wenn $\alpha \rightarrow \beta$ eine wohlgeformte Formel ist und die Verwendung einer vorherigen Regel mit den folgenden Einschr{\"a}nkungen die Hinzuf{\"u}gung rechtfertigt: f{\"u}r \hyperlink{rule:replaceFree}{Regel~3} kommt die ersetzte freie Variable nicht in $\alpha$ vor, f{\"u}r \hyperlink{rule:replacePred}{Regel~5} kommt die ersetzte Pr{\"a}dikatenvariable nicht in $\alpha$ vor, f{\"u}r \hyperlink{rule:replaceFunct}{Regel~6} kommt die ersetzte Funktionsvariable nicht in $\alpha$ vor. \end{rul} Basierend auf: \hyperlink{axiom:THEN-1}{Axiom~1} \hyperlink{axiom:THEN-2}{Axiom~2} Die folgenden Regeln m??ssen erweitert werden. \par \label{rule:CP!MP} \hypertarget{rule:CP!MP}{} {\em Name: \verb]MP] - Version: \verb]0.02.00] - Old Version: \hyperlink{rule:modusPonens}{0.01.00}} Siehe \hyperlink{rule:CP}{Regel~9}. \par \label{rule:CP!Add} \hypertarget{rule:CP!Add}{} {\em Name: \verb]Add] - Version: \verb]0.02.00] - Old Version: \hyperlink{rule:addProvenFormula}{0.01.00}} Siehe \hyperlink{rule:CP}{Regel~9}. \par \label{rule:CP!Rename} \hypertarget{rule:CP!Rename}{} {\em Name: \verb]Rename] - Version: \verb]0.02.00] - Old Version: \hyperlink{rule:renameBound}{0.01.00}} Siehe \hyperlink{rule:CP}{Regel~9}. \par \label{rule:CP!SubstFree} \hypertarget{rule:CP!SubstFree}{} {\em Name: \verb]SubstFree] - Version: \verb]0.02.00] - Old Version: \hyperlink{rule:replaceFree}{0.01.00}} Siehe \hyperlink{rule:CP}{Regel~9}. \par \label{rule:CP!SubstPred} \hypertarget{rule:CP!SubstPred}{} {\em Name: \verb]SubstPred] - Version: \verb]0.02.00] - Old Version: \hyperlink{rule:replacePred}{0.01.00}} Siehe \hyperlink{rule:CP}{Regel~9}. \par \label{rule:CP!SubstFun} \hypertarget{rule:CP!SubstFun}{} {\em Name: \verb]SubstFun] - Version: \verb]0.02.00] - Old Version: \hyperlink{rule:replaceFunct}{0.01.00}} Siehe \hyperlink{rule:CP}{Regel~9}. \par \label{rule:CP!Universal} \hypertarget{rule:CP!Universal}{} {\em Name: \verb]Universal] - Version: \verb]0.02.00] - Old Version: \hyperlink{rule:universalGeneralization}{0.01.00}} Siehe \hyperlink{rule:CP}{Regel~9}. \par \label{rule:CP!Existential} \hypertarget{rule:CP!Existential}{} {\em Name: \verb]Existential] - Version: \verb]0.02.00] - Old Version: \hyperlink{rule:existentialGeneralization}{0.01.00}} Siehe \hyperlink{rule:CP}{Regel~9}. \begin{proof} TODO 20110613 m31 \end{proof} Mittels Deduktionstheorem leiten wir im Folgenden weitere S{\"a}tze ab. \section{S{\"a}tze zur Implikation} \label{chapter4_section3} \hypertarget{chapter4_section3}{} Mittels \hyperlink{rule:CP}{Regel~9} leiten wir weitere S{\"a}tze ab, in deren Formeln nur die Implikation vorkommt. \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 \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication10!1}{(1)}, \hyperlink{proposition:implication10!2}{(2)}} \\ \label{proposition:implication10!4} \hypertarget{proposition:implication10!4}{\mbox{(4)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication10!3}{(3)}, \hyperlink{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} \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 \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:THEN-1}{Axiom~1}} \\ \label{proposition:implication11!2} \hypertarget{proposition:implication11!2}{\mbox{(2)}} \ & \ $D\ \rightarrow\ (B\ \rightarrow\ D)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $D$ in \hyperlink{proposition:implication11!1}{(1)}} \\ \label{proposition:implication11!3} \hypertarget{proposition:implication11!3}{\mbox{(3)}} \ & \ $D\ \rightarrow\ (A\ \rightarrow\ D)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication11!2}{(2)}} \\ \label{proposition:implication11!4} \hypertarget{proposition:implication11!4}{\mbox{(4)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $B$ in \hyperlink{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 \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication11!4}{(4)}, \hyperlink{proposition:implication11!7}{(7)}} \\ \label{proposition:implication11!9} \hypertarget{proposition:implication11!9}{\mbox{(9)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication11!5}{(5)}, \hyperlink{proposition:implication11!8}{(8)}} \\ \label{proposition:implication11!10} \hypertarget{proposition:implication11!10}{\mbox{(10)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication11!9}{(9)}, \hyperlink{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} \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 \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication12!1}{(1)}, \hyperlink{proposition:implication12!3}{(3)}} \\ \label{proposition:implication12!5} \hypertarget{proposition:implication12!5}{\mbox{(5)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication12!2}{(2)}, \hyperlink{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} \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 \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication13!1}{(1)}, \hyperlink{proposition:implication13!3}{(3)}} \\ \label{proposition:implication13!5} \hypertarget{proposition:implication13!5}{\mbox{(5)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication13!4}{(4)}, \hyperlink{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} \section{S{\"a}tze zur Konjunktion} \label{chapter4_section4} \hypertarget{chapter4_section4}{} Mittels \hyperlink{rule:CP}{Regel~9} leiten wir weitere S{\"a}tze ab, in deren Formeln die Konjunktion vorkommt. \begin{prop} \label{proposition:implication14} \hypertarget{proposition:implication14}{} {\tt \tiny [\verb]proposition:implication14]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $A\ \rightarrow\ (A\ \land\ A)$ \end{longtable} \end{prop} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{proposition:implication14!1} \hypertarget{proposition:implication14!1}{\mbox{(1)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \label{proposition:implication14!2} \hypertarget{proposition:implication14!2}{\mbox{(2)}} \ & \ $A\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ A))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication14!1}{(1)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication14!3} \hypertarget{proposition:implication14!3}{\mbox{(3)}} \ & \ \mbox{\qquad}$A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication14!4} \hypertarget{proposition:implication14!4}{\mbox{(4)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ (A\ \land\ A)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication14!2}{(2)}, \hyperlink{proposition:implication14!3}{(3)}} \\ \label{proposition:implication14!5} \hypertarget{proposition:implication14!5}{\mbox{(5)}} \ & \ \mbox{\qquad}$A\ \land\ A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication14!4}{(4)}, \hyperlink{proposition:implication14!3}{(3)}} \\ \label{proposition:implication14!6} \hypertarget{proposition:implication14!6}{\mbox{(6)}} \ & \ $A\ \rightarrow\ (A\ \land\ A)$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \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 \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication15!2} \hypertarget{proposition:implication15!2}{\mbox{(2)}} \ & \ $(A\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \rightarrow\ C$ in \hyperlink{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 \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication15!2}{(2)}} \\ \label{proposition:implication15!4} \hypertarget{proposition:implication15!4}{\mbox{(4)}} \ & \ $(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{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 \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \rightarrow\ C$ in \hyperlink{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 \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{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 \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication15!3}{(3)}, \hyperlink{proposition:implication15!7}{(7)}} \\ \label{proposition:implication15!9} \hypertarget{proposition:implication15!9}{\mbox{(9)}} \ & \ \mbox{\qquad}$B\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication15!6}{(6)}, \hyperlink{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 \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication12}{Proposition~7}} \\ \label{proposition:implication15!11} \hypertarget{proposition:implication15!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$(B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication15!10}{(10)}, \hyperlink{proposition:implication15!8}{(8)}} \\ \label{proposition:implication15!12} \hypertarget{proposition:implication15!12}{\mbox{(12)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication15!11}{(11)}, \hyperlink{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} \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 \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \label{proposition:implication17!2} \hypertarget{proposition:implication17!2}{\mbox{(2)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication17!1}{(1)}} \\ \label{proposition:implication17!3} \hypertarget{proposition:implication17!3}{\mbox{(3)}} \ & \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{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 \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication17!5}{(5)}, \hyperlink{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 \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication17!3}{(3)}, \hyperlink{proposition:implication17!7}{(7)}} \\ \label{proposition:implication17!9} \hypertarget{proposition:implication17!9}{\mbox{(9)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication17!4}{(4)}, \hyperlink{proposition:implication17!6}{(6)}} \\ \label{proposition:implication17!10} \hypertarget{proposition:implication17!10}{\mbox{(10)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication17!8}{(8)}, \hyperlink{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} \begin{prop} \label{proposition:implication18} \hypertarget{proposition:implication18}{} {\tt \tiny [\verb]proposition:implication18]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \land\ C)\ \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:implication18!1} \hypertarget{proposition:implication18!1}{\mbox{(1)}} \ & \ $(A\ \land\ B)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication18!2} \hypertarget{proposition:implication18!2}{\mbox{(2)}} \ & \ $(A\ \land\ C)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication18!1}{(1)}} \\ \label{proposition:implication18!3} \hypertarget{proposition:implication18!3}{\mbox{(3)}} \ & \ $(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{Axiom~4}} \\ \label{proposition:implication18!4} \hypertarget{proposition:implication18!4}{\mbox{(4)}} \ & \ $(A\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication18!3}{(3)}} \\ \label{proposition:implication18!5} \hypertarget{proposition:implication18!5}{\mbox{(5)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \label{proposition:implication18!6} \hypertarget{proposition:implication18!6}{\mbox{(6)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication18!5}{(5)}} \\ \label{proposition:implication18!7} \hypertarget{proposition:implication18!7}{\mbox{(7)}} \ & \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication18!6}{(6)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication18!8} \hypertarget{proposition:implication18!8}{\mbox{(8)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ B$ \ & \ {\tiny Hypothesis} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication18!9} \hypertarget{proposition:implication18!9}{\mbox{(9)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A\ \land\ C$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication18!10} \hypertarget{proposition:implication18!10}{\mbox{(10)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!2}{(2)}, \hyperlink{proposition:implication18!9}{(9)}} \\ \label{proposition:implication18!11} \hypertarget{proposition:implication18!11}{\mbox{(11)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!8}{(8)}, \hyperlink{proposition:implication18!10}{(10)}} \\ \label{proposition:implication18!12} \hypertarget{proposition:implication18!12}{\mbox{(12)}} \ & \ \mbox{\qquad}\mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!4}{(4)}, \hyperlink{proposition:implication18!9}{(9)}} \\ \label{proposition:implication18!13} \hypertarget{proposition:implication18!13}{\mbox{(13)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (B\ \land\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!7}{(7)}, \hyperlink{proposition:implication18!12}{(12)}} \\ \label{proposition:implication18!14} \hypertarget{proposition:implication18!14}{\mbox{(14)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!13}{(13)}, \hyperlink{proposition:implication18!11}{(11)}} \\ \label{proposition:implication18!15} \hypertarget{proposition:implication18!15}{\mbox{(15)}} \ & \ \mbox{\qquad}$(A\ \land\ C)\ \rightarrow\ (B\ \land\ C)$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication18!16} \hypertarget{proposition:implication18!16}{\mbox{(16)}} \ & \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \land\ C)\ \rightarrow\ (B\ \land\ C))$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication19} \hypertarget{proposition:implication19}{} {\tt \tiny [\verb]proposition:implication19]]} \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:implication19!1} \hypertarget{proposition:implication19!1}{\mbox{(1)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \label{proposition:implication19!2} \hypertarget{proposition:implication19!2}{\mbox{(2)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication19!1}{(1)}} \\ \label{proposition:implication19!3} \hypertarget{proposition:implication19!3}{\mbox{(3)}} \ & \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication19!2}{(2)}} \\ \label{proposition:implication19!4} \hypertarget{proposition:implication19!4}{\mbox{(4)}} \ & \ $A\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ A))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A$ in \hyperlink{proposition:implication19!3}{(3)}} \\ \label{proposition:implication19!5} \hypertarget{proposition:implication19!5}{\mbox{(5)}} \ & \ $(A\ \land\ B)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication19!6} \hypertarget{proposition:implication19!6}{\mbox{(6)}} \ & \ $(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{Axiom~4}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication19!7} \hypertarget{proposition:implication19!7}{\mbox{(7)}} \ & \ \mbox{\qquad}$A\ \land\ B$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication19!8} \hypertarget{proposition:implication19!8}{\mbox{(8)}} \ & \ \mbox{\qquad}$A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication19!5}{(5)}, \hyperlink{proposition:implication19!7}{(7)}} \\ \label{proposition:implication19!9} \hypertarget{proposition:implication19!9}{\mbox{(9)}} \ & \ \mbox{\qquad}$B\ \rightarrow\ (B\ \land\ A)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication19!4}{(4)}, \hyperlink{proposition:implication19!8}{(8)}} \\ \label{proposition:implication19!10} \hypertarget{proposition:implication19!10}{\mbox{(10)}} \ & \ \mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication19!6}{(6)}, \hyperlink{proposition:implication19!7}{(7)}} \\ \label{proposition:implication19!11} \hypertarget{proposition:implication19!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$B\ \land\ A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication19!9}{(9)}, \hyperlink{proposition:implication19!10}{(10)}} \\ \label{proposition:implication19!12} \hypertarget{proposition:implication19!12}{\mbox{(12)}} \ & \ $(A\ \land\ B)\ \rightarrow\ (B\ \land\ A)$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \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} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \ & \ Conditional Proof \ & \ \\ \label{proposition:implication20!1} \hypertarget{proposition:implication20!1}{\mbox{(1)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ & \ {\tiny Hypothesis} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication20!2} \hypertarget{proposition:implication20!2}{\mbox{(2)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A\ \land\ B$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication20!3} \hypertarget{proposition:implication20!3}{\mbox{(3)}} \ & \ \mbox{\qquad}\mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication20!4} \hypertarget{proposition:implication20!4}{\mbox{(4)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication20!3}{(3)}, \hyperlink{proposition:implication20!2}{(2)}} \\ \label{proposition:implication20!5} \hypertarget{proposition:implication20!5}{\mbox{(5)}} \ & \ \mbox{\qquad}\mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{Axiom~4}} \\ \label{proposition:implication20!6} \hypertarget{proposition:implication20!6}{\mbox{(6)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication20!5}{(5)}, \hyperlink{proposition:implication20!2}{(2)}} \\ \label{proposition:implication20!7} \hypertarget{proposition:implication20!7}{\mbox{(7)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication20!1}{(1)}, \hyperlink{proposition:implication20!4}{(4)}} \\ \label{proposition:implication20!8} \hypertarget{proposition:implication20!8}{\mbox{(8)}} \ & \ \mbox{\qquad}\mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication20!7}{(7)}, \hyperlink{proposition:implication20!6}{(6)}} \\ \label{proposition:implication20!9} \hypertarget{proposition:implication20!9}{\mbox{(9)}} \ & \ \mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ C$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication20!10} \hypertarget{proposition:implication20!10}{\mbox{(10)}} \ & \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ C)$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \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} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \ & \ Conditional Proof \ & \ \\ \label{proposition:implication21!1} \hypertarget{proposition:implication21!1}{\mbox{(1)}} \ & \ \mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ C$ \ & \ {\tiny Hypothesis} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication21!2} \hypertarget{proposition:implication21!2}{\mbox{(2)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication21!3} \hypertarget{proposition:implication21!3}{\mbox{(3)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \ & \ \mbox{\qquad}\mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication21!4} \hypertarget{proposition:implication21!4}{\mbox{(4)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication21!5} \hypertarget{proposition:implication21!5}{\mbox{(5)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ (A\ \land\ B)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication21!3}{(3)}, \hyperlink{proposition:implication21!4}{(4)}} \\ \label{proposition:implication21!6} \hypertarget{proposition:implication21!6}{\mbox{(6)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \land\ B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication21!5}{(5)}, \hyperlink{proposition:implication21!2}{(2)}} \\ \label{proposition:implication21!7} \hypertarget{proposition:implication21!7}{\mbox{(7)}} \ & \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication21!1}{(1)}, \hyperlink{proposition:implication21!6}{(6)}} \\ \label{proposition:implication21!8} \hypertarget{proposition:implication21!8}{\mbox{(8)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication21!9} \hypertarget{proposition:implication21!9}{\mbox{(9)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication21!10} \hypertarget{proposition:implication21!10}{\mbox{(10)}} \ & \ $((A\ \land\ B)\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication25} \hypertarget{proposition:implication25}{} {\tt \tiny [\verb]proposition:implication25]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $((A\ \rightarrow\ B)\ \land\ (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:implication25!1} \hypertarget{proposition:implication25!1}{\mbox{(1)}} \ & \ $(A\ \land\ B)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication25!2} \hypertarget{proposition:implication25!2}{\mbox{(2)}} \ & \ $(A\ \land\ C)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication25!1}{(1)}} \\ \label{proposition:implication25!3} \hypertarget{proposition:implication25!3}{\mbox{(3)}} \ & \ $((A\ \rightarrow\ B)\ \land\ C)\ \rightarrow\ (A\ \rightarrow\ B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication25!2}{(2)}} \\ \label{proposition:implication25!4} \hypertarget{proposition:implication25!4}{\mbox{(4)}} \ & \ $((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \rightarrow\ C$ in \hyperlink{proposition:implication25!3}{(3)}} \\ \label{proposition:implication25!5} \hypertarget{proposition:implication25!5}{\mbox{(5)}} \ & \ $(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{Axiom~4}} \\ \label{proposition:implication25!6} \hypertarget{proposition:implication25!6}{\mbox{(6)}} \ & \ $(A\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication25!5}{(5)}} \\ \label{proposition:implication25!7} \hypertarget{proposition:implication25!7}{\mbox{(7)}} \ & \ $((A\ \rightarrow\ B)\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication25!6}{(6)}} \\ \label{proposition:implication25!8} \hypertarget{proposition:implication25!8}{\mbox{(8)}} \ & \ $((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \rightarrow\ C$ in \hyperlink{proposition:implication25!7}{(7)}} \\ \label{proposition:implication25!9} \hypertarget{proposition:implication25!9}{\mbox{(9)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \label{proposition:implication25!10} \hypertarget{proposition:implication25!10}{\mbox{(10)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication25!9}{(9)}} \\ \label{proposition:implication25!11} \hypertarget{proposition:implication25!11}{\mbox{(11)}} \ & \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication25!10}{(10)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication25!12} \hypertarget{proposition:implication25!12}{\mbox{(12)}} \ & \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C)$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication25!13} \hypertarget{proposition:implication25!13}{\mbox{(13)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!4}{(4)}, \hyperlink{proposition:implication25!12}{(12)}} \\ \label{proposition:implication25!14} \hypertarget{proposition:implication25!14}{\mbox{(14)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!8}{(8)}, \hyperlink{proposition:implication25!12}{(12)}} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication25!15} \hypertarget{proposition:implication25!15}{\mbox{(15)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication25!16} \hypertarget{proposition:implication25!16}{\mbox{(16)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!13}{(13)}, \hyperlink{proposition:implication25!15}{(15)}} \\ \label{proposition:implication25!17} \hypertarget{proposition:implication25!17}{\mbox{(17)}} \ & \ \mbox{\qquad}\mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!14}{(14)}, \hyperlink{proposition:implication25!15}{(15)}} \\ \label{proposition:implication25!18} \hypertarget{proposition:implication25!18}{\mbox{(18)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (B\ \land\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!11}{(11)}, \hyperlink{proposition:implication25!17}{(17)}} \\ \label{proposition:implication25!19} \hypertarget{proposition:implication25!19}{\mbox{(19)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!18}{(18)}, \hyperlink{proposition:implication25!16}{(16)}} \\ \label{proposition:implication25!20} \hypertarget{proposition:implication25!20}{\mbox{(20)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ (B\ \land\ C)$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication25!21} \hypertarget{proposition:implication25!21}{\mbox{(21)}} \ & \ $((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C))$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication26} \hypertarget{proposition:implication26}{} {\tt \tiny [\verb]proposition:implication26]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(A\ \rightarrow\ (B\ \land\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))$ \end{longtable} \end{prop} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{proposition:implication26!1} \hypertarget{proposition:implication26!1}{\mbox{(1)}} \ & \ $(A\ \land\ B)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication26!2} \hypertarget{proposition:implication26!2}{\mbox{(2)}} \ & \ $(A\ \land\ C)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication26!1}{(1)}} \\ \label{proposition:implication26!3} \hypertarget{proposition:implication26!3}{\mbox{(3)}} \ & \ $(B\ \land\ C)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication26!2}{(2)}} \\ \label{proposition:implication26!4} \hypertarget{proposition:implication26!4}{\mbox{(4)}} \ & \ $(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{Axiom~4}} \\ \label{proposition:implication26!5} \hypertarget{proposition:implication26!5}{\mbox{(5)}} \ & \ $(A\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication26!4}{(4)}} \\ \label{proposition:implication26!6} \hypertarget{proposition:implication26!6}{\mbox{(6)}} \ & \ $(B\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication26!5}{(5)}} \\ \label{proposition:implication26!7} \hypertarget{proposition:implication26!7}{\mbox{(7)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \label{proposition:implication26!8} \hypertarget{proposition:implication26!8}{\mbox{(8)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication26!7}{(7)}} \\ \label{proposition:implication26!9} \hypertarget{proposition:implication26!9}{\mbox{(9)}} \ & \ $C\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication26!8}{(8)}} \\ \label{proposition:implication26!10} \hypertarget{proposition:implication26!10}{\mbox{(10)}} \ & \ $(A\ \rightarrow\ C)\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C)))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \rightarrow\ C$ in \hyperlink{proposition:implication26!9}{(9)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication26!11} \hypertarget{proposition:implication26!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ (B\ \land\ C)$ \ & \ {\tiny Hypothesis} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication26!12} \hypertarget{proposition:implication26!12}{\mbox{(12)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication26!13} \hypertarget{proposition:implication26!13}{\mbox{(13)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!11}{(11)}, \hyperlink{proposition:implication26!12}{(12)}} \\ \label{proposition:implication26!14} \hypertarget{proposition:implication26!14}{\mbox{(14)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!3}{(3)}, \hyperlink{proposition:implication26!13}{(13)}} \\ \label{proposition:implication26!15} \hypertarget{proposition:implication26!15}{\mbox{(15)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ B$ \ & \ {\tiny Conclusion} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication26!16} \hypertarget{proposition:implication26!16}{\mbox{(16)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication26!17} \hypertarget{proposition:implication26!17}{\mbox{(17)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!11}{(11)}, \hyperlink{proposition:implication26!16}{(16)}} \\ \label{proposition:implication26!18} \hypertarget{proposition:implication26!18}{\mbox{(18)}} \ & \ \mbox{\qquad}\mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!6}{(6)}, \hyperlink{proposition:implication26!17}{(17)}} \\ \label{proposition:implication26!19} \hypertarget{proposition:implication26!19}{\mbox{(19)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ C$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication26!20} \hypertarget{proposition:implication26!20}{\mbox{(20)}} \ & \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!10}{(10)}, \hyperlink{proposition:implication26!19}{(19)}} \\ \label{proposition:implication26!21} \hypertarget{proposition:implication26!21}{\mbox{(21)}} \ & \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!20}{(20)}, \hyperlink{proposition:implication26!15}{(15)}} \\ \label{proposition:implication26!22} \hypertarget{proposition:implication26!22}{\mbox{(22)}} \ & \ $(A\ \rightarrow\ (B\ \land\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication27} \hypertarget{proposition:implication27}{} {\tt \tiny [\verb]proposition:implication27]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $((A\ \land\ B)\ \land\ C)\ \rightarrow\ (A\ \land\ (B\ \land\ C))$ \end{longtable} \end{prop} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{proposition:implication27!1} \hypertarget{proposition:implication27!1}{\mbox{(1)}} \ & \ $(A\ \land\ B)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication27!2} \hypertarget{proposition:implication27!2}{\mbox{(2)}} \ & \ $(A\ \land\ C)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication27!1}{(1)}} \\ \label{proposition:implication27!3} \hypertarget{proposition:implication27!3}{\mbox{(3)}} \ & \ $((A\ \land\ B)\ \land\ C)\ \rightarrow\ (A\ \land\ B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \land\ B$ in \hyperlink{proposition:implication27!2}{(2)}} \\ \label{proposition:implication27!4} \hypertarget{proposition:implication27!4}{\mbox{(4)}} \ & \ $(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{Axiom~4}} \\ \label{proposition:implication27!5} \hypertarget{proposition:implication27!5}{\mbox{(5)}} \ & \ $(A\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication27!4}{(4)}} \\ \label{proposition:implication27!6} \hypertarget{proposition:implication27!6}{\mbox{(6)}} \ & \ $((A\ \land\ B)\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \land\ B$ in \hyperlink{proposition:implication27!5}{(5)}} \\ \label{proposition:implication27!7} \hypertarget{proposition:implication27!7}{\mbox{(7)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \label{proposition:implication27!8} \hypertarget{proposition:implication27!8}{\mbox{(8)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication27!7}{(7)}} \\ \label{proposition:implication27!9} \hypertarget{proposition:implication27!9}{\mbox{(9)}} \ & \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication27!8}{(8)}} \\ \label{proposition:implication27!10} \hypertarget{proposition:implication27!10}{\mbox{(10)}} \ & \ $(B\ \land\ C)\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ (B\ \land\ C)))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \land\ C$ in \hyperlink{proposition:implication27!7}{(7)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication27!11} \hypertarget{proposition:implication27!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$(A\ \land\ B)\ \land\ C$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication27!12} \hypertarget{proposition:implication27!12}{\mbox{(12)}} \ & \ \mbox{\qquad}$A\ \land\ B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!3}{(3)}, \hyperlink{proposition:implication27!11}{(11)}} \\ \label{proposition:implication27!13} \hypertarget{proposition:implication27!13}{\mbox{(13)}} \ & \ \mbox{\qquad}$A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!1}{(1)}, \hyperlink{proposition:implication27!12}{(12)}} \\ \label{proposition:implication27!14} \hypertarget{proposition:implication27!14}{\mbox{(14)}} \ & \ \mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!4}{(4)}, \hyperlink{proposition:implication27!12}{(12)}} \\ \label{proposition:implication27!15} \hypertarget{proposition:implication27!15}{\mbox{(15)}} \ & \ \mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!6}{(6)}, \hyperlink{proposition:implication27!11}{(11)}} \\ \label{proposition:implication27!16} \hypertarget{proposition:implication27!16}{\mbox{(16)}} \ & \ \mbox{\qquad}$B\ \rightarrow\ (B\ \land\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!9}{(9)}, \hyperlink{proposition:implication27!15}{(15)}} \\ \label{proposition:implication27!17} \hypertarget{proposition:implication27!17}{\mbox{(17)}} \ & \ \mbox{\qquad}$B\ \land\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!16}{(16)}, \hyperlink{proposition:implication27!14}{(14)}} \\ \label{proposition:implication27!18} \hypertarget{proposition:implication27!18}{\mbox{(18)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ (A\ \land\ (B\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!10}{(10)}, \hyperlink{proposition:implication27!17}{(17)}} \\ \label{proposition:implication27!19} \hypertarget{proposition:implication27!19}{\mbox{(19)}} \ & \ \mbox{\qquad}$A\ \land\ (B\ \land\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!18}{(18)}, \hyperlink{proposition:implication27!13}{(13)}} \\ \label{proposition:implication27!20} \hypertarget{proposition:implication27!20}{\mbox{(20)}} \ & \ $((A\ \land\ B)\ \land\ C)\ \rightarrow\ (A\ \land\ (B\ \land\ C))$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication28} \hypertarget{proposition:implication28}{} {\tt \tiny [\verb]proposition:implication28]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(A\ \land\ (B\ \land\ C))\ \rightarrow\ ((A\ \land\ B)\ \land\ C)$ \end{longtable} \end{prop} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{proposition:implication28!1} \hypertarget{proposition:implication28!1}{\mbox{(1)}} \ & \ $(A\ \land\ B)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{Axiom~3}} \\ \label{proposition:implication28!2} \hypertarget{proposition:implication28!2}{\mbox{(2)}} \ & \ $(A\ \land\ (B\ \land\ C))\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \land\ C$ in \hyperlink{proposition:implication28!1}{(1)}} \\ \label{proposition:implication28!3} \hypertarget{proposition:implication28!3}{\mbox{(3)}} \ & \ $(A\ \land\ C)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication28!1}{(1)}} \\ \label{proposition:implication28!4} \hypertarget{proposition:implication28!4}{\mbox{(4)}} \ & \ $(B\ \land\ C)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication28!3}{(3)}} \\ \label{proposition:implication28!5} \hypertarget{proposition:implication28!5}{\mbox{(5)}} \ & \ $(A\ \land\ B)\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{Axiom~4}} \\ \label{proposition:implication28!6} \hypertarget{proposition:implication28!6}{\mbox{(6)}} \ & \ $(A\ \land\ (B\ \land\ C))\ \rightarrow\ (B\ \land\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \land\ C$ in \hyperlink{proposition:implication28!5}{(5)}} \\ \label{proposition:implication28!7} \hypertarget{proposition:implication28!7}{\mbox{(7)}} \ & \ $(A\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication28!5}{(5)}} \\ \label{proposition:implication28!8} \hypertarget{proposition:implication28!8}{\mbox{(8)}} \ & \ $(B\ \land\ C)\ \rightarrow\ C$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication28!7}{(7)}} \\ \label{proposition:implication28!9} \hypertarget{proposition:implication28!9}{\mbox{(9)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{Axiom~5}} \\ \label{proposition:implication28!10} \hypertarget{proposition:implication28!10}{\mbox{(10)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication28!9}{(9)}} \\ \label{proposition:implication28!11} \hypertarget{proposition:implication28!11}{\mbox{(11)}} \ & \ $C\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ ((A\ \land\ B)\ \land\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \land\ B$ in \hyperlink{proposition:implication28!10}{(10)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication28!12} \hypertarget{proposition:implication28!12}{\mbox{(12)}} \ & \ \mbox{\qquad}$A\ \land\ (B\ \land\ C)$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication28!13} \hypertarget{proposition:implication28!13}{\mbox{(13)}} \ & \ \mbox{\qquad}$A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!2}{(2)}, \hyperlink{proposition:implication28!12}{(12)}} \\ \label{proposition:implication28!14} \hypertarget{proposition:implication28!14}{\mbox{(14)}} \ & \ \mbox{\qquad}$B\ \land\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!6}{(6)}, \hyperlink{proposition:implication28!12}{(12)}} \\ \label{proposition:implication28!15} \hypertarget{proposition:implication28!15}{\mbox{(15)}} \ & \ \mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!4}{(4)}, \hyperlink{proposition:implication28!14}{(14)}} \\ \label{proposition:implication28!16} \hypertarget{proposition:implication28!16}{\mbox{(16)}} \ & \ \mbox{\qquad}$C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!8}{(8)}, \hyperlink{proposition:implication28!14}{(14)}} \\ \label{proposition:implication28!17} \hypertarget{proposition:implication28!17}{\mbox{(17)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ (A\ \land\ B)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!9}{(9)}, \hyperlink{proposition:implication28!15}{(15)}} \\ \label{proposition:implication28!18} \hypertarget{proposition:implication28!18}{\mbox{(18)}} \ & \ \mbox{\qquad}$A\ \land\ B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!17}{(17)}, \hyperlink{proposition:implication28!13}{(13)}} \\ \label{proposition:implication28!19} \hypertarget{proposition:implication28!19}{\mbox{(19)}} \ & \ \mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ ((A\ \land\ B)\ \land\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!11}{(11)}, \hyperlink{proposition:implication28!16}{(16)}} \\ \label{proposition:implication28!20} \hypertarget{proposition:implication28!20}{\mbox{(20)}} \ & \ \mbox{\qquad}$(A\ \land\ B)\ \land\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!19}{(19)}, \hyperlink{proposition:implication28!18}{(18)}} \\ \label{proposition:implication28!21} \hypertarget{proposition:implication28!21}{\mbox{(21)}} \ & \ $(A\ \land\ (B\ \land\ C))\ \rightarrow\ ((A\ \land\ B)\ \land\ C)$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \section{S{\"a}tze zur Disjunktion} \label{chapter4_section5} \hypertarget{chapter4_section5}{} Die Disjunktion ist jetzt unser Thema. \begin{prop} \label{proposition:40} \hypertarget{proposition:40}{} {\tt \tiny [\verb]proposition:40]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(A\ \lor\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \end{longtable} \end{prop} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{proposition:40!1} \hypertarget{proposition:40!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ (A\ \lor\ B)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-1}{Axiom~6}} \\ \label{proposition:40!2} \hypertarget{proposition:40!2}{\mbox{(2)}} \ & \ $A\ \rightarrow\ (A\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:40!1}{(1)}} \\ \label{proposition:40!3} \hypertarget{proposition:40!3}{\mbox{(3)}} \ & \ $(A\ \lor\ B)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \lor\ B$ in \hyperlink{proposition:40!2}{(2)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:40!4} \hypertarget{proposition:40!4}{\mbox{(4)}} \ & \ \mbox{\qquad}$A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:40!5} \hypertarget{proposition:40!5}{\mbox{(5)}} \ & \ \mbox{\qquad}$A\ \lor\ B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!1}{(1)}, \hyperlink{proposition:40!4}{(4)}} \\ \label{proposition:40!6} \hypertarget{proposition:40!6}{\mbox{(6)}} \ & \ \mbox{\qquad}$(A\ \lor\ B)\ \lor\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!3}{(3)}, \hyperlink{proposition:40!5}{(5)}} \\ \label{proposition:40!7} \hypertarget{proposition:40!7}{\mbox{(7)}} \ & \ $A\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ & \ {\tiny Conclusion} \\ \label{proposition:40!8} \hypertarget{proposition:40!8}{\mbox{(8)}} \ & \ $A\ \rightarrow\ (B\ \lor\ A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-2}{Axiom~7}} \\ \label{proposition:40!9} \hypertarget{proposition:40!9}{\mbox{(9)}} \ & \ $C\ \rightarrow\ (B\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:40!8}{(8)}} \\ \label{proposition:40!10} \hypertarget{proposition:40!10}{\mbox{(10)}} \ & \ $C\ \rightarrow\ (A\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:40!9}{(9)}} \\ \label{proposition:40!11} \hypertarget{proposition:40!11}{\mbox{(11)}} \ & \ $B\ \rightarrow\ (A\ \lor\ B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $B$ in \hyperlink{proposition:40!10}{(10)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:40!12} \hypertarget{proposition:40!12}{\mbox{(12)}} \ & \ \mbox{\qquad}$B$ \ & \ {\tiny Hypothesis} \\ \label{proposition:40!13} \hypertarget{proposition:40!13}{\mbox{(13)}} \ & \ \mbox{\qquad}$A\ \lor\ B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!11}{(11)}, \hyperlink{proposition:40!12}{(12)}} \\ \label{proposition:40!14} \hypertarget{proposition:40!14}{\mbox{(14)}} \ & \ \mbox{\qquad}$(A\ \lor\ B)\ \lor\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!3}{(3)}, \hyperlink{proposition:40!13}{(13)}} \\ \label{proposition:40!15} \hypertarget{proposition:40!15}{\mbox{(15)}} \ & \ $B\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ & \ {\tiny Conclusion} \\ \label{proposition:40!16} \hypertarget{proposition:40!16}{\mbox{(16)}} \ & \ $C\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A\ \lor\ B$ in \hyperlink{proposition:40!9}{(9)}} \\ \label{proposition:40!17} \hypertarget{proposition:40!17}{\mbox{(17)}} \ & \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{Axiom~8}} \\ \label{proposition:40!18} \hypertarget{proposition:40!18}{\mbox{(18)}} \ & \ $(A\ \rightarrow\ D)\ \rightarrow\ ((B\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ D))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:40!17}{(17)}} \\ \label{proposition:40!19} \hypertarget{proposition:40!19}{\mbox{(19)}} \ & \ $(A\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ D))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:40!18}{(18)}} \\ \label{proposition:40!20} \hypertarget{proposition:40!20}{\mbox{(20)}} \ & \ $(B\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ D))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:40!19}{(19)}} \\ \label{proposition:40!21} \hypertarget{proposition:40!21}{\mbox{(21)}} \ & \ $(B\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((C\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $(A\ \lor\ B)\ \lor\ C$ in \hyperlink{proposition:40!20}{(20)}} \\ \label{proposition:40!22} \hypertarget{proposition:40!22}{\mbox{(22)}} \ & \ $(C\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!21}{(21)}, \hyperlink{proposition:40!15}{(15)}} \\ \label{proposition:40!23} \hypertarget{proposition:40!23}{\mbox{(23)}} \ & \ $(B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!22}{(22)}, \hyperlink{proposition:40!16}{(16)}} \\ \label{proposition:40!24} \hypertarget{proposition:40!24}{\mbox{(24)}} \ & \ $(A\ \rightarrow\ D)\ \rightarrow\ (((B\ \lor\ C)\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ (B\ \lor\ C))\ \rightarrow\ D))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \lor\ C$ in \hyperlink{proposition:40!18}{(18)}} \\ \label{proposition:40!25} \hypertarget{proposition:40!25}{\mbox{(25)}} \ & \ $(A\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ (((B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((A\ \lor\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $(A\ \lor\ B)\ \lor\ C$ in \hyperlink{proposition:40!24}{(24)}} \\ \label{proposition:40!26} \hypertarget{proposition:40!26}{\mbox{(26)}} \ & \ $((B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((A\ \lor\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!25}{(25)}, \hyperlink{proposition:40!7}{(7)}} \\ \label{proposition:40!27} \hypertarget{proposition:40!27}{\mbox{(27)}} \ & \ $(A\ \lor\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!26}{(26)}, \hyperlink{proposition:40!23}{(23)}} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication41} \hypertarget{proposition:implication41}{} {\tt \tiny [\verb]proposition:implication41]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \end{longtable} \end{prop} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{proposition:implication41!1} \hypertarget{proposition:implication41!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ (A\ \lor\ B)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-1}{Axiom~6}} \\ \label{proposition:implication41!2} \hypertarget{proposition:implication41!2}{\mbox{(2)}} \ & \ $A\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \lor\ C$ in \hyperlink{proposition:implication41!1}{(1)}} \\ \label{proposition:implication41!3} \hypertarget{proposition:implication41!3}{\mbox{(3)}} \ & \ $A\ \rightarrow\ (A\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication41!1}{(1)}} \\ \label{proposition:implication41!4} \hypertarget{proposition:implication41!4}{\mbox{(4)}} \ & \ $B\ \rightarrow\ (B\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication41!3}{(3)}} \\ \label{proposition:implication41!5} \hypertarget{proposition:implication41!5}{\mbox{(5)}} \ & \ $A\ \rightarrow\ (B\ \lor\ A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-2}{Axiom~7}} \\ \label{proposition:implication41!6} \hypertarget{proposition:implication41!6}{\mbox{(6)}} \ & \ $A\ \rightarrow\ (D\ \lor\ A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $D$ in \hyperlink{proposition:implication41!5}{(5)}} \\ \label{proposition:implication41!7} \hypertarget{proposition:implication41!7}{\mbox{(7)}} \ & \ $(B\ \lor\ C)\ \rightarrow\ (D\ \lor\ (B\ \lor\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B\ \lor\ C$ in \hyperlink{proposition:implication41!6}{(6)}} \\ \label{proposition:implication41!8} \hypertarget{proposition:implication41!8}{\mbox{(8)}} \ & \ $(B\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $A$ in \hyperlink{proposition:implication41!7}{(7)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication41!9} \hypertarget{proposition:implication41!9}{\mbox{(9)}} \ & \ \mbox{\qquad}$B$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication41!10} \hypertarget{proposition:implication41!10}{\mbox{(10)}} \ & \ \mbox{\qquad}$B\ \lor\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!4}{(4)}, \hyperlink{proposition:implication41!9}{(9)}} \\ \label{proposition:implication41!11} \hypertarget{proposition:implication41!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$A\ \lor\ (B\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!8}{(8)}, \hyperlink{proposition:implication41!10}{(10)}} \\ \label{proposition:implication41!12} \hypertarget{proposition:implication41!12}{\mbox{(12)}} \ & \ $B\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication41!13} \hypertarget{proposition:implication41!13}{\mbox{(13)}} \ & \ $C\ \rightarrow\ (B\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication41!5}{(5)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication41!14} \hypertarget{proposition:implication41!14}{\mbox{(14)}} \ & \ \mbox{\qquad}$C$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication41!15} \hypertarget{proposition:implication41!15}{\mbox{(15)}} \ & \ \mbox{\qquad}$B\ \lor\ C$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!13}{(13)}, \hyperlink{proposition:implication41!14}{(14)}} \\ \label{proposition:implication41!16} \hypertarget{proposition:implication41!16}{\mbox{(16)}} \ & \ \mbox{\qquad}$A\ \lor\ (B\ \lor\ C)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!8}{(8)}, \hyperlink{proposition:implication41!15}{(15)}} \\ \label{proposition:implication41!17} \hypertarget{proposition:implication41!17}{\mbox{(17)}} \ & \ $C\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication41!18} \hypertarget{proposition:implication41!18}{\mbox{(18)}} \ & \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{Axiom~8}} \\ \label{proposition:implication41!19} \hypertarget{proposition:implication41!19}{\mbox{(19)}} \ & \ $(A\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ ((B\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \lor\ (B\ \lor\ C)$ in \hyperlink{proposition:implication41!18}{(18)}} \\ \label{proposition:implication41!20} \hypertarget{proposition:implication41!20}{\mbox{(20)}} \ & \ $(B\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!19}{(19)}, \hyperlink{proposition:implication41!2}{(2)}} \\ \label{proposition:implication41!21} \hypertarget{proposition:implication41!21}{\mbox{(21)}} \ & \ $(A\ \lor\ B)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!20}{(20)}, \hyperlink{proposition:implication41!12}{(12)}} \\ \label{proposition:implication41!22} \hypertarget{proposition:implication41!22}{\mbox{(22)}} \ & \ $(A\ \rightarrow\ D)\ \rightarrow\ ((B\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ D))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:implication41!18}{(18)}} \\ \label{proposition:implication41!23} \hypertarget{proposition:implication41!23}{\mbox{(23)}} \ & \ $(A\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ D))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication41!22}{(22)}} \\ \label{proposition:implication41!24} \hypertarget{proposition:implication41!24}{\mbox{(24)}} \ & \ $((A\ \lor\ B)\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ (((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ D))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \lor\ B$ in \hyperlink{proposition:implication41!23}{(23)}} \\ \label{proposition:implication41!25} \hypertarget{proposition:implication41!25}{\mbox{(25)}} \ & \ $((A\ \lor\ B)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ ((C\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ (((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $A\ \lor\ (B\ \lor\ C)$ in \hyperlink{proposition:implication41!24}{(24)}} \\ \label{proposition:implication41!26} \hypertarget{proposition:implication41!26}{\mbox{(26)}} \ & \ $(C\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ (((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!25}{(25)}, \hyperlink{proposition:implication41!21}{(21)}} \\ \label{proposition:implication41!27} \hypertarget{proposition:implication41!27}{\mbox{(27)}} \ & \ $((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!26}{(26)}, \hyperlink{proposition:implication41!17}{(17)}} \\ & & \qedhere \end{longtable} \end{proof} \section{S{\"a}tze zur Negation} \label{chapter4_section6} \hypertarget{chapter4_section6}{} Wir kommen nun zur Negation. Hier m{\"u}ssen wir das erste Mal von dem Prinzip vom ausgeschlossenen Dritten Gebrauch machen. \begin{prop} \label{proposition:implication50} \hypertarget{proposition:implication50}{} {\tt \tiny [\verb]proposition:implication50]]} \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:implication50!1} \hypertarget{proposition:implication50!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:THEN-1}{Axiom~1}} \\ \label{proposition:implication50!2} \hypertarget{proposition:implication50!2}{\mbox{(2)}} \ & \ $A\ \rightarrow\ (\neg A\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $\neg A$ in \hyperlink{proposition:implication50!1}{(1)}} \\ \label{proposition:implication50!3} \hypertarget{proposition:implication50!3}{\mbox{(3)}} \ & \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-1}{Axiom~9}} \\ \label{proposition:implication50!4} \hypertarget{proposition:implication50!4}{\mbox{(4)}} \ & \ $(\neg A\ \rightarrow\ B)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg B)\ \rightarrow\ \neg \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication50!3}{(3)}} \\ \label{proposition:implication50!5} \hypertarget{proposition:implication50!5}{\mbox{(5)}} \ & \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication50!4}{(4)}} \\ \label{proposition:implication50!6} \hypertarget{proposition:implication50!6}{\mbox{(6)}} \ & \ $A\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implicationReflexive1}{Proposition~1}} \\ \label{proposition:implication50!7} \hypertarget{proposition:implication50!7}{\mbox{(7)}} \ & \ $\neg A\ \rightarrow\ \neg A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication50!6}{(6)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication50!8} \hypertarget{proposition:implication50!8}{\mbox{(8)}} \ & \ \mbox{\qquad}$A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication50!9} \hypertarget{proposition:implication50!9}{\mbox{(9)}} \ & \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication50!2}{(2)}, \hyperlink{proposition:implication50!8}{(8)}} \\ \label{proposition:implication50!10} \hypertarget{proposition:implication50!10}{\mbox{(10)}} \ & \ \mbox{\qquad}$(\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication50!5}{(5)}, \hyperlink{proposition:implication50!9}{(9)}} \\ \label{proposition:implication50!11} \hypertarget{proposition:implication50!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$\neg \neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication50!10}{(10)}, \hyperlink{proposition:implication50!7}{(7)}} \\ \label{proposition:implication50!12} \hypertarget{proposition:implication50!12}{\mbox{(12)}} \ & \ $A\ \rightarrow\ \neg \neg A$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication51} \hypertarget{proposition:implication51}{} {\tt \tiny [\verb]proposition:implication51]]} \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:implication51!1} \hypertarget{proposition:implication51!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:THEN-1}{Axiom~1}} \\ \label{proposition:implication51!2} \hypertarget{proposition:implication51!2}{\mbox{(2)}} \ & \ $C\ \rightarrow\ (B\ \rightarrow\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication51!1}{(1)}} \\ \label{proposition:implication51!3} \hypertarget{proposition:implication51!3}{\mbox{(3)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication51!2}{(2)}} \\ \label{proposition:implication51!4} \hypertarget{proposition:implication51!4}{\mbox{(4)}} \ & \ $B\ \rightarrow\ (A\ \rightarrow\ B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $B$ in \hyperlink{proposition:implication51!3}{(3)}} \\ \label{proposition:implication51!5} \hypertarget{proposition:implication51!5}{\mbox{(5)}} \ & \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-1}{Axiom~9}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication51!6} \hypertarget{proposition:implication51!6}{\mbox{(6)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ \neg B$ \ & \ {\tiny Hypothesis} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication51!7} \hypertarget{proposition:implication51!7}{\mbox{(7)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication51!8} \hypertarget{proposition:implication51!8}{\mbox{(8)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication51!4}{(4)}, \hyperlink{proposition:implication51!7}{(7)}} \\ \label{proposition:implication51!9} \hypertarget{proposition:implication51!9}{\mbox{(9)}} \ & \ \mbox{\qquad}\mbox{\qquad}$(A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication51!5}{(5)}, \hyperlink{proposition:implication51!8}{(8)}} \\ \label{proposition:implication51!10} \hypertarget{proposition:implication51!10}{\mbox{(10)}} \ & \ \mbox{\qquad}\mbox{\qquad}$\neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication51!9}{(9)}, \hyperlink{proposition:implication51!6}{(6)}} \\ \label{proposition:implication51!11} \hypertarget{proposition:implication51!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$B\ \rightarrow\ \neg A$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication51!12} \hypertarget{proposition:implication51!12}{\mbox{(12)}} \ & \ $(A\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg A)$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication52} \hypertarget{proposition:implication52}{} {\tt \tiny [\verb]proposition:implication52]]} \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:implication52!1} \hypertarget{proposition:implication52!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:THEN-1}{Axiom~1}} \\ \label{proposition:implication52!2} \hypertarget{proposition:implication52!2}{\mbox{(2)}} \ & \ $C\ \rightarrow\ (B\ \rightarrow\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication52!1}{(1)}} \\ \label{proposition:implication52!3} \hypertarget{proposition:implication52!3}{\mbox{(3)}} \ & \ $C\ \rightarrow\ (A\ \rightarrow\ C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication52!2}{(2)}} \\ \label{proposition:implication52!4} \hypertarget{proposition:implication52!4}{\mbox{(4)}} \ & \ $\neg B\ \rightarrow\ (A\ \rightarrow\ \neg B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $\neg B$ in \hyperlink{proposition:implication52!3}{(3)}} \\ \label{proposition:implication52!5} \hypertarget{proposition:implication52!5}{\mbox{(5)}} \ & \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-1}{Axiom~9}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication52!6} \hypertarget{proposition:implication52!6}{\mbox{(6)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ B$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication52!7} \hypertarget{proposition:implication52!7}{\mbox{(7)}} \ & \ \mbox{\qquad}$(A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication52!5}{(5)}, \hyperlink{proposition:implication52!6}{(6)}} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication52!8} \hypertarget{proposition:implication52!8}{\mbox{(8)}} \ & \ \mbox{\qquad}\mbox{\qquad}$\neg B$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication52!9} \hypertarget{proposition:implication52!9}{\mbox{(9)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ \neg B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication52!4}{(4)}, \hyperlink{proposition:implication52!8}{(8)}} \\ \label{proposition:implication52!10} \hypertarget{proposition:implication52!10}{\mbox{(10)}} \ & \ \mbox{\qquad}\mbox{\qquad}$\neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication52!7}{(7)}, \hyperlink{proposition:implication52!9}{(9)}} \\ \label{proposition:implication52!11} \hypertarget{proposition:implication52!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$\neg B\ \rightarrow\ \neg A$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication52!12} \hypertarget{proposition:implication52!12}{\mbox{(12)}} \ & \ $(A\ \rightarrow\ B)\ \rightarrow\ (\neg B\ \rightarrow\ \neg A)$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication54} \hypertarget{proposition:implication54}{} {\tt \tiny [\verb]proposition:implication54]]} \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:implication54!1} \hypertarget{proposition:implication54!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ \neg \neg A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication50}{Proposition~22}} \\ \label{proposition:implication54!2} \hypertarget{proposition:implication54!2}{\mbox{(2)}} \ & \ $(A\ \rightarrow\ B)\ \rightarrow\ (\neg B\ \rightarrow\ \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication52}{Proposition~24}} \\ \label{proposition:implication54!3} \hypertarget{proposition:implication54!3}{\mbox{(3)}} \ & \ $(A\ \rightarrow\ \neg \neg A)\ \rightarrow\ (\neg \neg \neg A\ \rightarrow\ \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $\neg \neg A$ in \hyperlink{proposition:implication54!2}{(2)}} \\ \label{proposition:implication54!4} \hypertarget{proposition:implication54!4}{\mbox{(4)}} \ & \ $\neg \neg \neg A\ \rightarrow\ \neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication54!3}{(3)}, \hyperlink{proposition:implication54!1}{(1)}} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication55} \hypertarget{proposition:implication55}{} {\tt \tiny [\verb]proposition:implication55]]} \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:implication55!1} \hypertarget{proposition:implication55!1}{\mbox{(1)}} \ & \ $A\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implicationReflexive1}{Proposition~1}} \\ \label{proposition:implication55!2} \hypertarget{proposition:implication55!2}{\mbox{(2)}} \ & \ $\neg A\ \rightarrow\ \neg A$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication55!1}{(1)}} \\ \label{proposition:implication55!3} \hypertarget{proposition:implication55!3}{\mbox{(3)}} \ & \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-1}{Axiom~9}} \\ \label{proposition:implication55!4} \hypertarget{proposition:implication55!4}{\mbox{(4)}} \ & \ $(\neg A\ \rightarrow\ B)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg B)\ \rightarrow\ \neg \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication55!3}{(3)}} \\ \label{proposition:implication55!5} \hypertarget{proposition:implication55!5}{\mbox{(5)}} \ & \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication55!4}{(4)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication55!6} \hypertarget{proposition:implication55!6}{\mbox{(6)}} \ & \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication55!7} \hypertarget{proposition:implication55!7}{\mbox{(7)}} \ & \ \mbox{\qquad}$(\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication55!5}{(5)}, \hyperlink{proposition:implication55!6}{(6)}} \\ \label{proposition:implication55!8} \hypertarget{proposition:implication55!8}{\mbox{(8)}} \ & \ \mbox{\qquad}$\neg \neg A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication55!7}{(7)}, \hyperlink{proposition:implication55!2}{(2)}} \\ \label{proposition:implication55!9} \hypertarget{proposition:implication55!9}{\mbox{(9)}} \ & \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ \neg \neg A$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication56} \hypertarget{proposition:implication56}{} {\tt \tiny [\verb]proposition:implication56]]} \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:implication56!1} \hypertarget{proposition:implication56!1}{\mbox{(1)}} \ & \ $A\ \lor\ \neg A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-3}{Axiom~11}} \\ \label{proposition:implication56!2} \hypertarget{proposition:implication56!2}{\mbox{(2)}} \ & \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{Axiom~8}} \\ \label{proposition:implication56!3} \hypertarget{proposition:implication56!3}{\mbox{(3)}} \ & \ $(A\ \rightarrow\ A)\ \rightarrow\ ((B\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ A))$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A$ in \hyperlink{proposition:implication56!2}{(2)}} \\ \label{proposition:implication56!4} \hypertarget{proposition:implication56!4}{\mbox{(4)}} \ & \ $A\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implicationReflexive1}{Proposition~1}} \\ \label{proposition:implication56!5} \hypertarget{proposition:implication56!5}{\mbox{(5)}} \ & \ $(B\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication56!3}{(3)}, \hyperlink{proposition:implication56!4}{(4)}} \\ \label{proposition:implication56!6} \hypertarget{proposition:implication56!6}{\mbox{(6)}} \ & \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ \neg A)\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $\neg A$ in \hyperlink{proposition:implication56!5}{(5)}} \\ \label{proposition:implication56!7} \hypertarget{proposition:implication56!7}{\mbox{(7)}} \ & \ $\neg A\ \rightarrow\ (A\ \rightarrow\ B)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-2}{Axiom~10}} \\ \label{proposition:implication56!8} \hypertarget{proposition:implication56!8}{\mbox{(8)}} \ & \ $\neg \neg A\ \rightarrow\ (\neg A\ \rightarrow\ B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication56!7}{(7)}} \\ \label{proposition:implication56!9} \hypertarget{proposition:implication56!9}{\mbox{(9)}} \ & \ $\neg \neg A\ \rightarrow\ (\neg A\ \rightarrow\ A)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication56!8}{(8)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication56!10} \hypertarget{proposition:implication56!10}{\mbox{(10)}} \ & \ \mbox{\qquad}$\neg \neg A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication56!11} \hypertarget{proposition:implication56!11}{\mbox{(11)}} \ & \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication56!9}{(9)}, \hyperlink{proposition:implication56!10}{(10)}} \\ \label{proposition:implication56!12} \hypertarget{proposition:implication56!12}{\mbox{(12)}} \ & \ \mbox{\qquad}$(A\ \lor\ \neg A)\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication56!6}{(6)}, \hyperlink{proposition:implication56!11}{(11)}} \\ \label{proposition:implication56!13} \hypertarget{proposition:implication56!13}{\mbox{(13)}} \ & \ \mbox{\qquad}$A$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication56!12}{(12)}, \hyperlink{proposition:implication56!1}{(1)}} \\ \label{proposition:implication56!14} \hypertarget{proposition:implication56!14}{\mbox{(14)}} \ & \ $\neg \neg A\ \rightarrow\ A$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} \begin{prop} \label{proposition:implication57} \hypertarget{proposition:implication57}{} {\tt \tiny [\verb]proposition:implication57]]} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(\neg B\ \rightarrow\ \neg A)\ \rightarrow\ (A\ \rightarrow\ B)$ \end{longtable} \end{prop} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{proposition:implication57!1} \hypertarget{proposition:implication57!1}{\mbox{(1)}} \ & \ $\neg \neg A\ \rightarrow\ A$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication56}{Proposition~27}} \\ \label{proposition:implication57!2} \hypertarget{proposition:implication57!2}{\mbox{(2)}} \ & \ $\neg \neg B\ \rightarrow\ B$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication57!1}{(1)}} \\ \label{proposition:implication57!3} \hypertarget{proposition:implication57!3}{\mbox{(3)}} \ & \ $(A\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg A)$ \ & \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication51}{Proposition~23}} \\ \label{proposition:implication57!4} \hypertarget{proposition:implication57!4}{\mbox{(4)}} \ & \ $(C\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication57!3}{(3)}} \\ \label{proposition:implication57!5} \hypertarget{proposition:implication57!5}{\mbox{(5)}} \ & \ $(C\ \rightarrow\ \neg A)\ \rightarrow\ (A\ \rightarrow\ \neg C)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication57!4}{(4)}} \\ \label{proposition:implication57!6} \hypertarget{proposition:implication57!6}{\mbox{(6)}} \ & \ $(\neg B\ \rightarrow\ \neg A)\ \rightarrow\ (A\ \rightarrow\ \neg \neg B)$ \ & \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $\neg B$ in \hyperlink{proposition:implication57!5}{(5)}} \\ \ & \ Conditional Proof \ & \ \\ \label{proposition:implication57!7} \hypertarget{proposition:implication57!7}{\mbox{(7)}} \ & \ \mbox{\qquad}$\neg B\ \rightarrow\ \neg A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication57!8} \hypertarget{proposition:implication57!8}{\mbox{(8)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ \neg \neg B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication57!6}{(6)}, \hyperlink{proposition:implication57!7}{(7)}} \\ \ & \ \mbox{\qquad}Conditional Proof \ & \ \\ \label{proposition:implication57!9} \hypertarget{proposition:implication57!9}{\mbox{(9)}} \ & \ \mbox{\qquad}\mbox{\qquad}$A$ \ & \ {\tiny Hypothesis} \\ \label{proposition:implication57!10} \hypertarget{proposition:implication57!10}{\mbox{(10)}} \ & \ \mbox{\qquad}\mbox{\qquad}$\neg \neg B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication57!8}{(8)}, \hyperlink{proposition:implication57!9}{(9)}} \\ \label{proposition:implication57!11} \hypertarget{proposition:implication57!11}{\mbox{(11)}} \ & \ \mbox{\qquad}\mbox{\qquad}$B$ \ & \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication57!2}{(2)}, \hyperlink{proposition:implication57!10}{(10)}} \\ \label{proposition:implication57!12} \hypertarget{proposition:implication57!12}{\mbox{(12)}} \ & \ \mbox{\qquad}$A\ \rightarrow\ B$ \ & \ {\tiny Conclusion} \\ \label{proposition:implication57!13} \hypertarget{proposition:implication57!13}{\mbox{(13)}} \ & \ $(\neg B\ \rightarrow\ \neg A)\ \rightarrow\ (A\ \rightarrow\ B)$ \ & \ {\tiny Conclusion} \\ & & \qedhere \end{longtable} \end{proof} %% end of chapter Aussagenlogik \backmatter \begin{thebibliography}{99} \addcontentsline{toc}{chapter}{Literaturverzeichnis} \bibitem{novikov} \emph{P.S. Novikov}, Grundz{\"u}ge der mathematischen Logik, VEB Deutscher Verlag der Wissenschaften, Berlin 1973 \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, 2. Ed., Springer, Berlin 1938. Siehe auch \url{http://www.math.uwaterloo.ca/~snburris/htdocs/scav/hilbert/hilbert.html} \bibitem{mendelson} \emph{E.~Mendelson}, Introduction to Mathematical Logic, 3. ed., Wadsworth, Belmont, CA 1987 %% QEDEQ modules that use this one: \bibitem{qedeq_logic_v1} qedeq\_logic\_v1 \url{http://www.qedeq.org/0_04_04/doc/math/qedeq_logic_v1.xml} \end{thebibliography} \addcontentsline{toc}{chapter}{\indexname} \printindex \end{document}