Sind Mengen und Symbole die Bausteine ​​der Mathematik?

Die Dinge, die Sie tatsächlich auf das Papier oder ein anderes Medium schreiben, sind nicht als mathematische Objekte definierbar. Mathematische Strukturen können höchstens verwendet werden, um die realen Weltstrukturen zu modellieren (oder anzunähern). Zum Beispiel könnten wir sagen, dass wir Zeichenketten beliebiger Länge haben können, aber in der realen Welt würden uns das Papier, die Tinte oder die Atome oder was auch immer wir zum Speichern unserer physischen Repräsentationen von Zeichenketten verwenden, ausgehen.

Mal sehen, was wir in welcher Reihenfolge nicht kreisförmig bauen können.

Natürliche Sprache

Letztlich läuft alles auf die natürliche Sprache hinaus. Wir können einfach nicht alles definieren, bevor wir es verwenden. Zum Beispiel können wir "define" nicht definieren... Wir hoffen jedoch, so wenige und so intuitive Konzepte wie möglich (in natürlicher Sprache beschrieben) zu verwenden, um zu formalen Systemen zu gelangen, die "mächtiger" sind. Fangen wir also an.

Natürliche Zahlen und Zeichenketten

Wir gehen einfach von den üblichen Eigenschaften natürlicher Zahlen (Arithmetik und Ordnung) und Zeichenketten (Symbolextraktion, Länge und Verkettung) aus. Wenn wir diese nicht einmal annehmen, können wir keine Zeichenfolgen manipulieren und keinerlei Syntax definieren. Es ist praktisch anzunehmen, dass jede natürliche Zahl eine Zeichenfolge ist (z. B. mit binärer Codierung).

Programmspezifikation

Wählen Sie eine vernünftige Programmiersprache. Ein Programm ist ein String, der eine Folge von Aktionen angibt , von denen jede entweder ein grundlegender String-Manipulationsschritt oder ein bedingter Sprung ist . In einem einfachen String-Manipulationsschritt können wir auf beliebige Strings mit Namen verweisen . Zunächst sind alle im Programm benannten Strings leer, mit Ausnahme des benannten Strings$input$, die die Eingabe für das Programm enthält. Ein bedingter Sprung ermöglicht es uns zu testen, ob eine grundlegende Bedingung wahr ist (sagen wir, dass eine Zahl ungleich Null ist) und zu einem anderen Schritt im Programm zu springen, wenn dies der Fall ist. Wir können einfach a implementieren$k$-fache Iteration einer Folge von Aktionen unter Verwendung eines natürlichen Zahlenzählers, der auf gesetzt ist$k$vor dieser Sequenz und wird um verringert$1$nach der Sequenz, und solange zum Anfang der Sequenz springen$k$ist ungleich Null. Die Ausführung eines Programms auf einem Eingang folgt einfach dem Programm (mit$input$mit der Eingabe am Anfang) bis wir das Ende erreichen, an welchem ​​Punkt das Programm angeblich anhält , und was auch immer in der Zeichenfolge named gespeichert ist$output$wird als Ausgabe des Programms übernommen. (Es ist möglich, dass das Programm nie das Ende erreicht, in diesem Fall wird es nicht angehalten. Beachten Sie, dass wir an dieser Stelle (noch) nicht bestätigen wollen, dass jede Programmausführung entweder anhält oder nicht anhält. In besonderen Fällen werden wir vielleicht können wir beobachten, dass es nicht aufhören wird, aber wenn wir es nicht sagen können, werden wir vorerst einfach sagen: "Wir wissen es nicht.")

Eine spezielle Klasse von Programmen sind diejenigen, bei denen bedingte Sprünge nur verwendet werden, um Iterationen durchzuführen (in der oben beschriebenen Weise). Diese Programme werden immer bei jeder Eingabe beendet und sind daher in gewisser Weise die primitivsten. Tatsächlich werden sie primitiv rekursiv genannt. Sie sind auch in dem Sinne am akzeptabelsten, dass Sie "deutlich sehen" können, dass sie immer anhalten, und daher ist es sehr "wohldefiniert", über die Sammlung von Zeichenfolgen zu sprechen, die sie akzeptieren (die Ausgabe ist nicht die leere Zeichenfolge). da sie immer innehalten und entweder akzeptieren oder nicht akzeptieren. Wir nennen solche Sammlungen auch primitiv rekursiv. (Nebenbei bemerkt gibt es Programme, die immer anhalten, aber nicht primitiv rekursiv sind.)

