% -*- TeX:EN -*-
%%% ====================================================================
%%% @LaTeX-file qedeq_logic_v1_1.00.00.tex
%%% Generated at 2007-01-14 21:55:27,328
%%% ====================================================================

%%% Permission is granted to copy, distribute and/or modify this document
%%% under the terms of the GNU Free Documentation License, Version 1.2
%%% or any later version published by the Free Software Foundation;
%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.

\documentclass[a4paper,german,10pt,twoside]{book}
\usepackage[english]{babel}
\usepackage{makeidx}
\usepackage{amsmath,amsthm,amssymb}
\usepackage{color}
\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,
   colorlinks,linkcolor=webgreen,pagebackref]{hyperref}
\definecolor{webgreen}{rgb}{0,.5,0}
\usepackage{graphicx}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{tabularx}

\newtheorem{thm}{Theorem}[chapter]
\newtheorem{cor}[thm]{Corollary}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{ax}{Axiom}
\newtheorem{rul}{Rule}

\theoremstyle{definition}
\newtheorem{defn}[thm]{Definition}
\newtheorem{idefn}[thm]{Initial Definition}

\theoremstyle{remark}
\newtheorem{rem}[thm]{Remark}
\newtheorem*{notation}{Notation}

\addtolength{\textheight}{7\baselineskip}
\addtolength{\topmargin}{-5\baselineskip}

\setlength{\parindent}{0pt}

\frenchspacing \sloppy

\makeindex


\title{Elements of Mathematical Logic}
\author{
Michael Meyling
}

\begin{document}

\maketitle

\setlength{\parskip}{0pt}
\tableofcontents
\setlength{\parskip}{5pt plus 2pt minus 1pt}

\chapter*{Summary\index{summary}} \label{chapter0} \hypertarget{chapter0}{}
\addcontentsline{toc}{chapter}{Summary\index{summary}}

