% !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 $<L,M>$ bzw. nur durch $<M>$ wenn L im Kontext klar ist.\\ 
Wenn M=$\emptyset$, dann  $<L,M>$:=$\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]_{<B(L) \cap frei(\exists x \varphi),L>}^{s(<B(L) \cap frei(\exists x \varphi),L>)}$ \\  \\
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_{<Bild(z)\cap frei(\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_{<Bild(L) \cap frei (\exists x \alpha)>}^{s(...)}$)=
frei$(\alpha) \setminus$ Bild$(<Bild(L) \cap$frei$(\exists x \alpha)>)$=
frei$(\alpha) \setminus$ (Bild(L)$\cap$frei$(\exists x \alpha))$
also:\\
frei($\alpha_{<Bild(L) \cap frei (\exists x \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_{<Bild(L) \cap frei (\exists x \alpha)>}^{s(...)}])$=
frei($[\alpha_{<Bild(L) \cap frei (\exists x \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]_{<Bild(L)\cap frei(\exists x \alpha)>}^{s(...)} $ \\ 
$[\exists x \alpha]_{F}^{s(F)} = \exists x [\alpha]_{<Bild(F)\cap frei(\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: \\
$<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]_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}$  und 
$[\exists x \alpha]_{F}^{s(F)} = \exists x [\alpha]_{<Bild(F) \cap frei(\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_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}]_{<Bild(F) \cap frei(\exists x \alpha) >}$=
$\alpha_{<Bild(L) \cap frei(\exists x \alpha)>+<Bild(F) \cap frei(\exists x \alpha) >}^{s(...)}$= \\
b) Es gilt:\\ 
$[\exists x \alpha]_{L}^{s(L)}]_{F}^{s(F)}$=
$[\exists x [\alpha_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}]]_{F}^{s(F)}$=\\
$\exists x[ [\alpha_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}]_{<Bild(F) \cap frei(\exists x \alpha_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...).})>}]$= \\
$\exists x [[\alpha_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}]_{<Bild(F) \cap [frei(\alpha_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...).})\setminus \{x\}]>}]$=  $\quad$(Substitutionslemma 2) $\ref{SUBLEM2}$ \\
$\exists x [[\alpha_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}]_{<Bild(F) \cap [(frei(\alpha)\setminus (Bild(L) \cap frei(\exists x \alpha))) \setminus \{x\}]>}]$=\\
$\exists x [[\alpha_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}]_{<Bild(F) \cap [(frei(\alpha)\setminus \{x\}\setminus (Bild(L) \cap frei(\exists x \alpha)) ]>}]$= \\
$\exists x [[\alpha_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}]_{<Bild(F) \cap [frei(\exists x \alpha)\setminus (Bild(L) \cap frei(\exists x \alpha)) ]>}]$= $\quad$(Beweishilfslemma 2)\\
$\exists x [[\alpha_{<Bild(L) \cap frei(\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_{<Bild(L) \cap frei(\exists x \alpha)>}^{s(...)}]_{<Bild(F) \cap frei(\exists x \alpha) >}]$= $\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<t$ vorkommen.
Dabei ist t ein Term und $\forall x<t \; \phi$ ist eine Abkürzung für $\forall x (x<t \rightarrow \phi)$ 
\\Man kann zeigen, daß es zu jeder PA-Formel $\phi$  (falls $\phi$ einen Allquantor enthält, muß er beschränkt sein) eine zu $\phi$ äquivalente Formel aus $\Sigma_1$ gibt.



\newpage
\section{Lemmata}

Das nachfolgende Axiomenschema-Lemma wird in vielen Beweisen verwendet.
\subsection{Axiomenschema-Lemma}
Wenn $PA \vdash A(\bar 0)$ und $PA \vdash A(y) \rightarrow A(y+1)$, dann $PA \vdash A(y)$ 


\begin{proof} ....\\
$PA \vdash A(\bar 0)$ und $PA \vdash (A(y) \rightarrow A(y+1) \quad \Longrightarrow$ \\ 
$PA \vdash A(\bar 0)$ und $PA \vdash \forall y (A(y) \rightarrow A(y+1)) \quad \Longrightarrow$ \\ 
$PA \vdash A(\bar 0) \land  \forall y (A(y) \rightarrow A(y+1)) \quad $ (*) \\
nach dem obigen Axiomenschema ist \\ 
$(A(\bar 0 )\land \forall y (A(y) \rightarrow A(y+1))) \; .\rightarrow. \; \forall y A(y)$\\ 
ein Axiom, also:\\
$PA \vdash (A(\bar 0 )\land \forall y (A(y) \rightarrow A(y+1))) \; .\rightarrow. \; \forall y A(y) \quad $ (**) \\ 
Aus (*) und (**) folgt: \\
$PA \vdash  \forall y A(y)$ \\
also: \\
$PA \vdash A(y)$  \\
\end{proof} 

Alle Sätze der elementaren Zahlentheorie lassen sich mit dem PA und den zugehörigen Schlussweisen ableiten. Einige davon werden hier bewiesen, andere werden nur zitiert:
\subsection{Einige unbewiesene Lemmata}
\subsubsection{}  $\label{PAL1}$
$PA \vdash x \oplus y= y \oplus x  $ 
\subsubsection{}  $\label{PAL2}$
$PA \vdash (x \oplus y) \oplus z= x \oplus (y \oplus z)  $ 
\subsubsection{}  $\label{PAL3}$
$PA \vdash x_1=y_1 \land x_2=y_2 \; .\rightarrow. \; x_1 \oplus x_2=y_1 \oplus y_2$ 
\subsubsection{}  $\label{PAL4}$
$PA \vdash x_1=y_1 \rightarrow (x_2=y_2 \; .\leftrightarrow. \; x_1 \oplus x_2=y_1 \oplus y_2)$
\subsubsection{}  $\label{PAL5}$
$PA \vdash x=y \land y=z \; .\rightarrow. \; x=z$ \\ \\
Bemerkungen:\\
1) Aus den Lemmata folgen sofort weitere, wie z.B: \\
PA$\vdash x_1=y_1$ und $PA \vdash x_2=y_2  \; \Longrightarrow \; PA \vdash x_1 \oplus x_2=y_1 \oplus y_2$ \\
2) Mit Hilfe der Substitutionsregel gelten diese Behauptungen auch für beliebige Terme, also z.B: für beliebige Terme $t_1, t_2$\\
PA$\vdash t_1 \oplus t_2= t_2 \oplus g  $ \\


\subsection{einfache Folgerungen aus den Schlussregeln und Axiomen}
\subsubsection{}  $\label{PAF1}$
PA $\vdash x_1=y_1$ und $PA \vdash x_2=y_2 \Longrightarrow PA \vdash x_1 \oplus x_2=y_1 \oplus y_2 $

\subsubsection{}  $\label{PAF2}$
PA $\vdash x_1=y_1 \Longrightarrow$ PA$\vdash (x_2=y_2 \; .\leftrightarrow. \; x_1 \oplus x_2=y_1 \oplus y_2)$

\begin{proof} ... \\
Es sei:\\
1) \\
$PA \vdash x_1=y_1$ und $PA \vdash x_2=y_2$, also gibt es eine PA-Beweisfolge\\  
...., $x_1=y_1, x_2=y_2, x_1=y_1 \land x_2=y_2, x_1=y_1 \land x_2=y_2 \rightarrow x_1 \oplus x_2=y_1 \oplus y_2, \\ x_1 \oplus x_2=y_1 \oplus y_2$
\end{proof}

\subsection{Lemma Kürzungsregel in Gleichungen}
$x=y \leftrightarrow  x \oplus z = y \oplus z$

\begin{proof} (ohne) \\
\end{proof}

\subsection{Lemma}
$n \in \mathbb{N}$  und  $n \neq 0 \implies PA \vdash \neg(n = 0) $

\begin{proof} (Induktion über die natürlichen Zahlen) \\
B(n):  $\Leftrightarrow \quad  n \in \mathbb{N}$  und  n $\neq 0 \implies PA \vdash \neg(n = 0) $ \\
1) zeige B(0), also:  \\
$0 \in \mathbb{N} \text{ und } 0 \neq 0 \implies PA \vdash \neg(n = 0) \\$
trivial, da Voraussetzung falsch\\ \\
2) Zeige: B(n) $\implies B(n+1)$, also \\
$n+1 \in \mathbb{N}$  und  $n+1 \neq 0 \implies PA \vdash \neg(n+1 = 0)$ 
\end{proof}
\subsection{Lemma}
$n \in \mathbb{N}$  und $\bar 0 \neq n \implies PA \vdash \neg(0 = n)$

\begin{proof} (Induktion über die natürlichen Zahlen) \\
analog zum vorigen Lemma
\end{proof}


\subsection{Lemma} $\label{NATADD}$
Für alle n,m $\in \mathbb{N} \quad$ PA $\vdash \overline{n+m} = \bar n \oplus \bar m $

\begin{proof} (Induktion über die natürlichen Zahlen)\\
B(n): $\Leftrightarrow \quad$ Für alle m $\in \mathbb{N} \quad$ PA $\vdash \overline{n+m} = \bar n \oplus \bar m$ \\
1) zeige B(0), also: \\
Für alle m $\in \mathbb{N} \quad$ PA $\vdash \overline{0+m} = \bar 0 \oplus \bar m \quad \iff$ \\
Für alle m $\in \mathbb{N} \quad   \bar m = \bar  m$ \\ \\
2) Zeige: B(n) $\implies B(n+1)$, also \\
Für alle m $\in \mathbb{N} \quad$ PA $\vdash \overline{(n+1)+m} = \overline{n+1} \oplus \bar m$\\
Nach Ind. Vor gilt: \\
$PA \vdash \overline{n+(m+1)} = \bar n \oplus \overline{m+1}  \quad \iff $\\
$PA \vdash \overline{(n+1)+m} = \bar n \oplus \bar m \oplus \bar 1  \quad \iff $\\
$PA \vdash \overline{(n+1)+m} = (\bar n \oplus \bar 1)  \oplus \bar m  \quad \iff $\\
$PA \vdash \overline{(n+1)+m} = \overline{n+1} \oplus \bar m) $\\
\end{proof}


