Logik und Berechnung: ein philosophischer Standpunkt zum Curry-Howard-Isomorphismus

Die Verbindung zwischen Logik und Berechnung ist stärker denn je, insbesondere seit der Etablierung des Curry-Howard-Isomorphismus, der spezifiziert, dass er als und als Programm proofsangesehen werden kann .programsformulastypes

Ich fragte mich, ob wir irgendwelche Texte finden könnten, die einen philosophischen Standpunkt der Beziehung zwischen Logik und Berechnung bieten. Ich konnte kein Dokument darüber finden.

Außerdem habe ich ein paar verwandte Fragen:

1) Da die meisten logischen Systeme (z. B. intuitionistische natürliche Deduktion, klassischer Folgenkalkül) Computersystemen entsprechen (z. B. einfach typisierter λ-Kalkül, System F, kombinatorische Logik ...), können wir sagen, dass Logik und Berechnung dieselbe Natur haben und Ursprung ? Viele Schwierigkeiten ergaben sich aus der Frage nach der Natur der Logik, gibt die Berechnung eine Antwort?

2) Können wir sagen, dass jedes System, das keine Recheneigenschaften mit einem Rechensystem teilt, keine "Logik" ist? (z. B. kein Schnitteliminationssatz, keine Konfluenz/Church-Rosser-Eigenschaft)

EDIT: Nach einiger Recherche

Das einzige, was ich finden konnte, war die Arbeit der französischen Gruppe LIGC, aber die meisten Artikel, die sie schreiben, sind nur auf Französisch.

Es scheint, dass die meisten Arbeiten, die Philosophie und Berechnung verbinden, die lineare Logik (die aus dem Curry-Howard-Isomorphismus hervorgeht) und den Lambda-Kalkül (der [funktionalen] Computerprogrammen eine formale Erklärung gibt) betreffen.

Wenn ich mich nicht irre, nimmt die lineare Logik die Berechnung (Eliminierung von Schnittregeln, die als Bewertung von Programmen angesehen wird) als Grundlage für Logik. Einige Eigenschaften von Programmen wie das Cut-Elimination-Theorem, Confluence oder die Church-Rosser-Eigenschaft stellen aus logischer Sicht sicher, dass sich unsere Logik kohärent verhält. Wir verlassen uns eher auf das operative Verhalten der Logik als auf Sprache oder rein philosophische Grundlagen.

Es scheint, dass diese Arbeiten die englische Community noch nicht erreicht haben, aber vielleicht findet man einige Artikel in englischer Sprache, die von den Mitgliedern der Gruppe geschrieben wurden.

Einige nicht allzu technische Abhandlungen (leider auf Französisch):