The project \textbf{Hilbert II} deals with the formal presentation and documentation of
mathematical knowledge. For this reason \textbf{Hilbert II} provides a program suite to
accomplish that tasks. The concrete documentation of mathematical basics is also a purpose
of this project.   
For further informations about the \textbf{Hilbert II} project see under
\url{http://www.qedeq.org/index_de.html}.

\par
This document describes the logical axoims and the rules and meta rules that are used to
derive new propositions.

\par
The presentation is axiomatic and in a formal form. A  
+++
Die Darstellung erfolgt in axiomatischer Weise und in formaler Form. Dazu wird ein Kalk{\"u}l
angegeben, der es gestattet alle wahren Formeln abzuleiten. Weitere abgeleitete Regeln,
Definitionen, Abk{\"u}rzungen und Syntaxerweiterungen entsprechen im Wesentlichen der mathematischen
Praxis.

\par
Dieses Dokument liegt auch selbst in einer formalen Sprache vor, der Ursprungstext ist eine XML-Datei, deren Syntax mittels der XSD \url{http://www.qedeq.org/0_01_10/xml/qedeq.xsd} definiert wird.

\par
Dieses Dokument ist noch sehr in Arbeit und wird von Zeit zu Zeit aktualisiert. Insbesondere werden
an den durch {\glqq+++\grqq} gekennzeichneten Stellen noch Erg{\"a}nzungen oder {\"A}nderungen vorgenommen.

%% end of chapter Summary\index{summary}

\chapter*{Foreword} \label{chapter1} \hypertarget{chapter1}{}
\addcontentsline{toc}{chapter}{Foreword}

MISSING! OTHER: Das ganze Universium der Mathematik kann mit den Mitteln der Mengenlehre
entfaltet werden. Au{\ss}er den Axiomen der Mengenlehre werden dazu nur noch
logische Axiome und Regeln ben{\"o}tigt. Diese elementaren Grundlagen 
gen{\"u}gen, um die komplexesten mathematischen Strukturen zu definieren und
S{\"a}tze {\"u}ber solche Strukturen beweisen zu k{\"o}nnen. Dieses Vorgehen l{\"a}sst 
sich vollst{\"a}ndig formalisieren und auf die einfache Manipulation von 
Zeichenketten zur{\"u}ckf{\"u}hren. Die inhaltliche Deutung der Zeichenfolgen 
stellt dann das mathematische Universum dar.

\par
Dabei ist es nat{\"u}rlich mehr als nur bequem, Abk{\"u}rzungen einzuf{\"u}hren und 
weitere abgeleitete Regeln zu verwenden. Diese Bequemlichkeiten k{\"o}nnen 
aber jederzeit\footnote{Zumindest ist eine solche R{\"u}ckf{\"u}hrung theoretisch 
immer m{\"o}glich. Praktisch kann sie jedoch an der Endlichkeit der zur
Verf{\"u}gung stehenden Zeit und des nutzbaren Raums scheitern. So wird es 
sicherlich nicht m{\"o}glich sein, die nat{\"u}rliche Zahl $1.000.000.000$ in 
Mengenschreibweise anzugeben.} eliminiert und durch die grundlegenden 
Begrifflichkeiten ersetzt werden.

\par
Dieses Projekt entspringt meinem Kindheitstraum eine solche 
Formalisierung konkret vorzunehmen. Inzwischen sind die technischen 
M{\"o}glichkeiten so weit entwickelt, dass eine Realisierung m{\"o}glich 
erscheint.

\par
Dank geb{\"u}hrt den Professoren \emph{W.~Kerby} und \emph{V.~G{\"u}nther} der 
Hamburger Universit{\"a}t f{\"u}r ihre inspirierenden Vorlesungen zu den Themen 
Logik und Axiomatische Mengenlehre. Ohne diese entscheidenden Impulse 
h{\"a}tte es dieses Projekt nie gegeben.

\par
Besondere Dank geht an meine Frau \emph{Gesine~Dr{\"a}ger} und unseren Sohn
\emph{Lennart} f{\"u}r ihre Unterst{\"u}tzung und ihr Verst{\"a}ndnis f{\"u}r ihnen 
fehlende Zeit -- wobei der Verst{\"a}ndnisgrad unseres Kleinkinds vielleicht 
noch nicht so stark ausgepr{\"a}gt ist.

\par
\vspace*{1cm} Hamburg, im August 2006 \\
\hspace*{\fill} Michael Meyling

%% end of chapter Foreword

\chapter*{Introduction} \label{chapter2} \hypertarget{chapter2}{}
\addcontentsline{toc}{chapter}{Introduction}

MISSING! OTHER: An den Anfang sei ein Zitat aus einem von \emph{D. Hilbert} im September
1922 gehaltenen Vortrag\footnote{Vortrag, gehalten in der Deutschen 
Naturforscher-Gesellschaft. September 1922.} mit dem programmatischen 
Titel {\glqq Die logischen Grundlagen der Mathematik\grqq} gesetzt.

\par
\begin{quote} {
\glqq Der Grundgedanke meiner Beweistheorie ist folgender:
\par
Alles, was im bisherigen Sinne die Mathematik ausmacht, wird streng 
formalisiert, so da{\ss} die eigentliche Mathematik oder die Mathematik in
engerem Sinne zu einem Bestande an Formeln wird. Diese unterscheiden 
sich von den gew{\"o}hnlichen Formeln der Mathematik nur dadurch, da{\ss} au{\ss}er 
den gew{\"o}hnlichen Zeichen noch die logischen Zeichen, insbesondere die 
f{\"u}r {\glqq folgt\grqq} ($\rightarrow$) und f{\"u}r {\glqq nicht\grqq} 
($\bar{\quad}$) darin vorkommen. Gewisse Formeln, die als Bausteine des 
formalen Geb{\"a}udes der Mathematik dienen, werden Axiome genannt. Ein 
Beweis ist die Figur, die uns als solche anschaulich vorliegen mu{\ss}; er
besteht aus Schl{\"u}ssen verm{\"o}ge des Schlu{\ss}schemas\\
\begin{eqnarray*}
& A & \\
& A \rightarrow B& \\
\cline{2-3}
 & B &
\end{eqnarray*}
wo jedesmal die Pr{\"a}missen, d.~h. die betreffenden Formeln $A$ und 
$A \rightarrow B$ jede entweder ein Axiom ist bzw. direkt durch 
Einsetzung aus einem Axiom entsteht oder mit der Endformel $B$
eines Schlusses {\"u}bereinstimmt, der vorher im Beweise vorkommt bzw. 
durch Einsetzung aus einer solchen Endformel entsteht. Eine Formel soll
beweisbar hei{\ss}en, wenn sie entweder ein Axiom ist bzw. durch Einsetzen 
aus einem Axiom entsteht oder die Endformel eines Beweises ist.\grqq}
\end{quote}

\par
In dem 1928 erschienenen Buch \emph{Grundz{\"u}ge der theoretischen Logik} 
formulierten \emph{D.~Hilbert} und \emph{W.~Ackermann} ein 
axiomatisches System der Aussagenlogik, welches die Ausgangsbasis f{\"u}r 
das hier verwendete bildet. Durch das von \emph{P.~S.~Novikov} 1959 
angegebene Axiomensystem und Regelwerk der Pr{\"a}dikatenlogik wird das 
System verfeinert.

\par
In diesem Text wird ein Pr{\"a}dikatenkalk{\"u}l erster Stufe mit Identit{\"a}t 
und Funktoren vorgestellt, der die Ausgangsbasis f{\"u}r die Entwicklung 
der mathematischen Theorie darstellt. Es werden im Folgenden  nur die 
Ergebnisse ohne weitere Beweise und in knapper Form pr{\"a}sentiert.

%% end of chapter Introduction

\chapter{Language} \label{chapter3} \hypertarget{chapter3}{}

At the beginning there is logic. Logic is the analysis of methods of resoning. It helps to derive new propositions from already given ones. Logic is universal.

+++ TODO translation
Die Grundlagen der bei \textbf{Hilbert II} verwendeten Logik werden hier
zusammengestellt. Die folgende Kalk{\"u}lsprache und ihre Axiome basieren 
auf den Formulierungen von \emph{D.~Hilbert}, \emph{W.~Ackermann}, 
\emph{P.~Bernays} und \emph{P.~S.~Novikov}. 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.

\section{Terme\index{term} and Formulas\index{formula}} \label{chapter3_section0} \hypertarget{chapter3_section0}{}
MISSING! OTHER: TODO +++ evtl. Beschreibung eines Kalk{\"u}ls \par

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.

\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} 
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 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\footnote{Dabei wird $\forall$ als
\emph{Allquantor}\index{Allquantor}\index{Quantor!All-} und $\exists$ 
als
\emph{Existenzquantor}\index{Existenzquantor}\index{Quantor!Existenz-} 
bezeichnet}, und bis auf $x_1$ bleiben alle freien Subjektvariablen von 
$\alpha$ auch frei, und zu den gebundenen Subjektvariablen von $\alpha$ 
kommt $x_1$ hinzu. 
\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$, $\beta$ frei (bzw. gebunden) vorkommen, bleiben frei (bzw. 
gebunden).
\end{enumerate}
Alle Formeln die nur durch Anwendung von 1. und 4. 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.

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

\chapter{Axioms and Rules} \label{chapter4} \hypertarget{chapter4}{}

MISSING! OTHER: Zun{\"a}chst einmal besch{\"a}ftigen wir uns mit den Grundlagen der
Aussagenlogik und wenden uns dann der Pr{\"a}dikatenlogik zu.

\section{MISSING! OTHER: Aussagenlogische Axiome\index{Axiome!aussagenlogische}} \label{chapter4_section0} \hypertarget{chapter4_section0}{}
MISSING! OTHER: Die aussagenlogischen Operatoren
\mbox{`$\neg$'}, \mbox{`$\vee$'}, \mbox{`$\wedge$'}, 
\mbox{`$\leftrightarrow$'} und \mbox{`$\rightarrow$'}
verkn{\"u}pfen beliebige \emph{Aussagen} zu neuen Aussagen.
Dabei verstehen wir unter einer Aussage eine Gr{\"o}{\ss}e,
die nur den Wert {\glqq wahr\grqq} und {\glqq falsch\grqq}
annehmen kann.\footnote{Sp{\"a}ter werden wir f{\"u}r die Wahrheitswerte
die Symbole $\top$ und $\bot$ definieren.}

\par
Der zweistellige Operator \mbox{`$\vee$'} (Oder-Verkn{\"u}pfung) legt
f{\"u}r die Aussagen $\alpha$ und $\beta$ die neue Aussage 
$\alpha \vee \beta$ fest. Sie ist dann und nur dann wahr, wenn 
wenigstens eine der urspr{\"u}nglichen Aussagen wahr ist.

\par
Durch den einstelligen Operator \mbox{`$\neg$'} wird zu einer Aussage
$\alpha$ ihre \emph{Negation} definiert. $\neg \alpha$ ist falsch,
wenn $\alpha$ wahr ist und wahr wenn $\alpha$ falsch ist.

MISSING! OTHER: Die Implikation, die Und-Verkn{\"u}pfung und die {\"A}quivalenz werden als 
Abk{\"u}rzungen definiert.\footnote{Eigentlich werden die 
Abk{\"u}rzungssymbole $\wedge, \rightarrow, \leftrightarrow$ erst an 
dieser Stelle definiert und erweitern die Sprachsyntax. Aus 
Bequemlichkeitsgr{\"u}nden wurden diese Symbole bereits als logische 
Symbole angegeben.}


\par
The logical conjunction (`and') could be defined with de Morgan.

\begin{defn}[Implication\index{definition!of implication}]
\label{definition:implication} \hypertarget{definition:implication}{}
$$\alpha \rightarrow \beta\ :\leftrightarrow \ \neg \alpha\ \lor \ \beta$$

\end{defn}




\par
The logical conjunction (`and') could be defined with de Morgan.

\begin{defn}[Conjunction\index{definition!of conjunction}]
\label{definition:conjunction} \hypertarget{definition:conjunction}{}
$$\alpha \land \beta\ :\leftrightarrow \ \neg (\neg \alpha\ \lor \ \neg \beta)$$

\end{defn}




\par
The logical equivalence (`iff') is defined as usual.

\begin{defn}[Equivalence\index{definition!of equivalence}]
\label{definition:equivalence} \hypertarget{definition:equivalence}{}
$$\alpha \land \beta\ :\leftrightarrow \ (\alpha\ \rightarrow \ \beta)\ \land \ (\beta\ \rightarrow \ \alpha)$$

\end{defn}




\par
Now we come to the first axiom of propositional calculus. This axiom 
enables us to get rid of an unnecessary disjunction.

\begin{ax}[Disjunction Idempotence\index{axiom!of disjunction idempotence}]
\label{axiom:disjunction_idempotence} \hypertarget{axiom:disjunction_idempotence}{}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \lor \ A)\ \rightarrow \ A$
\end{longtable}

\end{ax}




\par
If a proposition is true, any alternative may be added without 
making it false.

\begin{ax}[Axiom of Weakening\index{axiom!of weakening}]
\label{axiom:disjunction_weakening} \hypertarget{axiom:disjunction_weakening}{}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow \ (A\ \lor \ B)$
\end{longtable}

\end{ax}




\par
The disjunction should be commutative.

\begin{ax}[Commutativity of the Disjunction\index{axiom!of weakening}]
\label{axiom:disjunction_commutative} \hypertarget{axiom:disjunction_commutative}{}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \lor \ B)\ \rightarrow \ (B\ \lor \ A)$
\end{longtable}

\end{ax}




\par
An disjunction could be added ad both side of an implication.

\begin{ax}[Disunctive Addition\index{axiom!of disunctive addition}]
\label{axiom:disjunction_addition} \hypertarget{axiom:disjunction_addition}{}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow \ B)\ \rightarrow \ ((C\ \lor \ A)\ \rightarrow \ (C\ \lor \ B))$
\end{longtable}

\end{ax}




\par


\begin{rul}[Modus Ponens]
\label{rule:modusPonens} \hypertarget{rule:modusPonens}{}
If $\alpha$ and $\alpha \rightarrow \beta$ are already 
Wenn $\alpha$ und $\alpha \rightarrow \beta$ wahre Formeln sind, dann ist auch $\beta$ eine wahre Formel.
\end{rul}




MISSING! OTHER: \begin{rul}[Abtrennung, Modus Ponens\index{Modus Ponens}\index{Abtrennungsregel}]
Wenn $\alpha$ und $\alpha \rightarrow \beta$ wahre Formeln sind, dann ist auch $\beta$ eine wahre Formel.
\end{rul}

\begin{rul}[Einsetzung f{\"u}r Pr{\"a}dikatenvariable]\hypertarget{predreplace}{}
Es sei $\alpha$ eine Formel, die die $n$-stellige Pr{\"a}dikatenvariable $p$ enth{\"a}lt und $\beta(x_1,
\ldots, x_n)$ eine beliebige Formel mit den freien Variablen $x_1$, \ldots, $x_n$, welche nicht in
$\alpha$ vorkommen.\footnote{In der Formel $\beta(x_1, \ldots, x_n)$ k{\"o}nnen ausser den $n$
Subjektvariablen $x_1$, \ldots, $x_n$ noch weitere Variablen frei 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 $\alpha$ ist eine im Kalk{\"u}l wahre Formel \item die freien Variablen von $\alpha$ sind
disjunkt zu den gebundenen Variablen von $\beta(x_1, \ldots, x_n)$ und die gebundenen Variablen von
$\alpha$ disjunkt zu den freien Variablen von $\beta(x_1, \ldots, x_n)$ \item Liegt das zu
ersetzende $p(t_1, \ldots, t_n)$ in $\alpha$ im Wirkungsbereich eines Quantors, so kommt die
zugeh{\"o}rige Subjektvariable in $\beta(x_1, \ldots, x_n)$ nicht vor.\footnote{D.~h. nach dem
Einsetzen werden -- au{\ss}er den in den f{\"u}r $x_1$, \ldots, $x_n$ eingesetzten Termen vorkommenden --
keine weiteren Subjektvariablen gebunden.}
\end{itemize}
\end{rul}


\section{MISSING! OTHER: Pr{\"a}dikatenlogische Axiome\index{Axiome!predikatenlogische}} \label{chapter4_section1} \hypertarget{chapter4_section1}{}
MISSING! OTHER: \begin{ax}
$$(\forall x~\phi(x)) \rightarrow \phi(y)$$
\end{ax}

\begin{ax}
$$\phi(y) \rightarrow (\exists x~\phi(x))$$
\end{ax}

\begin{rul}[Einsetzung f{\"u}r Funktionsvariablen]\hypertarget{functreplace}{}
Es sei $\alpha$ eine Formel, die die $n$-stellige Funktionsvariable $\sigma$ enth{\"a}lt und $\tau(x_1,
\ldots, x_n)$ eine beliebiger Term mit den Subjektvariablen $x_1$, \ldots, $x_n$, welche nicht in
$\alpha$ vorkommen.\footnote{In dem Term $\tau(x_1, \ldots, x_n)$ k{\"o}nnen ausser den $n$
Subjektvariablen $x_1$, \ldots, $x_n$ noch weitere Variablen 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 $\alpha$ ist eine im Kalk{\"u}l wahre Formel \item die gebundenen Variablen von $\alpha$ sind
disjunkt zu den Subjektvariablen von $\tau(x_1, \ldots, x_n)$ \item Liegt das zu ersetzende
$\sigma(t_1, \ldots, t_n)$ in $\alpha$ im Wirkungsbereich eines Quantors, so kommt die zugeh{\"o}rige
Subjektvariable in $\beta(x_1, \ldots, x_n)$ nicht vor, d.~h. nach dem Einsetzen werden -- au{\ss}er
den f{\"u}r $x_1$, \ldots, $x_n$ eingesetzten -- keine weiteren Subjektvariablen gebunden.
\end{itemize}
\end{rul}

\begin{rul}[Ersetzung f{\"u}r freie Subjektvariablen]
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}

\begin{rul}[Umbenennung f{\"u}r gebundene Subjektvariablen]
Aus jeder im Kalk{\"u}l bereits gewonnenen Formel k{\"o}nnen weitere Formeln abgeleitet werden: Jede
gebundene Subjektvariable kann in eine andere, nicht bereits frei vorkommende, Subjektvariable
umbenannt werden. Die Umbenennung braucht nur im Wirkungsbereich eines bestimmten Quantors zu
erfolgen.
\end{rul}

\begin{rul}[Generalisierung\index{Generalisierung}]
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}[Partikularisierung\index{Partikularisierung}]
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}

\par
Die Aufl{\"o}sung und der Einsatz von Abk{\"u}rzungen ist auch mit der Anwendung von Regeln verbunden. In
vielen Texten zur mathematischen Logik werden diese Regeln nicht explizit formuliert, auch dieser
Text geht darauf nicht weiter ein. In dem exakten Qedeq-Format gibt es jedoch entsprechende Regeln
zur Verwendung von Abk{\"u}rzungen.


%% end of chapter Axioms and Rules

\chapter{Derived Propositions} \label{chapter5} \hypertarget{chapter5}{}

MISSING! OTHER: +++ Fehlt noch.

\section{Elementare aussagenlogische S{\"a}tze} \label{chapter5_section0} \hypertarget{chapter5_section0}{}
MISSING! OTHER: Aus den logischen Axiomen und Regeln von Abschnitt~\hyperref{chapter4_section0} lassen sich wichtige
elementare S{\"a}tze ableiten.

\begin{defn}
Die Pr{\"a}dikatskonstanten $\top$ f{\"u}r \emph{true} oder \emph{wahr} und $\bot$ f{\"u}r \emph{false} oder
\emph{falsch} werden wie folgt definiert:
\begin{eqnarray}
\top & \Leftrightarrow & A \lor \neg A \\
\bot & \Leftrightarrow & \neg \top
\end{eqnarray}
\end{defn}

Die folgenden Formeln lassen sich beweisen.
\begin{thm}
\begin{eqnarray}
& \top & \\
& \neg \bot & \\
A & \rightarrow & A \\
A & \leftrightarrow & A \\
A \lor B & \leftrightarrow & B  \lor A \\
A \land B & \leftrightarrow & B \land A \\
(A \leftrightarrow B) & \leftrightarrow & (B \leftrightarrow A) \\
A \lor (B \lor C) & \leftrightarrow & (A \lor B) \lor C \\
A \land (B \land C) & \leftrightarrow & (A \land B) \land C \\
A & \leftrightarrow & A \lor A \\
A & \leftrightarrow & A \land A \\
A & \leftrightarrow & \neg \neg A \\
(A \rightarrow B) & \leftrightarrow & (\neg B \rightarrow \neg A) \\
(A \rightarrow (B \rightarrow C)) & \leftrightarrow & (B \rightarrow (A \rightarrow C)) \\
\neg (A \lor B) & \leftrightarrow & \neg A \land \neg B \\
\neg (A \land B) & \leftrightarrow & \neg A \lor \neg B \\
A \lor (B \land C) & \leftrightarrow & (A \lor B) \land (A \lor C) \\
A \land (B \lor C) & \leftrightarrow & (A \land B) \lor (A \land C) \\
A \land \top & \leftrightarrow & A \\
A \land \bot & \leftrightarrow & \bot \\
A \lor \top & \leftrightarrow & \top \\
A \lor \bot & \leftrightarrow & A \\
A \lor \neg A & \leftrightarrow & \top \\
A \land \neg A & \leftrightarrow & \bot \\
(\top \rightarrow A) & \leftrightarrow & A \\
(\bot \rightarrow A) & \leftrightarrow & \top \\
(A \rightarrow B) \land (B \rightarrow C) & \rightarrow & A \rightarrow C \\
(A \leftrightarrow B) \land (B \leftrightarrow C) & \rightarrow & A \leftrightarrow C \hypertarget{andequi}{} \\
((A \land B) \leftrightarrow (A \land C)) & \leftrightarrow & (A \rightarrow (B \leftrightarrow C))
\end{eqnarray}
\end{thm}

\section{Elementary Predicate Calculus} \label{chapter5_section1} \hypertarget{chapter5_section1}{}
MISSING! OTHER: Aus den logischen Axiomen und Regeln von Abschnitt~\hyperref{chapter4_section1} lassen sich auch f{\"u}r
die Pr{\"a}dikatenlogik elementare S{\"a}tze ableiten.

\begin{thm}\hypertarget{elmpred}{}
\begin{eqnarray}
\forall x \ (\phi(x) \rightarrow \psi(x)) & \rightarrow & \forall x \ (\phi(x)) \rightarrow \forall x \ (\psi(x)) \\
\forall x \ (\phi(x) \rightarrow \psi(x)) & \rightarrow & \exists x \ (\phi(x)) \rightarrow \exists x \ (\psi(x)) \\
\exists x \ (\phi(x) \land \psi(x)) & \rightarrow & \exists x \ (\phi(x)) \land \exists x \ (\psi(x)) \\
\forall x \ (\psi(x)) \lor \forall x \ (\psi(x)) & \rightarrow & \forall x \ (\phi(x) \lor \psi(x)) \\
\exists x \ (\phi(x) \lor \psi(x))) & \leftrightarrow & \exists x \ (\phi(x)) \lor \exists x \ (\psi(x)) \\
\forall x \ (\phi(x) \land \psi(x))) & \leftrightarrow & \forall x \ (\phi(x)) \land \forall x \ (\psi(x)) \hypertarget{allandpp}{}\\
\forall x \ \forall y \ (\phi(x, y)) & \leftrightarrow & \forall y \ \forall x \ (\phi(x, y)) \\
\exists x \ \exists y \ (\phi(x, y)) & \leftrightarrow & \exists y \ \exists x \ (\phi(x, y)) \\
\forall x \ (\phi(x) \rightarrow A) & \leftrightarrow & (\forall x \ (\phi(x)) \rightarrow A) \\
\forall x \ (A \rightarrow \phi(x)) & \leftrightarrow & (A \rightarrow \forall x \ (\phi(x))) \\
\forall x \ (\phi(x) \land A) & \leftrightarrow & \forall x \ (\phi(x)) \land A \\
\forall x \ (\phi(x) \lor A) & \leftrightarrow & (\forall x \ (\phi(x)) \lor A) \\
\forall x \ (\phi(x) \leftrightarrow A) & \leftrightarrow & (\forall x \ (\phi(x)) \leftrightarrow A)
\end{eqnarray}
+++ erg{\"a}nzen
\end{thm}

\section{Derived Rules} \label{chapter5_section2} \hypertarget{chapter5_section2}{}
MISSING! OTHER: Aus den logischen Grundlagen lassen sich logische S{\"a}tze und Metaregeln ableiten, die eine bequemere
Argumentation erm{\"o}glichen. Erst mit diesem Regelwerk und zus{\"a}tzlichen Definitionen und Abk{\"u}rzungen
wird die restliche Mathematik entwickelt. Dabei wird stets nur eine
\emph{konservative}\index{konservativ} Erweiterung der bisherigen Syntax vorgenommen. D.~h. in dem
erweiterten System lassen sich keine Formeln ableiten, die in der alten Syntax formuliert, aber
dort nicht ableitbar sind. Im Folgenden werden solche Erweiterungen vorgestellt.

\begin{rul}[Ersetzung durch logisch {\"a}quivalente Formeln]
Sei die Aussage $\alpha \leftrightarrow \beta$ bereits bewiesen. Wird dann aus der Formel $\delta$ eine neue
Formel $\gamma$ dadurch gewonnen, dass ein beliebiges Vorkommen von $\alpha$ durch $\beta$
ersetzt\footnote{Bei dieser Ersetzung kann es erforderlich sein, dass gebundene Variablen von
$\beta$ umbenannt werden m{\"u}ssen, damit sich wieder eine Formel ergibt.} wird und besitzt $\gamma$
zumindest die freien Variablen (+++ unklar!) von $\delta$, dann gilt $\delta \leftrightarrow \gamma$.
\end{rul}

\begin{rul}[Allgemeine Assoziativit{\"a}t]
Falls ein zweistelliger Operator das Assoziativit{\"a}tsgesetz erf{\"u}llt, so erf{\"u}llt er auch das
allgemeine Assoziativit{\"a}tsgesetz. Dem Operator kann dann eine beliebige Stellenanzahl gr{\"o}{\ss}er eins
zugeschrieben werden. So wird beispielsweise anstelle f{\"u}r $(a + b) + (c + d)$ einfach $a + b + c +
d$ geschrieben.\footnote{Der $n$-stellig Operator wird mit einer bestimmten Klammerung definiert,
jede andere Klammerreihenfolge liefert jedoch dasselbe Ergebnis.}
\end{rul}

\begin{rul}[Allgemeine Kommutativit{\"a}t]
Falls ein Operator das allgemeine Assoziativit{\"a}tsgesetz erf{\"u}llt und kommutativ ist, so sind alle
Permutationen von Parameterreihenfolgen einander gleich oder {\"a}quivalent.\footnote{Je nachdem ob es
sich um einen Termoperator oder einen Formeloperator handelt.} So gilt beispielsweise $a + b + c +
d  = c + a + d + b$.
\end{rul}

\begin{defn}[Ableitbarkeit\index{Ableitbarkeit}]
Eine Formel $\beta$ hei{\ss}t \emph{aus der Formel $\alpha$ ableitbar}, wenn sich $\beta$ mit Hilfe
aller Regeln des Pr{\"a}dikatenkalk{\"u}ls und der um $\alpha$ vermehrten Gesamtheit aller wahren Formeln
des Pr{\"a}dikatenkalk{\"u}ls herleitbar und $\alpha \rightarrow \beta$ eine Formel ist. Dabei d{\"u}rfen die beiden
Quantifizierungsregeln, die Einsetzungsregel f{\"u}r Pr{\"a}dikatenvariable und die Umbenennungsregel f{\"u}r
freie Subjektvariable nur auf solche Variablen angewendet werden, die in der Formel $\alpha$ nicht
auftreten.
\par
Schreibweise: $\alpha \vdash \beta$.
\end{defn}
Die Ableitbarkeit einer Formel $\beta$ aus der Formel $\alpha$ ist streng zu unterscheiden von der
Ableitbarkeit einer wahren Formel aus den Axiomen des Kalk{\"u}ls, denn im zweiten Fall stehen mehr
Ableitungsregeln zur Verf{\"u}gung. Falls beispielsweise die Formel $A$ als Axiom aufgenommen wird, so
ist die Formel $A \rightarrow B$ herleitbar. Hingegen l{\"a}{\ss}t sich aus $A$ nicht $B$ ableiten.

\begin{rul}[Deduktionstheorem\index{Deduktionstheorem}]
Wenn eine Formel $\beta$ aus einer Formel $\alpha$ ableitbar ist, so ist die Formel $\alpha \rightarrow
\beta$ im Pr{\"a}dikatenkalk{\"u}l herleitbar.
\end{rul}


%% end of chapter Derived Propositions

\chapter{Identy} \label{chapter6} \hypertarget{chapter6}{}

MISSING! OTHER: +++ Fehlt noch

\section{Identy Axioms} \label{chapter6_section0} \hypertarget{chapter6_section0}{}
MISSING! OTHER: \index{Identit{\"a}t}\hypertarget{gleichheit}{}
Es wird eine zweistellige Funktionskonstante festgelegt, welche in der Interpretation die Identit{\"a}t
von Subjekten ausdr{\"u}cken soll.
\begin{defn}[Gleichheit]
$$x = y \ \Leftrightarrow \ c_1^2(x, y)$$
\end{defn}

Dazu werden zwei weitere Axiome, auch
\emph{Gleichheitsaxiome}\index{Gleichheit}\index{Axiome!Gleichheits-} genannt, formuliert.
\begin{ax}[Reflexivit{\"a}t der Gleichheit]
$$x = x$$
\end{ax}

\begin{ax}[Leibnizsche Ersetzbarkeit]\index{Leibnizsche Ersetzbarkeit}\hypertarget{leibniz}{}
$$x = y  \rightarrow (\phi(x) \rightarrow \phi(y))$$
\end{ax}

\begin{thm}[Symmetrie der Gleichheit]\index{Gleichheit!Symmetrie der}
\begin{equation}
x = y \leftrightarrow y = x
\end{equation}
\end{thm}

\begin{thm}[Transitivit{\"a}t der Gleichheit]\index{Gleichheit!Transitivit{\"a}t der}
\begin{equation}
x = y ~ \land ~ y = z \rightarrow x = z
\end{equation}
\end{thm}

\begin{thm}
\begin{equation}
x = y \rightarrow (\phi(x) \leftrightarrow \phi(y))
\end{equation}
\end{thm}

\begin{thm}
\begin{equation}
x = y \rightarrow f(x) = f(y)
\end{equation}
\end{thm}

\section{++ TODO Quantifiers\index{Quantifiers!+++TODO}} \label{chapter6_section1} \hypertarget{chapter6_section1}{}
MISSING! OTHER: Bei der folgenden Definition muss die f{\"u}r $\psi(x)$ eingesetzte Formel {\glqq erkennen
lassen\grqq}, {\"u}ber welche Subjektvariable quantifiziert wird. Das ist in der Regel dar{\"u}ber zu
entscheiden, welche freie Subjektvariable als erstes in der Formel
vorkommt.\footnote{Beispielsweise ist in der folgenden Formel erkennbar, dass die zweite
Quantifikation {\"u}ber die Subjektvariable $m$ l{\"a}uft: $\forall \ n \in \mathbb{N} \ \forall \ m \in n \ m < n
$.} In der exakten Syntax des Qedeq-Formats\footnote{Siehe unter
\url{http://www.qedeq.org/0_01_05/projektbeschreibung.pdf}.} ist die Subjektvariable immer
angegeben.
\begin{defn}[Eingeschr{\"a}nkter Allquantor]\index{Allquantor!eingeschr{\"a}nkter}
$$ \forall \ \psi(x) \ (\phi(x)) \ \Leftrightarrow \ \forall \ x \ (\psi(x) \rightarrow \phi(x))$$
\end{defn}

Dazu passt die folgende Definition f{\"u}r den eingeschr{\"a}nkten Existenzquantor.\footnote{Passend, da
$\neg \forall \ \psi(x) \ (\phi(x)) \leftrightarrow \exists \ x \ \neg (\psi(x) \rightarrow \phi(x)) \leftrightarrow \exists
\ x \ (\psi(x) \land \neg\phi(x)) \leftrightarrow \exists \ \psi(x) \ (\neg\phi(x))$.}
\begin{defn}[Eingeschr{\"a}nkter Existenzquantor]\index{Existenzquantor!eingeschr{\"a}nkter}
$$ \exists \ \psi(x) \ (\phi(x)) \ \Leftrightarrow \ \exists \ x \ (\psi(x) \land \phi(x))$$
\end{defn}

F{\"u}r die Existenz genau eines Individuums mit einer bestimmten Eigenschaft wird nun ein gesonderter
Quantor eingef{\"u}hrt.
\begin{defn}[Eingeschr{\"a}nkter Existenzquantor f{\"u}r genau ein Individuum]
$$ \exists! \ \psi(x) \ (\phi(x)) \ \Leftrightarrow \ \exists \ \psi(x) \ (\phi(x) \land \forall \ \psi(y) \ (\phi(y) \rightarrow x = y))$$
\end{defn}
Durch die G{\"u}ltigkeit von $\exists! \ \psi(x) (\phi(x))$ kann daher eine Subjektkonstante definiert
werden, wenn $\phi(x)$ und $\psi(x)$ durch Ausdr{\"u}cke ersetzt werden, die ausser $x$ keine freien
Variablen, keine Pr{\"a}dikatsvariablen und keine Funktionsvariablen mehr enth{\"a}lt.


\begin{rul}[Termdefinition durch Formel]\hypertarget{termdef}{}
Falls die Formel $\exists! x \ \alpha(x)$ gilt, dann kann die Termsyntax durch $D(x, \alpha(x))$
erweitert werden. Die Formel $alpha(x)$ m{\"o}ge die Variable $y$ nicht enthalten und $\beta(y)$ sei
eine Formel, welche die Variable $x$ nicht enth{\"a}lt. Dann wird durch $\beta(D(x, \alpha(x)))$ eine
Formel definiert durch $\beta(y) \land \exists! x \ (\alpha(x) \land x = y)$. Auch in der
abk{\"u}rzenden Schreibweise gilt die Subjektvariable $x$ als gebunden, die Subjektvariable $y$ ist mit
den obigen Einschr{\"a}nkungen frei w{\"a}hlbar und wird in der Abk{\"u}rzung nicht weiter beachtet.
Ver{\"a}nderungen von $\alpha$ in eine andere Formel $\alpha'$, die eventuell erforderlich sind, damit
keine Variablenkollisionen mit Variablen aus $\beta$ entstehen, m{\"u}ssen jedoch auch in der Abk{\"u}rzung
durchgef{\"u}hrt werden. Alle Termbildungsregeln werden entsprechend erweitert. Der Ausdruck ist auch
ersetzbar durch $\exists! y \ (\beta(y) \land \alpha(y)$ oder durch $\beta(y) \land \alpha(y)$.
\end{rul}


F{\"u}r eingeschr{\"a}nkte Quantoren gelten analog zu \hyperref{elmpred} entsprechende Formeln.
\\
+++


%% end of chapter Identy

\begin{thebibliography}{99}
\bibitem{witheruss} \emph{A.N. Whitehead, B. Russell}, Principia Mathematica, Cambridge University Press, London 1910

\bibitem{bernays} \emph{P. Bernays}, Axiomatische Untersuchung des Aussagen-Kalkuls der {\glqq Principia Mathematica\grqq}, Math. Zeitschr. 25 (1926), 305-320

\bibitem{hilback} \emph{D. Hilbert, W. Ackermann}, Grundz{\"u}ge der theoretischen Logik, Springer, Berlin 1928

\bibitem{novikov} \emph{P.S. Novikov}, Grundz{\"u}ge der mathematischen Logik, VEB Deutscher Verlag der Wissenschaften, Berlin 1973

\bibitem{guenter} \emph{V.~G{\"u}nther}, Vorlesung {\glqq Mathematik und Logik\grqq}, gehalten an der Universit{\"a}t Hamburg, Wintersemester 1994/1995

\bibitem{meyling} \emph{M. Meyling}, Hilbert II, Presentation of Formal Correct Mathematical Knowledge, Basic Concept,
\url{http://www.qedeq.org/0_01_10/doc/project/qedeq_basic_concept_en.pdf}

\end{thebibliography}
\addcontentsline{toc}{chapter}{Bibliography}
\backmatter

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

\end{document}