\newpage
\subsection{Lemma} $\label{UNGL}$ 
Für alle n,m $\in \mathbb{N} \quad  n \neq m \implies PA \vdash \neg(\bar n = \bar m) $

\begin{proof} (Induktion über die natürlichen Zahlen) \\
B(n): $\Leftrightarrow \quad \text{Für alle m} \in \mathbb{N} \quad  n \neq m \implies PA \vdash \neg(n = m)$\\
1) zeige B(0), also: \\
Für alle m $\in \mathbb{N} \quad  0 \neq m \implies PA \vdash \neg(0 = m)$\\
Dies gilt nach einem vorigen Lemma 1' \\ \\
2) Zeige: B(n) $\implies B(n+1)$, also \\
Für alle m $\in \mathbb{N} \quad  n+1 \neq m \implies PA \vdash \neg(n+1 = m) $\\
Fall1: n+1$>$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<b \Longrightarrow \bar a < \bar b$ \\

\begin{proof} .... \\
Zeige: PA$\vdash \neg \exists t \;  \bar b+t=\bar a$ \\
gleichbedeutend mit :  PA$\vdash \forall t \;  \neg  \bar b+t=\bar a$ \\
Sei a$<$ b.\\
Dann existiert ein r$>$ 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<y \leftrightarrow x \oplus z <y \oplus z) $ 

\begin{proof} (2 Richtungen)\\
"$\Rightarrow$" \\
$PA \vdash x<y \rightarrow x \oplus z <y \oplus z  \quad \iff$ \\
$PA \vdash \neg \exists s \; y \oplus s=x \rightarrow \neg \exists t \; y \oplus z \oplus t = x \oplus z  \quad \iff$ \\
$PA \vdash  \exists t \; y \oplus z \oplus t = x \oplus z \rightarrow \exists s \; y \oplus s=x $ \\
Es gilt aber: \\
$PA \vdash y \oplus s=x \rightarrow y \oplus s=x $ \\
Mit (Ph) folgt: \\
$PA \vdash y \oplus s=x \rightarrow \exists s \; y \oplus s=x $ \\
Mit (Sub) s/t folgt: \\
$PA \vdash y \oplus t=x \rightarrow \exists s \; y \oplus s=x $ \\
also: \\
$PA \vdash y \oplus t \oplus z=x \oplus z \rightarrow \exists s \; y \oplus s=x $ \\
Mit (Pv) folgt: \\
$PA \vdash \exists t \; y \oplus t \oplus z=x \oplus z \; .\rightarrow. \;  \exists s \; y \oplus s=x $ \\ \\
"$\Leftarrow$" \\
$PA \vdash x \oplus z <y \oplus z  \rightarrow x<y  \quad \iff$ \\
$PA \vdash \neg \exists s \; y \oplus z \oplus s = x \oplus z  \rightarrow \neg \exists t \; y \oplus t = x$ \\
Es gilt aber: \\
$PA \vdash y \oplus t=x \rightarrow y \oplus t=x $ \\
Mit (Ph) folgt: \\
$PA \vdash y \oplus t=x \rightarrow \exists t \; y \oplus t=x $ \\
Mit (Sub) t/s folgt: \\
$PA \vdash y \oplus s=x \rightarrow \exists t \; y \oplus t=x $ \\
also: \\
$PA \vdash y \oplus s \oplus z=x \oplus z \rightarrow \exists t \; y \oplus t=x $ \\
Mit (Pv) folgt: \\
$PA \vdash \exists s \; y \oplus s \oplus z=x \oplus z \rightarrow \exists t \; y \oplus t=x $ \\
\end{proof}


\subsection{Lemma}
$\quad PA \vdash x<\bar 1 \leftrightarrow x=\bar 0$ 

\begin{proof} (2 Richtungen) \\
"$\Rightarrow$" \\
1) zeige:  $PA \vdash \exists t \; t=x $\\
Es gilt: \\
$PA \vdash t=x \rightarrow t=x$ \\
Mit (Ph) folgt:\\
$PA \vdash t=x \rightarrow \exists t \; t=x$ \\
Mit (Sub) t/x folgt:\\
$PA \vdash x=x \rightarrow \exists t \; t=x$ \\
Mit Modus Ponens (MP) folgt:\\
$PA \vdash \exists t \; t=x$ \\ \\
2) \\
$\quad PA \vdash x<\bar 1 \rightarrow x=\bar 0 \quad \iff$ \\
$\quad PA \vdash (\neg \exists t \; \bar 1 \oplus t= x) \rightarrow x=\bar 0 $ \\
Definiere dazu: \\
$A(x) \equiv  \quad PA \vdash (\neg \exists t \; \bar 1 \oplus t= x) \rightarrow x=\bar 0 $ \\ \\
2.1) Zeige PA $\vdash A(0)$, also: \\
$PA \vdash (\neg \exists t \; \bar 1 \oplus t= \bar 0) \rightarrow \bar 0=\bar 0 $ \\
genügt: \\
$PA \vdash \bar 0=\bar 0 $ \\ \\
2.2) Zeige PA $\vdash A(n) \rightarrow A(n+1)$, also:\\
$\quad PA \vdash (\neg \exists t \; \bar 1 \oplus t= x) \rightarrow x=\bar 0 \; .\rightarrow. \;
(\neg \exists t \; \bar 1 \oplus t= x \oplus \bar 1) \rightarrow x \oplus \bar 1=\bar 0 \; \quad \iff $\\
$\quad PA \vdash (\neg \exists t \; \bar 1 \oplus t= x) \rightarrow x=\bar 0 \; .\rightarrow. \;
(\neg \exists t \; t=x) \rightarrow x \oplus \bar 1=\bar 0 \quad \iff $\\
$\quad PA \vdash (\neg \exists t \; \bar 1 \oplus t= x) \rightarrow x=\bar 0 \; .\rightarrow. \;
(\neg x \oplus \bar 1=\bar 0) \rightarrow \exists t \; t=x $\\ 
genügt:\\
$\quad PA \vdash \neg x \oplus \bar 1=\bar 0 \rightarrow \exists t \; t=x $\\ 
genügt:\\
$\quad PA \vdash \exists t \; t=x $\\  \\
"$\Leftarrow$" \\
1) zeige:  $PA \vdash x=\bar 0 \; .\rightarrow. \; \neg \exists t \; \bar 1 \oplus t=x $\\
Für alle Terme $\sigma, \tau$ und alle Formeln $\alpha$ gilt: \\
$\vdash \sigma = \tau \rightarrow \phi_x^{\sigma} \leftrightarrow\phi_x^{\tau} $\\
Setze: $\sigma=x$ und $\tau=\bar 0$, dann folgt:  \\
$\vdash x=\bar 0 \rightarrow (\phi_x^{x} \leftrightarrow \phi_x^{\bar 0}) \quad$ also\\
$\vdash x=\bar 0 \rightarrow (\phi \leftrightarrow \phi_x^{\bar 0}) \quad$ (*)\\
Mit einer Wahrheitstafel sieht man:  \\
$\vdash (\alpha \rightarrow (\beta \leftrightarrow \gamma)\quad .\rightarrow. \quad \gamma \rightarrow (\alpha \rightarrow \beta)) $ \\
also auch speziell: \\
$PA \vdash (\alpha \rightarrow (\beta \leftrightarrow \gamma)\quad .\rightarrow. \quad \gamma \rightarrow (\alpha \rightarrow \beta)) $ \\
Setze:
$\alpha \equiv x=\bar 0$ und $\beta \equiv \varphi$ und $\gamma \equiv \phi_x^{\bar 0}$ \\
also \\
$\vdash x=\bar 0 \rightarrow (\phi \leftrightarrow \phi_x^{\bar 0}) \quad  .\rightarrow. \quad
\phi_x^{\bar 0} \rightarrow (x=\bar 0 \rightarrow \phi) \quad$ \\
Mit (*) folgt dann:\\
$\vdash \phi_x^{\bar 0} \rightarrow (x=\bar 0 \rightarrow \phi) \quad$ \\
Setze: $\phi \equiv \neg \exists t \; \bar 1 \oplus t=x  \quad \Longrightarrow$\\
$PA \vdash \neg \exists t \; \bar 1 \oplus t=\bar 0 \; .\rightarrow. \;  (x=\bar 0 \rightarrow 
\neg \exists t \; \bar 1 \oplus t=x)    \quad \Longrightarrow$\\
Da gilt (Axiom): $PA \vdash \neg \exists t \; \bar 1 \oplus t=\bar 0$ folgt mit (MP) \\
$PA \vdash x=\bar 0 \rightarrow \neg \exists t \; \bar 1 \oplus t=x$\\
\end{proof}


\subsection{Lemma}
Für alle z$>$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<z \rightarrow \phi  $\\
$\implies$
PA $\vdash \forall n(n<z \rightarrow \phi)$ \\
\end{proof}



\newpage
\section{PA-Wahrheit und Beweisbarkeit}
\subsection{Definition}
$\Sigma_1$- Formeln sind PA-Zeichenfolgen, die man durch endlichmalige Anwendung der folgenden Regeln erhalten kann:\\
1) Jede Primformel ist eine $\Sigma_1$-Formel.\\
2) Wenn $\alpha$ eine Primformel ist, dann ist $\neg \alpha$ eine $\Sigma_1$-Formel.\\
3) Sind $\alpha$ und $\beta$ $\Sigma_1$-Formeln, dann  ist auch $\alpha \land \beta$ eine $\Sigma_1$-Formel.\\
4) Sind $\alpha$ und $\beta$ $\Sigma_1$-Formeln, dann  ist auch $\alpha \lor \beta$ eine $\Sigma_1$-Formel.\\
5) Wenn $\alpha$ eine $\Sigma_1$-Formel ist, dann ist auch $\exists x \; \alpha$ eine $\Sigma_1$-Formel.\\
6) Wenn $\alpha$ eine $\Sigma_1$-Formel ist, dann ist auch $\forall x<t \rightarrow \alpha$ eine $\Sigma_1$-Formel.\\
Der in der Formel verwendete Allquantor nennt man beschränkten Allquantor.\\
 Die Formel ist eine Kurzschreibweise für:\\
