Konstruktive Mengenlehre - Constructive set theory

Die konstruktive Mengenlehre ist ein Ansatz des mathematischen Konstruktivismus, der dem Programm der axiomatischen Mengenlehre folgt . Üblicherweise wird dieselbe Sprache erster Ordnung mit " " und " " der klassischen Mengenlehre verwendet, daher ist dies nicht mit einem konstruktiven Typenansatz zu verwechseln . Auf der anderen Seite werden einige konstruktiven Theorien in der Tat durch ihre Interpretierbarkeit in motivierten Art Theorien .

Neben der Ablehnung Satz vom ausgeschlossenen Dritten ( ), oft konstruktive Satz Theorien einige logische Quantoren in ihre Axiome erfordern werden begrenzt durch die Ergebnisse gebunden, motiviert impredicativity .

Einführung

Ausblick

Die Logik der hier diskutierten Mengentheorien ist insofern konstruktiv , als sie verwirft , dh dass die Disjunktion automatisch für alle Aussagen gilt. Dies erfordert dann die Ablehnung starker Wahlprinzipien und die Neuformulierung einiger Standardaxiome. Zum Beispiel kann das Auswahlaxiom impliziert für die Formeln in einem Adoptiv Trennung Schema, durch Diaconescu Theorem . Ähnliche Ergebnisse gelten für das Regularitätsaxiom in seiner Standardform. In der Regel muss zum Nachweis einer bestimmten Disjunktion entweder oder bewiesen werden. In diesem Fall sagt man, die Disjunktion sei entscheidbar. Im Gegenzug dazu neigen , konstruktive Theorien nicht viele klassische Beweise Eigenschaften ermöglichen , die beweisbar rechnerisch sind zB unentscheidbar . Im Gegensatz zur konservativeren Minimallogik erlaubt die zugrunde liegende Logik hier die Eliminierung der doppelten Negation für entscheidbare Prädikate und die Satzformulierungen bezüglich endlicher Konstruktionen unterscheiden sich tendenziell nicht von ihren klassischen Gegenstücken.

Bemerkenswerterweise führt eine Beschränkung auf die konstruktive Logik zu strengeren Anforderungen, welche Charakterisierungen einer Menge mit unbeschränkten Sammlungen eine (mathematische und damit immer implizierende totale ) Funktion darstellen. Dies liegt oft daran, dass das Prädikat in einer fallweisen Möchtegern-Definition möglicherweise nicht entscheidbar ist. Im Vergleich zum klassischen Gegenstück ist es in der Regel weniger wahrscheinlich, die Existenz nicht realisierbarer Beziehungen nachzuweisen. Dies betrifft dann auch die Beweisbarkeit von Aussagen über Gesamtordnungen wie die aller Ordnungszahlen , ausgedrückt durch Wahrheit und Negation der Terme in der ordnungsdefinierenden Disjunktion . Und dies wiederum beeinflusst die in der Ordinalanalyse definierte beweistheoretische Stärke .

Allerdings neigen konstruktive mathematische Theorien im Allgemeinen dazu, klassisch äquivalente Neuformulierungen klassischer Theoreme zu beweisen . Beispielsweise kann man in der Konstruktiven Analysis den Zwischenwertsatz nicht in seiner Lehrbuchformulierung beweisen, wohl aber Sätze mit algorithmischem Inhalt, die, sobald angenommen, klassisch äquivalent zur klassischen Aussage sind. Der Unterschied besteht darin, dass die konstruktiven Beweise schwerer zu finden sind.

Auf Modellen

Viele Theorien, die in der konstruktiven Mengenlehre untersucht wurden, sind nur Einschränkungen der Zermelo-Fraenkel-Mengentheorie ( ) in Bezug auf ihr Axiom sowie ihre zugrunde liegende Logik. Solche Theorien können dann auch in jedem beliebigen Modell von interpretiert werden . Was konstruktive Realisierungen angeht, gibt es eine Realisierbarkeitstheorie und Aczels Theorie konstruktives Zermelo-Fraenkel ( ) wurde in Theorien vom Martin-Löf-Typ interpretiert , wie unten beschrieben. Auf diese Weise sind in und schwächere Theorien beweisbare Mengenlehre Kandidaten für eine Computerrealisierung. In jüngerer Zeit wurden Presheaf- Modelle für konstruktive Mengentheorien eingeführt. Diese sind analog zu unveröffentlichten Presheaf-Modellen für die intuitionistische Mengenlehre, die Dana Scott in den 1980er Jahren entwickelt hat.

Überblick

Das Thema der konstruktiven Mengenlehre (oft " ") begann mit John Myhills Arbeit an der Theorie, die auch als Theorie verschiedener Arten und begrenzter Quantifizierung bezeichnet wird und darauf abzielt, eine formale Grundlage für Errett Bishops Programm der konstruktiven Mathematik zu schaffen. Unten ist eine Reihe von Theorien in derselben Sprache wie , die zu Peter Aczels gut studierten und darüber hinaus führen. zeichnet sich auch durch die beiden Merkmale aus, die auch in Myhills Theorie vorhanden sind: Einerseits verwendet sie das prädikative Separation anstelle des vollständigen, unbegrenzten Separation-Schemas, siehe auch Lévy-Hierarchie . Beschränktheit kann als syntaktische Eigenschaft behandelt werden oder alternativ können die Theorien mit einem höheren Beschränktheitsprädikat und seinen Axiomen konservativ erweitert werden. Zweitens wird das imprädikative Powerset-Axiom verworfen, im Allgemeinen zugunsten verwandter, aber schwächerer Axiome. Die starke Form wird in der klassischen allgemeinen Topologie sehr beiläufig verwendet . Das Hinzufügen zu einer Theorie, die noch schwächer ist als erholt , wie unten beschrieben. Das System, das als Intuitionistische Zermelo-Fraenkel-Mengentheorie ( ) bekannt wurde, ist eine starke Mengentheorie ohne . Es ist ähnlich , aber weniger konservativ oder prädikativ . Die angegebene Theorie ist die konstruktive Version von , der klassischen Kripke-Platek-Mengentheorie, bei der sogar das Sammlungsaxiom beschränkt ist.

Subtheorien von ZF

Notation

Unter dem Griechischen bezeichnen Sie eine Prädikatsvariable in Axiomenschemata und verwenden oder für bestimmte Prädikate. Eindeutige Existenz bedeutet zB . Quantifizierer reichen über den Satz und diese werden durch Kleinbuchstaben gekennzeichnet.

Wie im Studium der Mengentheorien üblich , verwendet man die Set-Builder-Notation für Klassen , die in den meisten Kontexten nicht Teil der Objektsprache sind, sondern für eine prägnante Diskussion verwendet werden. Insbesondere kann man mit " " Notationsdeklarationen der entsprechenden Klasse einführen , um als auszudrücken . Logisch äquivalente Prädikate können verwendet werden, um dieselbe Klasse einzuführen. Man schreibt auch als Abkürzung für .

Wie üblich ist, kann man abkürzen durch die Unterklasse und Anspruch exprimieren , das heißt , durch .

Für eine Eigenschaft trivialerweise . Und so folgt das .

Gemeinsame Axiome

Ein Ausgangspunkt von Axiomen, die praktisch immer als unumstritten gelten und Teil aller in diesem Artikel behandelten Theorien sind.

Bezeichnen Sie mit der Anweisung, die ausdrückt, dass zwei Klassen genau die gleichen Elemente haben, dh , oder äquivalent .

Das folgende Axiom gibt ein Mittel zum Beweisen der Gleichheit " " von zwei Mengen an , so dass durch Substitution jedes Prädikat über in eines von übersetzt wird .

Dehnbarkeit

Aufgrund der logischen Eigenschaften der Gleichheit gilt automatisch die umgekehrte Richtung.

In einer konstruktiven Interpretation können die Elemente einer Unterklasse von mit mehr Informationen ausgestattet sein als die von , in dem Sinne, dass urteilen können urteilen können . Und (es sei denn, die ganze Disjunktion folgt aus Axiomen) in der Brouwer-Heyting-Kolmogorov-Interpretation bedeutet dies, sie bewiesen oder abgelehnt zu haben. Da möglicherweise nicht für alle Elemente in entscheidbar ist , müssen die beiden Klassen a priori unterschieden werden.