In Bezug auf (1) sind Berechenbarkeitstheorie und Beweistheorie Zweige der (mathematischen) Logik, die die Logik zu sein scheinen, an der Sie interessiert sind, daher verstehe ich nicht, wie jemand sagen könnte, dass sie nichts miteinander zu tun haben. Aber denken Sie daran, dass der Begriff der Berechenbarkeit informell ist, die Church-Turing-These basiert auf der informellen Idee der Berechenbarkeit. In Bezug auf (2) hängt das davon ab, was Sie unter "einer Logik" verstehen, wenn Sie nur irgendein formales System meinen, dann nein. Dies über ein sehr grundlegendes axiomatisches, deduktives formales System wie das MU-System von Hofstadter. Verwenden Sie "eine Logik" synonym mit "einem formalen System"?
Aber Sie sollten auch darüber nachdenken, was ein „Computersystem“ ist. Es lässt sich leicht argumentieren, dass sogar ein einfaches System wie MU verwendet werden kann, um eine Art Berechnung darzustellen. Ich glaube, Scott Aaronson hat in einem Vortrag über die Grenzen der Berechnung den Witz gemacht, dass es möglich ist, jedes System als ein Computersystem zu betrachten, sogar einen Toaster, der Toast macht, aber das bedeutet nicht, dass es nützlich ist, dies zu tun. Ordnen Sie eine der deduktiven Regeln der Nachfolgefunktion zu, und wenn Sie einen Beweis zeigen können, dass es in dieser Sprache eine Ableitung einer Zeichenfolge gibt, können Sie eine Arithmetik beweisen.
@Not_Here (1) Ich habe gelesen, dass die "Natur" der Logik nicht klar war. Vielleicht bin ich ein bisschen veraltet, aber einige scheinen zu denken, dass Logik von den Ideen des Menschen abhängt (Psychologie), aus der Vernunft kommt usw., während die Berechnung "scheint" aus "der Natur" zu kommen. Ich dachte, es könnte zum Beispiel irgendwie Antworten auf die Begründung der logischen Regeln/Gesetze oder die Grundlagen der Logik geben.
@Not_Here (2) Ich gebe zu, es ist nicht klar. Ich bin mir selbst nicht sicher, aber ich glaube, ich meine "Logik" auf informelle Weise, an die wir denken, wenn wir über die menschliche Argumentation sprechen. Vielleicht habe ich immer noch eine naive Vorstellung von Logik, aber ich habe mich gefragt, ob logische Systeme ohne Entsprechung zu einem System wie dem Lambda-Kalkül den gleichen Status genießen sollten wie beispielsweise die natürliche Deduktion. JY Girard hat einmal gesagt, er sehe Logiken ohne Cut-Eliminierung wie Autos ohne Motor.
Konzentriert sich Girards transzendentale Syntax, nach der Sie zuvor gefragt haben, nicht genau auf diese Art von Problemen: Curry-Howard-Isomorphismus, rechnerische Rechtfertigung für logische Regeln usw.? Die zweite Frage geht zu weit, finde ich. Die klassische Logik schenkt der Standardinterpretation sicherlich keine Aufmerksamkeit, da dies ein konstruktivistisches/beweistheoretisches Merkmal zu sein scheint. Die Modallogik, jedenfalls Kripkes Version, hat eine noch aufgeblähtere platonische Semantik. Ich würde sagen, man kann rechenfreundliche Logiken hervorheben, muss es aber nicht.
@Conifold Sie haben Recht mit der transzendentalen Syntax, aber ich möchte alternative Meinungen zu diesem Thema. Ich möchte von Girards Standpunkten nicht zu voreingenommen sein. Soweit ich weiß, werden die Recheneigenschaften der klassischen Logik derzeit untersucht. Es scheint, dass es noch einige rechnerische Inhalte enthält (klassische Realisierbarkeit, Lambda-µ-Kalkül von Parigot, Lambda-µ-µ~-Kalkül von Curien und Herbelin usw.). Aber ich denke, das ist nicht das, was Sie mit "Standardinterpretation" gemeint haben.
Es scheint, dass klassische Verwendungen der klassischen Logik ihren rechnerischen Eigenschaften, was auch immer sie sein mögen, wenig Aufmerksamkeit geschenkt haben, und nichtkonstruktives Denken taucht bereits in Euklid auf. Wenn dem so ist, dann zeigt unser paradigmatisches Beispiel bereits, dass sich die Idee der Logik von der Idee des Algorithmus unterscheidet. Intuitiv geht es bei der Logik selbst in Computerkontexten nicht so sehr um das Rechnen an sich, sondern um die Überprüfung der Gültigkeit einer dokumentierten Berechnung, sie ist in einer Weise normativ, wie es das Rechnen nicht ist.
der zentrale Begriff der Berechenbarkeit ist der intuitive Begriff des effektiven Verfahrens ; Das zentrale Anliegen der Logik ist der intuitive Begriff der (logischen) Konsequenz . Turing gab uns ein formales Modell des ersteren; uns fehlt immer noch ein formelles Modell des ersteren. siehe home.uchicago.edu/~wwtx und Philosophy.su.se/english/research/our-researchers/emeriti/… , und folgen Sie den Bibliographien.

Antworten (1)

Ich glaube, Sie sind zu Recht von der Curry-Howard-Korrespondenz beeindruckt. Es ist ein detaillierter und umfassender Regel-für-Regel- und Merkmal-für-Merkmal-Isomorphismus. Dies deutet stark darauf hin, dass Beweis und Berechenbarkeit eng miteinander verbunden sind. Ich stimme auch zu, dass es in der Philosophie der Logik unterschätzt wird und dass wir es zulassen können und sollten, dass es unser Verständnis von Logik beeinflusst.

Logiker streiten gerne über Logik. Sie werden sogar über grundlegende Dinge uneins sein, wie zum Beispiel darüber, wie man den Begriff der Gültigkeit erklären soll . Fragen Sie Frege, Quine, Tarski, Davidson, Lewis, Prawitz, Etchemendy, McGee, Brandom und MacFarlane und Sie erhalten zehn verschiedene Antworten. Sie werden auch darüber streiten, ob es eine einzige Logik gibt, die alle beherrscht, und wenn ja, welche es ist, oder ob logischer Pluralismus vertretbar ist. Laut Dummett ist Intuitionismus der einzig richtige Weg; für Read ist es Relevanzlogik, für Priest parakonsistente Logik, für Quine klassische Logik.

Auf der Berechenbarkeitsseite des Zauns gibt es relativ wenig Streit darüber, was zur Berechenbarkeit zu sagen ist. Es gibt einige Fragen zur genauen Formulierung der Church-Turing-These, ob und wie sie auf interaktive Computer zutrifft und ob Überlegungen wie Naturgesetze das bestimmen dürfen, was wir als Berechnung bezeichnen können.

Da wir die Berechenbarkeit anscheinend ziemlich gut verstehen und die Logik eher weniger gut, scheint es sinnvoll zu sein, unser Verständnis der ersteren zu erlauben, uns bei der zweiten zu helfen.