Wenn $\alpha$ eine $\Sigma_1$-Formel ist, dann ist auch $\forall x \; (x<t \rightarrow \alpha)$ eine $\Sigma_1$-Formel.\\


\subsection{Hauptsatz} $\label{Hauptsatz}$
Für jede  $\Sigma_1$- Formel $\varphi$ gilt:   $\quad \mathfrak{N} \models \varphi \implies$ PA $\vdash \varphi$  \\ \\
Bemerkung: \\
Aus der \grqq Wahrheit \grqq einer Formel bzgl. des Standardmodells $\mathfrak{N}$ von PA kann also auf die Beweisbarkeit geschlossen werden.


\begin{proof} (mit vielen Unterbahauptungen) \\
Zeige obige Behauptung B für alle Formeln $\alpha$ und $\beta$:\\
1) Für jede Primformel $\alpha$ gilt B($\alpha$)\\
2) $\alpha$ ist  Primformel und B($\alpha$) $\Longrightarrow$ B($\neg \alpha$) \\
3) B($\alpha$) und B($\beta$) $\Longrightarrow$  B($\alpha \land \beta$) \\
4) B($\alpha$) und B($\beta$) $\Longrightarrow$  B($\alpha \lor \beta$) \\
5) B($\alpha$) $\Longrightarrow$ B($\exists x \; \alpha$) \\
6) B($\alpha$) $\Longrightarrow$ B($\forall x<t \rightarrow \alpha$)\\ \\

\newpage
\subsubsection{Unterbehauptung  0} $\label{UB0}$ 
Voraussetzungen:\\
$z1 \in \text{N} \text{ und } z2 \in \text{N} \text{ und } z3 \in \text{N} \\$
$\text{Behauptung:}\\$
$z1 + z2 = z3  \implies PA \vdash  \overline{z1} \oplus \overline{z2} = \overline{z3} \\$
$z1 * z2 = z3  \implies PA \vdash  \overline{z1} \otimes \overline{z2} = \overline{z3} \\ \\$
Unterbeweis: (Induktion über z1  $\in  \text{N})$ \\
$\text{B(z1):}  \Leftrightarrow \quad  \text{für alle z2} \in \text{N} \text{, für alle z3} \in \text{N}  \text{ gilt: }  \\$
$z1 + z2 = z3  \implies PA \vdash  \overline{z1} \oplus \overline{z2} = \overline{z3} \\$
$\text{zeige:}\\$
$\text{1) zeige B(0)} \\$
$\text{genügt: } 0 + z2 = z3  \implies PA \vdash  \bar 0 \oplus \overline{z2} = \overline{z3} \\$
$\text{es gilt: }  0 + z2 = z3 \implies z2 = z3  \implies $ 
$\text{PA } \vdash \overline{z2} = \overline{z3} \implies \text{PA } \vdash \bar 0 \oplus \overline{z2} = \overline{z3} \\$
$\text{2) Induktionsvoraussetzung: B(z1), also für alle z2} \in  \text{N} \text{ , für alle z3} \in \text{N} :   \\$
$z1 + z2 = z3  \implies PA \vdash  \overline{z1} \oplus \overline{z2} = \overline{z3} \\$
$\text{zeige Induktionsbehauptung B(z1+1), also für alle z2} \in  \text{N} \text{ , für alle z3} \in \text{N} :   \\$
$(z1 + 1) + z2 = z3   \implies PA \vdash  \overline{z1+1} \oplus \overline{z2} = \overline{z3} \\ $
$\text{es gilt aber: } \\$
$(z1 + 1) + z2 = z3 \implies z1 + (z2 + 1) = z3 \\$
$\text{also nach Induktionsvoraussetzung:  } \\ $
$\text{PA } \vdash \overline{z1} \oplus \overline{z2+1} = \overline{z3} \implies $
$\text{PA } \vdash \overline{z1} \oplus (\overline{z2} \oplus \bar 1) = \overline{z3} \implies $
$\text{PA } \vdash \overline{z1} \oplus (\bar 1 \oplus \overline{z2}) = \overline{z3} \implies $
$\text{PA } \vdash (\overline{z1} \oplus \bar 1) \oplus \overline{z2} = \overline{z3} \\$
$\text{3) Analog für } \otimes \\$

\newpage
\subsubsection{Unterbehauptung 1} $\label{UB1}$ 
Für alle Terme T, für alle z $\in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(T=\bar z)  \text{ gilt: }  \\$   
$\mathfrak{N} \models (T = \bar z)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash (T = \bar z)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

Unterbeweis:: (Induktion über Terme T)  \\
$\text{Es genügt die Behauptung zu zeigen für: } \{x_0, ... ,x_n\} = \text{frei}(T=\bar z) \\$

$\text{B(T):}  \Leftrightarrow \quad  \text{Für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(T=\bar z)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (T= \bar z)  \implies  PA  \vdash (T = \bar z)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

$\text{1) zeige B(T), wobei T eine beliebige Variable ist, d.h. T} = v_i , \text{zeige also:}\\$
$\text{Für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{v_i\} = \text{frei}(v_i=\bar z)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (v_i= \bar z)  \implies  PA  \vdash (v_i = \bar z)(\overline{h(v_i)}) \\$
$\text{Es sei: frei}(v_i=\bar z) = \{v_i\} \text{ und } \mathfrak{I} \models (v_i = \bar z) \\$
$\implies \mathfrak{I}(v_i) = \mathfrak{I}(\bar z) \implies  h(v_i) = z \implies 
PA  \vdash (\overline{h(v_i)} = \bar z) \implies \\$
$PA  \vdash (v_i = \bar z)(\overline{h(v_i)}) \\$

$\text{2) zeige B(T) wobei T}= \bar 0 \text{ oder T}= \bar 1  \\$
$\text{a) genügt zu zeigen: }\mathfrak{I} \models (\bar 0 = \bar z)  \implies  PA  \vdash (\bar 0 = \bar z) \\$
$\text{es sei:  }  \mathfrak{I} \models (\bar 0 = \bar z) \implies 0 = z   \implies  PA  \vdash (\bar 0 = \bar z) \\$
$\text{b) genügt zu zeigen: }\mathfrak{I} \models (\bar 1 = \bar z)  \implies  PA  \vdash (\bar 1 = \bar z) \\$
$\text{es sei:  }  \mathfrak{I} \models (\bar 1 = \bar z) \implies 1 = z   \implies  PA  \vdash (\bar 1 = \bar z) \\$


$\text{3) Zeige: B(T1) und B(T2)} \implies \text{B(T1} \oplus \text{T2)} \\$
$\text{Zeige B(T1} \oplus \text{T2), also} \\$ 
$\text{Für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(T1 \oplus T2 = \bar z)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (T1 \oplus T2 = \bar z)  \implies 
PA  \vdash (T1 \oplus T2 = \bar z)(\overline{h(v_0)}, ..., \overline{h(v_{n-1})}) \\$
$\text{Es sei: } \mathfrak{I} \models (T1 \oplus T2 = \bar z) \\$
$\implies \mathfrak{I}(T1) + \mathfrak{I}(T2) = \mathfrak{I}(\bar z)  \implies \mathfrak{I}(T1) + \mathfrak{I}(T2) = z$, also folgt mit mit $\ref{UB0} \\ 
PA \vdash \overline{\mathfrak{I}(T1)} \oplus \overline{\mathfrak{I}(T2)} = \bar z$
, also folgt durch Substitution mit $\ref{SR6}$ \\
$PA \vdash \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \bar z(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{ (*)} \\$
$\text{Außerdem gilt:} \\$
$\{ x_{i_1}, ..., x_{i_s}\} := \text{frei(}T1= \overline{\mathfrak{I}(T1)}) \subset \text{frei(}T1 \oplus T2 = \bar z)    \\$
$\{ x_{j_1}, ..., x_{j_s}\} := \text{frei(}T2= \overline{\mathfrak{I}(T2)}) \subset \text{frei(}T1 \oplus T2 = \bar z)    \\$
$\mathfrak{I} \models (T1= \overline{\mathfrak{I}(T1)} \text{ und } \mathfrak{I} \models (T2= \overline{\mathfrak{I}(T2)} \\$
$\text{also mit Ind.Vor:} \\$
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{x_{i_1}}, ... , \overline{x_{i_s}}) \text{ und } \\$
$ PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{x_{j_1}}, ... , \overline{x_{j_s}}) \\$
$\implies \\$
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und } 
PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und }  \\$
$PA \vdash T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)})   \\$
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \\$
$\hspace*{10mm} \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
\overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{(**)}\\$
$\text{Aus (*) und (**) folgt:} \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \bar z(\overline{h(x_0)}, ..., \overline{h(x_n)})\\$
$\text{und damit:} \\$
$PA \vdash (T1 \oplus T2 = \bar z)(\overline{h(x_0)}, ..., \overline{h(x_n)})$ \\ \\
4) analog mit  $\otimes $ \\ \\
Unterbehauptung  1': \\
Für alle Terme T, für alle z $\in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(T=\bar z)  \text{ gilt: }  \\$   
$\mathfrak{N} \models (\bar z=T)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash (\bar z=T)(\overline{h(x_0)}, ..., \overline{h(x_n)}) $ \\ \\
Unterbeweis: analog Unterbehauptung 1 \\