Betrachten Sie eine Eigenschaft , die beweisbar für alle Elemente einer Menge gilt , so dass , und nehmen Sie an, dass die Klasse auf der linken Seite eine Menge ist. Beachten Sie, dass, auch wenn diese Menge auf der linken Seite informell auch an beweisrelevante Informationen über die Gültigkeit von für alle Elemente bindet , das Extensionalitätsaxiom postuliert, dass in unserer Mengentheorie die Menge auf der linken Seite gleich der einer auf der rechten Seite.

Moderne Typentheorien können stattdessen darauf abzielen, die geforderte Äquivalenz " " in Bezug auf Funktionen zu definieren, siehe zB Typenäquivalenz . Das damit verbundene Konzept der Funktion Extensionalität wird oft nicht in Typentheorie angenommen.

Andere Rahmenwerke für konstruktive Mathematik könnten stattdessen eine bestimmte Regel für Gleichheit oder Getrenntheit für die Elemente jeder einzelnen diskutierten Menge verlangen . Selbst dann kann die obige Definition verwendet werden, um die Gleichheit von Teilmengen und zu charakterisieren .

Zwei weitere grundlegende Axiome wie folgt. Zuerst,

Paarung

sagen, dass es für zwei beliebige Mengen und mindestens eine Menge gibt , die mindestens diese beiden Mengen enthält ( ).

Und dann,

Union

sagt, dass es in jeder Menge mindestens eine Menge gibt , die alle Mitglieder der Mitglieder enthält .

Die beiden Axiome können auch stärker mit " " formuliert werden , zB im Zusammenhang mit Separation, dies ist nicht notwendig.

Zusammen implizieren diese beiden Axiome die Existenz der binären Vereinigung zweier Klassen und wenn sie als Mengen festgelegt wurden, und dies wird mit oder bezeichnet . Definieren Sie die Klassennotation für finite Elemente über Disjunktionen, zB sagt , und definieren Sie die Nachfolgermenge als . Eine Art Mischung zwischen Paarung und Vereinigung, ein Axiom, das leichter mit dem Nachfolger in Verbindung steht, ist das Axiom der Adjunktion . Sie ist relevant für die Standardmodellierung einzelner Neumann-Ordinalzahlen . Dieses Axiom würde auch ohne weiteres akzeptiert werden, ist aber im Zusammenhang mit stärkeren Axiomen unten nicht relevant. Bezeichnet durch das Standard- Ordered-Paar- Modell .

Die Eigenschaft, die für jede Menge falsch ist, entspricht der leeren Klasse, die mit oder Null bezeichnet wird, 0. Dass dies eine Menge ist, folgt leicht aus anderen Axiomen, wie dem folgenden Axiom der Unendlichkeit. Wenn man aber z. B. explizit daran interessiert ist, unendliche Mengen in seinem Studium auszuschließen, kann man an dieser Stelle das Axiom der leeren Menge übernehmen

BCST

Im Folgenden werden Axiomenschemata verwendet , dh Axiome für eine Sammlung von Prädikaten. Beachten Sie, dass einige der angegebenen Axiomenschemata oft auch mit festgelegten Parametern präsentiert werden , dh Varianten mit zusätzlichen universellen Schließungen, so dass die 's von den Parametern abhängen können.

Die grundlegende konstruktive Mengenlehre besteht aus mehreren Axiomen, die auch zur Standardmengentheorie gehören, außer dass das Trennungsaxiom abgeschwächt ist. Jenseits der drei obigen Axiome übernimmt es die

Axiomschema der prädikativen Trennung : Für jedes beschränkte Prädikat mit nicht frei darin

Das Axiom läuft darauf hinaus, die Existenz einer Menge zu postulieren, die durch die Schnittmenge einer beliebigen Menge und einer beliebigen prädikativ beschriebenen Klasse erhalten wird . Wenn das Prädikat als genommen für sich als ein Satz sein, erhält man die binäre Durchschnitt von Mengen und schreibt .

Das Schema wird auch Bounded Separation genannt, wie in Separation nur für mengenbegrenzte Quantoren . Es ist das Axiomenschema, das auf syntaktische Aspekte von Prädikaten Bezug nimmt. Die beschränkten Formeln werden ebenfalls durch bezeichnet in der eingestellten theoretischen Levy-Hierarchie, in Analogie zu in der arithmetischen Hierarchie . (Beachten Sie jedoch, dass die arithmetische Klassifikation manchmal nicht syntaktisch, sondern in Form von Unterklassen der Natürlichen ausgedrückt wird. Außerdem hat die unterste Ebene mehrere gemeinsame Definitionen, von denen einige die Verwendung einiger Gesamtfunktionen nicht zulassen. Die Unterscheidung ist auf der Ebene oder nicht relevant . höher) die Beschränkung im Axiom ist Gatekeeping auch imprädikative Definitionen: Existenz sollten allenfalls für Objekte nicht geltend gemacht werden , die nicht explizit beschreibbar sind, oder whos Definition handelt sich oder Verweis auf eine richtige Klasse, wie zum Beispiel , wenn eine Eigenschaft überprüft werden , beinhaltet ein universeller Quantor. In einer konstruktiven Theorie ohne Axiom der Potenzmenge sollte man also keine Klasse erwarten, die definiert ist als

dh

eine Menge sein, wobei bezeichnet ein 2-äres Prädikat. Beachten Sie, dass, wenn diese Unterklasse beweisbar eine Menge ist, der so definierte Begriff auch im unbegrenzten Geltungsbereich des Begriffs Variable liegt und das Prädikat in Klammern erfüllt , das verwendet wird, um sich selbst zu definieren. Während die prädikative Trennung dazu führt, dass weniger gegebene Klassendefinitionen Mengen sind, muss betont werden, dass viele klassisch äquivalente Klassendefinitionen dies nicht sind, wenn man sich auf die konstruktive Logik beschränkt. Auf diese Weise erhält man konstruktiv eine breitere Theorie. Aufgrund der potentiellen Unentscheidbarkeit allgemeiner Prädikate ist der Begriff der Unterklasse in konstruktiven Mengentheorien ausgefeilter als in klassischen.

Wie bereits erwähnt, folgt aus Trennung und der Existenz einer beliebigen Menge (z. B. Unendlichkeit unten) und dem Prädikat, das einer Menge falsch ist, die Existenz der leeren Menge.

Kraft des rein logischen Theorems zeigt Russels Konstruktion , dass allein die prädikative Trennung dies impliziert . Insbesondere existiert kein universelles Set .

In diesem konservativen Kontext von ist das Bounded Separation-Schema tatsächlich äquivalent zu Empty Set plus der Existenz der binären Schnittmenge für zwei beliebige Sets. Die letztere Variante der Axiomatisierung verwendet kein Schema. Da die Subtypisierung kein notwendiges Merkmal der konstruktiven Typentheorie ist , kann man sagen, dass sich die konstruktive Mengenlehre stark von diesem Rahmen unterscheidet.

Betrachten Sie als nächstes die

Axiom Schema Replacement : Für jedes Prädikat ,

Es gewährt die Existenz der Reihe funktionsähnlicher Prädikate als Mengen, die über ihre Domänen erhalten werden.

Mit dem Ersetzungsschema beweist diese Theorie, dass die Äquivalenzklassen oder indizierten Summen Mengen sind. Insbesondere ist das kartesische Produkt , das alle Paare von Elementen zweier Mengen enthält, eine Menge.

Ersetzung und das Axiom der Mengeninduktion (unten eingeführt) reichen aus, um erblich endliche Mengen konstruktiv zu axiomieren, und diese Theorie wird auch ohne Unendlichkeit studiert. Betrachten Sie zum Vergleich die sehr schwache klassische Theorie namens Allgemeine Mengenlehre , die die Klasse der natürlichen Zahlen und ihre Arithmetik nur über Extensionalität, Adjunktion und vollständige Trennung interpretiert.

In , Ersetzung ist vor allem wichtig, um die Existenz von Mengen von hohem Rang zu beweisen , nämlich durch Instanzen des Axiom-Schemas, in denen relativ kleine Mengen auf größere bezogen werden, .

Konstruktive Mengentheorien haben im Allgemeinen ein Axiom-Schema der Ersetzung, das manchmal auf beschränkte Formeln beschränkt ist. Wenn jedoch andere Axiome fallengelassen werden, wird dieses Schema tatsächlich oft verstärkt - nicht über , sondern lediglich, um etwas Beweiskraft zurückzugewinnen.

