1 + 1 = 2

08.09.2023, 08:11	Finn_	Auf diesen Beitrag antworten »
1 + 1 = 2 In der letzten Woche habe ich versucht, mehr Klarheit darüber zu gewinnen, wie die gemeinhin als gültig angenommene Gleichheit 1 + 1 = 2 zu verstehen wäre. Den vorläufigen Abschluss meines Gedankengangs stellt die folgende formale Abfassung klassischer Erwägungen dar, die schlussendlich zum Beweis der Aussage führen; zur Abwechslung mal nicht in ZFC, sondern in der Morse-Kelley-Mengenlehre. Aufgeführt werden neben dem Beweis nur transitive Abhängigkeiten; insgesamt sind es 8 Axiome, 30 Definitionen und 95 Theoreme. Coq-Quelltext, am besten mit CoqIDE durchschreiten: [attach]57267[/attach]
09.09.2023, 12:52	Elvis	Auf diesen Beitrag antworten »
Wenn ich Dedekind lese, glaube ich, dass ich die natürlichen Zahlen soweit verstanden habe, dass an der Formel 1+1=2 kein Zweifel besteht. Könntest du das Problem, die klassischen Erwägungen und deine Lösung im Klartext darstellen ? Darf ruhig etwas länger sein, aber von Coq-Quelltext und CoqIDE habe ich keine Ahnung. Wenn Klartext nicht möglich oder zu aufwendig ist, dann bitte ich um Aufklärung über CoQ.
09.09.2023, 20:40	Guppi12	Auf diesen Beitrag antworten »
Ich hab irgendwie nie verstanden, warum 1+1 = 2 so schwierig zu beweisen sein soll. Folgt das nicht in ein paar Zeilen aus den Peano Axiomen? Die 300-Seiten-Schrift, die es dazu wohl geben soll, wollte ich mir ehrlich gesagt nie durchlesen wollen.
09.09.2023, 22:43	Elvis	Auf diesen Beitrag antworten »
$\begin{eqnarray} n+1:=S(n)\wedge S(1)=:2\Rightarrow 1+1=2 \end{eqnarray}$ Ich weiß, dass Frege das nicht gefallen hätte, aber Dedekind kam damit klar.
10.09.2023, 11:39	Finn_	Auf diesen Beitrag antworten »
Zum mathematischen Inhalt. Um die Gleichheit als Aussage formulieren zu können, müssen die natürlichen Zahlen und ihre Addition zunächst einmal erklärt sein. Es wäre machbar, die Theorie auf das für die Aussage Nötige zu beschränken, aber wir wollen nicht mogeln, sondern die Zahlen und ihre Addition in allgemeiner Weise erklärt wissen. Gleichermaßen stehe als formales System nur die allgemeine Mengenlehre zur Verfügung. Man muss die natürlichen Zahlen daraufhin zwangsläufig irgendwie modellieren, was ich im üblichen Sinn gemacht habe, also als die endlichen Ordinalzahlen mit $\begin{eqnarray} \emptyset \end{eqnarray}$ als null und $\begin{eqnarray} \mathrm{succ}(n):=n\cup\{n\} \end{eqnarray}$ als Nachfolgerabbildung. Die natürlichen Zahlen werden als kleinste induktive Menge festgelegt, also als Schnittmenge aller induktiven Mengen. Mit dem Axiom des Unendlichen, das besagt, dass mindestens eine induktive Menge existiert, wird später gezeigt, dass die leere Klasse und die Klasse der natürlichen Zahlen Mengen sind. Daraufhin wird das Prinzip der Induktion bewiesen. Im Fortgang wird die Addition rekursiv definiert, also vermittels einer Rekursionsgleichung zuzüglich Anfangsbedingung. Es handelt sich hierbei allerdings um eine Funktionalgleichung, deren Lösung vermittels iota, des Operators der definiten Kennzeichnung, extrahiert wird. Es ist iota zu einer Aussageform schlicht als Bildung des Schnittes all der Mengen definiert, die die Aussageform erfüllen. Beschreibt bzw. kennzeichnet die Aussageform ein eindeutiges Objekt, so ist die Menge der Objekte, die die Aussageform erfüllen, eine Einermenge. Die Bildung der Schnittmenge extrahiert dieses Objekt aus der Einermenge. Insofern müssen wir aber wissen, dass die Rekursionsgleichung zuzüglich Anfangsbedingung eine eindeutige Lösung besitzt, das heißt, der dedekindsche Rekursionssatz muss bewiesen werden. Sonst könnten wir nicht ableiten, dass das Resultat von iota die Anfangsbedingung und die Rekursionsgleichung erfüllt. Im Rekursionssatz und dessen Beweis kommt nun außerdem der Begriff der Abbildung vor. Dementsprechend müssen erst einmal Abbildungen definiert und einige Aussagen über sie bewiesen werden. Damit einhergehend müssen auch geordnete Paare beschrieben werden, was ich im üblichen Sinne nach Kuratowski gemacht habe. Die Applikation oder Auswertung, die einer Abbildung $\begin{eqnarray} f\colon X\to Y \end{eqnarray}$ bzw. $\begin{eqnarray} \mathrm{mapping}\;f\;X\;Y \end{eqnarray}$ und einem Argument $\begin{eqnarray} x\in X \end{eqnarray}$ das eindeutig bestimmte Bild $\begin{eqnarray} f(x) \end{eqnarray}$ bzw. $\begin{eqnarray} \mathrm{app}\;f\;x \end{eqnarray}$ zuordnet, wird ebenfalls vermittels iota definiert, wobei iota an der Stelle ausgeschrieben steht, weil ich die später auftretende Definition von iota nicht aus dem zugehörigen Abschnitt zerren wollte. Zur Umsetzung. Die Überlegung wäre prinzipiell in unterschiedlichen Beweisassistenten umsetzbar. Coq bietet allerdings ein recht reichhaltiges System. Der zugrunde liegende Kalkül induktiver Konstruktionen ist ein Lambda-Kalkül mit Typsystem, der als abhängige Typentheorie eine Logik höherer Stufe kodiert, so dass wir auch Schemata als gewöhnliche Aussagen formulieren können. Will man sich faktisch auf Logik erster Stufe beschränken, muss man wohl ein wenig aufpassen. Weiterhin ist, wie der Name anmuten lässt, die Konstruktion neuer Strukturen einschließlich rekursiver Strukturen und struktureller Induktion im System enthalten. Mithin wird Gleichheit definierbar. Es wäre machbar, wenn auch umständlich, dieses System als Metalogik zu nutzen, um das gesamte formale System der Mengenlehre einschließlich der Formeln, Sequenzen und der logischen Schlussregeln zu definieren. Stattdessen wird die Mengenlehre in die Typentheorie eingebettet. Dazu führt man als neuen Typ lediglich $\begin{eqnarray} \mathrm{Class}, \end{eqnarray}$ den Typ aller Klassen, ein. Eine Aussage ist vom Typ $\begin{eqnarray} \mathrm{Prop} \end{eqnarray}$ für Proposition, eine Aussageform vom Typ $\begin{eqnarray} \mathrm{Class}\to\mathrm{Prop}. \end{eqnarray}$ Implikationen mit mehreren Prämissen oder allgemein Funktionen von mehreren Argumenten stehen in der Regel in geschönfinkelter Form. Das heißt, man formuliert $\begin{eqnarray} A\to(B\to C) \end{eqnarray}$ statt $\begin{eqnarray} A\land B\to C \end{eqnarray}$ und $\begin{eqnarray} \mathrm{Class}\to (\mathrm{Class}\to\mathrm{Prop}) \end{eqnarray}$ statt $\begin{eqnarray} \mathrm{Class}\times\mathrm{Class}\to\mathrm{Prop} \end{eqnarray}$ usw. Das Prädikat "ist Element von" hat diese Signatur. Man darf somit im Gegensatz zu einem System, wo Menge und Klasse unterschiedliche Sorten sind, über die Aussage sprechen, ob eine echte Klasse ein Element einer Klasse ist. Dass dies nicht möglich ist, liegt stattdessen in der Form des Komprehensionsaxioms begründet. Die Anwendung von Schlussregeln wird durch sogenannte Taktiken kodiert. Jede Taktik steht im Wesentlichen für eine bestimmte Schlussregel, eine Übersicht findet sich in [1]. In der Regel (nettes Wortspiel) verläuft der Beweis hierbei rückwärts, man sagt, die Regel führt ein Ziel auf ein oder mehrere Unterziele zurück. Bei einigen Taktiken verläuft das Schließen jedoch auch vorwärts, das sind assert und Taktiken mit "in" wie "apply h1 in h2" und "rewrite h1 in h2". Das h steht immer für Hypothese, und ih steht für Induktionshypothese, also die Induktionsvoraussetzung. Es ist auch üblich, das h als Großbuchstabe zu schreiben, was ich aber umständlich finde. Das gegenwärtige Ziel und die dabei zur Verfügung stehenden Hypothesen werden in CoqIDE im rechten Fenster aufgeführt. Ein kurzes Beispiel. Wir wollen $\begin{eqnarray} A\cap B \subseteq B\cap A \end{eqnarray}$ beweisen. Mit unfold subclass. entfaltet sich das Ziel zu $\begin{eqnarray} \forall x,\;x \in A\cap B \to x\in B\cap A. \end{eqnarray}$ Mit intro x. intro hx. werden die Variable $\begin{eqnarray} x \end{eqnarray}$ und die Hypothese hx: $\begin{eqnarray} x\in A\cap B \end{eqnarray}$ eingeführt, was man auch kurz intros x hx. schreiben kann. Das verbleibende Ziel ist $\begin{eqnarray} x\in B\cap A. \end{eqnarray}$ Man wendet mit apply comp. das Komprehensionsaxiom an, womit das Ziel in $\begin{eqnarray} \mathrm{set}\,x\land (x\in B\land x\in A) \end{eqnarray}$ aufgelöst wird, worin $\begin{eqnarray} \mathrm{set}\,x \end{eqnarray}$ für "x ist eine Menge" steht. Nun wird die Hypothese hx mit apply comp in hx. in die Form $\begin{eqnarray} \mathrm{set}\,x\land (x\in A\land x\in B) \end{eqnarray}$ gebracht. Es wird hx daraufhin mit destruct hx as (hsx, (hA, hB)). in die drei Hypothesen hsx: $\begin{eqnarray} \mathrm{set}\,x \end{eqnarray}$ und hA: $\begin{eqnarray} x\in A \end{eqnarray}$ und hB: $\begin{eqnarray} x\in B \end{eqnarray}$ zerlegt. Man kann das mit apply comp in hx as (hsx, (hA, hB)). auch in einem Rutsch bewerkstelligen. Weiterhin wird das Ziel mit split; [\| split]. auf dessen drei Unterziele zurückgeführt, was für soviel steht wie "teile die Konjunktion in Unterziele; tue daraufhin jeweils: links nichts \| rechts ist die Formel eine Konjunktion, trenne sie ebenfalls in Unterziele auf". Schließlich werden die drei Unterziele, deren Teilbeweisen man zur Übersicht jeweils ein Bullet voranstellt, jeweils bewiesen mit exact hsx. und exact hA. und exact hB. Statt mit exact darf man auch assumption. schreiben, das sucht sich die passende Hypothese automatisch. Man könnte die letzten Schritte darüber hinaus auch mit split; [\| split]; assumption. oder repeat split; assumption. oder kurzum auto. abklabüstern lassen. [1] Christine Paulin-Mohring: Introduction to the Coq proof-assistant for practical software verification. https://www.lri.fr/~paulin/LASER/course-notes.pdf
10.09.2023, 11:53	Elvis	Auf diesen Beitrag antworten »
Danke für die Erläuterungen. Eine kleine Einführung in CoqIDE habe ich mir heute morgen schon angesehen und werde das System gleich nach dem Mittagessen installieren. Ich kann allerdings nicht versprechen, dass meine Geduld ausreicht, um deinen Beweis durchzuarbeiten - es gibt zu viel zu tun, und meine Zeit wird knapp.
Anzeige

10.09.2023, 13:24	Elvis	Auf diesen Beitrag antworten »
CoqIDE installiert von https://coq.inria.fr/download. Avast Security hat einen Teil in Quarantäne verschoben, weil ein Trojaner erkannt wurde (siehe Anhang), CoqIDE läuft trotzdem problemlos. Dein Beweis ist hübsch übersichtlich dokumentiert, da lohnt sich die Arbeit einerseits, weil sich sicher etwas daraus lernen lässt und andererseits, weil man damit etwas über Coq lernen kann. Danke. Dein (* Beweis der Gleichheit 1 + 1 = 2 *) am Ende sieht meinem Beweis von gestern sehr ähnlich. (Du hast natürlich völlig recht, erst wenn man genau weiß, worüber man redet, kann man einen Beweis führen.) Nachtrag: Gibt es Möglichkeiten, den Beweis zu reduzieren ? Ist ein spezielles System der natürlichen Zahlen notwendig ? Funktioniert auch ein Beweis mit einem endlichen Abschnitt der natürlichen Zahlen ? Könnte man dann auf vollständige Induktion und den Rekursionssatz verzichten ?

1

Verwandte Themen