\newpage
\subsubsection{Unterbehauptung 2} $\label{UB2}$ 
Für alle Terme T, für alle z $\in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(T=v_i)  \text{ gilt: }  \\$   
$\mathfrak{N} \models (T = v_i)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash (T = v_i)(\overline{h(x_0)}, ..., \overline{h(x_n)}) $ \\ \\
Unterbeweis: (Induktion über Terme T) \\
Es genügt die Behauptung zu zeigen für: $\{x_0, ... ,x_n\} = \text{frei}(T=v_i) $ \\
B(T): $\Leftrightarrow \quad  \text{Für alle Variablen } v_i \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(T=v_i)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (T= v_i)  \implies  PA  \vdash (T = v_i)(\overline{h(x_0)}, ..., \overline{h(x_n)}) $\\ \\
1) zeige B(T), wobei T eine beliebige Variable ist, d.h. T$ = v_k , \text{zeige also:}\\$
$\text{Für alle Variablen } v_i  \text{ , für alle Belegungen h und alle Variablen  aus }\\$
$\{v_k , v_i\} = \text{frei}(v_k=v_i)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (v_k= v_i)  \implies  PA  \vdash (v_k = v_i)(\overline{h(v_i)}) \\$
Es sei:
$\text{frei}(v_k=v_i) =\{v_k , v_i\}  \text{ und } \mathfrak{I} \models (v_k = v_i) \\$
$\implies \mathfrak{I}(v_k)=\mathfrak{I}(v_i)  \implies  h(v_k) = h(v_i) \implies 
PA  \vdash (\overline{h(v_k)} = \overline{h(v_i)}) \implies \\$
$PA  \vdash (v_k = v_i)(\overline{h(v_k)}, \overline{h(v_i)}) $ \\ \\
2) zeige B(T) wobei T $= \bar 0 \text{ oder T}= \bar 1  $ \\
$\text{Für alle Variablen } v_i  \text{ , für alle Belegungen h und alle Variablen  aus }\\$
$\{v_i\} = \text{frei}(\bar 0=v_i)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (\bar 0= v_i)  \implies  PA  \vdash (\bar 0 = v_i)(\overline{h(v_i)}) \\$
$\text{Es sei:  }  \mathfrak{I} \models (\bar 0 = v_i) \implies \mathfrak{I}(\bar 0) = \mathfrak{I}(v_i)  \implies 0 = h(v_i) \implies  PA  \vdash (\bar 0 = \overline{h(v_i)})  \\$
$\implies  PA  \vdash (\bar 0 = v_i)(\overline{h(v_i)}) \\$
b) Analog für T$ = \bar 1 $   \\ \\
3) Zeige: B(T1) und B(T2) $\implies \text{B(T1} \oplus \text{T2)} \\$
$\text{Zeige B(T1} \oplus \text{T2), also} \\$ 
$\text{Für alle Variablen } v_i \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(T1 \oplus T2 = v_i)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (T1 \oplus T2 = v_i)  \implies 
PA  \vdash (T1 \oplus T2 = v_i)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Es sei: } \mathfrak{I} \models (T1 \oplus T2 = v_i) \\$
$\implies \mathfrak{I}(T1) + \mathfrak{I}(T2) = \mathfrak{I}(v_i)  \implies \mathfrak{I}(T1) + \mathfrak{I}(T2) = h(v_i)  \\$
$\implies PA \vdash \overline{\mathfrak{I}(T1)} \oplus \overline{\mathfrak{I}(T2)} = \overline{h(v_i)}  \implies$ (mit Substitution (SR6)) \\
$PA \vdash \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{h(v_i)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \implies \\$
$PA \vdash \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) = v_i(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{ (*)} \\$
(Beachte: aus $\{x_0, ... ,x_n\} = \text{frei}(T1 \oplus T2 = v_i)$ folgt $v_i \in \{x_0, ... ,x_n\}$)\\
$\text{Außerdem gilt:} \\$
$\{ x_{i_1}, ..., x_{i_s}\} := \text{frei(}T1= \overline{\mathfrak{I}(T1)}) \subset \text{frei(}T1 \oplus T2 = v_i)    \\$
$\{ x_{j_1}, ..., x_{j_s}\} := \text{frei(}T2= \overline{\mathfrak{I}(T2)}) \subset \text{frei(}T1 \oplus T2 = v_i)    \\$
$\mathfrak{I} \models (T1= \overline{\mathfrak{I}(T1)} \text{ und } \mathfrak{I} \models (T2= \overline{\mathfrak{I}(T2)} \\$
$\text{also mit \ref{UB1}}$ \\ 
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{x_{i_1}}, ... , \overline{x_{i_s}}) \text{ und } \\$
$ PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{x_{j_1}}, ... , \overline{x_{j_s}}) \\$
$\implies \\$
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und } 
PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und }  \\$
$PA \vdash T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)})   \\$
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \\$
$\hspace*{10mm} \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
\overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{(**)}\\$
$\text{Aus (**) und (*) folgt:} \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = v_i(\overline{h(x_0)}, ..., \overline{h(x_n)})\\$
$\text{und damit:} \\$
$PA \vdash (T1 \oplus T2 = v_i)(\overline{h(x_0)}, ..., \overline{h(x_n)})$ \\ \\
4) analog mit $\otimes $   \\ \\
Unterbehauptung  2': \\
$\text{Für alle Terme T, für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(T=v_i)  \text{ gilt: }  \\$   
$\mathfrak{N} \models (v_i=T)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash (v_i=T)(\overline{h(x_0)}, ..., \overline{h(x_n)}) $ \\ \\
Unterbeweis: analog Unterbehauptung 2  \\


\newpage
\subsubsection{Unterbehauptung 3} $\label{UB3}$ 
$\text{Für alle Terme T, S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(T=v_i)  \text{ gilt: }  \\$   
$\mathfrak{N} \models (T = S)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash (T = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

Unterbeweis: (Induktion über Terme T)  \\
$\text{Es genügt die Behauptung zu zeigen für: } \{x_0, ... ,x_n\} = \text{frei}(T=S) \\$

$\text{B(T):}  \Leftrightarrow \quad  \text{Für alle Terme S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(T=S)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (T= S)  \implies  PA  \vdash (T = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

$\text{1) zeige B(T), wobei T eine beliebige Variable ist, d.h. T} = v_i , \text{zeige also:}\\$
$\text{Für alle Terme S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(v_i=S)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (v_i= S)  \implies  PA  \vdash (v_i = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Dies gilt nach Unterbehauptung 2'} \\$

$\text{2) zeige B(T) wobei T}= \bar 0 \text{ oder T}= \bar 1  \\$
$\text{Für alle Terme S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\bar 0=S)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (\bar 0= S)  \implies  PA  \vdash (\bar 0 = S)({h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Dies gilt mit Unterbehauptung 1' mit } z=\bar 0  \\$
$\text{b) Analog für T=} \bar 1 \\$   

$\text{3) Zeige: B(T1) und B(T2)} \implies \text{B(T1} \oplus \text{T2)} \\$
$\text{Zeige B(T1} \oplus \text{T2), also} \\$ 
$\text{Für alle Terme S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(T1 \oplus T2 = S)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (T1 \oplus T2 = S)  \implies 
PA  \vdash (T1 \oplus T2 = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Es sei: } \mathfrak{I} \models (T1 \oplus T2 = S) \\$
$\implies \mathfrak{I}(T1) + \mathfrak{I}(T2) = \mathfrak{I}(S)  \implies 
PA \vdash \overline{\mathfrak{I}(T1)} \oplus \overline{\mathfrak{I}(T2)} = \overline{\mathfrak{I}(S)}  \implies \\$
$PA \vdash \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(S)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{ (*)} \\$ 
$\text{Außerdem gilt:} \\$
$\{ x_{i_1}, ..., x_{i_s}\} := \text{frei(}T1= \overline{\mathfrak{I}(T1)}) \subset \text{frei(}T1 \oplus T2 = S)    \\$
$\{ x_{j_1}, ..., x_{j_s}\} := \text{frei(}T2= \overline{\mathfrak{I}(T2)}) \subset \text{frei(}T1 \oplus T2 = S)    \\$
$\{ x_{k_1}, ..., x_{k_s}\} := \text{frei(}S= \overline{\mathfrak{I}(S)}) \subset \text{frei(}T1 \oplus T2 = S)    \\$
$\mathfrak{I} \models (T1= \overline{\mathfrak{I}(T1)}) \text{ und } \mathfrak{I} \models (T2= \overline{\mathfrak{I}(T2)}) \text{ und } \mathfrak{I} \models (S= \overline{\mathfrak{I}(S)}) \\$
$\text{also mit Ind.Vor:} \\$
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{x_{i_1}}, ... , \overline{x_{i_s}}) \text{ und } \\$
$ PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{x_{j_1}}, ... , \overline{x_{j_s}})$ 
und mit $\ref{UB1}$\\
$ PA  \vdash (S = \overline{\mathfrak{I}(S)})(\overline{x_{k_1}}, ... , \overline{x_{k_s}}) \\$
$\implies \\$
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und } \\$
$ PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und } \\$
$ PA  \vdash (S = \overline{\mathfrak{I}(S)})(\overline{h(x_0)}, ..., \overline{h(x_n)})  \\$ 
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und }  \\$
$PA \vdash T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)})   \text{ und }  \\$
$PA \vdash S(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(S)}(\overline{h(x_0)}, ..., \overline{h(x_n)})  \quad \text{(x)} \\$  
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \\$
$\hspace*{10mm} \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
\overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{(**)}\\$
$\text{Aus (**) und (*) folgt:} \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \mathfrak{I}(S)(\overline{h(x_0)}, ..., \overline{h(x_n)})\\$
$\text{Mit (x) folgt:} \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = S(\overline{h(x_0)}, ..., \overline{h(x_n)})\\$
$\text{also:} \\$ 
$PA \vdash (T1 \oplus T2 = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

$\text{4) analog mit } \otimes \\$