Formale Systemspezifikation

Wir können jetzt Programme verwenden, um ein formales System darzustellen. Insbesondere ein nützliches formales System$T$hat eine Sprache $L$, die eine primitive rekursive Sammlung von Zeichenfolgen ist, die hier als Sätze über bezeichnet werden$T$, von denen einige angeblich beweisbar sind$T$. Oft$T$kommt mit einem deduktiven System , das aus Regeln besteht , die festlegen, welche Sätze Sie bereits bewiesene Sätze beweisen können. Wir könnten jede Regel in der Form "$φ_1,φ_2,...,φ_k \vdash ψ$“, das sagt das, wenn Sie es bereits bewiesen haben$φ_1,φ_2,...,φ_k$dann kannst du es beweisen$ψ$. Es kann sogar unendlich viele Regeln geben, aber das wichtigste Merkmal ist ein nützliches$T$ist, dass es ein einziges primitives rekursives Programm gibt, das verwendet werden kann, um einen einzigen deduktiven Schritt zu überprüfen , nämlich eine einzige Anwendung einer der Regeln. Speziell für eine solche$T$Es gibt ein primitives rekursives Programm$P$die einen String akzeptiert$x$iff$x$codiert eine Folge von Sätzen$φ_1,φ_2,...,φ_k,ψ$so dass$φ_1,φ_2,...,φ_k \vdash ψ$.

Da alle nützlichen formalen Systeme ein solches Programm haben, können wir jeden Anspruch auf einen Satz überprüfen$φ$ist nachweisbar vorbei$T$, solange sie die gesamte Folge deduktiver Schritte liefern, was eine mögliche Form des Beweises ist .

Bis jetzt sehen wir, dass alles, wozu wir uns philosophisch verpflichten müssen, die Fähigkeit ist, (endlich viele) String-Manipulationen durchzuführen, und wir können an den Punkt kommen, an dem wir Beweise über jedes nützliche formale System verifizieren können. Dazu gehören die Systeme erster Ordnung PA und ZFC. In diesem Sinne können wir natürlich alles tun, was ZFC tun kann, aber ob unsere String-Manipulationen überhaupt eine Bedeutung haben oder nicht, kann nicht ohne stärkeres ontologisches Engagement beantwortet werden.

Gödels Unvollständigkeitssätze

An dieser Stelle können wir bereits Gödels Unvollständigkeitssätze sowohl in äußerer als auch in innerer Form „erhalten“. In beiden wird uns ein nützliches formales System gegeben$T$das kann auch beweisen, was PA beweisen kann (unter geeigneter Übersetzung). Angesichts eines beliebigen Satzes$P$über$T$, können wir einen Satz bilden$Prov_T(P)$über$T$das soll sagen "$P$ist nachweisbar vorbei$T$". Dann lassen wir$Con(T) = ¬Prov_T(\bot)$. Um die äußere Form zu „erhalten“ (ggf$T$beweist$Con(T)$Dann$T$beweist$\bot$), können wir explizit ein Programm aufschreiben, das als Eingabe irgendeinen Beweis dafür liefert$Con(T)$über$T$erzeugt als Ausgabe einen Proof of$\bot$über$T$. Und um die interne Form zu 'erhalten', können wir explizit einen Beweis darüber schreiben$T$des Satzes "$Con(T) \rightarrow \neg Prov_T(Con(T))$". (Siehe dies für genauere Aussagen zu dieser Art von Ergebnis.)

Der Haken ist, dass der Satz „$Prov_T(P)$" ist völlig bedeutungslos, es sei denn, wir haben eine Vorstellung von der Interpretation eines Satzes$T$, die wir bisher komplett vermieden haben, damit alles rein syntaktisch ist. Zu einer Grundform der Bedeutung kommen wir im nächsten Abschnitt.

Grundlegende Modelltheorie

