% !TEX TS-program = latexmk % !TEX encoding =latin 1 \documentclass{scrreprt} % Mathepakete von mir eingefügt \usepackage{amsmath,amssymb,amsfonts,amsthm,multicol,longtable,tabularx,fancybox,fancyhdr,lscape} \usepackage{stmaryrd} \usepackage[latin 1]{inputenc} \usepackage[]{fontenc} \usepackage{lmodern} \usepackage[ngerman]{babel} % hyperref sollte als letztes aller Paktete geladen werden \usepackage{hyperref} \pagestyle{headings} %Nummerierung geht bis Tiefe 6 \setcounter{secnumdepth}{6} %Nummerierung subsubsection \setcounter{tocdepth}{6} % subsubsection ins Inhaltsverzeichnis % Ränder setzen \usepackage[left=2cm,right=1cm,top=1.5cm,bottom=1cm,includeheadfoot]{geometry} \title{Peano und Goldbachsche Vermutung} \author{cx} \date{ \today} \begin{document} \maketitle \tableofcontents \chapter{Vorwort} 1) \\ In diesem Artikel soll gezeigt werden:\\ Wenn die Goldbachsche Vermutung (abgekürzt GC) unabhängig vom\\ Peanoschen Axiomensystem PA wäre, dann kann man zeigen, daß GC\\ im Standardmodell $\mathfrak{N}$ von PA wahr ist.\\ Auf math.stackexhange.com $\href{https://math.stackexchange.com/questions/1055381/goldbachs-conjecture-cant-be-proved-to-be-undecidable/1082723#1082723 }{hier klicken}$ \begin{verbatim} https://math.stackexchange.com/questions/1055381/ goldbachs-conjecture-cant-be-proved-to-be-undecidable/1082723#1082723 \end{verbatim} wird ein Beweis geliefert, der Argumente aus der Modelltheorie verwendet. \\ Da diese Argumente sich nicht auf explizit benannte Sätze der Modelltheorie beziehen, \\ und sich somit dem Autor dieses Artikels nicht erschliessen, wird ein Beweis geliefert, \\ der ohne Sätze aus der Modelltheorie auskommt. \\ \\ 2) Dieser Artikel verwendet folgende Quellen:\\ Die Formalisierung des Peanoschen Axiomensystems: \\ "Komplexitätstheorie" von W.J. Paul Teubner Studienbücher Informatik. \\ \\ Die Beweisidee (ohne Sätze der Modelltheorie zu verwenden) : \\ "Mathematische Logik" von Martin Ziegler Birkhäuser Verlag \\ \\ Die Grundlagen der Prädikatenlogik: \\ Einführung in die mathematische Logik" von Ebbinhaus, Flum, Thomas \\ Spektrum Akademischer Verlag.\\ \\ 3) Voraussetzungen, um den Artikel verstehen zu können: \\ Grundlagen der Prädikatenlogik. \\ \\ 4) Der Beweis beruht hauptsächlich auf dem Hauptsatz und den dann nachfolgenden Seiten.\\ Die meisten Sustitutionslemmata sind intuitiv klar. Einige werden für den Beweis gar nicht bernötigt. \\ \\ \chapter{Prädikatenlogik 1. Stufe (kurze Zusammenfassung)} \section{Definitionen} V :=$ \{v_0, v_1, ...\}$ : Variablenmenge der Sprache erster Stufe \\ $\Sigma$ : Menge von Formeln \\ A : Trägermenge \\ $\mathfrak{A}$ : S-Struktur \\ h: V $\rightarrow$ A eine Belegung in der Struktur $\mathfrak{A}$ \\ $\mathfrak{I} = (\mathfrak{A},h)$ : Interpretation. \\ \\ Dann wird definiert: \\ Eine S-Struktur $\mathfrak{A}$ ist ein Paar $\mathfrak{A}$ = (A,a), für die gilt:\\ A ist eine nichtleere Menge , die sogenannte Trägermenge von $\mathfrak{A}$, \\ a ist eine auf S definierte Abbildung. Für sie gilt:\\ Für jedes n-stellige Relationssymbol R aus S ist a(R) eine n-stellige Relation über A. \\ Für jedes n-stellige Funktionssymbol f aus S ist a(R) eine n-stellige Funktion über A. \\ Für jedes Kontante c aus S ist a(c) ein Element aus A. \\ Statt a(R), a(f), a(c) schreibt man auch: $R^\mathfrak{A}$ \subsection{Definitionen Ebbinghaus} 1) a) \\ $(\mathfrak{A},h)$ ist Modell von $\varphi \; ((\mathfrak{A},h) \models \varphi) :\iff (\mathfrak{A},h)$ erfüllt $\varphi$\\ $(\mathfrak{A},h)$ ist Modell von $\Sigma \; ((\mathfrak{A},h) \models \Sigma) :\iff$ für alle $\sigma \in \Sigma$ gilt: $(\mathfrak{A},h) \models \sigma$\\ b) Falls in $\varphi$ keine freien Variablen vorkommen, wird auf die Erwähnung einer Belegung verzichtet und man sagt dann, dass $\mathfrak{A}$ ein Modell von $\varphi$ ist und schreibt:\\ $\mathfrak{A} \models \varphi$ \\ Für eine Menge $\Sigma$ von Formeln (die alle keine freien Variablen haben), schreibt man dann:\\ $\mathfrak{A} \models \Sigma$ \\ \\ 2) \\ $\mathfrak{A} \models \varphi [h(v_0), ... , h(v_{n-1})] :\iff$ frei($\varphi) \subset \{v_0, ... , v_{n-1}\}$ und $(\mathfrak{A},h) \models \varphi $ \\ \\ 3) \\ $\Sigma \models \varphi$ (aus $\Sigma$ folgt $\varphi) :\iff$ \\ Jedes Modell von $\Sigma$ ist auch Modell von $\varphi$ \\ \\ 4) Simultane Substitution (intuitiv, informal) \\ Wenn man in der Formel $\phi$ die freien Variablen $x_0, ... , x_r$ durch die \\ Terme $t_0, ..., t_r$ ersetzt, wird das wie folgt notiert: $\varphi \overset{t_0} {x_0} ... \overset{t_r} {x_r} $ \\ Wenn eine Variablen nicht frei vorkommt, wird sie nicht ersetzt. \\ Bei der Substitution darf keine Variablenkonfusion entstehen: \\ (Ebbinghaus läßt das zwar zu, hier wird es aber nicht gebraucht. Deswegen wird dieser Fall hier nicht zugelassen).\\ $\varphi: \quad \neg (x=0) \rightarrow \exists y(y*x=1)$ \\ Wenn man jetzt x durch den Term 1-y ersetzen würde, würde folgende Formel entstehen:\\ $\neg (1-y=0) \rightarrow \exists y((1-y)*x=1)$ \\ Dadurch wird das y in 1-y durch $\exists$ in $\varphi$ gebunden.\\ Deshalb ist diese Substitution nicht erlaubt. \subsubsection{Simultane Substitution formal definiert} Die folgenden Buchstaben werden wie folgt verwendet:\\ $x_0, x_1, ...$ : Variablen \\ $t, t_0, t_1, ... $ : Terme \\ $s, s_0, s_1, ... $ : Terme \\ c : Konstante \\ f : Funktionssymbol \\ R : Relationssymbol \\ $\varphi, \psi$ : Formeln \\ Die eckigen Klammern [ und ] dienen der besseren Lesbarkeit. \\ \\ Durch die Angabe folgender Regeln wird die Substitution induktiv definiert. \\ 1) \\ $x_{x_0 ... x_r}^{t_0 ... t_r}$ := x , falls $x \not \in \{x_0 ... x_r\}$ \\ \\ $x_{x_0 ... x_r}^{t_0 ... t_r}$ := $t_i$ , falls $x=x_i$ \\ \\ 2)\\ $x_{x_0, ... , x_r}^{t_0, ... , t_r}$ := c \\ \\ 3)\\ $[f s_0 ... s_r]_{x_0, ... , x_r}^{t_0, ... , t_r}$ :=$ f{s_0}_{x_0, ... , x_r}^{t_0, ... , t_r} ... {s_r}_{x_0, ... , x_r}^{t_0, ... , t_r}$ \\ \\ 4)\\ $[s=t]_{x_0, ... , x_r}^{t_0, ... , t_r}$ :=$ s_{x_0, ... , x_r}^{t_0, ... , t_r} = t_{x_0, ... , x_r}^{t_0, ... , t_r}$ \\ \\ 5)\\ $[R s_1 ... s_n]_{x_0, ... , x_r}^{t_0, ... , t_r}$ :=$ R{s_1}_{x_0, ... , x_r}^{t_0, ... , t_r} ... {s_n}_{x_0, ... , x_r}^{t_0, ... , t_r}$ \\ \\ 6)\\ $[\neg \varphi]_{x_0, ... , x_r}^{t_0, ... , t_r}$ := $\neg [\varphi_{x_0, ... , x_r}^{t_0, ... , t_r}]$ \\ \\ 7)\\ $[\varphi \land \psi]_{x_0, ... , x_r}^{t_0, ... , t_r}$ :=$ \varphi_{x_0, ... , x_r}^{t_0, ... , t_r} \land \psi_{x_0, ... , x_r}^{t_0, ... , t_r}$ \\ \\ Die restlichen Junktoren: analog \\ \\ 8) \\ Voraussetzungen:\\ $\{x_{f_1}, ..., x_{f_k}\}$ sind die freien Variablen von $\exists x \varphi$, die in $\{x_0, ... , x_r\}$ vorkommen. Außerdem darf die Variable x nicht in den Termen $t_{f_1}, ..., t_{f_k}$ auftreten. Dann wird definiert:\\ $[\exists x \varphi]_{x_0, ... , x_r}^{t_0, ... , t_r}$ := $\exists x [\varphi_{x_{f_1}, ... , x_{f_k}}^{t_{f_1}, ... , t_{f_k}}]$ \\ Falls es keine freien Variablen in $\exists x \varphi$ gibt, gilt: $[\exists x \varphi]_{x_0, ... , x_r}^{t_0, ... , t_r}$ := $\exists x \varphi$ \\ Analoges gilt für den Allquantor. \\ 9) Weitere Definitionen zur Substitution:\\ a)\\ Eine Substitutionsfolge (kurz: Folge) ist entweder eine bijektive Abbildung: \\ L: $\{0, ...,n\} \rightarrow \{x_0, ..., x_n\}$ (mit n$\ge$ 0) \\und wird durch L=$(x_0, ..., x_n)$ abgekürzt oder eine Abbildung \\ L: $\{\} \rightarrow \{\}$\\ und wird durch L=() abgekürzt. Diese wird auch mit $\epsilon$ bezeichnet. \\ Die Klammern einer Folge kann man auch weglassen und sagt dann dazu Wort.\\ \\ Bemerkungen:\\ Aus der Definition einer Substitutionsfolge folgt, dass sie aus lauter voneinander \\ verschiedenen Folgengliedern besteht und dass für das Bild Bild(L) der Abbildung L gilt: \\ B($(x_0, ..., x_n)$) = $\{x_0, ..., x_n\}$ \\ und für die Anzahl der Elemente der Definitionsmenge D(L) bzw. der Bildmenge Bild(L) gilt:\\ $\vert$ D(L) $\vert$ = $\vert$ Bild(L) $\vert$ \\ \\ b)\\ Die Umkehrabbildung $L^{-1}$ gibt zu jedem Element der Substitutionsfolge den Index an, also:\\ $L^{-1}(x_i)=i$\\ \\ c)\\ s ist eine Abbildung, die jeder Variable der Variablenmenge V einen Term zuordnet.\\ Sie wird Substitutionsbelegung genannt.\\ s induziert die Liste s($x_1, ..., x_n$) := (s($x_1$ , ..., s($x_n$) ) und \\ s induziert die Menge s($\{x_1, ..., x_n\}$) := $\{s(x_1) , ..., s(x_n) \} $ \\ Dann kann man eine Substitution auch wie folgt definieren:\\ Für alle Substututionsfolgen L und alle Substitutionsbelegungen s und alle Formeln $\varphi$ wird eine Substitution wie folgt bezeichnet:\\ Falls L$\neq \epsilon$:$\quad$ $[\varphi]_L^{s(L)}$\\ Falls L=$\epsilon$:$\quad$ $[\varphi]_L^{s(L)}=\varphi$ \\ \\ d) Konkatenation von Substitutionsfolgen \\ Es sei L=($l_1, ... ,l_n$) und F=($f_1, ... ,f_m$). Dann ist: \\ L+F := ($l_1, ... ,l_n, f_1, ... ,f_m$) \\ die Konkatenation (Verkettung) der Substitutionsfolgen L und F. \\ \\ e) Definition einer speziellen Folge $<...>$\\ Mit der folgenden Definition kann man 8) auch anders formalisieren:\\ M $\neq \emptyset$ sei Teilmenge der Bildmenge einer Liste L (Substitutionsfolge), also: M $\subset$ Bild(L) \\ Dann induziert L die Liste $\{m_0, ... , m_k\}$ von M mit:\\ $L^{-1}(m_0) < L^{-1}(m_1) < ... < L^{-1}(m_k)$ \\ wobei $\{m_0, ... , m_k\}$ abgekürzt wird durch $$ bzw. nur durch $$ wenn L im Kontext klar ist.\\ Wenn M=$\emptyset$, dann $$:=$\epsilon$ (leere Folge)\\ Anschaulich bedeutet dies: \\ Die Menge M wird in der Reihenfolge des Auftretens ihrer Elemente in L (vom Anfang vonL beginnend) angeordnet. Die Ordnung von L wird also auf M übertragen.\\ \\ Beispiel:\\ L=(3,2,7,1,8) und M=$\{1,7,3\}$ M induziert die Liste: \\ M' = (3,7,1) = $<$1,7,3,L$>$ \\ \\ Damit folgt dann:\\ $[\exists x \varphi]_L^{s(L)}= \exists x [\varphi]_{}^{s()}$ \\ \\ Bemerkung:\\ Anschaulich wird die Menge B(L) $\cap$ frei(T) durch L durchnummeriert und gibt dann die \\ Substitutionsfolge: $<$B(L) $\cap$ frei(T)$>$ \\ \newpage \subsection{Definitionen Schwabhäuser} 1) \\ $\mathfrak{A} \; \vert \models \varphi$ ($\varphi$ ist in $\mathfrak{A}$ gültig) :$\iff$ für alle Belegungen h gilt: $(\mathfrak{A},h) \models \varphi$\\ \\ 2) \\ Der Begriff \grqq Modell \grqq wird bei Schwabhäuser anders definiert als bei Ebbinghaus.\\ Hier wird deshalb die Bezeichnung S-Modell für das Schwabhäusersche Modell verwendet.\\ Statt $\models$ wird die Bezeichnung $\vert \models$ benutzt.\\ $\mathfrak{A} \; \vert \models \Sigma :\iff$ für alle $\sigma \in \Sigma$ gilt: $\; \mathfrak{A} \; \vert \models \sigma$\\ \\ 3) Der Folgerungsbegriff von Schwabhäuser unterscheidet sich ebenfalls von Ebbinghaus. \\ Deswegen wird der Folgerungsbegriff von Schwabhäuser hier mit $\vert \models$ bezeichnet.\\ Bezüglich Formeln ohne freie Variablen sind die unterschiedlichen Folgerungsbegriffe aber äquivalent (siehe unten).\\ \\ $\Sigma \; \vert \models \varphi$ (aus $\Sigma$ folgt $\varphi) :\iff$ \\ $\varphi$ ist gültig in jedem S-Modell von $\Sigma$. \\ \\ 4) Definition Beweisbarkeit \\ $\Sigma \vdash_L \varphi$ (kurz: $\Sigma \vdash \varphi$) : $\iff$ \\ Es gibt eine endliche Folge ("$\Sigma$-Beweisfolge")$\varphi_1$ , ..., $\varphi_k$ von Formeln (von L) so daß $\varphi_k = \varphi$ und für jedes i mit 1 $\le$ i $\le$i k gilt: $\varphi_i$ ist ein logisches Axiom oder ein Elment von $\Sigma$ oder $\varphi_i$ entsteht aus früheren Gliedern der Folge durch Anwendung einer Schlußregel.\\ Falls $\Sigma = \emptyset$, schreibt man: $\vdash_L \varphi$ oder kurz $\vdash \varphi$ ) \section{Unterschiede} Ebbinghaus verwendet für die Beweisbarkeit den Sequenzkalkül. Dieser wird in dieser Ausarbeitung nicht verwendet, sondern der Beweisbarkeitsbegriff von Schwabhäuser.\\ Außerdem haben Ebbinghaus und Schwabhäuser auch jeweils andere, nicht äquivalente Definitionen für den Modell- und den Folgerungsbegriffe. Das hat verschiedene Konsequenzen: \\ \\ Schwabhäuser : \\ Für jede Formel $\varphi$, für jede Variable x und jede Formelmenge $\Sigma$ gilt:\\ $\Sigma \models \varphi \Longleftrightarrow \Sigma \models \forall x \varphi $ \\ \\ Ebbinghaus:\\ $\Sigma \models \varphi \not \Longleftrightarrow \Sigma \models \forall x \varphi $ \\ \\ Es gilt aber: \newpage \subsection{Zusammenhang Ebbinghaus - Schwabhäuser} 1) $\Sigma \models \varphi \Longrightarrow \Sigma \; \vert \models \varphi $ \\ \\ 2) Für alle Fomeln $\varphi$ ohne freie Variablen gilt:\\ $\mathfrak{A} \models \varphi \Longleftrightarrow \mathfrak{A} \; \vert \models \varphi $ \\ \begin{proof} ... \\ 1) \\ Es seien alle $\sigma$ aus $\Sigma$ in einer beliebigen Struktur $\mathfrak{A}$ gültig. (*) \\ Zeige: $\varphi$ ist in $\mathfrak{A}$ gültig. \\ genügt: $(\mathfrak{A},h) \models \varphi $ für alle h.\\ Nehme ein beliebiges aber festes h'\\ Für dieses h' gilt nach (*): Für alle alle $\sigma$ aus $\Sigma$ ist $(\mathfrak{A},h^{'}) \models \sigma$\\ Mit der Voraussetzung $\Sigma \models \varphi$ folgt dann: $(\mathfrak{A},h^{'}) \models \varphi $ \\ \\ 2) \\ a) \\ $\mathfrak{A} \models \varphi \Longleftrightarrow \;$ in $\varphi$ gibt es keine freien Variablen und für alle Belegungen h gilt: ($\mathfrak{A},h) \models \varphi \;$ \\ Dies gilt aber nach dem Koinzidenzlemma.\\ b) \\ $\mathfrak{A} \; \vert \models \varphi \Longleftrightarrow \quad $ Für alle Belegungen h gilt: ($\mathfrak{A},h) \models \varphi \;$ \end{proof} \subsection{Beispiel} $\Sigma=\emptyset$, \\ $\mathfrak{N}$ = Standardstruktur der natürlichen Zahlen, \\ $G^{\mathfrak{N}}$x :gdw x ist gerade\\ Dann gilt:\\ $\models$ Gx $\not \Longleftrightarrow \models \forall x \; Gx$ \\ \\ Beweis:\\ Wähle z.B: h(x)=10\\ Dann gilt:\\ ($\mathfrak{N},h) \models Gx \Longleftrightarrow G^{\mathfrak{N}} h(x) \Longleftrightarrow$ 10 gerade $\Longleftrightarrow$ wahr\\ aber:\\ ($\mathfrak{N},h) \models \forall x \; Gx \Longleftrightarrow (\mathfrak{N},h_x^{a})$Gx für alle a $\in \mathbb{N} \Longleftrightarrow$ \\ $G^{\mathfrak{N}}a \Longleftrightarrow$ alle a $\in \mathbb{N}$ sind gerade $\Longleftrightarrow$ falsch\\ \\ Falls keine freien Variablen in Formeln vorkommen, haben die unterschiedliche Definitionen (Schwabhäuser / Ebbinghaus) keine Auswirkungen. Siehe folgendes Lemma: \newpage \subsection{Lemma} Wenn alle Formeln aus $\Sigma$ und die Formel $\varphi$ keine freien Variablen enthalten, dann gilt:\\ $\Sigma \models \varphi \Longleftrightarrow \Sigma \; \vert \models \varphi$ \begin{proof} ... \\ "$\Rightarrow$" \\ Es seien alle $\sigma$ aus $\Sigma$ in einer beliebigen Struktur $\mathfrak{A}$ gültig. (*) \\ Zeige: $\varphi$ ist in $\mathfrak{A}$ gültig. \\ genügt: $(\mathfrak{A},h) \models \varphi $ für alle h.\\ Nehme ein beliebiges aber festes h*\\ Für dieses h* gilt nach (*): Für alle alle $\sigma$ aus $\Sigma$ ist $(\mathfrak{A},h^{*}) \models \sigma$\\ Mit der Voraussetzung $\Sigma \models \varphi$ folgt dann: $(\mathfrak{A},h^{*}) \models \varphi $ \\ \\ "$\Leftarrow$" \\ Es sei für alle alle $\sigma$ aus $\Sigma$ in einer beliebigen Struktur für ein beliebiges aber festes h : \\ $(\mathfrak{A},h) \models \sigma$ \\ Da alle $\sigma$ aus $\Sigma$ keine freien Variablen enthalten, sind alle $\sigma$ aus $\Sigma$ in $\mathfrak{A}$ gültig.\\ Mit der Voraussetzung $\Sigma \; \vert \models \varphi$folgt dann: $\varphi$ ist gültig in $(\mathfrak{A}$ \\ Also gilt speziell für das h: $(\mathfrak{A},h) \models \varphi $ \\ \end{proof} \subsection{Definition NNF} Eine Formel F ist in Negationsnormalform (NNF) genau dann, wenn \\ jedes Negationszeichen $\neg$ in F unmittelbar vor einer Primformel steht und F \\ die Junktoren $\rightarrow$ und $\leftrightarrow$ nicht enthält.\\ Enthält F dazu noch keine Variablen, ist sie in variablenfreier Negationsnormalform (VNNF).\\ \\ \newpage \section{Axiome und Schlussregeln} \subsection{Aussagenlogische Axiome} Voraussetzung: A, B, C seien Formeln\\ \\ Axiom A1 (Schema der Prämissenbelastung):\\ A $\rightarrow$ (B $\rightarrow$ A)\\ \\ Axiom A2 (Prämisenverschmenlzung):\\ (A $\rightarrow$ (A $\rightarrow$ B)) $\rightarrow$ (A $\rightarrow$ B) \\ \\ Axiom A3 (Kettenschluß):\\ (A $\rightarrow$ B) $\rightarrow$ ((B $\rightarrow$ C) $\rightarrow$ (A $\rightarrow$ C))\\ \\ Axiom A4 (Kontraposition):\\ (A $\rightarrow$ B) $\rightarrow$ ($\neg$ B $\rightarrow \neg$ A)\\ \\ Axiom A5: \\ A $\rightarrow \neg \neg$ A\\ \\ Axiom A6:\\ $\neg \neg$ A $\rightarrow$ A\\ \\ Axiom A7:\\ A $\land$ B $\rightarrow$ A\\ \\ Axiom A8:\\ A $\land$ B $\rightarrow$ B\\ \\ Axiom A9:\\ (A $\rightarrow$ B) $\rightarrow$ ((A $\rightarrow$ C) $\rightarrow$ (A $\rightarrow$ B $\land$ C))\\ \\ Axiom A10:\\ A $\rightarrow$ A $\lor$ B\\ \\ Axiom A11:\\ B $\rightarrow$ A $\lor$ B\\ \\ Axiom A12:\\ (A $\rightarrow$ C) $\rightarrow$ ((B $\rightarrow$ C) $\rightarrow$ (A $\lor$ B $\rightarrow$ C))\\ \\ Axiom A13:\\ (A $\leftrightarrow$ B) $\rightarrow$ (A $\rightarrow$ B)\\ \\ Axiom A14:\\ (A $\leftrightarrow$ B) $\rightarrow$ (B $\rightarrow$ A)\\ \\ Axiom A15:\\ (A $\rightarrow$ B) $\rightarrow$ ((B $\rightarrow$ A) $\rightarrow$ (A $\rightarrow$ B)) \subsection{Identitätstheoretische Axiome} Voraussetzungen:\\ $x_1$, $x_2$, .... x,y sind Variablen, r(f) ist die Stelligkeit des Funktionals f, \\ r(R) ist die Stelligkeit des Prädikats R\\ \\ Axiom I1:\\ x = x\\ \\ Axiom I2:\\ x=y $\rightarrow$ f$x_1$ ... f$x_{n-1}$ x $x_{n+1}$ ... $x_{r(f)}$ = f$x_1$ ... f$x_{n-1}$ y $x_{n+1}$ ... $x_{r(f)}$\\ \\ Axiom I3:\\ x=y $\rightarrow$ (R$x_1$ ... $x_{n-1}$ x $x_{n+1}$ ... $x_{r(R)}$ $\rightarrow$ $R{x_1}$ ... $x_{n-1}$ y $x_{n+1}$ ... $x_{r(R))}$ \\ \\ Axiom I4:\\ x = y $\rightarrow$ (x = z $\rightarrow$ y = z) \subsection{Schlussregeln} Schlussregel SR1 (Abtrennung, Modus Ponens MP)\\ A $\rightarrow$ B, A\\ --------------\\ B\\ \\ Schlussregel SR2 (Vordere Generalisierung Gv)\\ A $\rightarrow$ B\\ --------------\\ $\forall$ x A $\rightarrow$ B\\ \\ Schlussregel SR3 (hintere Partikularisierung Ph):\\ A $\rightarrow$ B\\ --------------\\ A $\rightarrow \exists$ x B\\ \\ Schlussregel SR4 (hintere Generalisierung Gh, falls x $\not \in$ Fr(A)\\ A $\rightarrow$ B\\ --------------\\ A $\rightarrow$ $\forall$ x B\\ \\ Schlussregel SR5 (vodere Partikularisierung Pv, falls x $\not \in$ Fr(B)\\ A $\rightarrow$ B\\ --------------\\ $\exists$ x A $\rightarrow$ B\\ \\ SR6 (Substitution, kurz Sub. falls B durch Substitution der Variablen x in A durch den Term t entsteht) $\label{SR6}$ \\ A\\ ---\\ B\\ \newpage \section{Lemma und Sätze der Prädikatenlogik} \subsection{Folgerungen aus dem Vollständigkeitssatz} Aus dem Vollständigkeitssatz folgt für jede Formel $\Phi$:\\ $\models \Phi \quad \Longrightarrow \quad \vdash \Phi$ \\ \\ Um also $\vdash \Phi$ zu zeigen genügt es mit Hilfe einer Wahrheitstabelle \\ $\models \Phi$ nachzuweisen.\\ \\ Deshalb sieht man sofort: \\ 1) $\vdash \alpha \rightarrow (\beta \rightarrow \alpha \land \beta)$ \\ 2) $\vdash t_1=t_2 \land \neg (t_2=t_3) \rightarrow \neg (t_1=t_3)$ \\ 3) $\vdash (\alpha \rightarrow (\beta \leftrightarrow \gamma)\quad .\rightarrow. \quad \gamma \rightarrow (\alpha \rightarrow \beta)) $ \\ usw. \begin{proof} (ohne) \\ \end{proof} \subsection{Einfache Folgerungen aus den Schlussregeln und den Axiomen} $\Sigma$ ist eine beliebige Formelmenge, $\alpha, \beta, \gamma$ sind beliebige Formeln, $\tau$ ein beliebiger Term\\ Dann gilt: \subsubsection{} $\label{FS1}$ $\Sigma \vdash \alpha \quad \Longrightarrow \quad \Sigma \vdash \alpha \rightarrow \beta $ \subsubsection{} $\label{FS2}$ $\Sigma\vdash \alpha$ und $\Sigma\vdash \beta \; \Longrightarrow \; \Sigma \vdash \alpha \land \beta$ \subsubsection{} $\label{FS3}$ $\Sigma \vdash \alpha \rightarrow \beta$ und $\Sigma \vdash \beta \rightarrow \gamma \quad \Longrightarrow \quad \Sigma \vdash \alpha \rightarrow \gamma $ \subsubsection{} $\label{FS4}$ $\Sigma \vdash x=y$ und $\Sigma \vdash y=z \; \Longrightarrow \; \Sigma \vdash x=z$ \subsubsection{} $\label{FS5}$ $\Sigma \vdash x=y$ und $\Sigma \vdash \neg (y=z) \; \Longrightarrow \; \Sigma \neg (x=z)$ \\ \\ Mit Hilfe der Substitutionsregel gelten diese Behauptungen auch für beliebige Terme, also z.B: für beliebeige Terme t, $t_1, t_2, t_3$\\ $\Sigma \vdash t_1=t_2$ und $PA \vdash t_2=t_3 \; \Longrightarrow \; \vdash t_1=t_3$ \\ und da x=x ein Axiom ist, folgt durch Substitution:\\ $\Sigma \vdash t = t$ \begin{proof} (einfach) \\ 1) \\ $\alpha \rightarrow (\alpha \rightarrow \beta)$ ist ein Axiom (A1), also:\\ $\Sigma \vdash \alpha \rightarrow (\alpha \rightarrow \beta)$ \\ Es sei:\\ $\Sigma \vdash \alpha$, also gibt es eine $\Sigma$-Beweisfolge\\ ...., $\alpha$\\ Da $\Sigma \vdash \alpha \rightarrow (\alpha \rightarrow \beta)$ gibt es eine $\Sigma$-Beweisfolge:\\ ..., $\alpha \rightarrow (\alpha \rightarrow \beta)$ \\ Also gibt es eine $\Sigma$-Beweisfolge:\\ ...., $\alpha$, $\alpha \rightarrow (\alpha \rightarrow \beta)$ \\ Durch Anwendung des Modus Ponesn (MP) folgt die $\Sigma$-Beweisfolge:\\ ...., $\alpha$, $\alpha \rightarrow (\alpha \rightarrow \beta)$, $\alpha \rightarrow \beta$ \\ also:\\ $\Sigma \vdash \alpha \rightarrow \beta$ \\ \\ 2) ...., $\alpha$, $\alpha \rightarrow (\beta \rightarrow \alpha \land \beta)$, $\beta \rightarrow \alpha \land \beta)$, $\beta$, $\alpha \land \beta$ \\ \\ Rest folgt analog. \end{proof} \subsection{Substitutions-Existenz-Lemma} $\label{SEL}$ t ist ein Term, x eine Variable, $\varphi$ eine Formel. Dann gilt: \\ $\vdash \varphi_x^{t} \rightarrow \exists x \varphi$ \begin{proof} (einfach) \\ $\varphi \rightarrow \varphi$ \\ $\varphi \rightarrow \exists x \varphi \quad$ (Ph) \\ $\varphi_x^{t} \rightarrow \exists x \varphi \quad$ (Sub) \\ \end{proof} \newpage \subsection{Substitutionslemma 1} $\label{SUBLEM1}$ Lemma Teil 1:\\ Für alle Variablen z und alle Terme T gilt: $ T_z^{z} = T$\\ \\ Lemma Teil 2:\\ Für alle Variablen z und alle Formeln $\varphi$ gilt: $\varphi_z^{z} = \varphi$ \begin{proof} ... \\ Beweis Lemma Teil 1:\\ Definiere für alle Terme T:\\ B(T): $\Leftrightarrow \quad$ Für alle Variablen z gilt: $ T_z^{z} = T$\\ \\ Unterbehauptung 1:\\ Für alle Variablen x gilt: B(x) \\ \\ Unterbeweis 1:\\ Es seien z und x beliebige Variablen und s eine beliebige Substitutionsbelegung und s(z)=z\\.\\ Fall 1: x$\neq$z\\ Dann gilt: $x_z^{z} = x$ \\ Fall 2: x=z\\ $x_z^{z} = z =x$ \\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$ und ... und $T_n$ und alle Funktionssymbole f gilt:\\ B$(T_0$) und ... und B($T_n$) $\Longrightarrow$ B(f$T_0 ... T_n$)\\ \\ Unterbeweis 2:\\ Es seien $T_0$ und ... und $T_n$ beliebige Terme und f ein beliebiges Funktionssymbol und z eine beliebige Variable und B($T_0$) und ... und B($T_n$). \\ zeige: $[fT_0 ... T_n]_{z}^{z}=f[T_0] ... [T_n]$ \\ \\ a) Es gilt:\\ $[fT_0 ... T_n]_{z}^{z}=f[T_0]_{z}^{z} ... [T_n]_{z}^{z}$ \\ b) Mit der Induktionsvoraussetzung folgt dann:\\ $[T_i]_{z}^{z} = T_i$ für alle 0 $\le$ i $\le$ n \\ Mit a) folgt dann die Behauptung:\\ $[fT_0 ... T_n]_{z}^{z}=f[T_0] ... [T_n]$ \\ \\ Beweis Lemma Teil 2:\\ I)\\ Unterbehauptung 1:\\ Für alle Variablen z und für alle Terme T und R gilt:\\ $[T \equiv R]_z^{z} = [T \equiv R]$\\ \\ Unterbeweis 1:\\ Es seien R und T beliebige Terme und z eine beliebige Variable \\ zeige: $[R \equiv T]_z^{z} = [R \equiv T]$\\ a) Es gilt: \\ $[R \equiv T]_z^{z}=[R]_z^{z} \equiv [T]_z^{z} $ $\quad (*)$ \\ b) Mit Lemma Teil 1 folgt dann:\\ $ [R]_{z}^{z} = R$ und $ [T]_{z}^{z} = T$ \\ Mit (*) folgt dann die Behauptung: \\ $[R \equiv T]_z^{z} = [R \equiv T]$\\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$, ... , $T_n$ und alle Relationssymbolen R und alle Variablen z gilt:\\ $[RT_0 ... T_n]_z^{z} = [RT_0 ... T_n]$ \\ \\ Unterbeweis 2 \\ analog zu Unterbeweis 1:\\ \\ II)\\ Definiere für alle Formeln $\varphi$:\\ B($\varphi$): $\Leftrightarrow \quad$ Für alle Variablen z gilt: $\varphi_z^{z} = \varphi$\\ \\ Unterbehauptung 3\\ Für alle Formeln $\alpha$ und $\beta$ gilt:$\quad$ B($\alpha$) und B($\beta$) $\Longrightarrow$ B($\alpha \land \beta$) \\ Analoges folgt für andere binäre Junktoren.\\ \\ Unterbeweis 3:\\ Es seien $\alpha$ und $\beta$ beliebige Formeln und z eine beliebige Variable und B($\alpha$) und B($\beta$) \\ zeige: $[\alpha \land \beta]_{z}^{z} = \alpha \land \beta$ \\ \\ a) Es gilt:\\ $[\alpha \land \beta]_z^{z} = [\alpha]_z^{z} \land [\beta]_z^{z}$ $\quad$ (*) \\ Mit der Induktionsvoraussetzung folgt daraus:\\ $[\alpha]_{z}^{z} = [\alpha]$ und $[\beta]_{z}^{z} = [\beta]$ \\ Mit (*) folgt dann die Behauptung:\\ $[\alpha \land \beta]_{z}^{z} = \alpha \land \beta$ \\ \\ Unterbehauptung 4\\ Für alle Formeln $\alpha$ gilt:$\quad$ B($\alpha$) $\Longrightarrow$ B($\neg \alpha$) \\ \\ Unterbeweis 4:\\ Es seien $\alpha$ eine beliebige Formel und z eine beliebige Variable und B($\alpha$)\\ a) Es gilt:\\ $[\alpha]_{z}^{z} = \alpha \Longrightarrow$ $[\neg \alpha]_{z}^{z} = \neg \alpha$ \\ b) Mit Induktionsvoraussetzung folgt dann:\\ $[\alpha]_{z}^{z} = \alpha$\\ Mit a) folgt dann die Behauptung:\\ $[\neg \alpha]_{z}^{z} = \neg \alpha$ \\ \\ Unterbehauptung 5:\\ Für alle Formeln $\varphi$ und allen Variablen x gilt: $\quad$ B($\varphi) \Longrightarrow B(\exists x \varphi$)\\ \\ Unterbeweis 5: \\ Es seien $\alpha$ eine beliebige Formel und x und z beliebige Variablen und s eine beliebige Substitutionsbelegung und s(z)=z und B($\alpha$)\\ zeige: $[\exists x \alpha]_{z}^{z} = \exists x \alpha$\\ a) Es gilt:\\ $[\exists x \alpha]_{z}^{z} = \exists x [\alpha_{}^{s(...)}]$= $\exists x [\alpha_{<\{z\}\cap frei(\exists x \alpha)>}^{s(...)}]$ \\ Fall1: $<\{z\}\cap frei(\exists x \alpha)>=\epsilon$\\ $\exists x [\alpha_{< \setminus \{z\} \cap (frei(\alpha)\setminus \{x\})>}^{s(...)}]$= $\exists x [\alpha_{\epsilon}^{s(\epsilon)}]$=$\exists x \alpha$\\ Fall2: $<\{z\}\cap frei(\exists x \alpha)>=(z)$\\ $\exists x [\alpha_{<\{z\} \cap (frei(\alpha)\setminus \{x\})>}^{s(...)}]$= $\exists x [\alpha_{z}^{s(z)}]$= $\exists x [\alpha_{z}^{z}]$\\ Mit der Induktionsvoraussetzung folgt:\\ $[\alpha_{z}^{z}]=\alpha$, also:\\ $\exists x [\alpha_{<\{z\} \cap (frei(\alpha)\setminus \{x\})>}^{s(...)}]$= $\exists x \alpha$\\ \\ \end{proof} \newpage \subsection{Substitutionslemma 2} $\label{SUBLEM2}$ Beispiel: \\ $c_1,c_2,c_3,c_4$ sind Konstanten (also variablenfrei).\\ frei($[\exists x [x_0+x_1 \equiv=x+y]_{x,x_0, x_1,y}^{c_1,c_2,c_3,c_4})$= frei($[\exists x [x_0+x_1 \equiv=x+y]) \setminus \{x,x_0, x_1,y\}=\{x_0, x_1\} $\\ Die Klammern dienen der besseren Lesbarkeit.\\ \\ Lemma Teil 1:\\ Für alle Terme T und alle Substitutionsfolgen L und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) sind variablenfreie Terme $\Longrightarrow$ frei($T_{L}^{s(L)})=$frei(T) $\setminus$ Bild(L) \\ \\ Lemma Teil 2:\\ Für alle Formeln $\varphi$ für alle Substitutionsfolgen L und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) sind variablenfreie Terme $\Longrightarrow$ frei($\varphi_{L}^{s(L)})=$frei($\varphi) \setminus$ Bild(L) \begin{proof} ... \\ Beweis Lemma Teil 1:\\ Definiere für alle Terme T:\\ B(T): $\Leftrightarrow \quad$ Für alle Substitutionsfolgen L und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) sind variablenfreie Terme $\Longrightarrow$ frei($T_{L}^{s(L)})=$frei(T) $\setminus$ Bild(L) \\ \\ Unterbehauptung 1:\\ Für alle Variablen x gilt: B(x) \\ Unterbeweis 1:\\ Es seien x eine beliebige Variable und L eine beliebige Substitutionsfolge und s eine beliebige Substitutionsbelegung und s(Bild(L)) sind variablenfreie Terme \\ zeige: frei($x_{L}^{s(L)})=$frei(x) $\setminus$ Bild(L) \\ \\ Fall 1: x kommt in L vor:\\ Bem: c sei ein variablenfreie Term.\\ frei($x_{L}^{s(L)})=$frei$(s(x))=$frei$(c) = \emptyset$ \\ frei(x)$\setminus$ Bild(L)=$\{x\}\setminus$ Bild(L)=$\emptyset$ \\ Fall 2: x kommt nicht in L vor:\\ Bem: c sei ein variablenfreie Term.\\ frei($x_{L}^{s(L)})=$frei$(x)=\{x\}$ \\ frei(x)$\setminus$ Bild(L)=$\{x\}\setminus$ Bild(L)=$\{x\}$ \\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$ und ... und $T_n$ und alle Funktionssymbole f gilt:\\ B$(T_0$) und ... und B($T_n$) $\Longrightarrow$ B(f$T_0 ... T_n$)\\ \\ Unterbeweis 2:\\ Es seien $T_0$ und ... und $T_n$ beliebige Terme und f ein beliebiges Funktionssymbol und L eine beliebige Substitutionsfolge und s eine beliebige Substitutionsbelegung und s(Bild(L)) sind variablenfreie Terme \\ zeige: frei(f$T_0 ... T_n)_{L}^{s(L)})=$frei(f$T_0 ... T_n$) $\setminus$ Bild(L) \\ a) Mit der Induktionsvoraussetzung folgt:\\ frei($[T_i]_{L}^{s(L)})=$frei($T_i) \setminus$ Bild(L) für alle $0\le i \le n$ $\quad$ (*)\\ b) Es gilt:\\ frei([f$T_0 ... T_n]_{L}^{s(L)})=$frei$(f[T_0]_{L}^{s(L)}$...$[T_n]_{L}^{s(L)})$= frei$([T_0]_{L}^{s(L)}) \cup$...$\cup$ frei$([T_n]_{L}^{s(L)})$= $\quad$ (siehe (*)) \\ frei$([T_0] \setminus$ Bild(L) $\cup$...$\cup$ frei$([T_n] \setminus$ Bild(L)= (frei$(T_0) \cup$...$\cup$ frei$(T_n)) \setminus$ Bild(L) \\ und\\ frei(f$T_0 ... T_n) \setminus$ Bild(L)=(frei$(T_0) \cup$...$\cup$ frei$(T_n)) \setminus$ Bild(L) \\ \\ Beweis Lemma Teil 2:\\ I)\\ Unterbehauptung 1:\\ Für alle Terme T und R und alle Substitutionsfolgen L und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) sind variablenfreie Terme $\Longrightarrow$ frei($[R \equiv T]_L^{s(L)})$ = frei$([R \equiv T]) \setminus$ Bild(L)\\ \\ Unterbeweis 1:\\ Es seien T und R beliebige Terme und L eine beliebige Substitutionsfolge und s eine beliebige Substitutionsbelegungen und s(Bild(L)) sind variablenfreie Terme \\ zeige: frei($[R \equiv T]_L^{s(L)})$=frei$([RT_0 ... T_n]) \setminus$ Bild(L)\\ a) Es gilt nach Lemma Teil 1:\\ frei($R_L^{s(L)})=$frei$(R) \setminus$ Bild(L) und frei($T_L^{s(L)})=$frei$(T) \setminus$ Bild(L) $\quad$ (*)\\ b) Es gilt:\\ frei($[R \equiv T]_L^{s(L)})$ = frei($R_L^{s(L)} \equiv T_L^{s(L)})$= frei($R_L^{s(L)}) \cup$ frei$(T_L^{s(L)})= \quad$ (siehe (*)) \\ (frei(R) $\setminus$ Bild(L)) $\cup$ (frei(T) $\setminus$ Bild(L)) = (frei(R) $\cup$ frei(T)) $\setminus$ Bild(L) = frei$([R \equiv T]) \setminus$ Bild(L)\\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$, ... , $T_n$ und allen Relationssymbolen R und alle Substitutionsfolgen L und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) sind variablenfreie Terme $\Longrightarrow$ frei($[RT_0 ... T_n]_L^{s(L)})$ = frei$([RT_0 ... T_n]) \setminus$ Bild(L)\\ \\ Unterbeweis 2 \\ analog zu Unterbeweis 1:\\ \\ II)\\ Definiere für alle Formeln $\varphi$:\\ B($\varphi$): $\Leftrightarrow \quad$ Für alle Substitutionsfolgen L und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) sind variablenfreie Terme $\Longrightarrow$ frei($\varphi_{L}^{s(L)})=$frei($\varphi) \setminus$ Bild(L) \\ \\ Unterbehauptung 3\\ Für alle Formeln $\alpha$ und $\beta$ gilt:$\quad$ B($\alpha$) und B($\beta$) $\Longrightarrow$ B($\alpha \land \beta$) \\ Analoges folgt für andere binäre Junktoren.\\ \\ Unterbeweis 3:\\ Es seien $\alpha$ und $\beta$ beliebige Formeln und L eine beliebige Substitutionsfolge und s eine beliebige Substitutionsbelegungen und s(Bild(L)) sind variablenfreie Terme \\ zeige: frei($\alpha \land \beta)_{L}^{s(L)}$=frei($\alpha \land \beta) \setminus$ Bild(L)\\ \\ Es seien $\alpha$ und $\beta$ beliebige Formeln und B($\alpha$) und B($\beta$) \\ Zeige: B($\alpha \land \beta$)\\ Dazu seien L eine beliebige Substitutionsfolge und s eine beliebige Substitutionsbelegungen und s(Bild(L)) sind variablenfreie Terme \\ a) Mit der Induktionsvoraussetzung folgt daraus:\\ frei($\alpha_L^{s(L)})=$frei$(\alpha) \setminus$ Bild(L) und frei($\beta_L^{s(L)})=$frei$(\beta) \setminus$ Bild(L) $\quad$ (*)\\ b) Es gilt:\\ frei($[\alpha \land \beta]_{L}^{s(L)})$= frei($\alpha_{L}^{s(L)} \land \beta_{L}^{s(L)}) $ = frei($\alpha_{L}^{s(L)}) \cup$ fre$i(\beta_{L}^{s(L)})= \quad$ (siehe (*)) \\ (frei($\alpha) \setminus$ Bild(L)) $\cup$ (frei($\beta) \setminus$ Bild(L)) = (frei($\alpha) \cup$ frei($\beta)) \setminus$ Bild(L) = frei$([\alpha \land \beta]) \setminus$ Bild(L)\\ \\ Unterbehauptung 4\\ Für alle Formeln $\alpha$ gilt:$\quad$ B($\alpha$) $\Longrightarrow$ B($\neg \alpha$) \\ \\ Unterbeweis 4:\\ Es seien $\alpha$ eine beliebige Formel und L eine beliebige Substitutionsfolge und s eine beliebige Substitutionsbelegungen und s(Bild(L)) sind variablenfreie Terme und B($\alpha$) \\ zeige: frei($\neg \alpha)_{L}^{s(L)}$=frei($\neg \alpha) \setminus$ Bild(L)\\ \\ Dazu seien L eine beliebige Substitutionsfolge und s eine beliebige Substitutionsbelegungen und s(Bild(L)) sind variablenfreie Terme \\ b) Mit Induktionsvoraussetzung folgt:\\ frei($\alpha_L^{s(L)})=$frei$(\alpha) \setminus$ Bild(L) $\quad$(*) \\ b) Es gilt:\\ frei($[\neg \alpha]_L^{s(L)})=$frei$(\neg [\alpha]_L^{s(L)})$= frei$([\alpha]_L^{s(L)})$=$\quad$ (siehe (*)) \\ frei$(\alpha) \setminus$ Bild(L)=frei$(\neg \alpha) \setminus$ Bild(L) \\ Damit folgt die Behauptung:\\ frei($[\neg \alpha]_L^{s(L)})=$frei$(\neg \alpha) \setminus$ Bild(L) \\ \\ Unterbehauptung 5:\\ Für alle Formeln $\alpha$ und allen Variablen x gilt: $\quad$ B($\alpha) \Longrightarrow B(\exists x \alpha$)\\ \\ Unterbeweis 5: \\ Es seien $\alpha$ eine beliebige Formel und x eine beliebige Variable und L eine beliebige Substitutionsfolge und s eine beliebige Substitutionsbelegungen und s(Bild(L)) sind variablenfreie Terme und und B($\alpha$) \\ zeige: frei($\exists x \alpha)_{L}^{s(L)}$=frei($\exists x \alpha) \setminus$ Bild(L)\\ a) Für alle Mengen A und B gilt: A $\setminus$ (B $\cap$ A)=A $\setminus$ B $\quad$(*)\\ b) Mit Induktionsvoraussetzung folgt:\\ frei($\alpha_{}^{s(...)}$)= frei$(\alpha) \setminus$ Bild$()$= frei$(\alpha) \setminus$ (Bild(L)$\cap$frei$(\exists x \alpha))$ also:\\ frei($\alpha_{}^{s(...)}$)= frei$(\alpha) \setminus$ (Bild(L)$\cap$frei$(\exists x \alpha))$ $\quad$(**)\\ c) Es gilt:\\ frei($[\exists x \alpha]_{L}^{s(L)}$)= frei($\exists x [\alpha_{}^{s(...)}])$= frei($[\alpha_{}^{s(...)}]) \setminus \{x\}$= (siehe (**)) \\ (frei$(\alpha) \setminus$ (Bild(L)$\cap$frei$(\exists x \alpha))) \setminus \{x\}$= (frei$(\alpha) \setminus \{x\}) \setminus$ (Bild(L)$\cap$ (frei$(\alpha) \setminus \{x\})) $=$\quad$(siehe (*)) \\ (frei$(\alpha) \setminus \{x\}) \setminus$ Bild(L)\\ \\ \end{proof} \newpage \subsection{Substitutionslemma 3} $\label{SUBLEM3}$ Eine simultane Substitution ist nur von der Substitution der freien Variablen abhängig, also unabhängig davon durch welchen Term eine nicht freie Variablen ersetzt wird. \\ \\ Beispiel: \\ $[x_0+x_1 \equiv x_2]_{y_0, y_1, x_2, y_2, x_1, y_3}^{t_0, t_1, r_2, t_2, r_1,t_3} = [x_0+x_1 \equiv x_2]_{y_3,x_1, y_2,x_2}^{t_3, r_1,t_2,r_2}$ \\ \\ Die Klammern dienen der besseren Lesbarkeit.\\ \\ Formalisierung des Lemmas:\\ Lemma Teil 1:\\ Für alle Folgen L, F und alle Substitutionsbelegungen s und alle Terme T gilt:\\ Bild(L) $\cap$ frei(T) = Bild(F) $\cap$ frei(T) $\Longrightarrow [T]_L^{s(L)} = [T]_{F}^{s(F)}$\\ \\ Lemma Teil 2:\\ Für alle Folgen L, F und alle Substitutionsbelegungen s und alle Formeln $\varphi$ gilt:\\ Bild(L) $\cap$ frei($\varphi$) = Bild(F) $\cap$ frei($\varphi$) $\Longrightarrow [\varphi]_L^{s(L)} = [\varphi]_{F}^{s(F)}$ \begin{proof} (mit Unterbehauptungen) \\ I)\\ Beweis Lemma Teil 1:\\ Definiere für alle Terme T:\\ B(T): $\Leftrightarrow \quad$ Für alle Substitutionsfolgen L,F und alle Substitutionsbelegungen s gilt: \\ Bild(L)$\cap$ frei(T) = Bild(F)$\cap$ frei(T) $\Longrightarrow [T]_{L}^{s(L)} = [T]_{F}^{s(F)}$ \\ \\ Unterbehauptung 1:\\ Für alle Variablen x gilt: B(x) \\ \\ Unterbeweis 1:\\ Es seien x eine beliebige Variable und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung s und Bild(L)$\cap$ frei(x) = Bild(F)$\cap$ frei(x) \\ Fall1: Bild(L)$\cap$ frei(x) = Bild(F)$\cap$ frei(x)=$\{x\}$\\ also enthalten L und F das Folgenglied x, also $[x]_{L}^{s(L)}=s(x)$ und $[x]_{F}^{s(F)}=s(x)$, also:\\ $[x]_{L}^{s(L)}= [x]_{F}^{s(F)}$\\ Fall2: Bild(L)$\cap$ frei(x) = Bild(F)$\cap$ frei(x)=$\emptyset$\\ also enthalten weder L noch F das Folgenglied x, also: $[x]_{L}^{s(L)}=x_{\epsilon}^{s(\epsilon))}=x$ und $[x]_{F}^{s(F)}=x_{\epsilon}^{s(\epsilon))}=x$, also:\\ $[x]_{L}^{s(L)}= [x]_{F}^{s(F)}$\\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$ und ... und $T_n$ und alle Funktionssymbole f gilt:\\ B$(T_0$) und ... und ... B($T_n$) $\Longrightarrow$ B(f$T_0 ... T_n$)\\ \\ Unterbeweis 2:\\ Es seien $T_0$ und ... und $T_n$ beliebige Terme und f ein beliebiges Funktionssymbol und L und F beliebige Substitutionsfolgen und s eine belieige Substitutionsbelegungen und\\ Bild(L) $\cap$ frei($fT_0 ... T_n$) = Bild(F) $\cap$ frei($fT_0 ... T_n$) und B$(T_0$) und ... und ... B($T_n$)\\ zeige: $[fT_0 ... T_n]_L^{s(L)} = [fT_0 ... T_n]_{F}^{s(F)}$ \\ a) Es gilt:\\ Aus Bild(L) $\cap$ frei($fT_0 ... T_n$) = Bild(F) $\cap$ frei($fT_0 ... T_n$) folgt:\\ Bild(L) $\cap$ (frei($fT_0) \cup ... \cup frei(T_n$)) = Bild(F) $\cap$ (frei($fT_0) \cup ... \cup frei(T_n$)) und damit:\\ Bild(L) $\cap$ frei($T_i$) = Bild(F) $\cap$ frei($T_i$) für alle 0 $\le$ i $\le$ n \\ Mit der Induktionsvoraussetzung folgt dann:\\ $[T_i]_{L}^{s(L)} = [T_i]_{F}^{s(F)}$ für alle 0 $\le$ i $\le$ n $\quad (*)$ \\ b) Es gilt:\\ $[fT_0 ... T_k]_L^{s(L)}=f[T_0]_L^{s(L)} ... [T_k]_L^{s(L)}$ und \\ $[fT_0 ... T_k]_F^{s(F)}=f[T_0]_F^{s(F)} ... [T_k]_F^{s(F)}$ \\ Mit (*) folgt dann die Behauptung: \\ $[fT_0 ... T_n]_L^{s(L)} = [fT_0 ... T_n]_{F}^{s(F)}$ \\ \\ Beweis Lemma Teil 2:\\ I)\\ Unterbehauptung 1:\\ Für alle Terme T und R und alle Substitutionsfolgen L und F und alle Substitutionsbelegungen s gilt:\\ Bild(L) $\cap$ frei([T $\equiv$ R])=Bild(F) $\cap$ frei([T $\equiv$ R]) $\Longrightarrow [T \equiv R]_L^{s(L)} = [T \equiv R]_F^{s(F)}$\\ \\ Unterbeweis 1:\\ Es seien T und R beliebige Terme und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und Bild(L) $\cap$ frei([T $\equiv R])=$Bild(F) $\cap$ frei([T $\equiv R])$ \\ zeige:$ [T \equiv R]_L^{s(L)} = [T \equiv R]_F^{s(F)}$\\ a) Es sei: Bild(L) $\cap$ frei([T $\equiv$ R])=Bild(F) $\cap$ frei([T $\equiv$ R]) , also gilt auch:\\ Bild(L) $\cap$ frei(T) = Bild(F) $\cap$ frei(T) und Bild(L) $\cap$ frei(R) = Bild(F) $\cap$ frei(R) \\ Mit Behauptung 1 folgt dann:\\ $ [T]_{L}^{s(L)} = [T]_{F}^{s(F)}$ und $ [R]_{L}^{s(L)} = [R]_{F}^{s(F)} \quad (*)$ \\ b) Es gilt:\\ $[R \equiv T]_L^{s(L)}=[R]_L^{s(L)} [T]_L^{s(L)} $ und \\ $[R \equiv T]_F^{s(F)}=[R]_F^{s(F)} [T]_F^{s(F)} $ \\ Mit (*) folgt dann die Behauptung \\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$, ... , $T_n$ und allen Relationssymbolen R und für alle Folgen L und F und alle Substitutionsbelegungen s gilt:\\ frei(L) $\cap$ frei($RT_0 ... T_n$) =frei(F) $\cap$ frei($RT_0 ... T_n$) $\Longrightarrow [RT_0 ... T_n]_L^{s(L)} = [RT_0 ... T_n]_{F}^{s(F)}$ \\ \\ Unterbeweis 2 \\ analog zu Unterbeweis 1:\\ \\ II)\\ Definiere für alle Formeln $\varphi$:\\ B($\varphi): \Leftrightarrow \quad$ Für alle Substitutionsfolgen L,F und alle Substitutionsbelegungen s gilt: \\ Bild(L)$\cap$ frei($\varphi$) = Bild(F)$\cap$ frei($\varphi$) $\Longrightarrow [\varphi]_{L}^{s(L)} = [\varphi]_{F}^{s(F)}$ \\ \\ Unterbehauptung 3\\ Für alle Formeln $\alpha$ und $\beta$ gilt:$\quad$ B($\alpha$) und B($\beta$) $\Longrightarrow$ B($\alpha \land \beta$) \\ Analoges folgt für andere binäre Junktoren.\\ \\ Unterbeweis 3:\\ Es seien $\alpha$ und $\beta$ beliebige Formeln und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und Bild(L) $\cap$ frei($\alpha \land \beta)$= Bild(F) $\cap$ frei($\alpha \land \beta)$ und B($\alpha$) und B($\beta$) \\ zeige: $[\alpha \land \beta]_{L}^{s(L)} = [\alpha \land \beta]_{F}^{s(F)}$ \\ \\ a) Daraus folgt:\\ Bild(L)$\cap$ (frei($\alpha) \cup$ frei($\beta$)) = Bild(F)$\cap$ (frei($\alpha) \cup$ frei($\beta$)), also:\\ Bild(L)$\cap$ frei($\alpha$) = Bild(F)$\cap$ frei($\alpha$) und Bild(L)$\cap$ frei($\beta$) = Bild(F)$\cap$ frei($\beta$) \\ Mit der Induktionsvoraussetzung folgt daraus:\\ $[\alpha]_{L}^{s(L)} = [\alpha]_{F}^{s(F)}$ und $[\beta]_{L}^{s(L)} = [\beta]_{F}^{s(F)} \quad (*)$ \\ b) Es gilt:\\ $[\alpha \land \beta]_L^{s(L)} = [\alpha]_L^{s(L)} \land [\beta]_L^{s(L)} $ und $[\alpha \land \beta]_F^{s(F)} = [\alpha]_F^{s(F)} \land [\beta]_F^{s(F)} $ \\ Mit (*) folgt dann die Behauptung:\\ $[\alpha \land \beta]_{L}^{s(L)} = [\alpha \land \beta]_{F}^{s(F)}$ \\ \\ Unterbehauptung 4\\ Für alle Formeln $\alpha$ gilt:$\quad$ B($\alpha$) $\Longrightarrow$ B($\neg \alpha$) \\ \\ Unterbeweis 4:\\ Es seien $\alpha$ eine beliebige Formel und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und Bild(L)$\cap$ frei($\neg \alpha$) = Bild(F)$\cap$ frei($\neg \alpha$) \\ zeige: $[\neg \alpha]_{L}^{s(L)} = [\neg \alpha]_{F}^{s(F)}$ \\ \\ a) Es gilt:\\ $[\alpha]_{L}^{s(L)} = [\alpha]_{F}^{s(F)} \Longrightarrow$ $\neg [\alpha]_{L}^{s(L)} = \neg [\alpha]_{F}^{s(F)}$ \\ Und außerdem:\\ frei($\neg \alpha$) = frei($\alpha$), also:\\ Bild(L)$\cap$ frei($\alpha$)=Bild(L)$\cap$ frei($\neg \alpha$)=Bild(F)$\cap$ frei($\neg \alpha$)= Bild(F)$\cap$ frei($\alpha$)\\ Also: Bild(L)$\cap$ frei($\alpha$)=Bild(F)$\cap$ frei($\alpha$)\\ b) Mit Induktionsvoraussetzung folgt dann:\\ $[\alpha]_{L}^{s(L)} = [\alpha]_{F}^{s(F)}$\\ Mit a) folgt dann die Behauptung:\\ $[\neg \alpha]_{L}^{s(L)} = \neg [\alpha]_{F}^{s(F)}$ und \\ \\ Unterbehauptung 5:\\ Für alle Formeln $\varphi$ und allen Variablen x gilt: $\quad$ B($\varphi) \Longrightarrow B(\exists x \varphi$)\\ \\ Unterbeweis 5: \\ Es seien $\alpha$ eine beliebige Formel und x eine beliebige Variable und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und Bild(L)$\cap$ frei($\exists x \alpha$)=Bild(F)$\cap$ frei($\exists x \alpha$) \\ zeige: B($\exists x \varphi$) für alle Variablen x, also: \\ \\ a) Es gilt:\\ $<$Bild(L)$\cap$ frei($\exists x \alpha$)$>$ = $<$Bild(F)$\cap$ frei($\exists x \alpha$)$> \quad$ (*) \\ b) Es gilt:\\ $[\exists x \alpha]_{L}^{s(L)} = \exists x [\alpha]_{}^{s(...)} $ \\ $[\exists x \alpha]_{F}^{s(F)} = \exists x [\alpha]_{}^{s(...)}$ \\ Mit (*) folgt dann die Behauptung. \end{proof} \newpage \subsection{Substitutionslemma 4} $\label{SUBLEM4}$ Eine simultane Substitution ist unabhängig von der Umordnung der Reihenfolge der Folgenglieder. \\ \\ Formal:\\ Für alle Terme $t_0$, ...,$t_n$ und alle Formeln $\varphi$ und alle Permutation $\pi$ der Zahlen 0, ..., n gilt: \\ $\varphi \overset{t_0}{x_0}$ ... $\overset{t_n}{x_n} = (\varphi \overset{t_{\pi (0)}}{x_{\pi(0)}}$ ... $\overset{t_{\pi (n-1)}}{x_{\pi(n-1)}}) \; \overset{t_{\pi (n)}}{x_{\pi(n)}}$ \\ \\ Beispiel: \\ $[x_0+x_1 \equiv x_2]_{y_0, y_1, x_2, y_2, x_1, y_3}^{t_0, t_1, r_2, t_2, r_1,t_3} = [x_0+x_1 \equiv x_2]_{y_3,y_2, y_1,y_0,x_2,x_1}^{t_3,t_2,t_1,t_0,r_2,r_1}$ \begin{proof} (mit Unterbehauptungen) \\ I) Andere Formalisierung des Lemmas:\\ Eine Substitutionsfolge L geht durch Umodnung der Reihenfolge der Folgenglieder in eine Substitutionsfolge F über (d.h. L und F unterscheiden sich nur in der Reihenfolge des Auftretens ihrer Elemente)\\ : gdw ($\inplus$ bedeutet Element einer Folge)\\ x $\inplus$ L $\Longleftrightarrow$ x $\inplus$ F und $\vert$D(L)$\vert$=$\vert$Bild(L)$\vert$ und $\vert$D(F)$\vert$=$\vert$ Bild(F)$\vert$ gdw\\ x $ \in$ Bild(L) $\Longleftrightarrow$ x $ \in$ Bild(F) und $\vert$D(L)$\vert$=$\vert$Bild(L)$\vert$ und $\vert$D(F)$\vert$=$\vert$ Bild(F)$\vert$ gdw\\ Bild(L)=Bild(F) und $\vert$D(L)$\vert$=$\vert$Bild(L)$\vert$ und $\vert$D(F)$\vert$=$\vert$ Bild(F)$\vert$ gdw\\ D(L)=D(F) und Bild(L)=Bild(F) \\ \\ Lemma Teil 1:\\ Für alle Terme T und alle Substitutionsfolgen L, F und allen Substitutionsbelegungen s gilt:\\ D(L)=D(F) und Bild(L)=Bild(F) $\Longrightarrow[T]_L^{s(L)} = [T]_{F}^{s(F)}$ \\ \\ Lemma Teil 2:\\ Für alle Formeln $\varphi$ und alle Substitutionsfolgen L und F mit gleicher Definitionsmenge D(L)=D(F) und gleicher Bildmenge Bild(L)=Bild(F) und allen Substitutionsbelegungen s gilt:\\ D(L)=D(F) und Bild(L)=Bild(F) $\Longrightarrow [\varphi]_L^{s(L)} = [\varphi]_{F}^{s(F)}$ \\ \\ Beweis Lemma Teil 1:\\ Für alle Terme T wird definiert:\\ B(T): $\Leftrightarrow \quad$ Für alle Substitutionsfolgen L und F und alle Substitutionsbelegungen s gilt: \\ D(L)=D(F) und Bild(L)=Bild(F) $\Longrightarrow [T]_L^{s(L)} = [T]_{F}^{s(F)}$ \\ \\ Unterbehauptung 1:\\ Für alle Variablen x gilt: B(x) \\ \\ Unterbeweis 1:\\ Es seien x eine beliebige Variable und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und D(L)=D(F) und Bild(L)=Bild(F)\\ zeige: $[x]_L^{s(L)} = [x]_{F}^{s(F)}$ \\ Da sich L und F nur in der Reihenfolge des Auftretens ihrer Elemente unterscheiden, folgt dies sofort.\\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$ und ... und $T_n$ und alle Funktionssymbole f gilt:\\ B$(T_0$) und ... und ... B($T_n$) $\Longrightarrow$ B(f$T_0 ... T_n$)\\ \\ Unterbeweis 2:\\ Es seien $T_0$ und ... und $T_n$ beliebige Terme und f ein beliebiges Funktionssymbol und L und F beliebige Substitutionsfolgen und s eine belieige Substitutionsbelegungen und D(L)=D(F) und Bild(L)=Bild(F)\\ zeige: $[fT_0 ... T_k]_L^{s(L)}=[fT_0 ... T_k]_F^{s(F)}$ \\ a) Mit der Induktionsvoraussetzung folgt dann:\\ $ [T_i]_{L}^{s(L)} = [T_i]_{F}^{s(F)}$ für alle 0$\le$ i$\le$n $\quad (*)$ \\ b) Es gilt:\\ $[fT_0 ... T_k]_L^{s(L)}=f[T_0]_L^{s(L)} ... [T_k]_L^{s(L)}$ und \\ $[fT_0 ... T_k]_F^{s(F)}=f[T_0]_F^{s(F)} ... [T_k]_F^{s(F)}$ \\ Mit (*) folgt dann die Behauptung \\ \\ Beweis Lemma Teil 2:\\ I)\\ Unterbehauptung 1:\\ Für alle Terme T und R und alle Substitutionsfolgen L und F und allen Substitutionsbelegungen s gilt: D(L)=D(F) und Bild(L)=Bild(F) $\Longrightarrow [T \equiv R]_L^{s(L)} = [T \equiv R]_F^{s(F)}$\\ \\ Unterbeweis 1:\\ Es seien T und R beliebige Terme und L und F beliebige Substitutionsfolgen und D(L)=D(F) und Bild(L)=Bild(F) \\ a) Mit Behauptung 1 folgt dann:\\ $ [T]_{L}^{s(L)} = [T]_{F}^{s(F)}$ und $ [R]_{L}^{s(L)} = [R]_{F}^{s(F)} \quad (*)$ \\ b) Es gilt:\\ $[R \equiv T]_L^{s(L)}=[R]_L^{s(L)} \equiv [T]_L^{s(L)} $ und \\ $[R \equiv T]_F^{s(F)}=[R]_F^{s(F)} \equiv [T]_F^{s(F)} $ \\ Mit (*) folgt dann die Behauptung \\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$ und ... und $T_n$ und allen Relationssymbolen R und alle Substitutionsfolgen L und F und allen Substitutionsbelegungen s gilt:\\ D(L)=D(F) und Bild(L)=Bild(F) $\Longrightarrow [RT_0 ... T_n]_L^{s(L)} = [RT_0 ... T_n]_{F}^{s(F)}$ \\ \\ Unterbeweis 2\\ analog zu Unterbeweis 1:\\ \\ II)\\ Definiere für alle Formeln $\varphi$:\\ B($\varphi): \Leftrightarrow \quad$ Für alle Substitutionsfolgen L, F und alle Substitutionsbelegungen s gilt:\\ D(L)=D(F) und Bild(L)=Bild(F) $\Longrightarrow$ $[\varphi]_L^{s(L)} = [\varphi]_{F}^{s(F)}$ \\ \\ Unterbehauptung 3\\ Für alle Formeln $\alpha$ und $\beta$ gilt:$\quad$ B($\alpha$) und B($\beta$) $\Longrightarrow$ B($\alpha \land \beta$) \\ Analoges folgt für andere binäre Junktoren.\\ \\ Unterbeweis 3:\\ Es seien $\alpha$ und $\beta$ beliebige Formeln und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und D(L)=D(F) und Bild(L)=Bild(F) und B($\alpha$) und B($\beta$) \\ Zeige: [$\alpha \land \beta)]_{L}^{s(L)}=[\alpha \land \beta)]_{F}^{s(F)}$ a) Daraus folgt mit Mit Induktionsvoraussetzung:\\ $[\alpha]_L^{s(L)} = [\alpha]_F^{s(F)}$ und $[\beta]_L^{s(L)} = [\beta]_F^{s(F)}\quad (*)$ \\ b) es gilt:\\ $[\alpha \land \beta]_L^{s(L)} = [\alpha]_L^{s(L)} \land [\beta]_L^{s(L)}$ \\ $[\alpha \land \beta]_F^{s(F)} = \alpha]_F^{s(F)} \land [\beta]_F^{s(F)}$ \\ Mit (*) folgt die Behauptung. \\ $[\alpha \land \beta]_L^{s(L)} = [\alpha \land \beta]_{F}^{s(F)}$ \\ \\ Unterbehauptung 4\\ Für alle Formeln $\alpha$ gilt:$\quad$ B($\alpha$) $\Longrightarrow$ B($\neg \alpha$) \\ \\ Unterbeweis 4:\\ Es seien $\alpha$ eine beliebige Formel und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und D(L)=D(F) und Bild(L)=Bild(F) und B($\alpha$) \\ zeige: $[\neg \alpha]_{L}^{s(L)} = \neg [\alpha]_{F}^{s(F)}$ \\ \\ a) Es gilt:\\ $[\alpha]_{L}^{s(L)} = [\alpha]_{L}^{s(L)} \Longrightarrow$ $[\neg \alpha]_{L}^{s(L)} = \neg [\alpha]_{L}^{s(L)}$ \\ b) Mit Induktionsvoraussetzung folgt:\\ $[\alpha]_{L}^{s(L)} = [\alpha]_{F}^{s(F)}$\\ Mit a) folgt dann die Behauptung:\\ $[\neg \alpha]_{L}^{s(L)} = \neg [\alpha]_{F}^{s(F)}$ und \\ \\ Unterbehauptung 5:\\ Für alle Formeln $\varphi$ und allen Variablen x gilt: $\quad$ B($\varphi) \Longrightarrow B(\exists x \varphi$)\\ \\ Unterbeweis 5: \\ Es seien $\alpha$ eine beliebige Formel und x eine beliebige Variable und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und D(L)=D(F) und Bild(L)=Bild(F) und B($\alpha$) \\ zeige: $[\exists x \alpha]_{L}^{s(L)} = [\exists x \alpha]_{F}^{s(F)}$ \\ \\ a)\\ Es sei: D(L)=D(F) und Bild(L)=Bild(F) \\ Aus Bild(L)=Bild(F) folgt: \\ $ = \quad (*) $ \\ b) Es gilt:\\ $[\exists x \alpha]_{L}^{s(L)} = \exists x [\alpha]_{}^{s(...)}$ und $[\exists x \alpha]_{F}^{s(F)} = \exists x [\alpha]_{}^{s(...)}$ \\ Mit (*) folgt dann die Behauptung. \end{proof} \newpage \subsection{Substitutionslemma 5} $\label{SUBLEM5}$ Beispiel: \\ $c_1,c_2,c_3,c_4,c_5,c_6$ sind Konstanten (also variablenfrei).\\ $[x_0-x_1 \equiv x_2-x_3]_{y,x_0,x_1 + x_2,x_3,z}^{c_1,c_2,c_3,c_4,c_5,c_6}$ = $[[x_0-x_1 \equiv x_2-x_3]_{y,x_0,x_1}^{c_1,c_2,c_3}]_{x_2,x_3,z}^{c_4,c_5,c_6}]$ = $[c_2-c_3 \equiv c_4-c_5]$ \\ \\ Lemma Teil 1:\\ Für alle Terme T und alle Substitutionsfolgen L und F und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ (d.h. L+F ist eine Substitutionsfolge) $\Longrightarrow$ $[T]_{L+F}^{s(L+F)}=[[T]_{L}^{s(L)}]_F^{s(F)}$ \\ \\ Lemma Teil 2:\\ Für alle Formeln $\varphi$ und alle Substitutionsfolgen L und F und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ (d.h. L+F ist eine Substitutionsfolge) $\Longrightarrow$ $[\varphi]_{L+F}^{s(L+F)}=[[\varphi]_{L}^{s(L)}]_F^{s(F)}$ \\ \begin{proof} (mit Unterbehauptungen) \\ Beweis zu Lemma Teil 1:\\ Definiere für alle Terme T:\\ B(T): $\Leftrightarrow \quad$ Für alle Substitutionsfolgen L und F und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ (d.h. L+F ist eine Substitutionsfolge) $\Longrightarrow$ $[T]_{L+F}^{s(L+F)}=[[T]_{L}^{s(L)}]_F^{s(F)}$ \\ \\ Unterbehauptung 1:\\ Für alle Variablen x gilt: B(x) \\ \\ Unterbeweis 1:\\ Es seien x eine beliebige Variable und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung s und s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ \\ zeige: $[x]_{L+F}^{s(L+F)}=[[x]_{L}^{s(L)}]_F^{s(F)}$ \\ Fall1: x ist in der Substitutionsfolge L enthalten:\\ $[x]_{L+F}^{s(L+F)}=s(x)=[[x]_{L}^{s(L)}]_F^{s(F)}$ \\ Fall2: x ist in der Substitutionsfolge F enthalten:\\ $[x]_{L+F}^{s(L+F)}=s(x)=[[x]_{L}^{s(L)}]_F^{s(F)}$ \\ Fall3: x ist weder in der Substitutionsfolge L noch in F enthalten:\\ $[x]_{L+F}^{s(L+F)}=x=[[x]_{L}^{s(L)}]_F^{s(F)}$ \\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0$ und ... und $T_n$ und alle Funktionssymbole f gilt:\\ B$(T_0$) und ... und ... B($T_n$) $\Longrightarrow$ B(f$T_0 ... T_n$)\\ \\ Unterbeweis 2:\\ Es seien $T_0$ und ... und $T_n$ beliebige Terme und f ein beliebiges Funktionssymbol und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ \\ zeige: $[fT_0, ..., T_n]_{L+F}^{s(L+F)}=[[fT_0, ..., T_n]_{L}^{s(L)}]_{F}^{s(F)} $ \\ a) Mit der Induktionsvoraussetzung folgt:\\ $[T_i]_{L+F}^{s(L+F)}=[[T_i]_{L}^{s(L)}]_F^{s(F)}$ für alle $0\le i \le n$ $\quad$ (*)\\ b) Es gilt:\\ $[fT_0, ..., T_n]_{L+F}^{s(L+F)}=f[T_0]_{L+F}^{s(L+F)}, ... , [T_n]_{L+F}^{s(L+F)} $ und \\ $[[fT_0, ..., T_n]_{L}^{s(L)}]_{F}^{s(F)} =[f[T_0]_{L}^{s(L)}, ..., [T_n]_{L}^{s(L)}]_{F}^{s(F)}=f[[T_0]_{L}^{s(L)}]_{F}^{s(F)}, ..., [[T_n]_{L}^{s(L)}]_{F}^{s(F)}$ \\ Mit (*) folgt die Behauptung\\ \\ Beweis zu Lemma Teil 2:\\ I)\\ Unterbehauptung 1:\\ Für alle Terme T und R und alle Substitutionsfolgen L und F und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ $\Longrightarrow$ \\ $[T \equiv R]_{L+F}^{s(L+F)}=[[T \equiv R]_{L}^{s(L)}]_F^{s(F)}$ \\ \\ Unterbeweis 1:\\ Es seien T und R beliebige Terme und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ \\ zeige: $[T \equiv R]_{L+F}^{s(L+F)}=[[T \equiv R]_{L}^{s(L)}]_F^{s(F)}$ \\ a) Es gilt mit Lemma Teil 1 : \\ $[T]_{L+F}^{s(L+F)}=[[T]_{L}^{s(L)}]_F^{s(F)}$ und $[R]_{L+F}^{s(L+F)}=[[R]_{L}^{s(L)}]_F^{s(F)}$ \\ b) Es gilt: \\ $[T \equiv R]_{L+F}^{s(L+F)}=[T]_{L+F}^{s(L+F)} \equiv[R]_{L+F}^{s(L+F)}$ und \\ $[[T \equiv R]_{L}^{s(L)}]_{F}^{s(F)} = [T_{L}^{s(L)} \equiv R_{L}^{s(L)}]_{F}^{s(F)}=$ $[[T]_{L}^{s(L)}]_F^{s(F)} \equiv [[R]_{L}^{s(L)}]_F^{s(F)}$ \\ Mit a) folgt dann die Behauptung \\ \\ Unterbehauptung 2:\\ Für alle Terme $T_0, ..., T_n$ und allen Relationssymbolen R und alle Substitutionsfolgen L und F und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ $\Longrightarrow$ $[RT_0, ...,T_n]_{L+F}^{s(L+F)}=[[RT_0, ...,T_n]_{L}^{s(L)}]_F^{s(F)}$ \\ Unterbeweis 2\\ analog zu Unterbeweis 1:\\ \\ II)\\ II.1)\\ Beweishilfslemma 1:\\ $A \cap B=\emptyset \Longrightarrow (A \cap C) \setminus (B \cap C)=A \cap C$ \\ Beweis: ohne \\ \\ Beweishilfslemma 2:\\ $A \cap( B \setminus C) =(A \cap B) \setminus C)$ \\ Beweis: ohne \\ \\ II.2) Definiere für alle Formeln $\varphi$:\\ B($\varphi$): $\Leftrightarrow \quad$ Für alle Substitutionsfolgen L und F und alle Substitutionsbelegungen s gilt:\\ s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ (d.h. L+F ist eine Substitutionsfolge) $\Longrightarrow$ $[\varphi]_{L+F}^{s(L+F)}=[[\varphi]_{L}^{s(L)}]_F^{s(F)}$ \\ \\ Unterbehauptung 3:\\ Für alle Formeln $\alpha$ und $\beta$ gilt:$\quad$ B($\alpha$) und B($\beta$) $\Longrightarrow$ B($\alpha \land \beta$) \\ Analoges folgt für andere binäre Junktoren.\\ \\ Unterbeweis 3:\\ Es seien $\alpha$ und $\beta$ beliebige Formeln und B($\alpha$) und B($\beta$) L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme \\ und Bild(L) $\cap$ Bild(F) = $\emptyset$ und B($\alpha$) und B($\beta$) \\ zeige: $[\alpha \land \beta]_{L+F}^{s(L+F)}=[[\alpha \land \beta]_{L}^{s(L)}]_{F}^{s(F)}$\\ a) Mit der Induktionsvoraussetzung folgt:\\ $[\alpha]_{L+F}^{s(L+F)}=[[\alpha_{L}^{s(L)}]_F^{s(F)}]$ und $[\beta]_{L+F}^{s(L+F)}=[[\beta_{L}^{s(L)}]_F^{s(F)}]$ \\ b) Es gilt:\\ $[[\alpha \land \beta]_{L}^{s(L)}]_{F}^{s(F)}= [[\alpha]_{L}^{s(L)} \land [\beta]_{L}^{s(L)}]_{F}^{s(F)}=$ $[[\alpha_{L}^{s(L)}]_{F}^{s(F)}] \land [[\beta_{L}^{s(L)}]_{F}^{s(F)}]$ = (siehe a) =\\ $[\alpha]_{L+F}^{s(L+F)} \land [\beta]_{L+F}^{s(L+F)} = [\alpha \land \beta]_{L+F}^{s(L+F)}$ Unterbehauptung 4:\\ Für alle Formeln $\alpha$ gilt: (B($\alpha$) $\Longrightarrow$ B($\neg \alpha))$ \\ \\ Unterbeweis 4:\\ Es seien $\alpha$ eine beliebige Formel und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme und Bild(L) $\cap$ Bild(F) = $\emptyset$ und B($\alpha$) \\ zeige: $[\neg \alpha]_{L+F}^{s(L+F)}=[[\neg \alpha]_{L}^{s(L)}]_{F}^{s(F)}$ \\ a) Mit der Induktionsvoraussetzung folgt:\\ $[\alpha_{L+F}^{s(L+F)}]=[[\alpha_{L}^{s(L)}]_{F}^{s(F)}] $ \\ b) Es gilt:\\ $[[\neg \alpha]_{L}^{s(L)}]_{F}^{s(F)}$= $[\neg [\alpha_{L}^{s(L)}]]_{F}^{s(F)}$= $\neg [[\alpha_{L}^{s(L)}]_{F}^{s(F)}]$= (siehe a) = $\neg [\alpha_{L+F}^{s(L+F)}]$= $[\neg \alpha]_{L+F}^{s(L+F)}$ \\ \\ Unterbehauptung 5:\\ Für alle Formeln $\alpha$ für alle Variablen x gilt: B($\alpha) \Longrightarrow$ B($\exists x \alpha)$ \\ \\ Unterbeweis 5:\\ Es seien $\alpha$ eine beliebige Formel und x eine beliebige Variable und L und F beliebige Substitutionsfolgen und s eine beliebige Substitutionsbelegung und s(Bild(L)) und s(Bild(F)) sind variablenfreie Terme \\und Bild(L) $\cap$ Bild(F) = $\emptyset$ und B($\alpha$) \\ zeige: $[\exists x \alpha]_{L+F}^{s(L+F)}=[\exists x \alpha]_{L}^{s(L)}]_{F}^{s(F)}$ \\ a) Mit der Induktionsvoraussetzung folgt:\\ $[\alpha_{}^{s(...)}]_{}$= $\alpha_{+}^{s(...)}$= \\ b) Es gilt:\\ $[\exists x \alpha]_{L}^{s(L)}]_{F}^{s(F)}$= $[\exists x [\alpha_{}^{s(...)}]]_{F}^{s(F)}$=\\ $\exists x[ [\alpha_{}^{s(...)}]_{}^{s(...).})>}]$= \\ $\exists x [[\alpha_{}^{s(...)}]_{}^{s(...).})\setminus \{x\}]>}]$= $\quad$(Substitutionslemma 2) $\ref{SUBLEM2}$ \\ $\exists x [[\alpha_{}^{s(...)}]_{}]$=\\ $\exists x [[\alpha_{}^{s(...)}]_{}]$= \\ $\exists x [[\alpha_{}^{s(...)}]_{}]$= $\quad$(Beweishilfslemma 2)\\ $\exists x [[\alpha_{}^{s(...)}]_{<(Bild(F) \cap frei(\exists x \alpha)) \setminus (Bild(L) \cap frei(\exists x \alpha))>}]$= $\quad$(Beweishilfslemma 1)\\ $\exists x [[\alpha_{}^{s(...)}]_{}]$= $\quad$(siehe a))\\ $[\exists x \alpha]_{L+F}^{s(L+F)}=[\exists x \alpha]_{L}^{s(L)}]_{F}^{s(F)}$ \end{proof} \subsection{Substitutionslemma 6} $\label{SUBLEM6}$ x ist eine Variable, $\varphi$ ist eine Formel, t ist ein Term. Dann gilt:\\ x $\not \in$ frei($\varphi) \Rightarrow$ $\varphi_x^{t} = \varphi$ \begin{proof} ...\\ L:=(x) und F:=()=$\epsilon$\\ Dann gilt: Bild(L) $\cap$ frei($\varphi)$ = Bild(F) $\cap$ frei($\varphi) = \emptyset$ \\ Mit Substitutionslemma 1 folgt dann: \\ $\varphi_x^{t} = \varphi_{\epsilon}^{s(\epsilon)}=\varphi$ \end{proof} \subsection{Nicht-Frei-und-Äquivalent-Lemma} $\label{NFAE}$ x ist eine Variable, $\Phi$ ist eine Formel. Dann gilt:\\ x $\not \in$ frei($\Phi) \quad \Rightarrow \quad$ $\vdash \forall x \Phi \; \leftrightarrow \; \Phi$ und $\vdash \exists x \Phi \; \leftrightarrow \; \Phi$ \subsection{Leibnitzschen Ersetzbarkeitskriterium} $\sigma$ und $\tau$ sind Terme, x ist eine Variable und $\varphi$ eine Formel.\\ Wenn beide Substitutionen existieren, dann gilt:\\ $\sigma = \tau \quad \rightarrow \quad (\varphi_x^{\sigma} \leftrightarrow \varphi_x^{\tau})$ \begin{proof} (ohne) \\ \end{proof} \subsection{Ersetzbarkeitskriterium für äquivalente Ausdrücke} Wenn $\alpha$ dadurch aus $\beta$ hervorgeht, dass an beliebigen Stellen von $\beta$\\ die Teilformel $\sigma$ durch $\gamma$ ersetzt wird, dann gilt:\\ $\Sigma \vdash \sigma \leftrightarrow \gamma \quad \Longrightarrow \quad \Sigma \vdash \alpha \leftrightarrow \beta$ \subsection{Substitutionskorrolar} $\label{SUBKOR}$ $\Phi$ ist eine Formel, n eine Variable und T ein Term. Dann gilt: \\ $\vdash \phi_n^{T} \rightarrow (n=T \rightarrow \phi) \quad$ \\ \begin{proof} ... \\ Nach dem Leibnitzschen Ersetzbarkeitskriterium gilt für alle Terme $\sigma, \tau$ \\ und alle Formeln $\Phi$: \\ $\vdash \sigma = \tau \rightarrow \phi_n^{\sigma} \leftrightarrow\phi_n^{\tau} $\\ Setze: $\sigma=n$ und $\tau=T$, dann folgt: \\ $\vdash n=T \rightarrow (\phi_n^{n} \leftrightarrow \phi_n^{T}) \quad$ also\\ $\vdash n=T \rightarrow (\phi \leftrightarrow \phi_n^{T}) \quad$ (*)\\ Mit einer Wahrheitstafel sieht man: \\ $\vdash (\alpha \rightarrow (\beta \leftrightarrow \gamma)\quad .\rightarrow. \quad \gamma \rightarrow (\alpha \rightarrow \beta)) $ \\ Setze: $\alpha \equiv n=T$ und $\beta \equiv \varphi$ und $\gamma \equiv \phi_n^{T}$ \\ also \\ $\vdash n=T \rightarrow (\phi \leftrightarrow \phi_n^{T}) \quad .\rightarrow. \quad \phi_n^{T} \rightarrow (n=T \rightarrow \phi) \quad$ \\ Mit (*) folgt dann:\\ $\vdash \phi_n^{T} \rightarrow (n=T \rightarrow \phi) \quad$ \\ \end{proof} \chapter{Peano } \section{Definitionen} Das Peanosche Axiomensystem wird durch eine Sprache der Prädikatenlogik ersten Stufe formalisiert. Die Symbolmenge S dieser Sprache wird durch 2 Konstanten und 2 Funktionssymbole gebildet: S := $\{ \bar 0$, $\bar 1$, $\oplus$, $\otimes$ $\}$ \\ Für alle S-Modelle $\mathfrak{M}$ = ( M , $\bar 0^M$ , $\bar 1^M$ , $\oplus^M$, $\otimes^M$ von PA und alle z $\in \mathbb{N}$ wird definiert: \\ $\bar z^M = \bar 1^M \; \oplus^M$ ... $\oplus^M \; \bar 1^M \quad$z - Mal \\ M bedeutet dabei die Trägermenge und die Funktionssymbole zusammen mit den \\ hochgestellten M's bedeuten die zu den Funktionssymbolen zugehörigen Interpretationen. \\ Mit $\mathfrak{N}$ = ( $\mathbb{N}$ , 0, 1 , + , * ) wird das das Standardmodell (ein S-Modell) von PA bezeichnet. \\ Mit $\mathbb{N}$ werden dabei die interpretierten natürlichen Zahlen aus $\mathbb{N}$ bezeichnet. Also: \\ $\mathbb{N} = \{\bar 0^N, \bar 1^N, \bar 2^N, ...\}$ \\ wobei $\bar 0^N := 0, \bar 1^N := 1, \bar 2^N := 2$, usw. \section{Axiome des Peanoschen Axiomensystems} Voraussetzungen: \\ y kommt in einer beliebigen Formel P frei vor, t und s sind beliebige Terme.\\ \\ Axiomenschema Pax1:\\ Für alle Formeln A, in denen y frei vorkommt, sind die Formeln der folgenden Form Axiome:\\ $(A(\bar 0 )\land \forall y (A(y) \rightarrow A(y+1))) \; .\rightarrow. \; \forall y A(y)$\\ \\ Axiom Pax2: $\quad t \oplus \bar 1=s \oplus \bar 1 \rightarrow t=s$ \\ \\ Axiom Pax3: $\quad \neg(t \oplus \bar 1) = \bar 0$ \\ \\ Axiom Pax4: $\quad t=s \rightarrow t \oplus \bar 1 = s \oplus \bar 1$ \\ \\ Axiom Pax5: $\quad t \oplus \bar 0 = t$ \\ \\ Axiom Pax6: $\quad t \oplus (s \oplus \bar 1) = (t \oplus s) \oplus \bar 1$ \\ \\ Axiom Pax7: $\quad t \otimes \bar 0 = \bar 0$ \\ \\ Axiom Pax8: $\quad t \otimes (s \oplus \bar 1) = (t \otimes s) \oplus \bar 1$ \\ \\ Die Menge der Axiome des Peanoschen Axiomensystems wird mit PA abgekürzt. \\ \section{Metasprachliche Abkürzungen} 1) spezielle Terme \\ $\bar 2 := (\bar 1 \oplus \bar 1)$ \\ $\bar 3 := (\bar 2 \oplus 1) = (\bar 1 \oplus (\bar 1) \oplus \bar 1)$ \\ usw. \\ allgemein definiert man für alle n$>$1: \\ $\bar n := (\overline{n-1} \oplus \bar 1)$ \\ \\ 2) Kleiner-Relation\\ Hier gibt es in PA keine Kleiner-Relation bzw. keine Kleiner-Gleich-Relation.\\ Diese wird als metasprachliche Abkürzung wie folgt definiert: (wobei x eine Variable und $t_0$ und $t_1$ Terme sind) \\ $t_0 \le t_1 : \iff \exists x \; t_0 \oplus x = t_1$ \\ $t_0 < t_1 : \iff \neg (t_1 \le t_0)$ \\ also: \\ $t_0 < t_1 : \iff \neg (\exists z \; t_1 + z = t_0)$ \\ Definiere: $A := \neg (\exists z \; t_1 + z = t_0)$ \\ Zu der Symbolmenge von PA wird das Symbol $<$ hinzugehügt. Das ergibt die neue Symbolmenge: $S' := S \bigcup \{<\}$ \\ Nach dem Satz über die Definitionserweiterung folgt dann für jede Formel $\varphi$ mit der neuen Symbolmenge S' : \\ $PA \bigcup \{A\} \vdash \varphi \iff PA \vdash \varphi^{I} $ \\ wobei $\varphi^{I} $ die zu $\varphi$ zugehörige Formel ist, bei der die Ersetzung von $<$ durch \\ $\neg (\exists z \; t_1 + z = t_0)$ vorgenommen wird. \\ Das um das Symbol $<$ erweiterte Peanosche Axiomensystem mit PA' bezeichnet. \\ Um unnötige Schreibarbeit zu vermeiden wird im Folgenden oft statt PA' auch PA geschrieben.\\ \\ 3) $\Sigma_1$ Formel \\ Eine $\Sigma_1$ Formel ist eine Formel in NNF (Negationsnormalform), was bedeutet, dass in ihr nur Negationen $\neg$ vor den Primformeln vorkommen dürfen. \\Außerdem dürfen nur beschränkte Allquantoren der Form $\forall x$m \\ $\implies n+1-m \neq 0$ Nach einem vorigen Lemma folgt dann: \\ $PA \vdash \neg(\overline{n+1-m} = \bar 0) \implies PA \vdash \neg(\overline{n+1-m} \oplus \bar m = \bar 0 \oplus \bar m) \implies$ \\ $PA \vdash \neg (\overline{n+1-m+ m} = \bar m) \implies PA \vdash \neg (\overline{n+1 } = \bar m) $\\ \\ Fall2: m$>$n+1 \\ $\implies m-(n+1) \neq 0$ Nach einem vorigen Lemma folgt dann: \\ $PA \vdash \neg(\overline{m-(n+1)} = \bar 0) \implies PA \vdash \neg(\overline{m-(n+1)} \oplus \overline{n+1} = \bar 0 \oplus \overline{n+1}) \implies$ \\ $PA \vdash \neg (\overline{m-(n+1)+(n+1)} = \overline{n+1}) \implies PA \vdash \neg (\bar m = \bar{n+1} ) \implies$ \\ $PA \vdash \neg (\overline{n+1} = \bar m) $\\ \end{proof} \subsection{Lemma} Für alle z $\in \mathbb{N}$ gilt:$\quad PA \vdash \bar z < \overline{z+1} $ \\ d.h. $\bar 0 < \bar 1 < \bar 2 < ... $ \\ \begin{proof} zeige: $PA \vdash \exists x \; \neg (z \oplus x=z \oplus \bar 1) $\\ $PA \vdash z \oplus x = z \oplus \bar 1 \rightarrow z \oplus x = z \oplus \bar 1 $ \\ $PA \vdash z \oplus x = z \oplus \bar 1 \rightarrow \exists x (z \oplus x = z \oplus \bar 1) $ (Ph) \\ $PA \vdash z \oplus \bar 1 = z \oplus \bar 1 \rightarrow \exists x (z \oplus x = z \oplus \bar 1) $ (Sub) \\ $PA \vdash \exists x (z \oplus x = z \oplus \bar 1) $ (MP) \\ \end{proof} \subsection{Kleiner-Isomorhismus-Lemma} $\label{KIL}$ Für alle a,b $\in \mathbb{N}$ gilt: $a$ 0 mit b=a+r, also: \\ PA$\vdash \bar b = \bar a \oplus \bar r$\\ Es gilt:\\ PA $\vdash \neg t \oplus \bar1 = \bar 0 \rightarrow \neg t \oplus \bar1 = \bar 0$\\ Also mit (Gv)\\ PA $\vdash (\forall t \; \neg t \oplus \bar1 = \bar 0) \rightarrow \neg t \oplus \bar1 = \bar 0$\\ Mit $\ref{PAF2}$ und dem Ersetzbarkeitskriterium für äquivalente Ausdrücke folgt:\\ PA $\vdash (\forall t \; \neg t \oplus \bar1 = \bar 0) \rightarrow \neg t \oplus \bar1 \oplus \bar b = \bar 0 \oplus \bar a \oplus \bar r$\\ Durch Substitution (Sub) t/t$\oplus \overline{r-1}$ folgt: \\ PA $\vdash (\forall t \; \neg t \oplus \bar1 = \bar 0) \rightarrow \neg t \oplus \overline{r-1} \oplus \bar1 \oplus \bar b = \bar 0 \oplus \bar a \oplus \bar r \quad \Longrightarrow$\\ PA $\vdash (\forall t \; \neg t \oplus \bar1 = \bar 0) \rightarrow \neg t \oplus \bar b = \bar a $\\ Also mit (Gh)\\ PA $\vdash (\forall t \; \neg t \oplus \bar1 = \bar 0) \rightarrow \forall t \; \neg t \oplus \bar b = \bar a $\\ und damit:\\ PA $\vdash \forall t \; \neg t \oplus \bar b = \bar a $\\ \end{proof} \subsection{Lemma Kürzungsregel in Ungleichungen} $PA \vdash \forall x \forall y \forall z \; (x$0 gilt:$\quad PA \vdash \bar 0 < \bar z$ \begin{proof} (Induktion über die natürlichen Zahlen) \\ $PA \vdash \bar 0 < \bar z \quad \iff $ \\ $PA \vdash \neg \exists x \; \bar z \oplus x = \bar 0 \quad \iff $ \\ $PA \vdash \forall x \; \neg \bar z \oplus x = \bar 0 $ \\ $B(z) :\iff PA \vdash \forall x \; \neg \bar z \oplus x = \bar 0 $ \\ Zeige B(z) für alle z$>$0 \\ 1) Zeige B(1), also: \\ $PA \vdash \forall x \; \neg \bar 1 \oplus x = \bar 0 $ \\ Dies ist aber ein Axiom aus PA \\ \\ 2) Induktionsvoraussetzung sei B(z) und Induktionsbehauptung B(z+1) \\ Zeige B(z+1), also: \\ $PA \vdash \forall x \; \neg \overline{z+1} \oplus x = \bar 0 $ \\ Es gilt: \\ $PA \vdash \neg \bar z \oplus x = \bar 0 \rightarrow \neg \bar z \oplus x = \bar 0 $ \\ Durch vordere Generalisierung (Gv) folgt: \\ $PA \vdash \forall x \; \neg \bar z \oplus x = \bar 0 \; .\rightarrow. \; \neg \bar z \oplus x = \bar 0 $ \\ Durch Substitution (Sub) x/x $\oplus \bar 1 $ folgt: \\ $PA \vdash \forall x \; \neg \bar z \oplus x = \bar 0 \; .\rightarrow. \; \neg \bar z \oplus x \oplus \bar 1 = \bar 0 \quad \Rightarrow$ \\ $PA \vdash \forall x \; \neg \bar z \oplus x = \bar 0 \; .\rightarrow. \; \neg \overline{z+1} \oplus \bar x = \bar 0$ \\ Es gilt aber nach Induktionsvoraussetzung: \\ $PA \vdash \forall x \; \neg \bar z \oplus x = \bar 0 $ \\ Dann folgt mit Modus Ponens (MP): \\ $PA \vdash \neg \overline{z+1} \oplus \bar x = \bar 0$ \\ also: \\ $PA \vdash \forall x \; \neg \overline{z+1} \oplus \bar x = \bar 0$ \\ \end{proof} \subsection{Lemma} Für alle $z>0$ gilt: \\ PA $\vdash n=\overline{z-1} \; \rightarrow \; n<\bar z $ \begin{proof} (mit Leibnitzschem Ersetzbarkeitskriterium)\\ PA $\vdash n=\overline{z-1} \; \rightarrow \; n<\bar z \quad \iff$\\ PA $\vdash n=\overline{z-1} \; \rightarrow \; \neg \exists t \; \bar z \oplus t = n \quad \iff$\\ PA $\vdash n=\overline{z-1} \; \rightarrow \; \forall t \; \neg \bar z \oplus t = n \quad \iff$\\ (denn nach dem Leibnitzschen Ersetzbarkeitskriterium folgt: \\ $\vdash \sigma=\tau \rightarrow A_x^{\sigma} \iff \vdash \sigma=\tau \rightarrow A_x^{\tau}$ \; )\\ PA$\vdash n=\overline{z-1} \; \rightarrow \; \forall t \; \neg \bar z \oplus t = \overline{z-1} \quad \iff$\\ PA$\vdash n=\overline{z-1} \; \rightarrow \; \forall t \; \neg \overline{z-1} \oplus \bar 1 \oplus t = \overline{z-1} \quad \iff$\\ PA$\vdash n=\overline{z-1} \; \rightarrow \; \forall t \; \neg t \oplus \bar 1 = \bar 0$\\ genügt: \\ PA$\vdash \forall t \; \neg t \oplus \bar 1 = \bar 0 \quad \iff$\\ PA$\vdash \neg t \oplus \bar 1 = \bar 0 $\\ Diese letzte Formel ist aber ein Axiom in PA \end{proof} \subsection{Lemma} Für alle $z>0$ gilt: \\ PA $\vdash n<\overline{z-1} \rightarrow n < \bar z $ \begin{proof} ....\\ PA $\vdash n<\overline{z-1} \rightarrow n < \bar z \quad \iff$ \\ PA $\vdash \neg \exists t \; \overline{z-1} \oplus t = n \rightarrow \neg \exists s \; \bar z + s= n \quad \iff$ \\ PA $\vdash \exists s \; \bar z + s= n \rightarrow \exists t \; \overline{z-1} \oplus t = n \quad \iff$ \\ Es gilt aber: \\ PA $\vdash \overline{z-1}+t=n \rightarrow \overline{z-1}+t=n$ \\ Durch hintere Parikularisierung (Ph) folgt: \\ PA $\vdash \overline{z-1}+t=n \rightarrow \exists t \; \overline{z-1}+t=n$ \\ Durch Substitution (Sub) t/ $\bar 1 \oplus s$ folgt: \\ PA $\vdash \overline{z-1}+\bar 1 \oplus s=n \rightarrow \exists t \; \overline{z-1}+t=n$ \\ also: \\ PA $\vdash \bar z \oplus s=n \rightarrow \exists t \; \overline{z-1}+t=n$ \\ Durch vordere Parikularisierung (Pv) folgt : \\ PA $\vdash \exists s \; \bar z \oplus s=n \rightarrow \exists t \; \overline{z-1}+t=n$ \\ \end{proof} \subsection{Lemma} Für alle $z>0$ gilt: \\ PA $\vdash \forall n(n<\bar z \; \leftrightarrow \; n<\overline{z-1} \lor n=\overline{z-1}) $ \begin{proof} (Induktion über die natürlichen Zahlen)\\ "$\Rightarrow$"\\ $B(z) :\iff PA \vdash n<\bar z \; \rightarrow \; n<\overline{z-1} \lor n=\overline{z-1} $\\ 1) Zeige B(1) \\ $PA \vdash n<\bar 1 \; \rightarrow \; n<\bar 0 \lor n=\bar 0 $\\ Dies gilt nach dem vorigen Lemma.\\ \\ 2) Induktionsvoraussetzung sei B(z) und Induktionsbehauptung B(z+1) \\ Zeige B(z+1), also: \\ $PA \vdash n<\overline{z+1} \; \rightarrow \; n<\bar{z} \lor n=\bar{z} $\\ Definiere dazu: \\ $A(n) \; \equiv \; n<\overline{z+1} \; \rightarrow \; n<\bar{z} \lor n=\bar{z} $\\ \\ 2.1) Zeige $PA \vdash A(0) $ also\\ $PA \vdash \bar 0<\overline{z+1} \; \rightarrow \; \bar 0<\bar{z} \lor \bar 0=\bar{z} $\\ Fall1: z=0\\ zeige: $PA \vdash \bar 0<\bar 1 \; \rightarrow \; \bar 0<\bar0 \lor \bar 0=\bar0 $\\ genügt: $PA \vdash \bar 0<\bar0 \lor \bar 0=\bar0 $\\ genügt: $PA \vdash \bar 0=\bar0 $\\ Fall2: z $>$0\\ Nach einem vorigem Lemma gilt:\\ $PA \vdash \bar 0 < z \quad \Longrightarrow $ \\ $PA \vdash \bar 0 < z \lor \bar 0 =z \quad \Longrightarrow $ \\ $PA \vdash \bar 0 < \overline{z+1} \rightarrow \bar 0 < z \lor \bar 0 =z$ \\ \\ 2.2) Zeige $PA \vdash A(n) \rightarrow A(n+1)$ also \\ $PA \vdash n<\overline{z+1} \; \rightarrow \; n<\bar{z} \lor n=\bar{z} \quad .\rightarrow. \; n+1<\overline{z+1} \; \rightarrow \; n+1<\bar{z} \lor n+1=\bar{z} $\\ $\iff$ \\ $PA \vdash n<\overline{z+1} \; \rightarrow \; n<\bar{z} \lor n=\bar{z} \quad .\rightarrow. $ \\ $n+1<\overline{z+1} \; \rightarrow \; n+1<\overline{z-1+1} \lor n+1=\overline{z-1+1} $\\ $\iff$ \\ $PA \vdash n<\overline{z+1} \; \rightarrow \; n<\bar{z} \lor n=\bar{z} \quad .\rightarrow. $ \\ $n+1<\bar z \oplus \bar 1 \; \rightarrow \; n+1<\overline{z-1} \oplus \bar 1 \lor n+1=\overline{z-1} \oplus \bar 1 $\\ $\iff$ \\ $PA \vdash n<\overline{z+1} \; \rightarrow \; n<\bar{z} \lor n=\bar{z} \quad .\rightarrow. $ \\ $n<\bar z \; \rightarrow \; n<\overline{z-1} \lor n=\overline{z-1} $\\ genügt:\\ $PA \vdash n<\bar z \; \rightarrow \; n<\overline{z-1} \lor n=\overline{z-1} $\\ Dies gilt aber nach Induktionsvoraussetzung B(z) \end{proof} \subsection{Oder-Endlichkeits-Lemma} $\label{OEL}$ Für alle z $>$0 gilt: \\ PA $\vdash \forall n(n<\bar z \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\overline{z-1})$ \begin{proof} (Induktion über die natürlichen Zahlen)\\ Es gilt: \\ PA $\vdash \forall n(n<\bar z \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\overline{z-1}) \quad \iff $\\ PA $\vdash n<\bar z \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\overline{z-1}$\\ Es genügt also zu zeigen: \\ PA $\vdash n<\bar z \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\overline{z-1}$\\ Definiere:\\ $B(z) :\iff PA \vdash n<\bar z \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\overline{z-1}$\\ \\ 1) Zeige B(1) also \\ $PA \vdash n<\bar 1 \; .\leftrightarrow. \; n=\bar 0 $\\ Dies gilt nach einem vorigen Lemma. \\ \\ 2) Induktionsvoraussetzung sei B(z) und Induktionsbehauptung B(z+1) \\ Zeige B(z+1), also: \\ $PA \vdash n<\overline{z+1} \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\bar z$ \\ Es gilt Mit der Induktionsvoraussetzung B(z): \\ $PA \vdash n<\bar z \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\overline{z-1} \quad \Longrightarrow $\\ $PA \vdash n<\bar z \lor n=z \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\overline{z-1} \lor n=z $\\ Mit einem vorigen Lemma folgt: \\ $PA \vdash n<\overline{z+1} \; .\leftrightarrow. \; n=\bar 0 \; \lor$ ... $\lor \; n=\overline{z-1} \lor n=z\\$ \end{proof} \subsection{All-Endlichkeits-Lemma} $\label{AEL}$ Für alle z$>$0 gilt: \\ PA $\vdash \forall n(n<\bar z \rightarrow \phi) \iff$ Für alle a mit $0 \le a \le z-1$ gilt: PA $\vdash \phi_n^{\bar a}$ \\ \\ andere Schreibweise:\\ \\ PA $\vdash \forall n(n<\bar z \rightarrow \phi) \iff$ PA $\vdash \phi_n^{\bar 0}$ und ... und PA $\vdash \phi_n^{\overline{z-1}}$ \begin{proof} (2 Teile) \\ "$\Rightarrow$"\\ Es sei: PA $\vdash \forall n(n<\bar z \rightarrow \phi)$ \\ $\implies PA \vdash n<\bar z \rightarrow \phi$ \\ Es gilt aber das Oder-Endlichkeits-Lemma, also $\ref{OEL}$: \\ $PA \vdash (n= \bar 0 \; \lor$ ... $ \lor\; n= \overline{z-1}) \leftrightarrow n< \bar z \quad$ also \\ $PA \vdash (n= \bar 0 \; \lor$ ... $\lor \; n= \overline{z-1}) \rightarrow \phi $\\ Daraus folgt mit Substitution:\\ $PA \vdash (\bar 0= \bar 0 \; \lor$ ... $\lor \; \bar 0= \overline{z-1}) \rightarrow \phi_n^{\bar 0} $\\ und ... und\\ $PA \vdash (\overline{z-1}= \bar 0 \; \lor$ ... $\lor \; \overline{z-1}= \overline{z-1}) \rightarrow \phi_n^{\overline{z-1}} $\\ $ \implies $\\ $PA \vdash \phi_n^{\bar 0} \quad$ und ... und $\quad PA \vdash \phi_n^{\overline{z-1}} $\\ \\ "$\Leftarrow$"\\ 1) \\ Nach dem Substitutionskorrolar, also $\ref{SUBKOR}$ gilt: \\ $\vdash \phi_n^{T} \rightarrow (n=T \rightarrow \phi) \quad$ \\ Setze: $T=\bar 0, T=\bar 1, T=\bar 2$, usw, dann folgt: \\ $PA \vdash \phi_n^{\bar 0} \rightarrow (n= \bar 0 \rightarrow \phi) $\\ $PA \vdash \phi_n^{\bar 1} \rightarrow (n= \bar1 \rightarrow \phi) $\\ ...\\ $PA \vdash \phi_n^{\overline{z-1}} \rightarrow (n= \overline{z-1} \rightarrow \phi) $\\ \\ 2) \\ Es sei: $PA \vdash \phi_n^{\bar 0}$ und ... und PA $\vdash \phi_n^{\overline{z-1}} $\\ Mit dem Substitutionskorrolar, also $\ref{SUBKOR}$ folgt dann: \\ $PA \vdash n= \bar 0 \rightarrow \phi$ und ... und PA $\vdash n= \overline{z-1} \rightarrow \phi$\\ $\implies PA \vdash n= \bar 0 \rightarrow \phi \land \text{ ... } \land n= \overline{z-1} \rightarrow \phi $\\ $\implies PA \vdash (n= \bar 0 \lor \text{ ... } \lor n= \overline{z-1}) \rightarrow \phi $\\ Es gilt aber: \\ $PA \vdash (n= \bar 0 \lor \text{ ... } \lor n= \overline{z-1}) \leftrightarrow n< \bar z $\\ $\implies$ PA$\vdash n