Freiburg, Univ., Diss., 2001.

Diss. University Amsterdam, 2000. / Namensvariante: Jaap Kamps.

Erfurt, Univ., Diss., 2003

Diss. Uppsala : Univ., 2001.

Stuttgart, Univ., Diss., 2006.

Konstanz, Univ., Diplomarb., 1998.

Stuttgart, Univ., Habil.-Schr., 2003.

1) Dass die „mathematische Logik“ keine mathematische Logik ist, duerfte auch anderen Kritikern aufgefallen sein, dass sich aber ihre (angebliche) Logik nur ausschliesslich mit sich selbst beschaeftigt und darin ihren Selbstzweck findet, wurde in der Literatur noch nirgends herausgearbeitet und ist Hauptgegenstand dieses Aufsatzes. 2) Auch eine deutliche Kritik des semantischen und (trotz gegenteiliger Behauptung) auch syntaktischen Niveaus von Aussagen- und Praedikatenlogik mit ihren undifferenzierten und auf Buchstaben (Symbole) reduzierten „Aussagen“ (die hier vollkommen unpassend sind, da mathematische Logik mit der Arithmetik nichts gemein hat) war ueberfaellig und wird in diesem Aufsatz belegt. 3) In der Logik der Realitaet haben alle von vornherein willkuerlich als falsch erklaerte Praemissen nichts zu suchen. Warum sie bei den einzelnen Operatoren jeweils in drei von vier theoretischen Kombinationen absichtlich eingebaut werden, entbehrt jeden praktischen, aber auch theoretischen, Sinns. 4) Die hier vorzutragenden Argumente fuer eine unbegrenzt mehrwertige Logik und das bisherige bewusste Missinterpretieren der sog. Fuzzy-Logik stellen ebenfalls eine eigene und offensichtlich neue Idee dar. 5) Ausserdem werden in diesem Aufsatz die Bezeichnungen Null (0) und (vor allem) Eins (1) hinterfragt, und es wird der naheliegende Vorschlag gemacht, die Benennungen Null (0) und Eins (1) von den benebelnden, das Weiterdenken blockierenden und trotz Boole auch falschen, Begriffen „wahr“ und „falsch“ zu trennen. 6) Das Zusammensetzen von (nur zwei) Aussagen, die a) fuer die Logik keineswegs verbunden werden muessten und b) deren zwangslaeufiges Zusammengehoeren sowohl in der Praxis, als auch in der Theorie, (mit Ausnahme von dem „wenn-dann“-Operator) bei allen Operatoren stets unpassend ist, wird ebenfalls in diesem Aufsatz dargelegt. 7) Die Unsinigkeit fuer jegliche Logik, a) einige Operatoren durch leichte Variationen zu ergaenzen (z.B. V und XOR) und b) fuer diese dann teilweise abweichende Wahrheitswerte zu behaupten, wird kritisch vermerkt (und offensichtlich erstmalig bemerkt). 8) Das starre und sowohl praktisch als auch theoretisch aussagelose System in den Wahrheitstabellen usw. wird ebenfalls konstatiert. Die Tatsache, dass es sich hier lediglich um eine im Voraus festgelegte und keineswegs durchgaengig logische Skala handelt, die die Informatiker seit Shannon freundlicherweise fuer ihre „Namensgebungen“ (mit jeweils ein paar definierten Eigenschaften) nutzen (aber nicht nutzen muessten), wird kritisch dargestellt. 9) Das in diesem Aufsatz kurz angerissene Thema zum Zaehlen von Zahlen ist simpel, aber selbst entwickelt und neu. Diese Festlegung, dass sich die Elemente einer Menge den in ihrer Reihenfolge und in ihrem Abstand zueinander im Voraus festgelegten Zahlen anpassen muessen und nicht umgekehrt, macht den Blick frei fuer den u.g. Punkt 10) dieses Resuemees. 10) Durch den vorgenannten Punkt 9) werden die umfassenden Unterschiede zwischen der Mathematik und der mathematischen Logik offensichtlich, die klar belegen, dass die mathematische Logik nichts mit Mathematik zu tun hat und dass darum der Anspruch der mathematischen Logik, ein „Sonderrecht“ darauf zu haben, auf Semantik keinen Wert legen zu muessen und selbst entscheiden zu koennen, was „wahr“ und was „falsch“ ist, nach logischen Gesichtspunkten unhaltbar ist.