Ersetzen kann als eine Form des Verstehens angesehen werden. Nur wenn man davon ausgeht, bedeutet der Austausch bereits eine vollständige Trennung.

ECST

Bezeichne durch die induktive Eigenschaft, zB . In Bezug auf ein Prädikat, das der Klasse zugrunde liegt, würde dies als übersetzt werden . Hier bezeichnet eine allgemeine Setvariable. Schreiben Sie für . Definieren Sie eine Klasse .

Für ein festes Prädikat drückt die Anweisung aus, dass dies die kleinste Menge unter allen Mengen ist, für die gilt. Die elementare konstruktive Mengenlehre hat das Axiom von sowie

Starke Unendlichkeit

Die zweite universell quantifizierte Konjunktion drückt die mathematische Induktion für alle im Diskursuniversum, dh für Mengen bzw. Mengen aus. für Prädikate, wenn sie tatsächlich Mengen definieren . Auf diese Weise liefern die in diesem Abschnitt diskutierten Prinzipien Beweise dafür, dass einige Prädikate zumindest für alle Elemente von gelten . Seien Sie sich bewusst, dass sogar das recht starke Axiom der vollständigen mathematischen Induktion (Induktion für jedes Prädikat, unten diskutiert) auch übernommen und verwendet werden kann, ohne jemals zu postulieren, dass es eine Menge bildet.

Es können schwache Formen von Unendlichkeitsaxiomen formuliert werden, die alle postulieren, dass einige Mengen mit den gemeinsamen natürlichen Zahleneigenschaften existieren. Dann kann die vollständige Trennung verwendet werden, um die "sparse" solche Menge zu erhalten, die Menge der natürlichen Zahlen. Im Kontext ansonsten schwächerer Axiomensysteme sollte ein Axiom der Unendlichkeit verstärkt werden, um die Existenz einer solchen spärlichen Menge für sich allein zu implizieren. Eine schwächere Form von Infinity liest sich

die auch mit prägnanter geschrieben werden können . Die so postulierte Existenz wird allgemein mit der kleinsten unendlichen von Neumann-Ordinalzahl bezeichnet . Für Elemente dieser Menge ist der Anspruch entscheidbar.

Damit beweist Induktion für alle durch begrenzte Formeln Prädikate. Die beiden der fünf Peano-Axiome bezüglich Null und eines bezüglich Geschlossenheit oder bezüglich bezüglich folgen ziemlich direkt aus den Axiomen der Unendlichkeit. Schließlich kann eine injektive Operation nachgewiesen werden.

Natürliche Zahlen sind unterscheidbar, was bedeutet, dass ihre Gleichheit (und damit Ungleichheit) entscheidbar ist. Die Grundordnung wird durch die Mitgliedschaft in diesem Modell erfasst. Um der Standardnotation willen bezeichnen wir ein Anfangssegment der natürlichen Zahlen für alle , einschließlich der leeren Menge.

Funktionen

Natürlich ist die logische Bedeutung von Existenzansprüchen ein Thema von Interesse in der intuitionistischen Logik. Hier stehen die Gesamtbeziehungen im Vordergrund .

Die Beweisrechnung in einem konstruktiven mathematischen Rahmen von Aussagen wie

in Form von Programmen auf vertretenen Domänen eingerichtet werden und möglicherweise Zeugen der Behauptung sein müssen. Dies ist im Sinne von informell zu verstehen , wobei , wie erwähnt, den Wert eines Programms bezeichnet, aber dies gerät in Fragen der Realisierbarkeitstheorie . Für einen stärkeren Kontext, wenn und wenn der Satz zutrifft, dann ist die Forderung, dass dies immer mit einer durch eine totale rekursive Funktion realisierten Funktion möglich sein soll, ein mögliches kirchliches Thesenpostulat, das im konsequent nicht-klassischen russischen Konstruktivismus übernommen wird . Im vorigen Absatz ist "Funktion" im berechenbaren Sinne der Rekursionstheorie zu verstehen - auf diese gelegentliche Mehrdeutigkeit muss auch im Folgenden geachtet werden.

Betrachten Sie in diesem Zusammenhang die Robinson-Arithmetik , eine klassische arithmetische Theorie, die das vollständige mathematische Induktionsschema für eine Existenzbehauptung einer Vorgängerzahl ersetzt. Es ist ein Theorem, dass diese Theorie genau die rekursiven Funktionen im Sinne der Definition von Prädikaten repräsentiert , die beweisbar totale funktionale Beziehungen sind,

.

Jetzt in der aktuellen Reihe theoretischer Ansatz, wdefine die Eigenschaft , um die Einbeziehung Funktionsanwendung Klammern, wie und einer Funktion sprechen , wenn beweisbar

,

dh

,

die insbesondere einen existenziellen Quantor beinhaltet. Ob eine Unterklasse als Funktion beurteilt werden kann, hängt von der Stärke der Theorie ab, dh von den Axiomen, die man annimmt.

Insbesondere könnte eine allgemeine Klasse das obige Prädikat erfüllen, ohne eine Unterklasse des Produkts zu sein , dh die Eigenschaft drückt nicht mehr oder weniger als die Funktionalität bezüglich der Eingaben von aus . Wenn Domäne und Kodomäne Mengen sind, dann beinhaltet das obige Prädikat nur beschränkte Quantoren. Vorsicht ist bei der Nomenklatur "Funktion" geboten, die in den meisten mathematischen Frameworks verwendet wird, auch weil einige einen Funktionsterm selbst an eine bestimmte Codomäne binden. Varianten der funktionalen Prädikatsdefinition, die Apartness-Relationen auf Setoiden verwenden, wurden ebenfalls definiert.

Lassen Sie (auch geschrieben , die Klasse solcher Satz Funktionen) bezeichnen. Unter Verwendung der Standard-Klassenterminologie kann man Funktionen frei verwenden, vorausgesetzt, ihre Domäne ist eine Menge. Die Funktionen als Ganzes werden gesetzt, wenn ihre Co-Domain ist. Wenn Funktionen wie oben nur als Funktionsgraphen verstanden werden, wird auch der Zugehörigkeitssatz geschrieben . Im Folgenden schreiben könnte für aus Gründen es von Ordnungs Potenzierung zu unterscheiden.

Separation ermöglicht die Verwendung von ausgeschnittenen Teilmengen von Produkten , zumindest wenn sie auf begrenzte Weise beschrieben werden. Schreiben Sie für . Angesichts einer beliebigen , wird man jetzt zu einer Überlegung über Klassen wie geführt

Die booleschen charakteristischen Funktionen gehören zu diesen Klassen. Aber seien Sie sich bewusst, dass dies im Allgemeinen nicht entscheidbar sein kann . Das heißt, in Abwesenheit nicht-konstruktiver Axiome ist die Disjunktion möglicherweise nicht beweisbar, da man einen expliziten Beweis für jede Disjunktion benötigt. Wann

nicht für alle bezeugt oder die Eindeutigkeit eines Begriffs nicht nachgewiesen werden kann, dann kann man die begriffene Sammlung nicht konstruktiv als funktionstüchtig beurteilen.

Für und jede natürliche , haben

.

In der klassischen Mengenlehre, bei der die Aussagen in der Definition durch , entscheidbar sind, gilt dies auch für die Unterklassenmitgliedschaft. Wenn die Menge nicht endlich ist, stellt das sukzessive "Auflisten" aller Zahlen durch einfaches Überspringen derjenigen mit klassisch eine steigende surjektive Folge dar . Dort erhält man eine bijektive Funktion . Auf diese Weise ist die klassische Klasse von Funktionen nachweislich reich, da sie auch Objekte enthält, die über das hinausgehen, was wir wissen, um effektiv berechenbar oder in der Praxis programmatisch auflistbar zu sein.

Im Gegensatz dazu sind in der Berechenbarkeitstheorie die berechenbaren Mengen Bereiche von nicht abnehmenden Gesamtfunktionen (im rekursiven Sinne) auf der Ebene der arithmetischen Hierarchie und nicht höher. Die Entscheidung für ein Prädikat auf dieser Ebene kommt der Lösung der Aufgabe gleich, schließlich ein Zertifikat zu finden , das die Mitgliedschaft entweder bestätigt oder ablehnt. Da nicht jedes Prädikat berechenbar entscheidbar ist, wird die Theorie allein nicht behaupten (beweisen), dass alle Unendlichen der Bereich einer bijektiven Funktion mit dem Bereich sind .

