Warum brauchen wir formale Semantik für Prädikatenlogik?

Betrachten Sie diese Frage als gelöst. Ich werde nicht die beste Antwort auswählen, da sie alle zu meinem Verständnis des Themas beigetragen haben.

Ich bin mir nicht sicher, welchen Nutzen es hat, die Semantik der Prädikatenlogik formal zu definieren. Aber ich sehe Wert darin, eine formale Beweisrechnung zu haben. Mein Punkt ist, dass wir keine formale Semantik benötigen würden, um die Inferenzregeln von Beweiskalkülen zu rechtfertigen.

Wir könnten einen Kalkül definieren, der die "Gesetze des Denkens" nachahmt, dh die Schlußregeln, die seit Hunderten von Jahren von Mathematikern verwendet werden, um ihre Theoreme zu beweisen. Ein solcher Kalkül existiert bereits: natürlicher Abzug. Dann würden wir diesen Kalkül als solide und vollständig definieren.

Dies kann durch die Erkenntnis gerechtfertigt werden, dass die formale Semantik der Prädikatenlogik nur ein Modell ist. Die Angemessenheit des Modells kann nur intuitiv begründet werden. Indem gezeigt wird, dass natürliche Deduktion unter Bezugnahme auf die formale Semantik fundiert und vollständig ist, wird natürliche Deduktion nicht "wahrer". Genauso gut wäre es, wenn wir die Regeln der natürlichen Folgerung intuitiv direkt begründen würden. Der Umweg mit formaler Semantik bringt uns nichts.

Wenn wir dann die natürliche Folgerung als gesund und vollständig definieren, können wir die Solidität und Vollständigkeit anderer Kalküle zeigen, indem wir zeigen, dass die Beweise, die sie produzieren, in natürliche Folgerung übersetzt werden können und umgekehrt.

Sind meine obigen Überlegungen korrekt? Warum ist es wichtig, die Richtigkeit und Vollständigkeit von Beweiskalkülen anhand der formalen Semantik zu beweisen?

Ein kleiner Kommentar und eine ernstere Antwort.

Erstens ist es nicht sinnvoll, ein natürliches Abzugssystem zu deklarieren, das von fiat vervollständigt wird. Natürlicher Abzug ist gerade deshalb interessant, weil er einen natürlichen inneren Begriff von Konsistenz und / oder Vollständigkeit hat - nämlich die Beseitigung von Schnitten. Dies ist ein fantastischer Satz, und IMO rechtfertigt Versuche, eine rein beweistheoretische Semantik zu liefern (und durch die CH-Entsprechung auch die Verwendung von Operationsmethoden in der Programmiersprachensemantik). Dies ist jedoch gerade deshalb interessant, weil es eine verfeinerte Vorstellung davon bietet, wie die Logik richtig ist, als dass es um Konsistenz geht. Wenn Sie sich für die Beweistheorie entscheiden, bedeutet dies, dass Sie mehr arbeiten müssen, aber im Gegenzug bessere Ergebnisse erzielen.

Es kommt jedoch manchmal vor, dass die Logik an sichspielt eine untergeordnete Rolle. Wir können mit einer (Familie von) Modellen beginnen und dann anhand einer Logik nach Wegen suchen, wie wir syntaktisch über sie sprechen können. Die Richtigkeit und Vollständigkeit einer Logik in Bezug auf eine Modellfamilie zeigt, dass die Logik wirklich alles erfasst, was über die Modellklasse interessant und wahr ist. Ein konkretes Beispiel dafür, wann Modelle interessanter sind als die logischen Theorien, ist die Programmanalyse und Modellprüfung. Dort ist es üblich, Ihr Modell als Ausführung eines Programms und die Logik als Fragment einer zeitlichen Logik zu betrachten. Die Aussagen, die Sie in diesen Sprachen machen können, sind (absichtlich) nicht besonders aufregend - z. B. treten keine Nullzeiger-Dereferenzen auf - aber es ist die Tatsache, dass sie für tatsächliche Programmläufe gelten, die das Interesse wecken.