Nehmen wir an, wir möchten bestätigen können, dass jedes gegebene Programm bei einer gegebenen Eingabe entweder anhält oder nicht anhält. Wir können dies tun, wenn wir LEM (das Gesetz des ausgeschlossenen Dritten) akzeptieren . Damit können wir nun grundlegende Eigenschaften etwa ausdrücken$T$, zum Beispiel, ob es konsistent ist (beweist nicht sowohl einen Satz als auch seine Negation), und ob es vollständig ist (beweist immer entweder einen Satz oder seine Negation). Dies gibt den Unvollständigkeitssätzen von Gödel eine Bedeutung. Von der externen Form, wenn$T$wirklich konsistent ist, dann kann es nicht beweisen$Con(T)$wenngleich$Con(T)$entspricht über die Übersetzung einer Aussage über die natürlichen Zahlen, die gilt gw$T$ist konsistent.

Aber wenn wir weiterhin in der Lage sein wollen, über die Sammlung von Strings zu sprechen, die von einem Programm akzeptiert werden (nicht nur primitive rekursive), fordern wir in diesem Fall im Wesentlichen ein stärkeres Mengenverständnis- Axiom$Σ^0_1$-Verständnis (nicht nur$Δ^0_0$-Verständnis). Der Bereich der umgekehrten Mathematik umfasst das Studium der Unterscheidung zwischen solchen schwachen mengentheoretischen Axiomen, und der verlinkte Wikipedia-Artikel erwähnt diese Konzepte und andere, über die ich später sprechen werde, aber eine viel bessere Referenz ist dieses kurze Dokument von Henry Towsner . Mit$Σ^0_1$-Verständnis können wir von der Sammlung aller Sätze sprechen, die beweisbar sind$T$, wohingegen wir früher über einen solchen Satz sprechen konnten, aber nicht über die gesamte Sammlung als ein einzelnes Objekt.

Um nun den Kompaktheitssatz auch für die (klassische) Aussagenlogik zu beweisen, brauchen wir noch mehr, nämlich WKL (schwaches Lemma von König) . Und da der Kompaktheitssatz eine triviale Folge des Vollständigkeitssatzes ist (z. B. für die natürliche Deduktion), muss WKL auch den Vollständigkeitssatz beweisen. Dasselbe gilt für die Logik erster Ordnung.

Turing-Sprünge

Nun macht es aus philosophischer Sicht nicht wirklich Sinn, nur zu haben$Σ^0_1$-Verständnis. Schließlich ist das in gewisser Weise gleichbedeutend damit, ein Orakel für das Halteproblem (für gewöhnliche Programme) zu haben, das der erste Turing-Sprung ist . Das Halteproblem ist unentscheidbar , was bedeutet, dass es kein Programm gibt, das bei jeder Eingabe immer anhält$(P,x)$und akzeptiert iff$P$hält an$x$. Indem man es zulässt$Σ^0_1$-Verständnis erhalten wir gewissermaßen Zugang zu einem solchen Orakel. Aber wenn wir dann erweiterte Programme betrachten, die den ersten Turing-Sprung verwenden dürfen (er wird die Antwort in einem Schritt erhalten), wird das Halteproblem für diese Programme wieder von jedem selbst unentscheidbar sein, aber wir können uns ein Orakel vorstellen auch dafür, das ist der zweite Turing-Sprung. Da wir das erste zugelassen haben, gibt es keinen wirklich guten Grund, das zweite zu verbieten. Usw.

Das Endergebnis ist, dass wir genauso gut ein vollständiges arithmetisches Verständnis akzeptieren könnten (wir können jede Menge von Strings oder natürlichen Zahlen konstruieren, die durch eine Formel definiert werden können, in der alle Quantoren über natürlichen Zahlen oder Strings stehen). Und aus metalogischer Sicht sollten wir auch das vollständige Induktionsschema zweiter Ordnung haben, weil wir bereits davon ausgehen, dass wir nur Annahmen akzeptiert haben, die für die natürlichen Standardzahlen gelten, nämlich solche, die in der Form ausdrückbar sind$1+1+\cdots+1$".

Beachten Sie, dass alles bis zu diesem Punkt als prädikativ angesehen werden kann, in dem Sinne, dass wir zu keinem Zeitpunkt ein Objekt konstruieren, dessen Definition vom Wahrheitswert einer Behauptung abhängt, die sich selbst betrifft (z. B. über einen Quantor, dessen Bereich das zu konstruierende Objekt umfasst). ). Damit sind die meisten konstruktiv veranlagten Logiker bis hierher vollkommen zufrieden.