Endlich bedeutet, dass ein Natürliches eine bijektive Funktion besitzt. Unterendlich zu sein bedeutet, eine Teilmenge einer endlichen Menge zu sein. Die Behauptung, eine endliche Menge zu sein, sei gleichbedeutend mit unterfinit, ist gleichbedeutend mit .

Die Entwicklung in diesem Abschnitt erlaubt aber, kompatibel mit , auch immer, "Funktion auf " als nicht unbedingt als gesetzmäßige Folge gegebenes Objekt zu interpretieren . Anwendungen finden sich in den gängigen Modellen für Wahrscheinlichkeitsaussagen, zB Aussagen, die die Vorstellung beinhalten, eine endlose zufällige Folge von Münzwürfen "gegeben zu bekommen".

Auswahl

  • Axiom der abzählbaren Wahl : Wenn , kann man die Eins-zu-Viele-Beziehungsmenge bilden . Das Axiom der abzählbaren Auswahl würde gewährleisten, dass man immer dann eine Funktion bilden kann, die jede Zahl auf einen eindeutigen Wert abbildet. Die zählbare Auswahl kann auch weiter abgeschwächt werden, zB durch Einschränkung der möglichen Kardinalitäten der Mengen im Bereich von , oder durch Einschränkung der beteiligten Definitionen bezüglich ihres Platzes in den syntaktischen Hierarchien.
  • Relativisierte abhängige Wahl: Das stärker relativierte Prinzip der abhängigen Wahl ist eine Variante davon - ein Schema, das eine zusätzliche Prädikatsvariable beinhaltet. Diese Annahme für nur begrenzt in den Formeln , die Theorie beweist bereits die - Induktion , weiter unten diskutiert.
  • Auswahlaxiom : Das Auswahlaxiom bezüglich Funktionen auf allgemeinen Gebieten. Es impliziert eine abhängige Wahl.

Um die Stärke der vollen Auswahl und ihre Beziehung zu Fragen der Intentionalität hervorzuheben, sollte man die subfiniten Klassen betrachten

Dabei sind und so kontingent wie die Prädikate, die an ihrer Definition beteiligt sind. Nehmen Sie nun einen Kontext an, in dem sie als Mengen festgelegt sind, also auch. Hier würde das Auswahlaxiom dann die Existenz einer Karte mit unterscheidbaren Elementen gewähren . Das impliziert das nun tatsächlich . Die Existenzbehauptung allgemeiner Wahlfunktionen ist also nicht-konstruktiv. Um dieses Phänomen besser zu verstehen, muss man Fälle mit logischen Implikationen berücksichtigen, wie z. B. et cetera. Der Unterschied zwischen dem diskreten Kobereich einiger natürlicher Zahlen und dem Bereich liegt darin, dass über letztere a priori wenig bekannt ist. Es ist der Fall, dass und , unabhängig von , möglicherweise einen Anwärter auf eine Wahlfunktion machen. Aber im Fall von , wie durch die Beweisbarkeit von impliziert , hat man so, dass es extensional nur eine mögliche Funktionseingabe zu einer Wahl-Wahl-Funktion gibt, jetzt mit nur könnten Wahl-Funktionen oder sein . Betrachtet man also die funktionale Zuordnung , dann wäre unbedingtes Deklarieren nicht konsistent. Die Wahl kann in einer ansonsten starken Mengentheorie nicht übernommen werden, da die bloße Behauptung der Existenz einer Funktion eine bestimmte Funktion nicht realisiert. Unterklassenverständnis (verwendet , um sie zu trennen und von , dh zu definieren) bindet darin beteiligte Prädikate auf die beschriebene Weise an Gleichheit, und dies bezieht sich auf Informationen über Funktionen.

Die konstruktive Entwicklung verläuft oft agnostisch zu den diskutierten Wahlprinzipien.

Arithmetik