Ich füge nur eine andere Perspektive hinzu, um die obigen Antworten zu ergänzen. Erstens lohnen sich diese Überlegungen, und viele Menschen hatten ähnliche Vorstellungen. In der Philosophie wird dies manchmal als "beweistheoretische Semantik" bezeichnet, was sich auf Arbeiten von Nuel Belnap, Dag Prawitz, Michael Dummett und anderen in den 60er und 70er Jahren bezieht, die sich selbst auf Gentzens Arbeiten zur natürlichen Deduktion berufen. Per Martin-Löf und Jean-Yves Girard scheinen in ihren Schriften ebenfalls Varianten dieser Position vorzuschlagen. In Programmiersprachen ist dies der "syntaktische Ansatz zur Typisierung".

Die Sache ist, dass, selbst wenn Sie akzeptieren, dass die Regeln der Logik keine separate semantische Interpretation benötigen, es nicht sehr interessant / nützlich ist zu sagen, dass sie selbst gerechtfertigt sind und es dabei belassen. Die Frage ist, was eine formale Semantik leistet und ob es möglich ist, dasselbe mit weniger Umwegen zu erreichen. Das Projekt, die Modelltheorie mit der analytischen Beweistheorie zu vereinen, ist wichtig, aber immer noch ungelöst und wird an vielen verschiedenen Fronten aktiv verfolgt, einschließlich kategorialer Logik, Spielesemantik und Girards "Ludics". Zusätzlich zu dem, was Charles erwähnte, besteht ein weiterer qualitativer Vorteil von Modellen in der Fähigkeit , Nicht- Anwendern konkrete Gegenbeispiele zu liefern-theorems, und die Frage ist, wie dies in einem "direkten" Ansatz sinnvoll ist. Eine ludics-inspirierte Antwort finden Sie unter "Über die Bedeutung der logischen Vollständigkeit" von Michele Basaldella und Kazushige Terui.

Eine formale Semantik liefert eine direkte Bedeutung der Ausdrücke im Kalkül, unabhängig von den syntaktischen Beweisregeln für deren Manipulation. Wie können Sie ohne formale Semantik feststellen, ob die Abzugsregeln korrekt sind (Richtigkeit) oder ob Sie genug davon haben (Vollständigkeit)?

Es wurden "Denkgesetze" vorgeschlagen, bevor es zu einem natürlichen Abzug kam. Aristoteles 'Syllogismen waren eine solche Sammlung. Wenn wir sie als solide und vollständig definieren würden, würden wir sie vielleicht noch heute verwenden, anstatt fortschrittlichere logische Techniken zu entwickeln. Der Punkt ist, wenn die Syllogismen die Denkgesetze vollständig erfassen, warum sollten wir dann weitere Logiken entwickeln müssen. Was wäre, wenn sie tatsächlich inkonsistent wären? Eine Semantik zusammen mit dem formalen Beweiskalkül und den damit verbundenen Korrektheits- und Vollständigkeitsnachweisen liefert einen Maßstab für die Beurteilung des Werts eines solchen Argumentationssystems. Es würde nicht länger isoliert stehen.

$X\lor \neg X$Gehen Sie sogar so weit zu argumentieren, dass wir akzeptieren sollten, dass es keine wahre Logik gibt, und nehmen Sie eine pluralistische Haltung ein, wobei Sie die für den Anlass am besten geeignete Logik verwenden. Angesichts der Fülle an Logik, die Informatikern zur Verfügung steht (lineare Logik, Trennungslogik, konstruktive Logik höherer Ordnung, viele modale Logiken, alle in klassischen und intuitionistischen Varianten), haben die meisten von uns wahrscheinlich keine Sekunde gegeben, um eine pluralistische Haltung einzunehmen dachte, weil Logik ein Werkzeug ist, um ein bestimmtes Problem zu lösen, und wir versuchen, das am besten geeignete auszuwählen. Eine formale Semantik ist eine Möglichkeit, die Angemessenheit der Logik zu beurteilen.