\newpage
\subsubsection{Unterbehauptung 4} $\label{UB4}$ 
$\text{Für alle Terme T, für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(\neg T=\bar z)  \text{ gilt: }  \\$   
$\mathfrak{N} \models \neg(T = \bar z)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash \neg(T = \bar z)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

Unterbeweis:: (Induktion über Terme T)  \\
$\text{Es genügt die Behauptung zu zeigen für: } \{x_0, ... ,x_n\} = \text{frei}(\neg T=\bar z) \\$
$\text{B(T):}  \Leftrightarrow \quad  \text{Für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\neg T=\bar z)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg(T= \bar z)  \implies  PA  \vdash \neg(T = \bar z)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

$\text{1) zeige B(T), wobei T eine beliebige Variable ist, d.h. T} = v_i , \text{zeige also:}\\$
$\text{Für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{v_i\} = \text{frei}(\neg v_i=\bar z)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg(v_i= \bar z)  \implies  PA  \vdash \neg(v_i = \bar z)(\overline{h(v_i)}) \\$
$\text{Es sei: frei}(\neg v_i=\bar z) = \{v_i\} \text{ und } \mathfrak{I} \models \neg(v_i = \bar z) \\$
$\implies \mathfrak{I}(v_i) \neq \mathfrak{I}(\bar z) \implies  h(v_i) \neq z$ \\
Daraus folgt mit $\ref{UNGL}$\\
$PA  \vdash \neg (\overline{h(v_i)} = \bar z) \implies$
$PA  \vdash \neg (v_i = \bar z)(\overline{h(v_i)}) \\$

$\text{2) zeige B(T) wobei T}= \bar 0 \text{ oder T}= \bar 1  \\$
$\text{a) genügt zu zeigen: }\mathfrak{I} \models \neg (\bar 0 = \bar z)  \implies  PA  \vdash \neg (\bar 0 = \bar z) \\$
$\text{es sei:  }  \mathfrak{I} \models \neg (\bar 0 = \bar z) \implies 0 \neq z   \implies  PA  \vdash \neg(\bar 0 = \bar z) \\$
$\text{b) genügt zu zeigen: }\mathfrak{I} \models \neg(\bar 1 = \bar z)  \implies  PA  \vdash \neg(\bar 1 = \bar z) \\$
$\text{es sei:  }  \mathfrak{I} \models \neg(\bar 1 = \bar z) \implies 1 \neq z   \implies  PA  \vdash \neg(\bar 1 = \bar z) \\$

$\text{3) Zeige: B(T1) und B(T2)} \implies \text{B(T1} \oplus \text{T2)} \\$
$\text{Zeige B(T1} \oplus \text{T2), also} \\$ 
$\text{Für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\neg T1 \oplus T2 = \bar z)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg (T1 \oplus T2 = \bar z)  \implies 
PA  \vdash \neg (T1 \oplus T2 = \bar z)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Es sei: } \mathfrak{I} \models \neg (T1 \oplus T2 = \bar z) \\$
$\implies \mathfrak{I}(T1) + \mathfrak{I}(T2) \neq \mathfrak{I}(\bar z)  \implies \mathfrak{I}(T1) + \mathfrak{I}(T2) \neq z  \implies PA \vdash \neg (\overline{\mathfrak{I}(T1) + \mathfrak{I}(T2)} = \bar z)  \\$
Also folgt ('Addition von nat. Zahlen ist beweisbar') mit $\ref{NATADD}$ \\
$PA \vdash \neg (\overline{\mathfrak{I}(T1)} \oplus \overline{\mathfrak{I}(T2)} = \bar z)  \\$
$\implies PA \vdash \neg (\overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \bar z(\overline{h(x_0)}, ..., \overline{h(x_n)})) \quad \text{ (*)} \\$
$\text{Außerdem gilt:} \\$
$\{ x_{i_1}, ..., x_{i_s}\} := \text{frei(}T1= \overline{\mathfrak{I}(T1)}) \subset \text{frei(}\neg T1 \oplus T2 = \bar z)    \\$
$\{ x_{j_1}, ..., x_{j_s}\} := \text{frei(}T2= \overline{\mathfrak{I}(T2)}) \subset \text{frei(}\neg T1 \oplus T2 = \bar z)    \\$
$\mathfrak{I} \models (T1= \overline{\mathfrak{I}(T1)} \text{ und } \mathfrak{I} \models (T2= \overline{\mathfrak{I}(T2)} \\$
$\text{also mit \ref{UB1}}:$\\
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{x_{i_1}}, ... , \overline{x_{i_s}}) \text{ und } \\$
$ PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{x_{j_1}}, ... , \overline{x_{j_s}}) \\$
also folgt mit mit Substitutionskorollar $\ref{SUBKOR}$\\
PA$\vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{h(x_0)}, ..., \overline{h(x_n)})$ und  \\
PA$\vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und }  \\$
$PA \vdash T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)})   \\$
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \\$
$\hspace*{10mm} \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
\overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{(**)}\\$
$\text{Aus (**) und (*) folgt:} \\$
$PA \vdash \neg (T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \bar z(\overline{h(x_0)}, ..., \overline{h(x_n)}))\\$
$\text{und damit:} \\$
$PA \vdash \neg (T1 \oplus T2 = \bar z)(\overline{h(x_0)}, ..., \overline{h(x_n)})\\$

$\text{4) analog mit } \otimes \\$

$\text{Unterbehauptung  4':} \\$
$\text{Für alle Terme T, für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(\neg(\bar z = T)  \text{ gilt: }  \\$   
$\mathfrak{N} \models \neg(\bar z = T)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash \neg(\bar z= T)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

Unterbeweis:: analog Unterbehauptung 4  \\

\newpage
\subsubsection{Unterbehauptung 5} $\label{UB5}$ 
$\text{Für alle Terme T, für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(\neg T=v_i)  \text{ gilt: }  \\$   
$\mathfrak{N} \models (\neg T = v_i)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash (\neg T = v_i)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

Unterbeweis:: (Induktion über Terme T)  \\
$\text{Es genügt die Behauptung zu zeigen für: } \{x_0, ... ,x_n\} = \text{frei}(\neg T=v_i) \\$

$\text{B(T):}  \Leftrightarrow \quad  \text{Für alle Variablen } v_i \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\neg T=v_i)  \text{ gilt: }  \\$   
$\mathfrak{I} \models (\neg T= v_i)  \implies  PA  \vdash (\neg T = v_i)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

$\text{1) zeige B(T), wobei T eine beliebige Variable ist, d.h. T} = v_k , \text{zeige also:}\\$
$\text{Für alle Variablen } v_i  \text{ , für alle Belegungen h und alle Variablen  aus }\\$
$\{v_k , v_i\} = \text{frei}(\neg v_k=v_i)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg (v_k= v_i)  \implies  PA  \vdash \neg (v_k = v_i)(\overline{h(v_i)}) \\$
Es sei:
$\text{frei}(\neg v_k=v_i) =\{v_k , v_i\}  \text{ und } \mathfrak{I} \models \neg (v_k = v_i) \\$
$\implies \mathfrak{I}(v_k) \neq \mathfrak{I}(v_i)  \implies  h(v_k) \neq h(v_i) \implies 
PA  \vdash \neg (\overline{h(v_k)} = \overline{h(v_i)}) \implies \\$
$PA  \vdash \neg (v_k = v_i)(\overline{h(v_k)}, \overline{h(v_i)}) \\$

$\text{2) zeige B(T) wobei T}= \bar 0 \text{ oder T}= \bar 1$ , zeige also:\\
$\text{Für alle Variablen } v_i  \text{ , für alle Belegungen h und alle Variablen  aus }\\$
$\{v_i\} = \text{frei}(\neg \bar 0=v_i)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg (\bar 0= v_i)  \implies  PA  \vdash \neg (\bar 0 = v_i)(\overline{h(v_i)}) \\$
$\text{Es sei:  }  \mathfrak{I} \models \neg (\bar 0 = v_i) \implies \mathfrak{I}(\bar 0) \neq  \mathfrak{I}(v_i)  \implies 0 \neq h(v_i) \implies  PA  \vdash \neg (\bar 0 = \overline{h(v_i)})  \\$
$\implies  PA  \vdash \neg (\bar 0 = v_i)(\overline{h(v_i)}) \\$
$\text{b) Analog für T=} \bar 1 \\$   

$\text{3) Zeige: B(T1) und B(T2)} \implies \text{B(T1} \oplus \text{T2)} \\$
$\text{Zeige B(T1} \oplus \text{T2), also} \\$ 
$\text{Für alle Variablen } v_i \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\neg T1 \oplus T2 = v_i)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg (T1 \oplus T2 = v_i)  \implies 
PA  \vdash \neg (T1 \oplus T2 = v_i)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Es sei: } \mathfrak{I} \models \neg (T1 \oplus T2 = v_i) \implies \\$
$\mathfrak{I}(T1) + \mathfrak{I}(T2) \neq \mathfrak{I}(v_i)  \implies \mathfrak{I}(T1) + \mathfrak{I}(T2) \neq  h(v_i)  \implies  \\$
$ PA \vdash \neg (\overline{\mathfrak{I}(T1) + \mathfrak{I}(T2)} = \overline{h(v_i)}) \implies  \\$ 
$PA \vdash \neg (\overline{\mathfrak{I}(T1)} \oplus \overline{\mathfrak{I}(T2)} = \overline{h(v_i)})  \implies \\$
$PA \vdash \neg (\overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{h(v_i)}(\overline{h(x_0)}, ..., \overline{h(x_n)})) \implies \\$
$PA \vdash \neg \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) = v_i(\overline{h(x_0)}, ..., \overline{h(x_n)})) \quad \text{ (*)} \\$
$\text{Außerdem gilt:} \\$
$\{ x_{i_1}, ..., x_{i_s}\} := \text{frei(}T1= \overline{\mathfrak{I}(T1)}) \subset \text{frei(}\neg T1 \oplus T2 = v_i)    \\$
$\{ x_{j_1}, ..., x_{j_s}\} := \text{frei(}T2= \overline{\mathfrak{I}(T2)}) \subset \text{frei(}\neg T1 \oplus T2 = v_i)    \\$
$\mathfrak{I} \models (T1= \overline{\mathfrak{I}(T1)} \text{ und } \mathfrak{I} \models (T2= \overline{\mathfrak{I}(T2)} \\$
also mit  $\ref{UB1}$ \\
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{x_{i_1}}, ... , \overline{x_{i_s}})$  und 
$ PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{x_{j_1}}, ... , \overline{x_{j_s}}) \\$
$\implies \\$
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und } 
PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und }  \\$
$PA \vdash T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)})   \\$
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \\$
$\hspace*{10mm} \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
\overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{(**)}\\$
Aus (**) und (*) folgt mit $\ref{FS5}$: \\ 
$PA \vdash \neg(T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = v_i(\overline{h(x_0)}, ..., \overline{h(x_n)}))\\$
$\text{und damit:} \\$
$PA \vdash \neg (T1 \oplus T2 = v_i)(\overline{h(x_0)}, ..., \overline{h(x_n)})\\$