Die Annahmen, die notwendig sind, um eine Theorie der Arithmetik zu erhalten, werden in der Beweistheorie gründlich untersucht . Zum Kontext hier ein Absatz zu den darin enthaltenen Klassifikationen: Die klassischen Theorien, die mit beschränkter Arithmetik beginnen , verwenden verschiedene konservative Induktionsschemata und können Symbole für bestimmte Funktionen hinzufügen, was zu Theorien zwischen Robinson- und Peano-Arithmetik führt . Die meisten dieser Theorien sind jedoch relativ schwach in Bezug auf den Totalitätsbeweis für einige schneller wachsende Funktionen . Einige der grundlegendsten Beispiele umfassen die elementare Funktionsarithmetik mit einer beweistheoretischen Ordinalzahl (die am wenigsten nicht beweisbar rekursive Wohlordnung ) von . hat Ordinalzahlen , was bedeutet, dass die Theorie Ordinalzahlen von schwächeren (in diesem Sinne der Ordinalanalyse ) Theorien (z . Das -Induktionsschema, wie es zB durch die relativierte abhängige Wahl impliziert wird, bedeutet Induktion für diejenigen Unterklassen von Naturals, die über eine endliche Suche mit ungebundener (endlicher) Laufzeit berechenbar sind. Das Schema entspricht auch dem -Induktionsschema. Die relativ schwache klassische Arithmetik erster Ordnung, die dieses Schema annimmt, wird bezeichnet . Die -Induktion wird auch das klassische angenommen zweite Ordnung Reverse Mathematik Basissystem . Diese Theorie zweiter Ordnung ist gegenüber der primitiven rekursiven Arithmetik -konservativ , beweist also, dass alle primitiven rekursiven Funktionen total sind. Die zuletzt erwähnten arithmetischen Theorien haben alle Ordinalzahlen . Die erwähnte Arithmetik höherer Ordnung ist insofern ein relevanter Bezugspunkt dieser Diskussion, als ihre Sprache nicht nur arithmetische Mengen ausdrückt , während alle Mengen von Naturals, von denen die Theorie beweist, dass sie existieren, nur berechenbare Mengen sind .

Abgesehen davon interpretiert die Mengentheorie nicht einmal die vollständige primitive Rekursion. Tatsächlich beweist die Theorie trotz des Ersatz-Axioms nicht, dass die Additionsfunktion eine Mengenfunktion ist. Andererseits lassen sich in dieser Theorie viele Aussagen pro individueller Menge belegen (im Gegensatz zu Ausdrücken mit universellem Quantor, wie sie z Individuelle Basis. Als solche reichen die bisher aufgeführten Axiome als grundlegende Arbeitstheorie für einen guten Teil der grundlegenden Mathematik aus. Über die Arithmetik hinausgehend muss das Axiom hinzugefügt werden , das die Definition von Mengenfunktionen über Mengenfunktionen in Iterationsschritten gewährt . Notwendig ist das mengentheoretische Äquivalent eines natürlichen Zahlenobjekts . Dies ermöglicht dann eine Interpretation der Heyting-Arithmetik , . Damit kann dann auch die Arithmetik rationaler Zahlen definiert und deren Eigenschaften, wie Eindeutigkeit und Abzählbarkeit, nachgewiesen werden. Eine Mengentheorie damit wird auch beweisen, dass für alle Naturals und die Funktionsräume

sind Sätze.

Umgekehrt kann ein Beweis des gesuchten Iterationsprinzips auf der Sammlung von Funktionen basieren, als die man schreiben möchte, und die Existenz dieser wird durch die Annahme impliziert, dass die einzelnen Funktionsräume auf endlichen Domänen in Mengen selbst Mengen bilden. Diese Bemerkung sollte die Annahme eines Axioms mit stärkerem theoretischem Flair motivieren, anstatt nur arithmetische Prinzipien direkt in unsere Theorie einzubetten. Das durch das nächste, mehr gesetzte theoretische Axiom erhaltene Iterationsprinzip wird jedoch immer noch nicht das vollständige mathematische Induktionsschema beweisen .

Potenzierung

Eine abgeschwächte Form des Trennungsschemas wurde bereits angenommen, und für eine prädikativere und konstruktivere Theorie sollen weitere der Standardaxiome abgeschwächt werden. Das erste davon ist das Powerset-Axiom , das faktisch für entscheidbare Teilmengen der Theorie übernommen wurde.

Die Charakterisierung der Klasse aller Teilmengen einer Menge beinhaltet eine unbegrenzte universelle Quantifizierung, nämlich . Hier wurde in Bezug auf das Mitgliedschaftsprädikat oben definiert. Die Aussage selbst ist . In einem mathematischen mengentheoretischen Rahmen wird die Potenzklasse also nicht in einer Bottom-up-Konstruktion aus ihren Bestandteilen (wie ein Algorithmus auf einer Liste, der zB mappt ) definiert, sondern über ein Verständnis über alle Mengen.

Der Reichtum der Potenzklasse in einer Theorie ohne ausgeschlossene Mitte lässt sich am besten verstehen, wenn man kleine klassisch endliche Mengen betrachtet. Für jede Formel ist die Klasse gleich 0, wenn sie abgelehnt werden kann und 1, wenn sie bewiesen werden kann, aber möglicherweise auch überhaupt nicht entscheidbar ist. In dieser Sicht wird die Potenzklasse des Singletons , dh die Klasse , oder andeutend " ", und normalerweise mit bezeichnet , als Wahrheitswertalgebra bezeichnet. Die -wertigen Funktionen einer Menge injizieren in ihre entscheidbaren Teilmengen und entsprechen somit ihren entscheidbaren Teilmengen.

Betrachten Sie als nächstes das Axiom .

Potenzierung

Die Formulierung hier verwendet die bequeme Notation für Funktionsräume. Andernfalls ist das Axiom länger und beinhaltet einen durch das Gesamtfunktionsprädikat begrenzten Quantor . In Worten, das Axiom besagt, dass bei zwei Mengen die Klasse aller Funktionen tatsächlich auch eine Menge ist. Dies ist sicherlich erforderlich, um zum Beispiel die Objektkarte eines internen Hom-Funktors wie zu formalisieren . Die Verwendung der Exponentiationsaxiome leitet sich aus der Tatsache ab, dass Funktionsräume, die Mengen sind, die Quantifizierung ihrer Funktionen ein beschränkter Begriff sind, der die Verwendung von Separation ermöglicht. Es hat bemerkenswerte Implikationen: Seine Übernahme bedeutet, dass die Quantifizierung über die Elemente bestimmter Funktionsklassen zu einem beschränkten Begriff wird, auch wenn die Funktionsräume sogar klassisch abzählbar sind . ZB ist die Sammlung aller Funktionen , dh die Menge der dem Cantor-Raum zugrunde liegenden Punkte , nach Cantors Diagonalargument abzählbar und kann bestenfalls als unterzählbar angesehen werden . (In diesem Abschnitt beginnen wir, das Symbol für den Halbring natürlicher Zahlen in Ausdrücken wie oder zu verwenden, nur um eine Verschmelzung von Kardinal- mit ordinaler Exponentiation zu vermeiden.)

Die Mengenlehre mit Exponentiation beweist nun auch die Existenz beliebiger primitiver rekursiver Funktionen auf den Naturals , als Mengenfunktionen in der Menge . Erhalten Sie in diesem Zusammenhang die ordinal- exponentielle Zahl , die als charakterisiert werden kann . Allgemeiner gesprochen beweist die Exponentiation, dass die Vereinigung aller endlichen Folgen über eine abzählbare Menge eine abzählbare Menge ist. Und tatsächlich sind Vereinigungen der Bereiche jeder abzählbaren Familie von Zählfunktionen abzählbar.

Soweit das Verständnis reicht, beweist die Theorie nun, dass die Sammlung aller abzählbaren Teilmengen einer beliebigen Menge (die Sammlung ist eine Unterklasse der Potenzklasse) eine Menge ist. Auch das Schubladenprinzip kann nachgewiesen werden.

Um auf die ursprüngliche Potenzklassenbetrachtung zurückzukommen: Unter der Annahme, dass alle Formeln entscheidbar sind, also unter der Annahme von , kann man nicht nur zeigen, dass eine Menge wird, sondern konkreter, dass es sich um diese Zwei-Elemente-Menge handelt. Angenommen für beschränkte Formeln, lässt sich mit Separation demonstrieren, dass jede Potenzklasse eine Menge ist. Alternativ ist die vollständige Powerset äquivalent zu der bloßen Annahme, dass die Klasse aller Teilmengen von eine Menge bildet. Vollständige Trennung entspricht der Annahme, dass jede einzelne Unterklasse von eine Menge ist.

Kategorie- und typtheoretische Begriffe

In diesem Zusammenhang sind also bei der Exponentiation Funktionsräume leichter zugänglich als Klassen von Teilmengen, wie dies bei exponentiellen Objekten bzw. Objekten der Fall ist . Teilobjekte der Kategorientheorie. In der Kategorie theoretische Begriffe, die Theorie entspricht im wesentlichen konstruktiv gut zackigen cartesianischen geschlossen Heyting vor toposes mit (wann immer Unendlichkeit angenommen wird) , um eine natürliche Zahlen Objekt . Die Existenz eines Powersets würde einen Heyting-Pretopos in einen elementaren Topos verwandeln . Jeder solche interpretierende Topos ist natürlich ein Modell dieser schwächeren Theorien, aber es wurden lokal kartesische geschlossene Prätoposen definiert, die zB Theorien mit Exponentiation interpretieren, aber volle Trennung und Potenzmenge ablehnen.

In der Typentheorie existiert der Ausdruck " " für sich allein und bezeichnet Funktionsräume , einen primitiven Begriff. Diese Typen (oder in der Mengenlehre Klassen oder Mengen) erscheinen natürlich zum Beispiel als der Typ der Currying- Bijektion zwischen und , einer Adjunktion . Eine typische Typentheorie mit allgemeinen Programmierfähigkeiten - und sicherlich diejenigen, die modellieren können , die als konstruktive Mengentheorie angesehen wird - haben einen Typ von ganzen Zahlen und Funktionsräumen, die darstellen und als solche auch Typen enthalten, die nicht zählbar sind. Dies impliziert und bedeutet nur, dass unter den Funktionstermen keiner die Eigenschaft hat, eine Bijektion zu sein.

Konstruktive Mengentheorien werden auch im Kontext applikativer Axiome untersucht .

Analyse

In diesem Abschnitt wird die Stärke von ausgearbeitet. Als Kontext werden mögliche weitere Prinzipien genannt, die nicht unbedingt klassisch sind und auch nicht allgemein als konstruktiv angesehen werden. Hier ist eine allgemeine Warnung angebracht: Beim Lesen von Aussagen zur Äquivalenz von Aussagen im berechenbaren Kontext sollte man sich immer bewusst sein, welche Wahl- , Induktions- und Verständnisprinzipien stillschweigend angenommen werden. Siehe auch die verwandte Konstruktive Analyse und Berechenbare Analyse .

Zu den Realen

Exponentiation impliziert Rekursionsprinzipien und so kann man in , über Folgen oder über schrumpfende Intervalle in nachdenken, und dies ermöglicht auch, von Cauchy-Folgen und ihrer Arithmetik zu sprechen . Jede reelle Zahl von Cauchy ist eine Sammlung von Folgen, dh eine Teilmenge einer Menge von Funktionen auf . Es sind mehr Axiome erforderlich, um immer die Vollständigkeit der Äquivalenzklassen solcher Folgen zu gewährleisten, und es müssen starke Prinzipien postuliert werden, die die Existenz eines Konvergenzmoduls für alle Cauchy-Folgen implizieren . Eine schwache abzählbare Wahl ist im Allgemeinen der Kontext für den Beweis der Eindeutigkeit der Cauchy-Reellen als vollständiger (pseudo-)geordneter Körper. "Pseudo-" unterstreicht hier, dass die Reihenfolge ohnehin konstruktiv nicht immer entscheidbar sein wird.

Wie in der klassischen Theorie werden Dedekind-Schnitte durch Teilmengen algebraischer Strukturen charakterisiert wie : Struktur. Ein Standardbeispiel für einen Schnitt, bei dem die erste Komponente tatsächlich diese Eigenschaften aufweist, ist die Darstellung von gegeben durch

(Je nach Konvention für Kürzungen darf einer der beiden Teile oder keiner, wie hier, das Zeichen verwenden .)

Die bisherige Theorie der Axiome bestätigt, dass ein pseudo- geordneter Körper , der auch archimedisch und dedekindisch vollständig ist , wenn er überhaupt existiert, auf diese Weise bis auf Isomorphie eindeutig charakterisiert ist. Die Existenz nur von Funktionsräumen wie z. B. bedeutet jedoch nicht, dass es sich um eine Menge handelt, und daher erfüllt auch die Klasse aller Teilmengen davon nicht die genannten Eigenschaften. Damit die Klasse der Dedekindschen Realen eine Menge ist, ist ein Axiom bezüglich der Existenz einer Menge von Teilmengen erforderlich.

In beiden Fällen sind im Vergleich zur klassischen Theorie weniger Aussagen über die Arithmetik der reellen Zahlen entscheidbar .

Konstruktive Schulen

Nicht-konstruktive Behauptungen, die für das Studium der konstruktiven Analyse wertvoll sind, werden im Allgemeinen so formuliert, dass sie alle binären Folgen, dh Funktionen, betreffen . Das sind Ansprüche, die durch quantifiziert werden .

Ein prominentestes Beispiel ist das begrenzte Prinzip der Allwissenheit , das eine disjunktive Eigenschaft postuliert, etwa auf der Ebene von -Sätzen oder Funktionen. ( Beispielfunktionen können in Rohform konstruiert werden, so dass, falls konsistent, die konkurrierenden Disjunkte -nicht beweisbar sind.) Das Prinzip ist unabhängig von zB unten eingeführtem. In dieser konstruktiven Mengenlehre impliziert ihre "geringere" Version, die als eingeschränkte Variante des De Morganschen Gesetzes bezeichnet wird . Es impliziert außerdem Markov-Prinzip , eine Form des Widerspruchsbeweis und die -Version des Lüftersatz . Die Erwähnung solcher Prinzipien, die für -Sätze gelten, deutet im Allgemeinen auf äquivalente Formulierungen in Bezug auf Sequenzen hin, die über die Trennung von Realen entscheiden. In einem konstruktiven Analysekontext mit abzählbarer Auswahl entspricht dies zB der Behauptung, dass jedes Reale entweder rational oder irrational ist - wiederum ohne die Notwendigkeit, eine der Disjunkten zu bezeugen.

Für einige Sätze, die in Theorien der konstruktiven Analyse verwendet werden und die nicht mit einfacher intuitionistischer Logik beweisbar sind, siehe oder sogar die These der nichtklassischen konstruktiven Kirche oder einige ihrer Konsequenzen auf der Seite der rekursiven Mathematik ( oder ), sowie Kripkes Schema (alle Unterklassen von abzählbar drehend ), Balkeninduktion , der entscheidbare Fächersatz oder sogar das nichtklassische Stetigkeitsprinzip, das Funktionen auf unendlichen Folgen durch endliche Anfangssegmente auf der Brouwerschen intuitionistischen Seite bestimmt ( ). Beide Schulen widersprechen , so dass die Entscheidung, solche Gesetze zu übernehmen, die Theorie inkonsistent mit den Theoremen der klassischen Analysis macht.

Unendliche Bäume

Durch den Zusammenhang zwischen Berechenbarkeit und arithmetischer Hierarchie sind die Erkenntnisse dieser klassischen Studie auch für konstruktive Überlegungen aufschlussreich. Eine grundlegende Erkenntnis der Umkehrmathematik betrifft berechenbare unendliche, endlich verzweigte Binärbäume. Ein solcher Baum kann zB als unendliche Menge endlicher Mengen kodiert werden

,

mit entscheidbarer Zugehörigkeit, und diese Bäume enthalten dann nachweislich Elemente beliebiger großer endlicher Größe. Das Lemma von Weak Königs besagt: Für solche gibt es immer einen unendlichen Pfad in , dh eine unendliche Folge, so dass alle ihre Anfangssegmente Teil des Baumes sind. In der umgekehrten Mathematik beweist die Arithmetik zweiter Ordnung nicht . Um dies zu verstehen, beachten Sie, dass es berechenbare Bäume gibt, für die kein berechenbarer solcher Pfad existiert. Um dies zu beweisen, zählt man die partiellen berechenbaren Folgen auf und diagonalisiert dann alle gesamten berechenbaren Folgen in einer partiellen berechenbaren Folgen . Man kann dann einen bestimmten Baum ausrollen , einen exakt kompatibel mit den noch möglichen Werten von überall, der konstruktionsbedingt mit keinem total berechenbaren Pfad kompatibel ist.

In impliziert das Prinzip das nicht-konstruktive, weniger begrenzte Prinzip der Allwissenheit . In einem konservativeren Kontext sind sie äquivalent unter der Annahme - (eine sehr schwache zählbare Wahl). Es ist auch äquivalent zum Brouwer Fixpunktsatz und anderen Sätzen über Werte stetiger Funktionen auf den reellen Zahlen. Der Fixpunktsatz wiederum impliziert den Zwischenwertsatz , aber seien Sie sich bewusst, dass die klassischen Sätze in einem konstruktiven Kontext in verschiedene Varianten übersetzt werden können.

Das betrifft unendliche Graphen und so gibt sein Kontrapositiv eine Bedingung für die Endlichkeit. Gegenüber der klassischen arithmetischen Theorie gibt dies der Borelschen Kompaktheit bezüglich endlicher Teilüberdeckungen des reellen Einheitsintervalls Äquivalenz . Eine eng verwandte Existenzbehauptung, die endliche Folgen in einem unendlichen Kontext einbezieht, ist der entscheidbare Fächersatz . Über die sind sie eigentlich gleichwertig. In sind diese unterschiedlich, aber wiederum eine Auswahl vorausgesetzt, impliziert .

Funktionsräume einschränken

In der folgenden Bemerkung ist wieder Funktion und darüber aufgestellte Behauptungen im Sinne der Berechenbarkeitstheorie gemeint. Der μ-Operator ermöglicht alle partiellen allgemeinen rekursiven Funktionen (oder Programme, in dem Sinne, dass sie Turing-berechenbar sind), einschließlich solcher, die nicht-primitiv, aber total sind, wie die Ackermann-Funktion . Die Definition des Operators beinhaltet Prädikate gegenüber den Natürlichen, und so hängt die theoretische Analyse von Funktionen und ihrer Gesamtheit vom vorliegenden formalen Rahmen ab. In jedem Fall befinden sich die natürlichen Zahlen, die in der Berechenbarkeitstheorie als Indizes für die berechenbaren Funktionen, die total sind, betrachtet werden , in der arithmetischen Hierarchie . Das heißt, es ist immer noch eine Unterklasse der Naturmenschen. Und dort ist die Totalität als Prädikat aller Programme bekanntlich berechenbar unentscheidbar .

Eine nichtklassisch- konstruktive Kirchenthese betrifft, wie in ihrer Vorannahme angenommen, die nachweislich totalen Prädikatendefinitionen (und damit hier Mengenfunktionen) und postuliert, dass sie berechenbaren Programmen entsprechen. Die Übernahme des Postulats macht aus der klassischen Mengenlehre eine "sparse" Menge. Siehe Unterzählbarkeit .

Das Postulat ist immer noch konsequente intuitionistische Arithmetik oder Wahl. Aber es widerspricht klassisch gültigen Prinzipien wie und , die zu den schwächsten oft diskutierten Prinzipien gehören.

Induktion

Mathematische Induktion

In den vorherigen Abschnitten hat die beschränkte Trennung bereits die Gültigkeit der Induktion für beschränkte Definitionen begründet. In der Satzsprache können Induktionsprinzipien mit dem weiter oben definierten Antezedens gelesen werden . Es ist aufschlussreich zu beobachten , dass ein Satz in der Konsequenz , wie hier in der Klassennotation ausgedrückt , der eine Unterklasse beinhaltet , die möglicherweise keine Menge bildet - was bedeutet, dass viele Axiome nicht gelten - und die Ebene nur zwei Möglichkeiten sind, dieselbe gewünschte Behauptung zu formulieren (an -indizierte Konjunktion von Behauptungen hier insbesondere.) So kann ein festgelegter theoretischer Rahmen mit gerade beschränkter Trennung durch arithmetische Induktionsschemata für unbeschränkte Prädikate gestärkt werden.

Das oben erwähnte Iterationsprinzip für Mengenfunktionen wird, alternativ zur Exponentiation, auch durch das vollständige Induktionsschema über die eigene Strukturmodellierung der Naturals (zB ) impliziert . Dies ist auch das arithmetische Prinzip erster Ordnung, um mehr Funktionen insgesamt zu beweisen, als dies tut. Es wird oft direkt in Form von Prädikaten wie folgt formuliert. Betrachten Sie das Schema - :

Axiom-Schema der vollständigen mathematischen Induktion : Für jedes Prädikat auf ,

Hier bezeichnet die 0 wie oben und die Menge bezeichnet die Nachfolgemenge von , mit . Nach dem obigen Axiom of Infinity ist es wieder Mitglied von .

Wie im Abschnitt über die Auswahl dargelegt, werden Induktionsprinzipien auch durch verschiedene Formen von Auswahlprinzipien impliziert. Das vollständige Induktionsschema wird durch das vollständige Trennungsschema impliziert.

Um die Existenz eines transitiven Abschlusses für jede Menge in Bezug auf zu beweisen , wird mindestens ein beschränktes Iterationsschema benötigt. Es ist erwähnenswert, dass im Programm der prädikativen Arithmetik das vollständige mathematische Induktionsschema als möglicherweise imprädikativ kritisiert wurde , wenn natürliche Zahlen als das Objekt definiert werden, das dieses Schema erfüllt.

Induktion einstellen

Full Set Induction in beweist die vollständige mathematische Induktion über die natürlichen Zahlen. Tatsächlich gibt es Induktion auf Ordinalzahlen und Ordinalarithmetik. Die Ersetzung ist nicht erforderlich, um die Induktion über die Menge der Natürlichen zu beweisen, aber sie wird für ihre Arithmetik innerhalb der Mengentheorie modelliert.

Das stärkere Axiom - lautet dann wie folgt:

Axiomschema der Mengeninduktion : Für jedes Prädikat gilt

Hier gilt trivial und entspricht dem "bottom case" im Standardframework. Die Variante des Axioms nur für beschränkte Formeln wird ebenfalls unabhängig studiert und kann von anderen Axiomen abgeleitet werden.

Das Axiom erlaubt Definitionen von Klassenfunktionen durch transfinite Rekursion . Das Studium der verschiedenen Prinzipien, die Mengendefinitionen durch Induktion gewähren, also induktive Definitionen, ist ein Hauptthema im Kontext der konstruktiven Mengenlehre und ihrer vergleichsweise schwachen Stärken . Dies gilt auch für ihre Pendants in der Typentheorie.

Das Axiom der Regularität zusammen mit der beschränkten /unbeschränkten Trennung impliziert Mengeninduktion, aber auch beschränkt/unbeschränkt , also ist Regularität nicht-konstruktiv. Umgekehrt impliziert die Mengeninduktion zusammen mit der Mengeninduktion Regularität.

Metalogik

Dies umfasst nun Varianten aller acht Zermelo-Fraenkel-Axiome . Extensionalität, Pairing, Union und Replacement sind tatsächlich identisch. Unendlich wird in einer starken Formulierung angegeben und impliziert wie im klassischen Fall Emty Set. Trennung, klassisch redundant angegeben, wird durch Ersetzung konstruktiv nicht impliziert. Ohne das Gesetz der ausgeschlossenen Mitte fehlt der Theorie hier in ihrer klassischen Form die vollständige Trennung, Potenzmenge sowie Regularität.

Die Theorie überschreitet nicht die Konsistenz Stärke Heyting Arithmetik aber das Hinzufügen in dieser Phase zu einer Theorie über die Kraft der typischen führen würde Art Theorie : Unter der Annahme , Trennung in unbeschränkter Form, dann Zugabe zu gibt eine Theorie beweist die gleichen Sätze wie minus Gleichmäßigkeits! Somit ergibt das Hinzufügen von Separation und Regularity zu diesem Framework vollständige und das Hinzufügen von Choice dazu .

Die zusätzliche beweistheoretische Stärke, die mit Induktion im konstruktiven Kontext erreicht wird, ist signifikant, auch wenn das Weglassen der Regularität im Kontext von die beweistheoretische Stärke nicht verringert. Aczel war auch einer der Hauptentwickler der nicht fundierten Mengenlehre , die dieses letzte Axiom ablehnt.

Starke Sammlung

Angesichts all der abgeschwächten Axiome dieser Axiome, die jetzt auch in Myhills typisiertem Ansatz zu sehen sind, und die jetzt darüber hinausgehen, betrachten wir die Theorie mit Exponentiation, die jetzt durch das Sammlungsschema verstärkt wird . Es handelt sich um eine Eigenschaft für Relationen, wodurch sich in seiner Formulierung erster Ordnung ein etwas repetitives Format ergibt.

Axiom-Schema von Strong Collection: Für jedes Prädikat ,

Es besagt, dass wenn eine Relation zwischen Mengen ist, die über eine bestimmte Domänenmenge total ist (dh sie hat mindestens einen Bildwert für jedes Element in der Domäne), dann gibt es eine Menge, die mindestens ein Bild unter jeder enthält Element der Domäne. Und diese Formulierung besagt dann außerdem, dass nur solche Bilder Elemente dieser Codomänenmenge sind. Der letzte Satz macht das Axiom - in diesem konstruktiven Kontext - stärker als die Standardformulierung von Collection. Es garantiert, dass die Kodomäne von nicht überschritten wird, und somit drückt das Axiom eine gewisse Kraft eines Trennverfahrens aus.

Das Axiom ist eine Alternative zum Ersatzschema und ersetzt es tatsächlich, da die binäre Relationsdefinition nicht funktional sein muss.

Fragen mittlerer Kardinalität sind in der Regel in einem konstruktiven Setting subtiler. Da die Arithmetik hier gut verfügbar ist, hat die Theorie abhängige Produkte, beweist, dass die Klasse aller Teilmengen natürlicher Zahlen nicht unterzählbar sein kann und beweist auch, dass abzählbare Vereinigungen von Funktionsräumen abzählbarer Mengen abzählbar bleiben.

Metalogik

Diese Theorie ohne , unbegrenzte Trennung und "naive" Machtmenge erfreut sich verschiedener netter Eigenschaften. Zum Beispiel hat sie die Existenzeigenschaft : Wenn die Theorie für eine beliebige Eigenschaft beweist, dass eine Menge mit dieser Eigenschaft existiert, dh wenn die Theorie die Aussage beweist , dann gibt es auch eine Eigenschaft , die eine solche Mengeninstanz eindeutig beschreibt. Dh die Theorie beweist dann auch . Dies kann mit der Heyting-Arithmetik verglichen werden, bei der Sätze durch konkrete natürliche Zahlen realisiert werden und diese Eigenschaften haben. In der Mengenlehre spielen definierte Mengen die Rolle. Für dagegen erinnert , dass in impliziert das Auswahlaxiom den Wohlordnungssatz , so dass insgesamt Ordnungen mit kleinstem Elemente für Teilmengen von Sets , wie an exist formal bewiesen, auch wenn nachweislich keine solche Anordnung beschrieben werden kann.

Konstruktives Zermelo–Fraenkel

Man kann sich Powerset weiter annähern, ohne eine typtheoretische Interpretation zu verlieren. Die bekannte Theorie sind die obigen Axiome plus eine stärkere Form der Exponentiation. Dies geschieht durch die Annahme der folgenden Alternative, die wiederum als konstruktive Version des Potenzmengen-Axioms angesehen werden kann :

Axiom-Schema der Teilmengensammlung: Für jedes Prädikat ,

Dieses Axiomschema der Teilmengensammlung entspricht einem einzelnen und etwas klareren alternativen Axiom der Fülle. Sei dazu die Klasse aller totalen Beziehungen zwischen a und b , diese Klasse ist gegeben als

Damit ist state eine Alternative zur Subset Collection. Es garantiert, dass es zumindest eine Menge gibt , die eine gute Menge der gewünschten Beziehungen enthält. Genauer gesagt gibt es zwischen zwei beliebigen Mengen und eine Menge, die eine Gesamtunterbeziehung für jede Gesamtbeziehung von bis enthält .

Axiom der Fülle:

Das Füllheitsaxiom wiederum wird durch das sogenannte Präsentationsaxiom über Abschnitte impliziert , das auch kategorietheoretisch formuliert werden kann .

Fülle impliziert die binäre Verfeinerungseigenschaft, die notwendig ist, um zu beweisen, dass die Klasse der Dedekind-Schnitte eine Menge ist. Dies erfordert keine Einführung oder Abholung.

Weder Linearität von Ordinalzahlen noch Existenz von Potenzmengen endlicher Mengen sind in dieser Theorie ableitbar. Angenommen, eine der beiden impliziert in diesem Zusammenhang eine Potenzmenge.

Metalogik

Dieser Theorie fehlt die Existenzeigenschaft aufgrund des Schemas, aber 1977 zeigte Aczel, dass die Typtheorie nach Martin-Löf immer noch interpretiert werden kann (unter Verwendung des Propositions-as-Types- Ansatzes), was heute als Standardmodell der In-Typentheorie gilt . Dies geschieht in Form von Bildern seiner Funktionen sowie einer ziemlich direkten konstruktiven und prädikativen Begründung unter Beibehaltung der Sprache der Mengenlehre. Dieses unterzählbare Modell validiert viele Auswahlprinzipien . Mit einem typtheoretischen Modell hat es eine bescheidene Beweiskraft, siehe : Bachmann-Howard-Ordinal .

Achtung: Brechen mit ZF

Man kann noch die nichtklassische Behauptung hinzufügen, dass alle Mengen als Axiom unterzählbar sind . Dann ist eine Menge (nach Unendlichkeit und Exponentiation), während die Klasse oder sogar nach Cantors diagonalem Argument nachweisbar keine Menge ist . Diese Theorie lehnt also Powerset und logisch ab .

1989 zeigte Ingrid Lindström, dass nicht begründete Mengen, die durch Ersetzen des Äquivalents des Stiftungsaxioms (Induktion) in durch Aczels Antifundamentaxiom ( ) erhalten wurden, auch in der Martin-Löf-Typentheorie interpretiert werden können.

Intuitionistisches Zermelo–Fraenkel

Die Theorie ist mit dem Standard Separation and Power Set .

Hier kann man anstelle des Axiom-Schemas der Ersetzung das

Axiom-Schema der Sammlung : Für jedes Prädikat ,

Während das Axiom des Ersatzes die Beziehung erfordert seine funktional über den Satz (wie in, für jeden in genau einer zugeordnet ist ), funktioniert das Axiom der Sammlung nicht. Es erfordert lediglich, dass mindestens eins assoziiert ist , und es behauptet die Existenz einer Menge, die mindestens ein solches für jedes solche sammelt . zusammen mit der Sammlung bedeutet Ersatz.

Als solche kann es als die geradlinigste Variante von ohne angesehen werden .

Die Theorie stimmt sowohl mit der Unterzählbarkeit als auch mit Churchs These für zahlentheoretische Funktionen überein . Aber wie oben angedeutet, kann die Unterzählbarkeitseigenschaft nicht für alle Mengen übernommen werden, da sich die Theorie als Menge erweist .

Metalogik

Wenn man das Axiom-Schema der Ersetzung in das Axiom-Schema der Sammlung ändert, hat die resultierende Theorie die Numerical-Existence-Eigenschaft .

Auch ohne ist die beweistheoretische Stärke von gleich der von .

Es basiert zwar eher auf intuitionistischer als auf klassischer Logik, gilt jedoch als imprädikativ . Es ermöglicht die Bildung von Mengen unter Verwendung des Trennungsaxioms mit jedem Satz, einschließlich solchen, die Quantoren enthalten, die nicht beschränkt sind. Somit können neue Mengen in Bezug auf das Universum aller Mengen gebildet werden. Außerdem impliziert das Potenzmengen-Axiom die Existenz einer Menge von Wahrheitswerten . Bei Vorhandensein einer ausgeschlossenen Mitte existiert diese Menge und hat zwei Elemente. Ist dies nicht der Fall, wird die Menge der Wahrheitswerte auch als imprädikativ angesehen.

Geschichte

1973 schlug John Myhill ein System der Mengenlehre vor, das auf intuitionistischer Logik basiert , die die gängigste Grundlage nimmt und das Auswahlaxiom und das Gesetz der ausgeschlossenen Mitte wegwirft und alles andere so lässt, wie es ist. Jedoch sind verschiedene Formen einiger der Axiome, die im klassischen Rahmen äquivalent sind, im konstruktiven Rahmen unäquivalent, und einige Formen implizieren . In diesen Fällen wurden dann die intuitiv schwächeren Formulierungen für die konstruktive Mengenlehre übernommen.

Intuitionistisches Z

Wiederum am schwächeren Ende, wie bei ihrem historischen Gegenstück Zermelo Mengenlehre , kann man durch die intuitionistische Theorie aufgestellt wie, aber ohne Ersatz, Sammlung oder Induktion, bezeichnen.

Intuitionistische KP

Lassen Sie uns eine andere sehr schwache Theorie erwähnen, die untersucht wurde, nämlich die Intuitionistische (oder konstruktive) Kripke-Platek-Mengentheorie . Die Theorie hat nicht nur die Trennung, sondern auch die Sammlung beschränkt, dh sie ist ähnlich, aber mit Induktion statt vollständiger Ersetzung. Es ist besonders schwach, wenn es ohne Infinity studiert wird. Die Theorie passt nicht in die oben dargestellte Hierarchie, einfach weil sie von Anfang an das Axiom-Schema der Mengeninduktion hat . Dies ermöglicht Theoreme, die die Klasse der Ordinalzahlen beinhalten.

Sortierte Theorien

Konstruktive Mengenlehre

Wie er es präsentierte, ist Myhills System eine Theorie, die eine konstruktive Logik erster Ordnung mit Identität und drei Arten verwendet , nämlich Mengen, natürliche Zahlen , Funktionen . Seine Axiome sind:

  • Das übliche Extensionalitätsaxiom für Mengen sowie eines für Funktionen und das übliche Vereinigungsaxiom .
  • Das Axiom der eingeschränkten oder prädikativen Trennung , das eine abgeschwächte Form des Trennungsaxioms aus der klassischen Mengenlehre ist und erfordert, dass alle Quantifizierungen , wie diskutiert, auf eine andere Menge beschränkt sind.
  • Eine Form des Axioms der Unendlichkeit, die behauptet, dass die Sammlung natürlicher Zahlen (für die er eine Konstante einführt ) tatsächlich eine Menge ist.
  • Das Axiom der Exponentiation, das behauptet, dass es für zwei beliebige Mengen eine dritte Menge gibt, die alle (und nur) die Funktionen enthält, deren Bereich die erste Menge und deren Bereich die zweite Menge ist. Dies ist eine stark abgeschwächte Form des Axioms der Potenzmenge in der klassischen Mengenlehre, dem unter anderem Myhill wegen seiner Unvorhersehbarkeit widersprach .

Und außerdem:

  • Die üblichen Peano-Axiome für natürliche Zahlen.
  • Axiome, die behaupten, dass sowohl der Bereich als auch der Bereich einer Funktion Mengen sind. Darüber hinaus behauptet ein Axiom der Nicht-Wahl die Existenz einer Wahlfunktion in Fällen, in denen die Wahl bereits getroffen wurde. Zusammen wirken diese wie das übliche Ersetzungsaxiom in der klassischen Mengenlehre.

Man kann die Stärke dieser Theorie grob mit einer konstruktiven Teiltheorie identifizieren, wenn man sie mit den vorherigen Abschnitten vergleicht.

Und schließlich nimmt die Theorie an

Mengenlehre im Bishop-Stil

Die Mengenlehre im Stil der konstruktivistischen Schule von Errett Bishop spiegelt die von Myhill wider, ist jedoch so aufgebaut, dass Mengen mit Beziehungen ausgestattet sind, die ihre Diskretion bestimmen. Üblicherweise wird Dependent Choice angenommen.

In diesem Zusammenhang wurde viel Analyse- und Modultheorie entwickelt.

Kategorietheorien

Nicht alle formalen logischen Theorien von Mengen müssen das binäre Zugehörigkeitsprädikat " " direkt axiomisieren . Und eine elementare Theorie der Kategorien der Menge ( ), zB das Erfassen von Paaren von zusammensetzbaren Abbildungen zwischen Objekten, kann auch mit einer konstruktiven Hintergrundlogik ( ) ausgedrückt werden . Die Kategorientheorie kann als Theorie von Pfeilen und Objekten aufgestellt werden, obwohl Axiomatisierungen erster Ordnung nur in Bezug auf Pfeile möglich sind.

Gute Modelle konstruktiver Mengentheorien in der Kategorientheorie sind die im Abschnitt Exponentiation erwähnten Prätoposen – möglicherweise erfordern sie auch genügend Projektive , ein Axiom über surjektive "Darstellungen" von Mengen, das Countable Dependent Choice impliziert.

Darüber hinaus haben Topoi auch interne Sprachen , die selbst intuitiv sein können und eine Vorstellung von Mengen erfassen .

Siehe auch

Verweise

Weiterlesen

Externe Links