Ein weiterer Grund für eine formale Semantik ist, dass es mehr Logik als Prädikatenkalkül gibt. Viele dieser Logiken sind so konzipiert, dass sie sich auf eine bestimmte Art von System beziehen. (Ich denke über Modallogik nach). Hier ist die Klasse der Systeme bekannt und die Logik kommt später (obwohl dies historisch gesehen auch nicht zutrifft). Erneut sagt uns die Solidität, ob die Axiome der Logik das "Verhalten" des Systems korrekt erfassen, und die Vollständigkeit sagt uns, ob wir genug Axiome haben. Woher wissen wir ohne Semantik, ob die Abzugsregeln ausreichen und nicht Unsinn?

Eine Beispiellogik, die rein syntaktisch definiert wurde und an deren formaler Semantik noch gearbeitet wird, ist die BAN-Logik zur Begründung kryptografischer Protokolle. Die logischen Inferenzregeln scheinen vernünftig zu sein. Warum also eine formale Semantik bereitstellen? Leider kann die BAN-Logik verwendet werden, um zu beweisen, dass ein Protokoll korrekt ist, es kann jedoch zu Angriffen auf solche Protokolle kommen. Die Abzugsregeln sind daher zumindest in Bezug auf die erwartete Semantik falsch .

Ich bin mit Supercooldave einverstanden, aber es gibt einen anderen, pragmatischeren Grund dafür, mehr als eine Reihe von Folgerungsregeln zu wollen, die eine Logik charakterisieren: Eine bestimmte Reihe von Folgerungsregeln ist in der Regel nicht gut, um die Art von Problemen zu beantworten, mit denen die Logik konfrontiert ist benutzen.

Wenn Sie als Hilbert-System eine Logik haben, die durch eine Liste von Axiomen und ein paar Regeln spezifiziert ist, wird es in der Regel schwierig sein, herauszufinden, wie ein gegebenes Theorem im System bewiesen werden kann, und ohne eine theoretische Einsicht werden Sie es nicht tun in der Lage zu sein zu beweisen, dass ein gegebener Satz im System nicht bewiesen werden kann. Traditionelle Modelle sind gut, um Eigenschaften, die für die gesamte Logik gelten, durch Induktion zu beweisen.

Vier Arten von Werkzeugen sind nützlich, um Probleme zu lösen, die die meisten Logiker lösen möchten, und zwar von der niedrigsten zur semantischsten:

1. Hilbert-artige Systeme eignen sich gut zur Charakterisierung der logischen Konsequenzbeziehung einer Logik, und sie eignen sich normalerweise zur Kategorisierung mehrerer Logiken, beispielsweise konkurrierender modaler Logiken.
2. Tableau-Systeme eignen sich gut zur Formalisierung von Entscheidungsalgorithmen. Wenn eine Logik entscheidbar ist, kann man normalerweise ein terminierendes Tableausystem als Entscheidungsalgorithmus finden, und wenn nicht, kann man ein möglicherweise nicht terminierendes Tableausystem finden, das eine Halbentscheidungsprozedur bereitstellt. Wenn man eine Obergrenze für die Komplexität der Entscheidbarkeit (dh die Komplexitätsklasse einer Logik) aufzeigen will, sind Tableausysteme im Allgemeinen der erste Ort, auf den man schaut.
3. Analytische Beweistheorien, wie Gentzens natürliche Deduktion und Folgerechnung, geben Darstellungen von Beweisen, die für die Argumentation gut sind, und bieten den Begriff des analytischen Beweises, der nützlich ist, um nützliche Eigenschaften wie die Interpolation für eine Theorie zu beweisen.
4. Tarski-artige Modelltheorien eignen sich oft noch besser für logische Überlegungen, da sie sich fast vollständig von den syntaktischen Details der Logik entfernen. In der Modallogik und Mengenlehre liefern sie die Ergebnisse so viel besser, dass diese Logiker in der Regel nur ein sehr geringes Interesse an Tableau- und analytischer Beweistheorie haben.

Da Supercooldave die intuitionistische Logik erwähnte: Ohne die Regel der ausgeschlossenen Mitte wird die Modelltheorie viel komplizierter und analytische Beweistheorien werden wichtiger, typischerweise die Semantik der Wahl. Algebraische Techniken wie die Kategorietheorie werden bevorzugt, um sich von der syntaktischen Komplexität zu lösen.