$\text{4) analog mit } \otimes \\$

$\text{Unterbehauptung  5':} \\$
$\text{Für alle Terme T, für alle z} \in \mathbb{N} \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(\neg v_i = T)  \text{ gilt: }  \\$   
$\mathfrak{N} \models (\neg v_i = T)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash (\neg v_i = T)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

Unterbeweis:: analog Unterbehauptung 5  \\

\newpage
\subsubsection{Unterbehauptung 6} $\label{UB6}$ 
$\text{Für alle Terme T, S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} \supset \text{frei}(\neg T=S)  \text{ gilt: }  \\$   
$\mathfrak{N} \models \neg (T = S)[h(x_0), ..., h(x_n)]  \implies  PA  \vdash \neg (T = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

Unterbeweis: (Induktion über Terme T)  \\
$\text{Es genügt die Behauptung zu zeigen für: } \{x_0, ... ,x_n\} = \text{frei}(\neg T=S) \\$

$\text{B(T):}  \Leftrightarrow \quad  \text{Für alle Terme S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\neg T=S)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg (T= S)  \implies  PA  \vdash \neg (T = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

1) zeige B(T), wobei T eine beliebige Variable ist, d.h. setze T $\equiv v_i$ , zeige also: \\
$\text{Für alle Terme S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\neg v_i=S)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg (v_i= S)  \implies  PA  \vdash \neg (v_i = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Dies gilt nach Unterbehauptung 5'} \\$

2) zeige B(T) wobei T= $\bar 0$ oder T= $\bar 1$  \\
a) Für alle Terme S, für alle Belegungen h und alle Variablen  aus \\
$\{x_0, ... ,x_n\} = \text{frei}(\neg \bar 0=S)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg (\bar 0= S)  \implies  PA  \vdash \neg (\bar 0 = S)({h(x_0)}, ..., \overline{h(x_n)}) \\$
Dies gilt mit Unterbehauptung 4'. Setze dort $z \equiv \bar 0$ \\
b) Analog für T=$\bar 1$  \\ 

3) Zeige: B(T1) und B(T2) $\implies$ B$(T1 \oplus T2)$ \\
$\text{Zeige B(T1} \oplus \text{T2), also} \\$ 
$\text{Für alle Terme S, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\neg T1 \oplus T2 = S)  \text{ gilt: }  \\$   
$\mathfrak{I} \models \neg (T1 \oplus T2 = S)  \implies 
PA  \vdash \neg (T1 \oplus T2 = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
Es sei: $\mathfrak{I} \models \neg (T1 \oplus T2 = S) \\$
$\implies \mathfrak{I}(T1) + \mathfrak{I}(T2) \neq \mathfrak{I}(S)$  
Es folgt mit Lemma $\ref{UNGL}$ \\
PA$\vdash \neg (\overline{\mathfrak{I}(T1)} \oplus \overline{\mathfrak{I}(T2)} = \overline{\mathfrak{I}(S)})  \implies \\$
$PA \vdash \neg (\overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(S)}(\overline{h(x_0)}, ..., \overline{h(x_n)})) \quad \text{ (*)} \\$ 

