% -*- TeX:DE -*-
%%% ====================================================================
%%% @LaTeX-file  qedeq_logic_v1_de.tex
%%% Generated at 2007-02-25 22:46:13,250
%%% ====================================================================

%%% 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}[chapter]
\newtheorem{cor}[thm]{Korollar}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{ax}{Axiom}
\newtheorem{rul}{Regel}

\theoremstyle{definition}
\newtheorem{defn}[thm]{Definition}
\newtheorem{idefn}[thm]{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{Anfangsgr{\"u}nde der mathematischen Logik}
\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://qedeq.org/0_03_02/doc/math/qedeq_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 Addresse \url{mailto:mime@qedeq.org}

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

Das Projekt \textbf{Hilbert II} besch{\"a}ftigt sich mit der formalen Darstellung und Dokumentation 
von mathematischem Wissen. Dazu stellt \textbf{Hilbert II} eine Programmsuite zur L{\"o}sung 
der damit zusammenh{\"a}ngenden Aufgaben bereit. Auch die konkrete Dokumentation mathematischen Grundlagenwissens 
mit diesen Hilfsmitteln geh{\"o}rt zum Ziel dieses Projekts. 
F{\"u}r weitere Information {\"u}ber das Projekt \textbf{Hilbert II} siehe auch unter
\url{http://www.qedeq.org/index_de.html}.

\par
Dieses Dokument beschreibt die logischen Axiome, Schluss- und Metaregeln mit denen logische
Schl{\"u}sse durchgef{\"u}hrt werden k{\"o}nnen.

\par
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/current/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 Zusammenfassung\index{Zusammenfassung}

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

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, january 2007 \\
\hspace*{\fill} Michael Meyling

%% end of chapter Vorwort

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

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 Einleitung

\chapter{Sprache} \label{chapter3} \hypertarget{chapter3}{}

Am Anfang steht die Logik. Sie stellt das R{\"u}stzeug zur Argumentation bereit. Sie hilft beim Gewinnen von neuen Aussagen aus bereits vorhandenen. Sie ist universell anwendbar. 

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} und Formeln\index{Formel}} \label{chapter3_section0} \hypertarget{chapter3_section0}{}
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}\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.

\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{chapter4} \hypertarget{chapter4}{}

Nun geben wir das Axiomensystem f{\"u}r die Pr{\"a}dikatenlogik an und formulieren die Regeln um daraus neue Formeln zu gewinnen.

\section{Axiome\index{Axiome!der Pr{\"a}dikatenlogik}\index{Pr{\"a}dikatenlogik!Axiome der}} \label{chapter4_section0} \hypertarget{chapter4_section0}{}
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.}

F{\"u}r die Pr{\"a}dikatenlogik wird der Umgang mit Quantoren hinzugef{\"u}gt.

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.
            
\par
Die Implikation, die Und-Verkn{\"u}pfung und die logische {\"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
Die logische Implikation kann wie folgt definiert werden.

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

\end{defn}




\par
Definition der Und-Verkn{\"u}pfung mittels De-Morgan.

\begin{defn}[Und-Verkn{\"u}pfung\index{Definition!der Und-Verkn{\"u}pfung}]
\label{definition:conjunction} \hypertarget{definition:conjunction}{}
$$\alpha \land \beta\ :\leftrightarrow \ \neg (\neg \alpha\ \lor \ \neg \beta)$$

\end{defn}




\par
Die logische {\"A}quivalenz ({\glqq genau dann, wenn\grqq}) wird wie 
{\"u}blich definiert.

\begin{defn}[{\"A}quivalenz\index{Definition!der {\"A}quivalenz}]
\label{definition:equivalence} \hypertarget{definition:equivalence}{}
$$\alpha \land \beta\ :\leftrightarrow \ (\alpha\ \rightarrow \ \beta)\ \land \ (\beta\ \rightarrow \ \alpha)$$

\end{defn}




\par
Nun folgt unser erstes Axiom der Aussagenlogik. Mithilfe dieses 
Axioms k{\"o}nnen {\"u}berfl{\"u}ssige Oder-Verkn{\"u}pfungen entfernt werden.

\begin{ax}[Oder-K{\"u}rzung\index{Axiom!der Oder-K{\"u}rzung}]
\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
Wenn eine Aussage wahr ist, dann kann eine beliebige weitere Aussage mittels Oder-Verkn{\"u}pfung hinzugef{\"u}gt werden, 
ohne dass die Aussage falsch wird.

\begin{ax}[Oder-Verd{\"u}nnung\index{Axiom!der Oder-Verd{\"u}nnung}]
\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
Die Oder-Verkn{\"u}pfung soll kommutativ sein.

\begin{ax}[Oder-Vertauschung\index{Axiom!der Oder-Vertauschung}]
\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
Eine Oder-Verkn{\"u}pfung kann auf beiden Seiten einer Implikation 
hinzugef{\"u}gt werden.

\begin{ax}[Oder-Vorsehung\index{Axiom!der Oder-Vorsehung}]
\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
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}{}
\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}{}
\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{chapter4_section1} \hypertarget{chapter4_section1}{}
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.

\par


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




\par


\begin{rul}[Ersetzung f{\"u}r freie Subjektvariable]
\label{rule:replaceFree} \hypertarget{rule:replaceFree}{}
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 Axiom~\ref{axiom:universalInstantiation} \\
  $\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.


\par


\begin{rul}[Umbenennung f{\"u}r gebundene Subjektvariable]
\label{rule:renameBound} \hypertarget{rule:renameBound}{}
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}




\par


\begin{rul}[Einsetzung f{\"u}r Pr{\"a}dikatenvariable]
\label{rule:replacePred} \hypertarget{rule:replacePred}{}
Es sei $\alpha$ eine wahre Formel, die die $n$-stellige Pr{\"a}dikatenvariable $p$ enth{\"a}lt,
$x_1$, \ldots, $x_n$ seien Subjektvariable und 
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 der 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 Axiom~\ref{axiom:existencialGeneralization} \\
  $ (\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~\ref{rule:replacePred} k{\"o}nnen wir auch Funktionsvariablen ersetzen.

\begin{rul}[Einsetzung f{\"u}r Funktionsvariable]
\label{rule:replaceFunct} \hypertarget{rule:replaceFunct}{}
Es sei $\alpha$ eine bereits bewiesene Formel, die die $n$-stellige Funktionsvariable $\sigma$ enth{\"a}lt, $x_1$, \ldots, $x_n$ seien 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 $\beta(x_1, \ldots, x_n)$

\item
das Ergebnis der Substitution ist eine wohlgeformte Formel

\end{itemize}
\end{rul}




\par


\begin{rul}[Hintere Generalisierung\index{Generalisierung!hintere}]
\label{rule:universalIntroduction} \hypertarget{rule:universalIntroduction}{}
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}




\par


\begin{rul}[Vordere Partikularisierung\index{Partikularisierung!vordere}]
\label{rule:existentialIntroduction} \hypertarget{rule:existentialIntroduction}{}
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}




Die Aufl{\"o}sung und der Einsatz von Abk{\"u}rzungen und Konstanten 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.



%% end of chapter Axiome und Schlussregeln

\chapter{Abgeleitete S{\"a}tze} \label{chapter5} \hypertarget{chapter5}{}

+++ Fehlt noch.

\section{Aussagenlogik} \label{chapter5_section0} \hypertarget{chapter5_section0}{}
Aus den logischen Axiomen und Regeln von Kapitel~\ref{chapter4} 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{Pr{\"a}dikatenlogik} \label{chapter5_section1} \hypertarget{chapter5_section1}{}
Aus den logischen Axiomen und Regeln von Kapitel~\ref{chapter4} 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{Abgeleitete Regeln} \label{chapter5_section2} \hypertarget{chapter5_section2}{}
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 Abgeleitete S{\"a}tze

\chapter{Identit{\"a}t} \label{chapter6} \hypertarget{chapter6}{}

+++ Fehlt noch

\section{Axiome der Identit{\"a}t} \label{chapter6_section0} \hypertarget{chapter6_section0}{}
\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{Eingeschr{\"a}nkte Quantoren\index{Quantor!eingeschr{\"a}nkter}} \label{chapter6_section1} \hypertarget{chapter6_section1}{}
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 Identit{\"a}t

\begin{thebibliography}{99}
\addcontentsline{toc}{chapter}{Literaturverzeichnis}
\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, 2. Ed., Springer, Berlin 1938.
Siehe auch \url{http://www.math.uwaterloo.ca/~snburris/htdocs/scav/hilbert/hilbert.html}

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

\bibitem{mendelson} \emph{E. Mendeslson}, Introduction to Mathematical Logic, 3. ed., Wadsworth, Belmont, CA 1987

\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, Darstellung von formal korrektem mathematischen Wissen, Grobkonzept, \url{http://www.qedeq.org/current/doc/project/qedeq_basic_concept_de.pdf}



%% QEDEQ modules that use this one:
\bibitem{qedeq_set_theory_v1} qedeq\_set\_theory\_v1


\end{thebibliography}
\backmatter

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

\end{document}

