% -*- TeX:DE -*- %%% ==================================================================== %%% @LaTeX-file qedeq_logic_v1_de.tex %%% Generated at 2007-05-10 03:41:41,734 %%% ==================================================================== %%% 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_04/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.\footnote{ Andere Formalisierungen erlauben z.~B. $\forall x_1~\alpha$ auch dann, wenn $x_1$ schon in $\alpha$ gebunden vorkommt. Auch Ausdr{\"u}cke wie $\alpha(x) \land (\forall x_1 \beta)$ sind erlaubt. Dort wird dann f{\"u}r ein einzelnes Vorkommen einer Variablen definiert ob es sich um ein freies oder gebundenes Vorkommen handelt.} \par Falls eine Formel die Gestalt $\forall x_1 ~ \alpha$ bzw. $\exists x_1 ~ \alpha$ besitzt, dann hei{\ss}t die Formel $\alpha$ der \emph{Wirkungsbereich} des Quantors $\forall$ bzw. $\exists$. \par Alle Formeln, die beim Aufbau einer Formel mittels 1. bis 4. ben{\"o}tigt werden, hei{\ss}en \emph{Teilformeln}. %% end of chapter Sprache \chapter{Axiome und Schlussregeln} \label{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}{} Mit den im Kapitel~\ref{chapter4} angegebenen Axiomen und Schlussregeln lassen sich elementare logische Gesetzm{\"a}{\ss}igkeiten ableiten. \section{Aussagenlogik} \label{chapter5_section0} \hypertarget{chapter5_section0}{} Zun{\"a}chst behandeln wir die Aussagenlogik. \par Um das Pr{\"a}dikat \emph{wahr} zu definieren, kombinieren wir einfach ein Pr{\"a}dikat und seine Negation. \begin{defn}[Wahr\index{wahr}] \label{definition:True} \hypertarget{definition:True}{} $$\top\ :\leftrightarrow \ A\ \lor \ \neg A$$ \end{defn} \par F{\"u}r das Pr{\"a}dikat \emph{falsch} negieren wir einfach \emph{wahr}. \begin{defn}[Falsch\index{falsch}] \label{definition:False} \hypertarget{definition:False}{} $$\bot\ :\leftrightarrow \ \neg \top$$ \end{defn} \par Wir haben die folgenden elementaren Aussagen. \begin{prop}[Elementare S{\"a}tze\index{S{\"a}tze!der Aussagenlogik}] \label{theorem:propositionalCalculus} \hypertarget{theorem:propositionalCalculus}{} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{0.9\linewidth}l}} \centering $\top$ & \label{theorem:propositionalCalculus:aa} \hypertarget{theorem:propositionalCalculus:aa}{} \mbox{\emph{(aa)}} \\ \centering $\neg \bot$ & \label{theorem:propositionalCalculus:ab} \hypertarget{theorem:propositionalCalculus:ab}{} \mbox{\emph{(ab)}} \\ \centering $A\ \rightarrow \ A$ & \label{theorem:propositionalCalculus:ac} \hypertarget{theorem:propositionalCalculus:ac}{} \mbox{\emph{(ac)}} \\ \centering $A\ \leftrightarrow \ A$ & \label{theorem:propositionalCalculus:ad} \hypertarget{theorem:propositionalCalculus:ad}{} \mbox{\emph{(ad)}} \\ \centering $(A\ \lor \ B)\ \leftrightarrow \ (B\ \lor \ A)$ & \label{theorem:propositionalCalculus:ae} \hypertarget{theorem:propositionalCalculus:ae}{} \mbox{\emph{(ae)}} \\ \centering $(A\ \land \ B)\ \leftrightarrow \ (B\ \land \ A)$ & \label{theorem:propositionalCalculus:af} \hypertarget{theorem:propositionalCalculus:af}{} \mbox{\emph{(af)}} \\ \centering $(A\ \land \ B)\ \rightarrow \ A$ & \label{theorem:propositionalCalculus:ag} \hypertarget{theorem:propositionalCalculus:ag}{} \mbox{\emph{(ag)}} \\ \centering $(A\ \leftrightarrow \ B)\ \leftrightarrow \ (B\ \leftrightarrow \ A)$ & \label{theorem:propositionalCalculus:ah} \hypertarget{theorem:propositionalCalculus:ah}{} \mbox{\emph{(ah)}} \\ \centering $(A\ \lor \ (B\ \lor \ C))\ \leftrightarrow \ ((A\ \lor \ B)\ \lor \ C)$ & \label{theorem:propositionalCalculus:ai} \hypertarget{theorem:propositionalCalculus:ai}{} \mbox{\emph{(ai)}} \\ \centering $(A\ \land \ (B\ \land \ C))\ \leftrightarrow \ ((A\ \land \ B)\ \land \ C)$ & \label{theorem:propositionalCalculus:aj} \hypertarget{theorem:propositionalCalculus:aj}{} \mbox{\emph{(aj)}} \\ \centering $A\ \leftrightarrow \ (A\ \lor \ A)$ & \label{theorem:propositionalCalculus:ak} \hypertarget{theorem:propositionalCalculus:ak}{} \mbox{\emph{(ak)}} \\ \centering $A\ \leftrightarrow \ (A\ \land \ A)$ & \label{theorem:propositionalCalculus:al} \hypertarget{theorem:propositionalCalculus:al}{} \mbox{\emph{(al)}} \\ \centering $A\ \leftrightarrow \ \neg \neg A$ & \label{theorem:propositionalCalculus:am} \hypertarget{theorem:propositionalCalculus:am}{} \mbox{\emph{(am)}} \\ \centering $(A\ \rightarrow \ B)\ \leftrightarrow \ (\neg B\ \rightarrow \ \neg A)$ & \label{theorem:propositionalCalculus:an} \hypertarget{theorem:propositionalCalculus:an}{} \mbox{\emph{(an)}} \\ \centering $(A\ \leftrightarrow \ B)\ \leftrightarrow \ (\neg A\ \leftrightarrow \ \neg B)$ & \label{theorem:propositionalCalculus:ao} \hypertarget{theorem:propositionalCalculus:ao}{} \mbox{\emph{(ao)}} \\ \centering $(A\ \rightarrow \ (B\ \rightarrow \ C))\ \leftrightarrow \ (B\ \rightarrow \ (A\ \rightarrow \ C))$ & \label{theorem:propositionalCalculus:ap} \hypertarget{theorem:propositionalCalculus:ap}{} \mbox{\emph{(ap)}} \\ \centering $\neg (A\ \lor \ B)\ \leftrightarrow \ (\neg A\ \land \ \neg B)$ & \label{theorem:propositionalCalculus:aq} \hypertarget{theorem:propositionalCalculus:aq}{} \mbox{\emph{(aq)}} \\ \centering $\neg (A\ \land \ B)\ \leftrightarrow \ (\neg A\ \lor \ \neg B)$ & \label{theorem:propositionalCalculus:ar} \hypertarget{theorem:propositionalCalculus:ar}{} \mbox{\emph{(ar)}} \\ \centering $(A\ \lor \ (B\ \land \ C))\ \leftrightarrow \ ((A\ \lor \ B)\ \land \ (A\ \lor \ C))$ & \label{theorem:propositionalCalculus:as} \hypertarget{theorem:propositionalCalculus:as}{} \mbox{\emph{(as)}} \\ \centering $(A\ \land \ (B\ \lor \ C))\ \leftrightarrow \ ((A\ \land \ B)\ \lor \ (A\ \land \ C))$ & \label{theorem:propositionalCalculus:at} \hypertarget{theorem:propositionalCalculus:at}{} \mbox{\emph{(at)}} \\ \centering $(A\ \land \ \top)\ \leftrightarrow \ A$ & \label{theorem:propositionalCalculus:au} \hypertarget{theorem:propositionalCalculus:au}{} \mbox{\emph{(au)}} \\ \centering $(A\ \land \ \bot)\ \leftrightarrow \ \bot$ & \label{theorem:propositionalCalculus:av} \hypertarget{theorem:propositionalCalculus:av}{} \mbox{\emph{(av)}} \\ \centering $(A\ \lor \ \top)\ \leftrightarrow \ \top$ & \label{theorem:propositionalCalculus:aw} \hypertarget{theorem:propositionalCalculus:aw}{} \mbox{\emph{(aw)}} \\ \centering $(A\ \lor \ \bot)\ \leftrightarrow \ A$ & \label{theorem:propositionalCalculus:ax} \hypertarget{theorem:propositionalCalculus:ax}{} \mbox{\emph{(ax)}} \\ \centering $(A\ \lor \ \neg A)\ \leftrightarrow \ \top$ & \label{theorem:propositionalCalculus:ay} \hypertarget{theorem:propositionalCalculus:ay}{} \mbox{\emph{(ay)}} \\ \centering $(A\ \land \ \neg A)\ \leftrightarrow \ \bot$ & \label{theorem:propositionalCalculus:az} \hypertarget{theorem:propositionalCalculus:az}{} \mbox{\emph{(az)}} \\ \centering $(\top\ \rightarrow \ A)\ \leftrightarrow \ A$ & \label{theorem:propositionalCalculus:ba} \hypertarget{theorem:propositionalCalculus:ba}{} \mbox{\emph{(ba)}} \\ \centering $(\bot\ \rightarrow \ A)\ \leftrightarrow \ \top$ & \label{theorem:propositionalCalculus:bb} \hypertarget{theorem:propositionalCalculus:bb}{} \mbox{\emph{(bb)}} \\ \centering $(A\ \rightarrow \ \bot)\ \leftrightarrow \ \neg A$ & \label{theorem:propositionalCalculus:bc} \hypertarget{theorem:propositionalCalculus:bc}{} \mbox{\emph{(bc)}} \\ \centering $(A\ \rightarrow \ \top)\ \leftrightarrow \ \top$ & \label{theorem:propositionalCalculus:bd} \hypertarget{theorem:propositionalCalculus:bd}{} \mbox{\emph{(bd)}} \\ \centering $(A\ \leftrightarrow \ \top)\ \leftrightarrow \ A$ & \label{theorem:propositionalCalculus:be} \hypertarget{theorem:propositionalCalculus:be}{} \mbox{\emph{(be)}} \\ \centering $((A\ \rightarrow \ B)\ \land \ (B\ \rightarrow \ C))\ \rightarrow \ (A\ \rightarrow \ C)$ & \label{theorem:propositionalCalculus:bf} \hypertarget{theorem:propositionalCalculus:bf}{} \mbox{\emph{(bf)}} \\ \centering $((A\ \leftrightarrow \ B)\ \land \ (B\ \leftrightarrow \ C))\ \rightarrow \ (A\ \leftrightarrow \ C)$ & \label{theorem:propositionalCalculus:bg} \hypertarget{theorem:propositionalCalculus:bg}{} \mbox{\emph{(bg)}} \\ \centering $((A\ \land \ B)\ \leftrightarrow \ (A\ \land \ C))\ \leftrightarrow \ (A\ \rightarrow \ (B\ \leftrightarrow \ C))$ & \label{theorem:propositionalCalculus:bh} \hypertarget{theorem:propositionalCalculus:bh}{} \mbox{\emph{(bh)}} \\ \centering $((A\ \land \ B)\ \leftrightarrow \ (A\ \land \ \neg B))\ \leftrightarrow \ \neg A$ & \label{theorem:propositionalCalculus:bi} \hypertarget{theorem:propositionalCalculus:bi}{} \mbox{\emph{(bi)}} \\ \centering $(A\ \leftrightarrow \ (A\ \land \ B))\ \leftrightarrow \ (A\ \rightarrow \ B)$ & \label{theorem:propositionalCalculus:bj} \hypertarget{theorem:propositionalCalculus:bj}{} \mbox{\emph{(bj)}} \end{longtable} \end{prop} \section{Pr{\"a}dikatenlogik} \label{chapter5_section1} \hypertarget{chapter5_section1}{} F{\"u}r die Pr{\"a}dikatenlogik ergeben sich die folgenden S{\"a}tze. \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}