$\text{Außerdem gilt:} \\$
$\{ x_{i_1}, ..., x_{i_s}\} := \text{frei(}T1= \overline{\mathfrak{I}(T1)}) \subset \text{frei(}\neg T1 \oplus T2 = S)    \\$
$\{ x_{j_1}, ..., x_{j_s}\} := \text{frei(}T2= \overline{\mathfrak{I}(T2)}) \subset \text{frei(}\neg T1 \oplus T2 = S)    \\$
$\{ x_{k_1}, ..., x_{k_s}\} := \text{frei(}S= \overline{\mathfrak{I}(S)}) \subset \text{frei(}\neg T1 \oplus T2 = S)    \\$
$\mathfrak{I} \models (T1= \overline{\mathfrak{I}(T1)}) \text{ und } \mathfrak{I} \models (T2= \overline{\mathfrak{I}(T2)}) \text{ und } \mathfrak{I} \models (S= \overline{\mathfrak{I}(S)}) \\$
also mit Unterbehauptung $\ref{UB1} $ \\
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{x_{i_1}}, ... , \overline{x_{i_s}}) \text{ und } \\$
$ PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{x_{j_1}}, ... , \overline{x_{j_s}}) \text{ und } \\$
$ PA  \vdash (S = \overline{\mathfrak{I}(S)})(\overline{x_{k_1}}, ... , \overline{x_{k_s}}) \\$
$\implies \\$
$ PA  \vdash (T1 = \overline{\mathfrak{I}(T1)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und } \\$
$ PA  \vdash (T2 = \overline{\mathfrak{I}(T2)})(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und } \\$
$ PA  \vdash (S = \overline{\mathfrak{I}(S)})(\overline{h(x_0)}, ..., \overline{h(x_n)})  \\$ 
$\implies \\$
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \text{ und }  \\$
$PA \vdash T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)})   \text{ und }  \\$
$PA \vdash S(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \overline{\mathfrak{I}(S)}(\overline{h(x_0)}, ..., \overline{h(x_n)})  \quad \text{(x)} \\$  
Es folgt aus Lemma $\ref{PAF1}$ \\ 
$PA \vdash T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = $ \\
$\hspace*{10mm} \overline{\mathfrak{I}(T1)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
\overline{\mathfrak{I}(T2)}(\overline{h(x_0)}, ..., \overline{h(x_n)}) \quad \text{(**)}\\$
$\text{Aus (*) und (**) folgt:} \\$
$PA \vdash \neg (T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = \mathfrak{I}(S)(\overline{h(x_0)}, ..., \overline{h(x_n)}))  \\$
$\text{Mit (x) folgt:} \\$
$PA \vdash \neg (T1(\overline{h(x_0)}, ..., \overline{h(x_n)}) \oplus 
T2(\overline{h(x_0)}, ..., \overline{h(x_n)}) = S(\overline{h(x_0)}, ..., \overline{h(x_n)})) \\$
$\text{also:} \\$ 
$PA \vdash \neg (T1 \oplus T2 = S)(\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$

$\text{4) analog mit } \otimes \\$

\newpage
\subsubsection{Unterbehauptung 7} $\label{UB7}$ 
Definiere:\\
B($\varphi):  \Leftrightarrow \quad  \text{Für alle Formeln } \varphi  \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\varphi)  \text{ gilt: }  \\$   
$(\mathfrak{N},h) \models \varphi  \implies  PA  \vdash \phi (\overline{h(x_0)}, ..., \overline{h(x_n)}) $ \\ \\ Behauptung:\\
Für alle Formeln $\alpha$ und $\beta$ gilt:\\
$B(\alpha$) und $B(\beta) \Longrightarrow         B(\alpha \land \beta)$  \\ \\
Unterbeweis:  \\
Es sei B($\alpha$) und B($\beta$) \\
Zeige B($\alpha \land \beta$) , also \\ 
$\text{Für alle Formeln } \alpha \land \beta \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\alpha \land \beta)  \text{ gilt: }  \\$   
$(\mathfrak{N},h) \models \alpha \land \beta  \implies  PA  \vdash (\alpha \land \beta) (\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Es sei: } (\mathfrak{N},h) \models \alpha \land \beta \\$
$\implies (\mathfrak{N},h) \models \alpha \text{ und } \mathfrak{I} \models \beta \\$
also mit den Voraussetzungen \\
$PA \vdash \alpha (\overline{h(x_{i_1}}), ..., \overline{h(x_{i_s}}) \text{  wobei } \{x_{i_1}, ... , x_{i_s} \} := \text{frei(} \alpha) \subset$ frei($\alpha \land \beta$) = $\{x_0, ... ,x_n\}$
und \\
$PA \vdash \beta (\overline{h(x_{j_1}}), ..., \overline{h(x_{j_s}}) \text{  wobei } \{x_{j_1}, ... , x_{j_s} \} := \text{frei(} \beta) \subset$ frei($\alpha \land \beta$) = $\{x_0, ... ,x_n\}$ \\
$\implies \\$
$PA  \vdash \alpha (\overline{h(x_0)}, ..., \overline{h(x_n)})  \text{ und}\\$
$PA  \vdash \beta (\overline{h(x_0)}, ..., \overline{h(x_n)})  \\$
$\implies \\$
$PA  \vdash \alpha (\overline{h(x_0)}, ..., \overline{h(x_n)}) \land  
\beta (\overline{h(x_0)}, ..., \overline{h(x_n)})  \\$
$\implies \\$
$PA  \vdash (\alpha \land \beta) (\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$





\newpage
\subsubsection{Unterbehauptung 8} $\label{UB8}$ 
Definiere:\\
B($\varphi):  \Leftrightarrow \quad  \text{Für alle Formeln } \varphi  \text{, für alle Belegungen h und alle Variablen  aus }\\$
$\{x_0, ... ,x_n\} = \text{frei}(\varphi)  \text{ gilt: }  \\$   
$(\mathfrak{N},h) \models \varphi  \implies  PA  \vdash \varphi (\overline{h(x_0)}, ..., \overline{h(x_n)}) $ \\ \\ Behauptung:\\
Für alle Formeln $\alpha$ und $\beta$ gilt:\\
$B(\alpha$) und $B(\beta) \Longrightarrow         B(\alpha \lor\beta)$  \\ \\

Unterbeweis:  \\
Es sei B($\alpha$) und B($\beta$) \\
Zeige B($\alpha \lor \beta$) , also \\ 
Für alle Formeln $\alpha \lor \beta$ , für alle Belegungen h und alle Variablen  aus  \\
$\{x_0, ... ,x_n\} = \text{frei}(\alpha \lor \beta)$  gilt: \\
$(\mathfrak{N},h) \models \alpha \lor \beta  \implies  PA  \vdash (\alpha \lor \beta) (\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$
$\text{Es sei: } (\mathfrak{N},h) \models \alpha \lor \beta \\$
$\implies (\mathfrak{N},h) \models \alpha \text{ oder } (\mathfrak{N},h) \models \beta \\$
$\text{also mit den Voraussetzungen:} \\$
$PA \vdash \alpha (\overline{h(x_{i_1}}), ..., \overline{h(x_{i_s}}) \text{  wobei } \{x_{i_1}, ... , x_{i_s} \} := \text{frei(} \alpha) \subset$ frei($\alpha \land \beta$) = $\{x_0, ... ,x_n\}$
oder \\
$PA \vdash \beta (\overline{h(x_{j_1}}), ..., \overline{h(x_{j_s}}) \text{  wobei } \{x_{j_1}, ... , x_{j_s} \} := \text{frei(} \beta) \subset$ frei($\alpha \land \beta$) = $\{x_0, ... ,x_n\}$ \\
$\implies \\$
$PA  \vdash \alpha (\overline{h(x_0)}, ..., \overline{h(x_n)})  \text{ oder}\\$
$PA  \vdash \beta (\overline{h(x_0)}, ..., \overline{h(x_n)})  \\$
$\text{Es gilt aber:} \\$
$PA  \vdash \alpha (\overline{h(x_0)}, ..., \overline{h(x_n)}) \implies 
PA  \vdash (\alpha(\overline{h(x_0)}), ..., \overline{h(x_n)}) \lor \beta(\overline{h(x_0)}, ..., \overline{h(x_n)})) \\$
$\text{und} \\$
$PA  \vdash \beta (\overline{h(x_0)}, ..., \overline{h(x_n)}) \implies 
PA  \vdash (\alpha(\overline{h(x_0)}), ..., \overline{h(x_n)}) \lor \beta(\overline{h(x_0)}, ..., 
\overline{h(x_n)})) \\$
$\implies \\$
$PA  \vdash (\alpha(\overline{h(x_0)}), ..., \overline{h(x_n)}) \lor \beta(\overline{h(x_0)}, ..., 
\overline{h(x_n)})) \\$
$\implies \\$
$PA  \vdash (\alpha \lor \beta) (\overline{h(x_0)}, ..., \overline{h(x_n)}) \\$


\newpage
\subsubsection{Unterbehauptung 9} $\label{UB9}$ 
Definiere:\\
B($\varphi):  \Leftrightarrow \quad$  Für alle Formeln $\varphi$  , für alle Belegungen h und alle Variablen  aus \\
$\{x_0, ... ,x_n\} =$ frei($\varphi$)  gilt: \\   
$(\mathfrak{N},h) \models \varphi  \implies$  PA  $\vdash \varphi (\overline{h(x_0)}, ..., \overline{h(x_n)}) $ \\ \\ Behauptung:\\
Für alle Formeln $\varphi$ und alle Variablen x gilt:\\
B$(\varphi)  \Longrightarrow$ B($\exists x \varphi)$  \\ 

Unterbeweis:   \\
$\text{Es genügt die Behauptung zu zeigen für: } \{x_0, ... ,x_n\} = \text{frei}(\exists x \varphi) \\$

$\text{Es sei: } (\mathfrak{N},h) \models \exists x \varphi  \\$
$\implies \text{es existiert ein a}  \in \mathbb{N} \quad (\mathfrak{N}, h_x^{a}) \models \varphi  \\$
Fall1:  $x \in$ frei($\varphi$) \\
Nach Definition einer freien Variablen gilt:\\
frei($\exists x \varphi$) = frei($\varphi) \setminus \{x\}$, also:\\
frei($\varphi$) = frei($\exists x \varphi) \bigcup \{x\}  = \{x_0, ... ,x_n, x\} $\\
frei($\varphi$) = frei($\exists x \varphi) \bigcup \{x\}  = \{x_0, ... ,x_n, x\} $\\
Dann gilt nach Voraussetzung:\\
$PA \vdash \varphi (\overline{h_x^{a}(x_0)}, ..., \overline{h_x^{a}(x_n)}, \overline{h_x^{a}(x)})  \\$
$\implies PA \vdash \varphi (\overline{h(x_0)}, ..., \overline{h(x_n)}, \overline{a})  \\$
$\implies PA \vdash (\varphi (\overline{h(x_0)}, ..., \overline{h(x_n)}))_x^{\overline{a}}  \\$
Mit dem Substitutions-Existenz-Lemma $\ref{SEL}$ folgt:\\
$PA  \vdash \exists x \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)}) $ \\ \\
Fall2: $x \not \in$ frei($\varphi$) \\ 
es gilt wieder: frei($\exists x \varphi$) = frei($\varphi) \setminus \{x\}$, also:\\
frei($\varphi$) = frei($\exists x \varphi)$\\
Dann gilt nach Voraussetzung:  \\
$PA \vdash \varphi (\overline{h_x^{a}(x_0)}, ..., \overline{h_x^{a}(x_n)})  \\$
$\implies PA \vdash \varphi (\overline{h(x_0)}, ..., \overline{h(x_n)})  \\$
Da x $\not \in$ frei($\varphi$) gilt auch auch:\\
$\implies x \not \in \text{frei}(\varphi(\overline{h(x_0)}, ..., \overline{h(x_n)})))  \\$
Nach dem dem Nicht-Frei-und-Äquivalent-Lemma $\ref{NFAE}$ folgt dann:\\
$\implies \vdash \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)}) \leftrightarrow \exists x \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)})  \\$
$\implies PA \vdash  \exists x \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)})$ \\ \\


\newpage
\subsubsection{Unterbehauptung 10} $\label{UB10}$ 
Definiere:\\
B($x<y \rightarrow \varphi):  \Leftrightarrow \quad$  Für alle Formeln $\varphi$, für alle Variablen x, y, für alle Belegungen h und alle Variablen  aus 
$\{x_0, ... ,x_n\} =$ frei($x<y \rightarrow \varphi$)  gilt: \\   
$(\mathfrak{N},h) \models x<y \rightarrow \varphi  \implies$  PA  $\vdash (x<y \rightarrow \varphi) (\overline{h(x_0)}, ..., \overline{h(x_n)}) $ \\ \\
Behauptung:\\
Für alle Formeln $\varphi$ und alle Variablen x gilt:\\
B$(x<y \rightarrow \varphi)  \Longrightarrow$ B($\forall x(x<y \rightarrow \varphi))$  \\ 
Unterbeweis: \\
I) Beweishilfslemma:\\
Für beliebige Mengen A, B, C gilt: $A=B\setminus C$ und $C\subset B \Rightarrow B = A \stackrel{.}{\cup} C$ \\ 
II)
Hier (unter II) gilt generell die folgende  Voraussetzung: \\
$\{x_0, ... ,x_n\}$ =frei($\forall x(x<y \rightarrow \varphi))$ \\
1) \\
Es folgt aus der Definition der Substitution:\\
$\{x\} \subset$ frei$(x<y \rightarrow \varphi$ und  
frei($\forall x(x<y \rightarrow \varphi))$ = frei$(x<y \rightarrow \varphi) \setminus \{x\}$\\
Mit 1a) folgt dann:\\
frei$(x<y \rightarrow \varphi)$= frei($\forall x(x<y \rightarrow \varphi)) 
\stackrel{.}{\cup} \{x\} = \{x_0, ... ,x_n,x\}$  \\ 
Also: 
frei$(x<y \rightarrow \varphi)= \{x_0, ... ,x_n,x\}$  \\ 
2)\\
Es folgt aus der Definition der Substitution:\\
$\{x_0, ... ,x_n\}$=frei($\forall x(x<y \rightarrow \varphi))$ = frei$(x<y \rightarrow \varphi) \setminus \{x\}$=\\
$(\{x,y\} \cup$ frei($\varphi)) \setminus \{x\}$=
$(\{x,y\} \setminus \{x\}) \cup$ (frei($\varphi) \setminus \{x\})$=
$\{y\} \cup$ (frei($\varphi) \setminus \{x\})$ \\
Also:
$y \in \{x_0, ... ,x_n\}$ \\
3) \\
$(\forall x (x<y \rightarrow \varphi))  (\overline{h(x_0)}, ..., \overline{h(x_n)}) =$ \\
$\forall x (x<y(\overline{h(x_0)}, ..., \overline{h(x_n)}) \rightarrow \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)})= \quad$ (da $y \in \{x_0, ... ,x_n\}$) \\
$\forall x (x<\overline{h(y)} \rightarrow \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)})$ \\ \\
III) zum eigentlichen Beweis:\\
$\text{Es genügt die Behauptung zu zeigen für: } \{x_0, ... ,x_n\} = \text{frei}(\forall x(x<y \rightarrow \varphi))$ \\ \\
Zeige: B($\forall x (x<y \rightarrow \varphi)$) \\
Es seien:
x, y beliebige Variablen, $\varphi$ eine beliebige Formel, h eine beliebige Belegung und \\
$x_0, ... ,x_n$ beliebige Variablen  mit $\{x_0, ... ,x_n\} =$ frei($\forall x (x<y \rightarrow \varphi)$)  und \\
$(\mathfrak{N},h) \models \forall x(x<y \rightarrow \varphi)  \\$
Nach Definition folgt dann: \\
für alle a $ \in \mathbb{N} \quad (\mathfrak{N}, h_x^{a}) \models (x<y \rightarrow \varphi)  \\$
Da nach 1) gilt: frei$(x<y \rightarrow \varphi)= \{x_0, ... ,x_n,x\}$, folgt mit der 
Induktionsvoraussetzung für alle a $\in \mathbb{N} :$ \\
$PA \vdash (x<y \rightarrow \varphi)(\overline{h_x^{a}(x_0)}, ..., \overline{h_x^{a}(x_n)}, \overline{h_x^{a}(x)}) \Longrightarrow $ \\
$PA \vdash (x<y \rightarrow \varphi)(\overline{h(x_0)}, ..., \overline{h(x_n)}, \bar a)  $ \\
Nach Definition der Substitution folgt dann mit II 1):\\
$(x<y \rightarrow \varphi)(\overline{h(x_0)}, ..., \overline{h(x_n)}, \bar a) =$\\
$\bar a <\overline{h(y)} \rightarrow \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)}, \bar a)$\\
Deshalb folgt:\\
PA$ \vdash \bar a< \overline{h(y)} \rightarrow \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)}, \overline{a}) $\\
Für alle a $ \in \mathbb{N}$ mit a $<$ h(y) gilt nach dem Kleiner-Isomorphismus-Lemma $\ref{KIL}$ \\
PA $\vdash  \bar a < \overline{h(y)}$ \\
Also gilt für alle a $<$ h(y):\\
PA$ \vdash \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)}, \bar a) $\\
Da nach dem Substitutionslemma 5 $\ref{SUBLEM5}$ gilt: 
$\; \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)}, \bar a) $ =
$(\varphi(\overline{h(x_0)}, ..., \overline{h(x_n)})) (\bar a) $ \\ 
also folgt für alle a $<$ h(y):\\
PA$ \vdash (\varphi(\overline{h(x_0)}, ..., \overline{h(x_n)))}, (\bar a) $\\
Mit dem All-Endlichkeitslemma $\ref{AEL}$ folgt dann:\\ 
PA$\vdash \forall x (x<\overline{h(y)} \rightarrow \varphi(\overline{h(x_0)}, ..., \overline{h(x_n)})) $\\  \\
Mit 3) folgt dann: \\
$\forall x (x<y \rightarrow \varphi)(\overline{h(x_0)}, ..., \overline{h(x_n)}) =$ \\
\end{proof}


