Detailansicht
Syntactical consistency proofs for term induction revisited
two different methods
Michael Toppel
Art der Arbeit
Diplomarbeit
Universität
Universität Wien
Fakultät
Fakultät für Mathematik
Betreuer*in
Jakob Kellner
DOI
10.25365/thesis.15798
URN
urn:nbn:at:at-ubw:1-29853.14758.972365-3
Link zu u:search
(Print-Exemplar eventuell in Bibliothek verfügbar)
Abstracts
Abstract
(Deutsch)
GIn [6] wird von Gerhard Gentzen die Widerspruchsfreiheit der Peano Arithmetik erster Stufe PA bewiesen. Die Methode geht dabei folgendermaßen
vor: Man deniert einen simplen Teil SPA der Peano Arithmetik (SPA enthält im speziellen keine Anwendung des Induktionsschemas) und zeigt zuerst die von SPA. Der Rest des Arguments verläuft indirekt. Man nimmt an, dass PA einen Widerspruch ableitet und zeigt das dessen Deduktion zu einer Deduktion in SPA transformiert werden kann,
was der Widerspruchsfreiheit von SPA widerspricht. Diese Transformation verläuft wie folgt: Jeder Deduktion in PA wird eine Ordinalzahl (oder genauer, ein Ordinalzahlterm eines Ordinalzahlnotations Systems) zugeordnet,
diese wird der Rang der Deduktion genannt. Dann wird gezeigt, dass es zu jeder Deduktion eines Widerspruches (die nicht in SPA verläuft) eine Deduktion
(ebenfalls eines Widerspruches) gibt die einen kleineren Rang hat.
Diese Methode benötigt daher die Wohlfundiertheit des verwendeten Ordinalzahlnotations
Systems (in diesem Fall bis "0). Bei näherer Betrachtung
von Gentzens Methode fällt auf, dass sie lediglich folgende Eigenschaften von PA verwendet:
1. Alle Axiome von PA sind Allsätze oder Instanzen des Induktionsschemas
φ(0) ^ ∀ x[φ(x) -> φ(x + 1)] -> ∀ xφ(x):
2. Alle geschlossenen Terme sind beweisbar (in SPA) gleich zu einem
Term der lediglich aus 0 und dem Symbol der Nachfolgerfunktion aufgebaut
ist.
Dies erlaubt eine Verallgemeinerung von Gentzens Methode. In dieser Diplomarbeit
werden wir daher Theorien Tf = (Tf )0 [ (Tf )Ind betrachten die
folgende Eigenschaften erfüllen:
1. (Tf )0 besteht lediglich aus Allsätzen.
2. (Tf )Ind beinhaltet alle Instanzen des Induktionsschemas
φ(c1)^:::^φ(cm)^∀ ~x[φ(x1)^:::^φ(xn) -> φ(f(x1; :::; xn))] -> ∀ xφ(x):
3. Der simple Teil von Tf beweist für jeden geschlossenen Term t, dass t
gleich einem Term _t ist der lediglich aus den symbolen c1; :::; cm und f
aufgebaut ist.
Die Widerspruchsfreiheit von Tf kann nun, wie in [6] für PA, relativ zu
ihrem simplen Teil (wo Induktion wie zuvor bei Gentzen nicht möglich ist)
gezeigt werden. Eine Konsequenz dieses Resultates ist das folgende Korollar.
Korollar. Sei φ(a) quantorenfrei und Tf widerspruchsfrei.
Wenn Tf j= 9xφ(x), dann (Tf )0 j= 9xφ(x).
Insbesondere ist Tf _0
1 -konservativ über (Tf )0.
Es scheint mir als wäre die Methode, die von Kurt Schütte in seinem
Widerspruchsfreiheitsbeweis von PA verwendet wird, eine gänzlich andere.
Schütte, Tait und Andere verwenden Kalküle mit unendlichen Deduktionsregeln
um, in einem gewissen Sinne, die Beweistheoretische Ordinalzahl
einer Theorie zu berechnen. Dies erfolgt über eine Transformation der endlichenDeduktionen der Theorie (in der Logik erster Stufe) in Deduktionen ineinem unendlichen Kalkül, das Schnittelimination erlaubt. Im Gegensatz zu Gentzens Methode hat die von Schütte eine enge Beziehung zu den beweistheoretischenOrdinalzahlen.
Auf die Unterschiede der beiden Methoden wird nicht weiter eingegangen werden. Anstatt dieses Vergleiches wird lediglich eine Variante von Taits
Methode dazu verwendet die _1
1-Ordinalzahl, wie von Wolfram Pohlers in
[∀ ] beschrieben, von Theorien TAf (aufgefasst als Taitkalkühl) zu messen.
Es wird angenommen das TAf folgende Eigenschaften erfüllt:
1. TAf enthält für jede primitiv rekursive Funktion die denierenden
Formeln als Axiome.
2. Weiters enthält TAf alle Instanzen des Schemas
φ(c1)^:::^φ(cm)^∀ ~x[φ(x1)^:::^φ(xn) -> φ(f(x1; :::; xn))] -> ∀ xφ(x):
Hierbei ist f ein m-stelliges Symbol einer gleichstelligen primitiv rekursiven
Funktion und c1; :::; cl Individuenkonstanten.
3. Es wird außerdem angenommen das jedes n 2 N gleich einer Komposition
aus fN und den natürlichen Zahlen cN1;:::; cN
l ist.
Abstract
(Englisch)
Gerhard Gentzen proves the consistency of first-order Peano arithmetic \textbf{PA}. His method works as follows: Define a simple part \textbf{SPA} of peano arithmetic (\textbf{SPA} does in particular not contain induction) and first show the consistency of \textbf{SPA}. Now assume towards a contradiction that \textbf{PA} deducts an contradiction. Show that this deduction can be transformed into a deduction in \textbf{SPA}, this contradicts the consistency of \textbf{SPA}. How to get a deduction in \textbf{SPA}: We assign an ordinal (more exact an ordinal term of an ordinal notation system) to each deduction in \textbf{PA}, called the rank of the deduction. Next show that for each deduction which deducts a contradiction (and is not in \textbf{SPA}) there is a deduction (also deducting and contradiction) with smaller rank.
This method requires that the ordinal notation system (which goes up to $\varepsilon_0$) is well-founded. It turns out that Gentzen's method requires only to the following properties of \textbf{PA}:
\begin{enumerate}
\item All axioms of \textbf{PA} are universal sentences or instances of the induction schema
$$ \varphi(0) \wedge \forall x [\varphi(x) \rightarrow \varphi(x+1)] \rightarrow \forall x \varphi(x).$$
\item All closed terms are provable equal to a term build up just from $0$ and the symbol of the successor function.
\end{enumerate}
This allows a slight generalisation of Gentzen's method.
In this Diploma Thesis we consider theories $T_f = (T_f)_0 \cup (T_f)_{\text{Ind}}$ with the following properties:
\begin{enumerate}
\item $(T_f)_0$ contains only universal sentences.
\item $(T_f)_{\text{Ind}}$ contains all instances of the general induction schema
$$\varphi(c_1)\wedge ... \wedge \varphi(c_m) \wedge \forall \vec{x} [\varphi(x_1)\wedge...\wedge \varphi(x_n) \rightarrow \varphi(f(x_1,...,x_n))] \rightarrow \forall x \varphi(x).$$
\item The simple part of $T_f$ proves for every closed term $t$ the equality of $t$ to a term $\bar{t}$ build up just from $c_1,...,c_m$ and $f$.
\end{enumerate}
As Gentzen did for \textbf{PA}, the consistency of $T_f$ can be shown with respect to their simple part which corresponds to the simple part of Gentzen (also without induction). As a consequence, one gets the following result for all such theories.
\begin{cor2}
Assume $\varphi(a)$ is quantifier free and $T_f$ consistent.\\
If $T_f \models \exists x \varphi(x)$, then $(T_f)_0 \models \exists x \varphi(x)$.\\
I.e., $T_f$ is $\Sigma_1^0$-conservative over $(T_f)_0$.
\end{cor2}
It seems that this method is different in an essential way to the method Kurt Sch\"{u}tte uses in his consistency proof of \textbf{PA}. Sch\"{u}tte, Tait and others uses calculi with infinite deduction rules. These methods compute, in some sense, the proof theoretical ordinal of the considered theory by embedding the deductions of the theory (in ordinary first-order logic) in an infinite system which allows cut-elimination. In contrast to Gentzen's method Sch\"{u}tte's and Tait's methods are closely related to the proof theoretical ordinals.\\
We do not provide an analysis of the disparities of both methods. Instead we present the point of view Wolfram Pohlers propose, to measure the $\Pi_1^1$-ordinal of theories $\mathsf{TA}_f$ (presented as a Tait-calculus) satisfying the following conditions:
\begin{enumerate}
\item $\mathsf{TA}_f$ includes all defining axioms for primitive recursive functions.
\item All instances of the schema $$\varphi(c_1)\wedge ... \wedge \varphi(c_m) \wedge \forall \vec{x} [\varphi(x_1)\wedge...\wedge \varphi(x_n) \rightarrow \varphi(f(x_1,...,x_n))] \rightarrow \forall x \varphi(x)$$ are included. Here $f$ is an $m$-array primitive recursive function constant and $c_1,...,c_l$ are individual constants.
\item Every $n \in \mathbb{N}$ is equal to a composition of $f^\mathbb{N}$ and the elements $c_1^\mathbb{N},...,c_l^\mathbb{N}$.
\end{enumerate}
Schlagwörter
Schlagwörter
(Englisch)
Proof Theory Ordinal Analysis Cut-Elimination Consistency Proof
Schlagwörter
(Deutsch)
Beweistheorie Ordinalzahlanalyse Schnittelimination Konsistenzbeweis
Autor*innen
Michael Toppel
Haupttitel (Englisch)
Syntactical consistency proofs for term induction revisited
Hauptuntertitel (Englisch)
two different methods
Paralleltitel (Deutsch)
Syntaktische Konsistenzbeweise für Terminduktion wiederaufbereitet ; zwei unterschiedliche Methoden
Publikationsjahr
2011
Umfangsangabe
V, 71 S.
Sprache
Englisch
Beurteiler*in
Jakob Kellner
Klassifikation
31 Mathematik > 31.10 Mathematische Logik, Mengenlehre
AC Nummer
AC08704395
Utheses ID
14181
Studienkennzahl
UA | 405 | | |