Höhere Modelltheorie

Wenn Sie nur zählbare prädikative Mengen als ontologisch gerechtfertigte akzeptieren, insbesondere prädikative Mengen von Zeichenfolgen (oder gleichwertige Teilmengen der natürlichen Zahlen), dann ist das Obige so ziemlich alles, was Sie brauchen. Beachten Sie, dass wir von Anfang an implizit ein endliches Alphabet für alle Zeichenketten angenommen haben. Dies impliziert, dass wir nur abzählbar viele Strings haben und daher keine Dinge wie formale Systeme mit überabzählbar vielen Symbolen haben können. Diese kommen häufig in der höheren Modelltheorie vor. Wenn wir also in der Lage sein wollen, etwas Unzählbares zu konstruieren, bräuchten wir viel mehr, wie z. B. ZFC.

Ein Beispiel für die Verwendung der Macht von ZFC ist die Konstruktion von Nicht-Standard-Modellen über Ultrakräfte , die die Verwendung einer schwachen Art des Axioms der Wahl erfordern . Das Schöne an dieser Konstruktion ist, dass sie elegant ist, und zum Beispiel kann man sehen, dass das resultierende nicht standardmäßige Modell der reellen Zahlen die Idee recht gut einfängt, Sequenzen von reellen Zahlen modulo einer Äquivalenzrelation als Modell für die erste Ordnung zu verwenden Theorie der reellen Zahlen, bei der ein eventuell konsistentes Verhalten die entsprechenden Eigenschaften impliziert. Der nicht-konstruktive Ultrafilter wird benötigt, um zu spezifizieren, ob die Eigenschaft in dem Fall ohne letztendlich konsistentes Verhalten gilt.

Ich hoffe, ich habe überzeugend gezeigt, dass, obwohl wir sehr wenig brauchen, um mit der Definition und Verwendung eines formalen Systems, einschließlich ZFC, zu beginnen , das ganze Symbol-Pushing bedeutungslos ist, es sei denn, wir nehmen mehr an und je mehr Bedeutung wir ausdrücken wollen oder beweisen , desto stärkere Annahmen brauchen wir. ZFC (mit Ausnahme des Gründungsaxioms) ist historisch gesehen das erste ausreichend starke System, das alles kann, was Mathematiker getan haben, und daher ist es nicht verwunderlich, dass es auch als Metasystem zum Studium der Logik verwendet wird. Aber Sie werden ZFC nicht ontologisch rechtfertigen können , wenn Sie danach suchen.

Mengen in Mengentheorien

Schließlich könnte Ihre Frage auf einem weit verbreiteten Missverständnis beruhen, dass Sie in ZFC einen Begriff von "Set" haben. Nicht wirklich. ZFC ist nur ein weiteres formales System und hat kein Symbol, das "Set" darstellt. Es ist einfach so, dass die Axiome von ZFC so gemacht wurden, dass es vernünftig erscheint anzunehmen, dass sie für einen vagen Begriff von "Mengen" in natürlicher Sprache gelten. Innerhalb von ZFC erstreckt sich jeder Quantor über die gesamte Domäne, und daher kann man nicht über Mengen sprechen, als ob es andere Arten von Objekten gäbe. Wenn wir ein Metasystem verwenden, das keine Mengen hat, dann hat ein Modell von ZFC möglicherweise überhaupt keine „Mengen“, was auch immer „Menge“ bedeuten mag!

In ZFC kann man nicht von "der Russell-Menge" sprechen, da uns das Verstehensaxiom nicht erlaubt, eine solche Sammlung zu konstruieren. In der MK-Mengentheorie (Morse-Kelley) gibt es einen internen Begriff von Mengen, und man kann jede Klasse von Mengen konstruieren, die durch eine Formel definierbar ist, aber man kann aus demselben Grund wie Russell nichts konstruieren, das einer "Klasse von Klassen" ähnelt Paradox.

In der Nicht-Mainstream-Mengentheorie NFU hat man sowohl Mengen als auch Urelemente (Extensionalität gilt nur für Mengen), und daher kann es sinnvoll sein, hier über Mengen zu sprechen. Aber NFU ist sowieso kein sehr benutzerfreundliches System.

Und hier soll auch meine Antwort aufhören.