In this thesis, we use the means of reverse mathematics in order to study the proof-theoretic strength of several principles involving well orders and well partial orders. The strengths of our considered statements cover each of the Big Five, the most prominent systems of reverse mathematics, as well as some outliers of the so-called "zoo". We begin by exploring effective transfinite recursion, a concept from recursion theory that can be used for the definition of computable functions along ordinals. In the context of second-order arithmetic, the logical framework of reverse mathematics, we can formulate a similar principle, that allows for the recursive definition of a family of sets using effective means along well orders. We compare a definition due to Dzhafarov, Flood, Solomon, and Westrick with a variation due to Freund and determine their proof-theoretic strengths, characterized by the systems WKL\(_0\) and ACA\(_0\), respectively. Also, we discuss a rule version of this recursion principle, which is already available in the weakest of the Big Five: RCA\(_0\). It is easy to define a partial order on finite sequences. This operation preserves well partial orders, a result known as Higman's lemma, and can be used to characterize arithmetical comprehension. Gordeev could show that a variant of Higman's lemma involving a so-called gap condition, which goes back to Friedman, captures ATR\(_0\). We reproduce his result by a simpler proof and extend it to well partial orders as well as other variants of the gap condition and certain trees. For the case of well orders, we determine the maximal order types of all considered structures. The termination of Goodstein sequences is a popular example of a true statement that cannot be proved using the means of Peano arithmetic or, in our case, arithmetical comprehension. In order to obtain a higher proof-theoretic strength using such a principle, Abrusci, Girard, and van de Wiele combined a similar construction with Girard's concept of dilators. The termination of the resulting inverse Goodstein sequence is true, but not provable in certain impredicative systems such as ID\(_1\). In fact, the termination happens at the well-known Bachmann-Howard ordinal. Inspired by a conjecture due to Andreas Weiermann, we capture the strength of general increasing dilator sequences using \(\Pi^1_1\)-comprehension, the characterizing axiom of \(\Pi^1_1\)-CA\(_0\). For this, we employ the new tool of 1-fixed points due to Freund and Rathjen, which is based on the earlier concept of Bachmann-Howard fixed points due to Freund. The close connection between points of termination of increasing dilator sequences and 1-fixed points allows explicit notation systems for the reached ordinals and is valid even outside the confines of second-order arithmetic. Our final topic considers the uniform Kruskal theorem due to Freund, Rathjen, and Weiermann. This principle, which is closely related to Bachmann-Howard- and 1-fixed points, generalizes the well-known Kruskal theorem and allows for the construction of recursive data types that are well partial orders. The main result of these authors is the equivalence between their theorem and the principle of \(\Pi^1_1\)-comprehension. However, this equivalence is not proved over only RCA\(_0\), but requires a further axiom ADS, a weak consequence of Ramsey's theorem. Following from an observation on a proof due to Hirst, we show that this additional axiom can be omitted. In joint work with Anton Freund, however, we reveal by certain conservativity results that assumptions like ADS are crucial for giving fragments of the uniform Kruskal theorem proof-theoretic strength. / In dieser Arbeit nutzen wir die Mittel der reversen Mathematik um die beweistheoretische Stärke einiger Prinzipien über Wohlordnungen und Wohlpartialordnungen zu studieren. Die Stärken der betrachteten Aussagen decken alle der Big Five ab, die bedeutendsten Systeme der reversen Mathematik, sowie einige Sonderfälle im sogenannten "Zoo". Zunächst beschäftigen wir uns mit effektiver transfiniter Rekursion, einem Konzept aus der Rekursionstheorie, mit dessen Hilfe sich berechenbare Funktionen entlang von Ordinalzahlen definieren lassen. Im Kontext der zweitstufigen Arithmetik, dem logischen Rahmen der reversen Mathematik, lässt sich ein sehr ähnliches Prinzip formulieren, das die rekursive Definition einer Familie von Mengen entlang einer Wohlordnung durch effektive Mittel erlaubt. Wir vergleichen eine Definition durch Dzhafarov, Flood, Solomon und Westrick mit einer Abwandlung durch Freund und bestimmen ihre jeweiligen beweistheoretischen Stärken, charakterisiert durch die Systeme WKL\(_0\) und ACA\(_0\). Außerdem diskutieren wir eine Version dieses Rekursionsprinzips als Regel, die bereits im schwächsten System der Big Five verfügbar ist: RCA\(_0\). Auf endlichen Folgen lässt sich eine einfache partielle Ordnung definieren. Diese Operation erhält Wohlpartialordnungen, ein Resultat bekannt als Higmans Lemma, und kann genutzt werden um arithmetische Komprehension zu charakterisieren. Gordeev konnte zeigen, dass eine Variante von Higmans Lemma mit einer sogenannten Lückenbedingung versehen, die auf Friedman zurückgeht, ATR\(_0\) charakterisiert. Wir reproduzieren sein Resultat durch einen einfacheren Beweis und erweitern es sowohl für Wohlpartialordnungen als auch für andere Varianten der Lückenbedingung und gewisse Bäume. Im Fall für Wohlordnungen bestimmen wir die maximalen Ordnungstypen aller betrachteten Strukturen. Die Terminierung von Goodstein-Folgen ist ein beliebtes Beispiel für eine wahre Aussage, die sich mit den Mitteln der Peanoarithmetik oder, in unserem Fall, arithmetischer Komprehension nicht beweisen lässt. Um eine höhere beweistheoretische Stärke durch ein solches Prinzip zu erhalten, kombinierten Abrusci, Girard und van de Wiele eine ähnliche Konstruktion mit Girards Konzept der Dilatoren. Die Terminierung der so entstandenen inversen Goodstein-Folge ist wahr, aber in gewissen imprädikativen Systemen, wie etwa ID\(_1\), nicht mehr beweisbar. Tatsächlich findet die Terminierung an der bekannten Bachmann-Howard-Ordinalzahl statt. Inspiriert durch eine Vermutung von Andreas Weiermann charakterisieren wir hier die Stärke von allgemeinen aufsteigenden Dilator-Folgen durch das charakterisierende Axiom von \(\Pi^1_1\)-CA\(_0\). Dafür benutzen wir das neue Werkzeug der 1-Fixpunkte von Freund und Rathjen, welches auf dem früheren Konzept der Bachmann-Howard-Fixpunkte durch Freund basiert. Die enge Beziehung zwischen den Terminierungspunkten von aufsteigenden Dilator-Folgen und 1-Fixpunkten erlaubt explizite Notationssysteme für die erreichten Ordinalzahlen und ist auch außerhalb der zweitstufigen Arithmetik gültig. Unser letztes Thema behandelt das uniforme Kruskal-Theorem von Freund, Rathjen und Weiermann. Dieses Prinzip, stark verwandt mit Bachmann-Howard- und 1-Fixpunkten, verallgemeinert das bekannte Kruskal-Theorem und erlaubt die Konstruktion von rekursiven Datentypen, die zugleich Wohlpartialordnungen sind. Das Hauptergebnis dieser Autoren ist die Äquivalenz des Theorems mit dem Prinzip der \(\Pi^1_1\)-Komprehension. Jedoch findet diese Charakterisierung nicht über RCA\(_0\) statt, sondern benötigt ein weiteres Axiom ADS, eine schwache Konsequenz von Ramseys Theorem. Als Folge einer Beobachtung in einem Beweis durch Hirst zeigen wir, dass dieses zusätzliche Axiom nicht benötigt wird. In gemeinsamer Arbeit mit Anton Freund zeigen wir jedoch durch gewisse Konservativitätsresultate, dass die Annahme von Axiomen wie ADS entscheidend ist um Abschwächungen des uniformen Kruskal-Theorems beweistheoretische Stärke zu verleihen.

Inhalt der Dissertation ist der Einfluß, den die von Alfred Tarski formulierte mathematische Logik auf die Entstehung der drei Computerkonzepte des Konrad Zuse hatte.