\newpage
\section{Zusammenhang: Peano und Goldbach}
Das nächste Ziel ist es, die Negation der Goldbachschen Vermutung als eine $\Sigma_1$ Formel zu formulieren. \\ \\
Dazu macht man die Abkürzung:\\
Pp ist eine Abkürzung für die Formel (und intendiert p ist Primzahl) \\
$\forall i<p \; \forall j<p \; (p=i \otimes j \rightarrow  i=p \lor i=\bar 1)$ 
\subsection{Negation der Goldbachschen Vermutung formalisieren}
1) \\
GC ist eine Abkürzung für die Formel (und intendiert die Goldbachsche Vermutung) \\
$\forall n \exists p<\bar 2 \otimes n \oplus \bar 5 \; \exists q<\bar 2 \otimes n \oplus \bar 5 \; (\neg \bar 2 \otimes n \oplus \bar 4=p \oplus q \land \neg Pp \land \neg Pq)$ \\  \\
nonGC ist eine Abkürzung für die Formel (und intendiert die Negation der Goldbachschen Vermutung) \\
$\exists n \forall p<\bar 2 \otimes n \oplus \bar 5 \; \forall q<\bar 2 \otimes n \oplus \bar 5 \; (\neg \bar 2 \otimes n \oplus \bar 4=p \oplus q \lor \neg Pp \lor \neg Pq)$ \\  \\
Damit gilt:\\
PA$\; \vdash$ (nonGC $\leftrightarrow \neg$ GC) $\quad$ also \\
PA$\; \vdash$ nonGC $\iff$ PA$\; \vdash \neg$ GC $\quad$ also \\
PA$\; \vert \models$ nonGC $\iff$ PA$\; \vert \models \neg$ GC $\quad$ also \\
PA$\; \vert \models$ nonGC $\iff$ 
Für jedes S-Modell $\mathfrak{M}$ von PA gilt: ($\mathfrak{M}\; \vert \models \neg$ GC)  also
\\ 
PA$\; \vert \models$ nonGC $\iff$ 
Für jedes S-Modell $\mathfrak{M}$ von PA gilt: nicht ($\mathfrak{M}\; \vert \models$ GC) $\quad$ (*)   $\label{GC_NONGC1}$\\ \\ 
Des Weitern gilt:\\
PA$\; \vert \vdash$ (nonGC $\leftrightarrow \neg$ GC) $\quad$ also \\
PA$\; \vert \models$ (nonGC $\leftrightarrow \neg$ GC) $\quad$ also \\
Für jedes Modell $\mathfrak{M}$ von PA gilt: 
$\mathfrak{M}\; \vert \models$ (nonGC $\leftrightarrow \neg$ GC) $\qquad \qquad \qquad$ also \\
Für jedes Modell $\mathfrak{M}$ von PA gilt: 
($\mathfrak{M}\; \vert \models$ nonGC) $\iff$ ($\mathfrak{M} \; \vert \models \neg$ GC) $\quad$ also \\
Für jedes Modell $\mathfrak{M}$ von PA gilt: 
($\mathfrak{M}\; \vert \models$ nonGC) $\iff$ nicht ($\mathfrak{M} \; \vert \models$ GC) 
bzw. anders formuliert: \\
Für jedes Modell $\mathfrak{M}$ von PA gilt: 
($\mathfrak{M}\; \vert \models \neg$ nonGC) $\iff$ ($\mathfrak{M} \; \vert \models$ GC) $\quad$ (**) $\label{GC_NONGC2}$\\ \\
3) \\
nonGC ist damit ausführlich geschrieben:\\
$\exists n \forall p<\bar 2 \otimes n \oplus \bar 5 \; \forall q<\bar 2 \otimes n \oplus \bar 5((\neg \bar 2 \otimes n \oplus \bar 4=p \oplus q) \lor \\
\neg (\forall i<p \; \forall j<p \; (p=i \otimes j \rightarrow  i=p \lor i=\bar 1)) \lor \\
\neg (\forall i<q \; \forall j<q \; (q=i \otimes j \rightarrow  i=q \lor i=\bar 1)))$ \\  \\
und damit ist nonGC eine $\Sigma_1$ Formel. \\ \\




\newpage
\section{Satz: GC unabhängig von PA und PA wahr}
Wenn die Goldbachsche Vermutung unabhängig von PA ist, \\
dann gilt $\mathfrak{N} \models GC$ d.h. GC ist wahr.

\begin{proof}
$\\$
Bemerkung: 
nonGC (siehe oben) ist eine $\Sigma_1$-Formel: \\
1) \\
Annahme: \\
$\mathfrak{N} \models$ nonGC \\
Da nonGC eine $\Sigma_1$ Formel ist, folgt mit dem Hausptsatz $\ref{Hauptsatz}$: \\
PA$\; \vdash$ nonGC \\
also folgt mit dem Vollständigkeitssatz: \\
PA$\; \models$ nonGC \\
Da gilt (siehe *): $\ref{GC_NONGC1}$ \\
PA$\; \vert \models$ nonGC $\iff$ 
Für jedes S-Modell $\mathfrak{M}$ von PA gilt: nicht ($\mathfrak{M}\; \vert \models$ GC)  \\
folgt sofort:\\
Für jedes S-Modell $\mathfrak{M}$ von PA gilt: nicht ($\mathfrak{M}\; \vert \models$ GC) $\quad$(*w*)\\  \\
2) \\
GC ist unabhängig von PA $\quad \iff$ \\
nicht PA$\; \vdash GC$ und nicht $PA \vdash \neg$ GC $\quad \iff$ \\
nicht PA$\; \vert \models$ GC und nicht $PA\; \vert \models \neg$ GC$ \quad \iff$ \\
nicht (für alle S-Modelle $\mathfrak{M}$ von PA gilt: $\mathfrak{M}\; \vert \models GC$) und \\
nicht (für alle S-Modelle $\mathfrak{M}$ von PA gilt: $\mathfrak{M}\; \vert \models \neg$ GC) $\quad \iff$ \\
es existiert ein S-Modell $\mathfrak{M_1}$ von PA mit nicht $\mathfrak{M_1}\; \vert \models GC$ und \\
es existiert ein S-Modell $\mathfrak{M_2}$ von PA mit nicht $\mathfrak{M_2}\; \vert \models \neg$ GC $\quad \iff$ \\
es existiert ein S-Modell $\mathfrak{M_1}$ von PA mit $\mathfrak{M_1}\; \vert \models \neg$ GC und \\
es existiert ein S-Modell $\mathfrak{M_2}$ von PA mit $\mathfrak{M_2}\; \vert \models$ GC$ \quad \Longrightarrow$\\
es existiert ein S-Modell $\mathfrak{M_2}$ von PA mit $\mathfrak{M_2}\; \vert \models$ GC \\
Dies ist ein Widerspruch zu (*w*) \\ \\
3) \\
Also ist die Annahme falsch.\\
also:
nicht $\mathfrak{N} \; \vert \models$ nonGC \\
also:
$\mathfrak{N} \; \vert \models \neg$ nonGC \\
also (siehe **) $\ref{GC_NONGC2}$):\\
$\mathfrak{N} \; \vert \models$ GC \\



\end{proof}


















\end{document}
