Wie wurden formale Systeme und der Begriff syntaktische Konsequenz (Beweis) entwickelt?

Sie schrieben...

Aber wie haben Menschen formale Systeme und den Begriff der syntaktischen Konsequenz überhaupt entwickelt? Hätten sie solche Systeme nicht entwickeln müssen, basierend auf den semantischen Konsequenzen, denen sie zugestimmt haben?

... und Sie haben vollkommen Recht: Wie in den Kommentaren ausgeführt wurde, führte das Studium der semantischen Konsequenz zum Begriff der syntaktischen Konsequenz. Die Anfangszeilen von George Booles The Laws of Thought (der Titel ist selbst suggestiv) sagen:

1. Das Design der folgenden Abhandlung besteht darin, die Grundgesetze jener Operationen des Geistes zu untersuchen, durch die logisches Denken durchgeführt wird; ihnen in der symbolischen Sprache eines Kalküls Ausdruck zu verleihen und auf dieser Grundlage die Wissenschaft der Logik zu begründen und ihre Methode zu konstruieren; diese Methode selbst zur Grundlage einer allgemeinen Methode zur Anwendung der mathematischen Wahrscheinlichkeitslehre zu machen; und schließlich, um aus den verschiedenen Wahrheitselementen, die im Laufe dieser Untersuchungen ans Licht kamen, einige wahrscheinliche Andeutungen über die Natur und Beschaffenheit des menschlichen Geistes zu sammeln.

In der Einleitung wird dann ausgehend von Aristoteles kurz auf die historische Entwicklung einer solchen Untersuchung eingegangen.

Sobald ein System der symbolischen Logik entwickelt wurde, das auf semantischer Argumentation, dh wahrheitsbewahrender Argumentation, basiert, kann dieses System isoliert untersucht werden, wodurch das Studium der syntaktischen Konsequenz beginnt, wo die Regeln des logischen Schlusses rein mechanisch werden. Vereinfacht gesagt – Leibniz, Babbage und Lovelace waren beispielsweise ihrer Zeit voraus – waren die Fortschritte wie folgt:

1. Menschen argumentieren natürlich miteinander.
2. Es wird bemerkt, dass einige Argumente gültig sind, während andere es nicht sind.
3. Es werden verschiedene Versuche unternommen, Punkt 2 zu analysieren.
4. Symbolische Logik basierend auf semantischem Denken wird entwickelt.
5. Die Leute entdecken, dass symbolische Logik, auch bekannt als syntaktisches Denken, an sich schon interessant ist. Diese Phase hat viel zu bieten, aber ein wichtiger Schritt auf dem Weg dorthin war die Entdeckung nicht-euklidischer Geometrien . Peano und Pieri waren wichtige Persönlichkeiten in der frühen Untersuchung des syntaktischen Denkens um seiner selbst willen.
6. Das Studium des symbolischen Denkens führt zur modernen mathematischen Logik und auch zur Berechenbarkeitstheorie (Turing-Maschinen und all das).

Symbolische Logik ist natürlich entscheidend für die moderne Logik und Mengenlehre, aber es ist interessant festzustellen, dass Zermelo seine gleichnamigen Axiome 1908 entwickelte , ein Jahrzehnt bevor die Logik erster Ordnung 1917 von Hilbert und Bernays in ihre heutige Form gebracht wurde – 1918 .

Eine letzte Anmerkung: Die Entwicklung des Studiums der Logik und des logischen Denkens ist derjenigen der Grammatik ziemlich ähnlich, was angesichts der Verbindungen zwischen beiden nicht so überraschend ist. Eine stark vereinfachte Rechnung:

1. Menschen folgen von Natur aus ungeschriebenen grammatikalischen Regeln.*
2. Die Leute beginnen, diese Regeln zu analysieren , was zu Grammatik als Studienfach führt.**
3. Die Leute entdecken, dass Grammatik im Abstrakten interessant ist, was schließlich zu formalen Grammatiken führt .***
4. Die Leute erkennen, dass formale Grammatiken beim praktischen Rechnen ziemlich nützlich sind .

*Muttersprachler sprechen grammatikalisch, ohne Grammatik lernen zu müssen.

**Es scheint uns jetzt so offensichtlich, aber grammatikalische Kategorien (Substantive, Verben, Präpositionen usw.) zu entwickeln, war ein enormer Durchbruch.

***Damit wird viel von der eigentlichen historischen Motivation, zB der Idee einer universellen Grammatik , übersehen .

Nicht wirklich eine Antwort, aber ein Versuch, eine Vorstellung von einem syntaktischen Ansatz zu geben.

• Angenommen, Sie wollen beweisen, dass n = a+a logischerweise n = 2a ist.

• Wenn Sie beweisen möchten, dass die Aussage für einen kleinen Bereich gilt, sagen wir für 0, 1, 2...... 9 , können Sie eine semantische Methode verwenden. Das heißt, Sie werden alle möglichen Interpretationen des Satzes berücksichtigen:

0+0 = 2,0

1+1 = 2,1

2+2 = 2,2

usw.

und sobald Sie verifiziert haben, dass der Satz für alle möglichen Interpretationen wahr ist, können Sie sagen, dass der Satz gültig ist, was bedeutet, dass man aus " n = a + a" schließen kann, dass n = 2.a " gültig ist .

• Wenn Sie jedoch mit einem unendlichen Zahlenbereich arbeiten, steht die semantische Methode nicht mehr zur Verfügung, Sie können nicht unendlich viele Interpretationen überprüfen.

Sie werden also auf eine syntaktische Methode zurückgreifen. Das heißt, Sie werden versuchen, die Konsequenz aus dem Vordersatz der Bedingung abzuleiten, indem Sie nur Symbole gemäß den syntaktischen Regeln manipulieren.

wenn n = a+a

dann n = 1.a + 1.a = a . ( 1+1) = a.2 = 2.a.

(unter Verwendung von: „1 ist das Identitätselement für die Multiplikation“, „Distributivitätsgesetz“ und „Kommutativgesetz für die Addition“).

• Dies zeigt, wie nützlich der syntaktische Ansatz (mechanische Manipulation von Symbolen) ist. Aber es stellt sich die Frage: Ist diese syntaktische Methode vernünftig? Was beweist, dass tatsächlich in allen möglichen Interpretationen (und es gibt unendlich viele Interpretationen) „a+a = 2.a“ wahr ist? Gibt es auch Formeln, die in allen Interpretationen wahr sind, obwohl wir sie nicht mit syntaktischen Methoden beweisen können?

• In der Aussagenlogik können Sie die Gültigkeit einer Argumentation mit einer semantischen Methode (nämlich Wahrheitstabellen) überprüfen, aber wenn die Anzahl der atomaren Sätze höher als 3 ist, verwenden Sie gerne eine synkatische Methode (z. B. natürliche Deduktion).

• Wir brauchen also formale Systeme (aber wir brauchen auch Beweise dafür, dass sie solide und hoffentlich vollständig sind).