Es ist wichtig zu beachten, dass sich die Curry-Howard-Korrespondenz auf die klassische Logik erstreckt. Curry und Howard selbst waren sich dessen nicht bewusst, als sie die Korrespondenz formulierten. Sie gingen von der BHK-Interpretation des Intuitionismus aus und nutzten die Tatsache, dass intuitionistische Beweise konstruktiv sind, um diese Beweise als Rezepte für eine Berechnung zu lesen. Aber spätere Arbeiten von Informatikern, darunter Griffin, Parigot, Aschieri und andere, zeigten, dass sogar die klassische Logik die Korrespondenz teilt. In der Praxis bedeutet dies, dass es rechnerische Interpretationen klassischer Systeme gibt, die normalisierbar sind und es ermöglichen, Berechnungen aus klassischen Beweisen zu extrahieren.

Das bedeutet nicht, dass jeder klassische Satz berechenbar ist: Es gibt offensichtlich eine beliebige Anzahl unentscheidbarer Sätze. Der volle Umfang dessen, was klassisch berechenbar ist, ist noch ein Forschungsgebiet. Aber es bedeutet, dass wir auf die vereinfachende Vorstellung verzichten können, dass die klassische Logik nicht-konstruktiv ist, während die intuitionistische Logik konstruktiv ist. Klassische Disjunktionen können beispielsweise Gegenstand von schnittfreien Beweisen sein, wie Girard in seinem Artikel A New Constructive Logic: Classical Logic feststellte .

Um Ihre spezifischen Fragen zu beantworten:

  1. Logik und Berechenbarkeit sind in der Tat eng miteinander verbunden. Sie sind jedoch nicht identisch. Zumindest finden Berechnungen im Laufe der Zeit statt und erfordern eine Art Rechenmaschine. Beweise werden oft als abstrakte Strukturen betrachtet, obwohl jede Instanz eines Beweises eine physische Form erfordert.

  2. Die Idee, dass eine Logik einen berechenbaren Apparat besitzen sollte, um sich als Logik zu qualifizieren, ist nicht so seltsam, wie es klingen mag. Es würde die klassische Logik nicht von der Qualifikation ausschließen. Es ist jedoch eine starke Anforderung und könnte von denen bestritten werden, die der Ansicht sind, dass die Semantik der Logik Vorrang vor der Beweistheorie einnimmt.

Als letzte Spekulation vermute ich, dass die Verbindung zwischen Logik und Berechenbarkeit die Ansicht stützt, dass wir Logik als wesentlich formaler Natur verstehen sollten. Logische Darstellungen, die die Formalität herunterspielen, hätten größere Schwierigkeiten, den Zusammenhang mit der Berechenbarkeit zu erklären. Außerdem könnten einige sehr allgemeine Vorstellungen davon, was als Gültigkeit gilt, mit der Begründung abgelehnt werden, dass sie nicht direkt in eine berechenbare Form gebracht werden können.

Sehr klare und interessante Antwort. Ich hatte auch das Gefühl, dass es "unterschätzt" wird, wie Sie sagten. Nun habe ich einige Fragen und Anmerkungen. (1) Sind wir sicher, dass Logik und Berechenbarkeit nicht identisch sind? Verstehen wir wirklich, was ein Beweis ist? Es scheint, dass Girards Ludics Beweisen einen rechnerischen / interaktiven Charakter verleihen. Ich weiß nicht, ob dies in unserem Kontext relevant ist. (2) Was meinen Sie mit "formaler Natur" (über Logik) (3) Sie haben keine Referenzen, die die Korrespondenz aus philosophischer Sicht diskutieren?
Man könnte argumentieren, dass das, was berechenbar ist, durch die Naturgesetze eingeschränkt ist. Es gibt mehrere vorgeschlagene „Hypercomputer“, dh Geräte, die über das hinausgehen, was durch Turing berechenbar ist, aber sie können in unserem Universum nicht gebaut werden. Logik wird meist als abstrakter verstanden. Mit „formaler Natur“ meine ich nur Erklärungen zur Logik, in denen die Formalität ein wesentliches Merkmal dessen ist, was wir unter Logik verstehen, und nicht ein Produkt der Art und Weise, wie wir sie studieren. Es gibt verschiedene Möglichkeiten, wie Logik formal sein kann. Wenn Sie nach John MacFarlanes Ph.D. Dissertation online, er hat einen guten Bericht darüber ...
Was philosophische Referenzen zur Curry-Howard-Korrespondenz selbst betrifft, so gibt es meiner Meinung nach nur sehr wenige: Die meisten Diskussionen konzentrieren sich auf die technischen Aspekte.
Logik und Berechnung: ein philosophischer Standpunkt zum Curry-Howard-Isomorphismus
AntwortenHierDatenschutz-Bestimmungen1y, 0v