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

%%% 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[bookmarks,bookmarksnumbered,bookmarksopen,
   colorlinks,linkcolor=webgreen,pagebackref]{hyperref}
\definecolor{webgreen}{rgb}{0,.5,0}
\usepackage{graphicx}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{tabularx}

\newtheorem{thm}{Theorem}
\newtheorem{cor}[thm]{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{Aussagenlogik}
\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_02/doc/math/qedeq_propositional_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{chapter0} \hypertarget{chapter0}{}
\addcontentsline{toc}{chapter}{Zusammenfassung\index{Zusammenfassung}}

In diesem Text wird die Aussagenlogik in axiomatischer Weise entwickelt.
Hintergrundinformationen stehen unter \url{http://en.wikipedia.org/wiki/Propositional_calculus}
und \url{http://www.ltn.lv/~podnieks/mlog/ml1.htm#axioms}.

%% end of chapter Zusammenfassung\index{Zusammenfassung}

\chapter{Axiome und Schlussregeln} \label{chapter1} \hypertarget{chapter1}{}

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{chapter1_section0} \hypertarget{chapter1_section0}{}
Nun listen wir einfach alle Axiome ohne weitere Erl{\"a}uterungen auf.

\par


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




\par


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




\par


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




\par


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




\par


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




\par


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




\par


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




\par


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

\end{ax}




\par


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




\par


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




\par


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




\par


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




\par


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




\par


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




\section{First Propositions} \label{chapter1_section1} \hypertarget{chapter1_section1}{}
Hier nehmen wir die ersten Ableitungen vor.

\par


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

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implicationReflexive1:1} \hypertarget{proposition:implicationReflexive1:1}{} \mbox{\emph{(1)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny Add \hyperref[axiom:THEN-1]{Axiom~1}} \\ 
\label{proposition:implicationReflexive1:2} \hypertarget{proposition:implicationReflexive1:2}{} \mbox{\emph{(2)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny Add \hyperref[axiom:THEN-2]{Axiom~2}} \\ 
\label{proposition:implicationReflexive1:3} \hypertarget{proposition:implicationReflexive1:3}{} \mbox{\emph{(3)}}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny Add \hyperref[axiom:OR-2]{Axiom~7}} \\ 
\label{proposition:implicationReflexive1:4} \hypertarget{proposition:implicationReflexive1:4}{} \mbox{\emph{(4)}}  \ &  \ $A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ A)$ \ &  \ {\tiny SubstPred $B$ by $B\ \lor\ A$ in \hyperref[proposition:implicationReflexive1/1]{(1)}} \\ 
\label{proposition:implicationReflexive1:5} \hypertarget{proposition:implicationReflexive1:5}{} \mbox{\emph{(5)}}  \ &  \ $(A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ C))\ \rightarrow\ ((A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny SubstPred $B$ by $B\ \lor\ A$ in \hyperref[proposition:implicationReflexive1/2]{(2)}} \\ 
\label{proposition:implicationReflexive1:6} \hypertarget{proposition:implicationReflexive1:6}{} \mbox{\emph{(6)}}  \ &  \ $(A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ A))\ \rightarrow\ ((A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ A))$ \ &  \ {\tiny SubstPred $C$ by $A$ in \hyperref[proposition:implicationReflexive1/5]{(5)}} \\ 
\label{proposition:implicationReflexive1:7} \hypertarget{proposition:implicationReflexive1:7}{} \mbox{\emph{(7)}}  \ &  \ $(A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ A)$ \ &  \ {\tiny MP \hyperref[proposition:implicationReflexive1/6]{(6)}, \hyperref[proposition:implicationReflexive1/4]{(4)}} \\ 
\label{proposition:implicationReflexive1:8} \hypertarget{proposition:implicationReflexive1:8}{} \mbox{\emph{(8)}}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny MP \hyperref[proposition:implicationReflexive1/7]{(7)}, \hyperref[proposition:implicationReflexive1/3]{(3)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}




\par


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

\end{prop}





%% end of chapter Axiome und Schlussregeln

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

\end{document}

