Das Zeigen eines axiomatischen Beweissystems im Hilbert-Stil und eines natürlichen Gentzen-Abzugs im sequentiellen Stilkalkül sind äquivalent

Question

Das Zeigen eines axiomatischen Beweissystems im Hilbert-Stil und eines natürlichen Gentzen-Abzugs im sequentiellen Stilkalkül sind äquivalent

Logik
Mathematik
Beweistheorie
Intuitionistische Logik

Benutzer65526

Kann mir jemand einen Beweis dafür geben, dass eine gegebene Axiomatisierung der intuitionistischen Aussagenlogik im Hilbert-Stil ( $H$ ) und eine gegebene natürliche Deduktionsformulierung der intuitionistischen Logik im sequentiellen Stil ( $N$ ) im folgenden Sinne äquivalent sind?

für alle Formeln, $M$ , $\hspace{0.3cm} \Gamma \vdash_{H} M$ iff $\Gamma \vdash_N M$ ableitbar ist, wo $\Gamma$ ist endlich und $M$ enthält höchstens eine Formel.

Mein Interesse an dieser Frage rührt daher, dass ich beweisen möchte $THEOREM \thinspace 2.3$ In

Matt Fairtlough und Michael Mendler, Propositional Lax Logic (1997): THEOREM 2.3 , Seite 7.

Ein beispielhafter Beweis einer Äquivalenz zwischen einem natürlichen Hilbert- und einem Gentzen-Deduktionssystem im sequentiellen Stil würde mir helfen.

Benutzer65526

Ich habe es bearbeitet. Es war ein Fehler.

DanielV

Sie müssen die Transformation definieren, unter der sie gleich sind. Die Hauptidee davon ist, dass in ND ein Satz

P

$P$ unter den Annahmen

A_{0}, A_{1}, \dots

$A_0, A_1, \dots$ ist äquivalent zu einem Satz in Hilbert

A_{0} \to (A_{1} \to (\dots \to P))

$A_0 \to (A_1 \to (\dots \to P))$ . Dann ist der Modus Ponens von ND mechanisch anders als der Modus Ponens von Hilbert: Er übersetzt tatsächlich von ND zu Hilbert in nichts.

Daniel Schepler

Ich habe gerade diese Frage gesehen - es könnte erwähnenswert sein, dass ich in Coq einen formalen Beweis der Äquivalenz für eine bestimmte Formulierung von jeder habe (obwohl es in diesem Fall für die intuitionistische Aussagenlogik gilt, aber dasselbe für die klassische Aussagenlogik tun sollte). sehr ähnlich). github.com/dschepler/coq-sequent-calculus/blob/master/Hilbert.v und schau dir das Ergebnis ND_hilbert_equivam Ende an.

Antworten (1)

Das Zeigen eines axiomatischen Beweissystems im Hilbert-Stil und eines natürlichen Gentzen-Abzugs im sequentiellen Stilkalkül sind äquivalent

Sie müssen die Transformation definieren, unter der sie gleich sind. Die Hauptidee davon ist, dass in ND ein Satz $P$ unter den Annahmen $A_0, A_1, \dots$ ist äquivalent zu einem Satz in Hilbert $A_0 \to (A_1 \to (\dots \to P))$ . Dann ist der Modus Ponens von ND mechanisch anders als der Modus Ponens von Hilbert: Er übersetzt tatsächlich von ND zu Hilbert in nichts.
Ich habe gerade diese Frage gesehen - es könnte erwähnenswert sein, dass ich in Coq einen formalen Beweis der Äquivalenz für eine bestimmte Formulierung von jeder habe (obwohl es in diesem Fall für die intuitionistische Aussagenlogik gilt, aber dasselbe für die klassische Aussagenlogik tun sollte). sehr ähnlich). github.com/dschepler/coq-sequent-calculus/blob/master/Hilbert.v und schau dir das Ergebnis ND_hilbert_equivam Ende an.

hmakholm hat Monica übrig gelassen · Answer 1

Das wirst du separat beweisen wollen $\Gamma \vdash_H M$ impliziert $\Gamma \vdash_N M$ und umgekehrt. Jeder dieser Fälle kann durch Induktion über die Struktur des Beweisbaums (oder über die Länge eines Beweises, falls vorhanden) durchgeführt werden $H$ stellt Beweise eher als flache Folgen von Formeln als als Bäume dar).

Die Richtung ${\vdash_H} \Rightarrow {\vdash_N}$ ist einfach, da die einzige Inferenzregel in $H$ ist modus ponens, was auch eine Regel von ist $N$ (normalerweise genannt $\to$ -Eliminierung in dieser Einstellung). Alles, was Sie also wirklich tun müssen, ist zu zeigen, dass jede (Instanz eines) logischen Axioms von $H$ kann nachgewiesen werden $N$ .

Für die Richtung ${\vdash_N} \Rightarrow {\vdash_H}$ , die meisten Fälle sind einfach. Die Schlußregeln von $N$ die dem nichts hinzufügen $\Gamma$ s kann einfach durch lokale Ableitungen von ersetzt werden $H$ . Zum Beispiel für $\land$ -Einführung

\frac{Γ ⊢_{N} M Γ ⊢_{N} K}{Γ ⊢_{N} M \land K} \land ICH

$\frac{\Gamma\vdash_N M \qquad \Gamma\vdash_N K}{\Gamma \vdash_N M\land K} \,{\land I}$ zeige das ein für allemal

⊢_{H} M \to (K \to M \land K)

$\vdash_H M \to ( K \to M \land K )$ für alle

M

$M$ Und

K

$K$ -- normalerweise sofort, da dies ein Axiom des Hilbert-Systems ist, aber für einige Systeme ist ein wenig Korrekturarbeit erforderlich. Dann jede Anwendung von

\land I

$\land I$ kann durch diesen Nachweis und zwei Anwendungen von MP ersetzt werden, nachdem die Prämissen übersetzt worden sind

⊢_{H}

$\vdash_H$ nach der Induktionshypothese.

Der Hauptfall in einem typischen natürlichen Deduktionssystem (für Aussagenkalkül), in dem dies nicht funktioniert, ist $\to$ -Einführung. Hier ist genau das, was Sie brauchen, um den Fall durchzugehen, das Deduktionstheorem $\vdash_H$ , was Sie hoffentlich schon um seiner selbst willen bewiesen haben.

Der $\lor$ -Eliminierungsregel in ihrer gebräuchlichsten Formulierung erfordert eine Kombination dieser Ansätze. Wenden Sie den Deduktionssatz auf die beiden Prämissen an, die sich ausdehnen $\Gamma$ , und zeige das dann

⊢_{H} (K \lor L) \to ((K \to M) \to ((L \to M) \to M))

$\vdash_H (K\lor L)\to((K\to M)\to((L\to M)\to M))$ und wende MP dreimal an.

Warum in dem Artikel verwendet es $\vee$ (was meiner Meinung nach verallgemeinerte Vereinigung bedeutet) in "Man beweist einen stärkeren Satz und zeigt, dass wann $\Gamma$ ist endlich und $\Delta$ enthält höchstens eine Formel, die Folge $\Gamma \vdash_{N}\Delta$ ist ableitbar gff $\Gamma \vdash_{H} \vee \Delta$ , Wo $\vee \Delta = M$ Wenn $\Delta = \{ M \}$ , Und $\vee \emptyset$ = falsch." ?
Ich würde diese Verwendung von verstehen $\vee$ wenn es mehr als eine Formel im Konsequens gab, dies aber ausdrücklich ausgeschlossen ist.
@ user65526 - vielleicht weil in der klassischen Logik die Konsequenz $\Delta$ kann mehr als ein Element haben.
@user65526: Ah! Jetzt, da ich mir das Papier ansehe, auf das Sie verlinken (ich dachte, der Link sei falsch, weil Seite 5 nichts Relevantes enthielt; Seite 7 jedoch schon!), sehe ich die Quelle einiger Ihrer Verwirrung. Was es als "Gentzen-Regeln" präsentiert, ist kein natürliches Deduktionssystem , sondern ein Folgerechnung a la Gentzens LJ. (Gentzen hat diese beiden Arten von Beweissystemen erfunden, aber sie sind nicht gleich). In dieser Antwort ging ich davon aus, dass es sich tatsächlich um ein natürliches Abzugssystem handelt, wie Sie sagten. Die zweiteilige Gesamtstrategie, die ich vorschlage, wird immer noch funktionieren, die Details, die ich skizziert habe, nicht.

Das Zeigen eines axiomatischen Beweissystems im Hilbert-Stil und eines natürlichen Gentzen-Abzugs im sequentiellen Stilkalkül sind äquivalent

Benutzer65526

Benutzer65526

DanielV

Daniel Schepler

Antworten (1)

hmakholm hat Monica übrig gelassen

Benutzer65526

Benutzer65526

Mauro ALLEGRANZA

hmakholm hat Monica übrig gelassen

Eine Verwirrung über Churchs einfache Typentheorie und den Curry-Howard-Isomorphismus

Unter welchen Bedingungen hat ein axiomatisches Beweissystem ein natürliches Deduktionsäquivalent?

Warum können wir Schlußregeln nicht generell durch Axiome ersetzen?

Welche Sätze der klassischen Mathematik lassen sich ohne Anwendung des Satzes vom ausgeschlossenen Dritten nicht beweisen?

Wie genau erfasst die Curry-Howard-Formalisierung der Logik die Semantik des Nichthaltens von LEM?

Bedeuten Inferenzregeln in einem Hilbert-System dasselbe wie in einem natürlichen deduktiven System?

Logiksymbole "fließend" in der Mathematik verwenden. Wie kann ich zeigen, dass ein Satz von Bedingungen, dargestellt durch logische Symbole, unabhängig von einem anderen ist?

Klarstellung bezüglich der Substitution im Folgenkalkül

Interpretation der Implikation in der intuitionistischen Logik

Der Hilbert-artige Beweis von Γ⊢ψΓ⊢ψ\Gamma\vdash\psi und Γ⊢χΓ⊢χ\Gamma\vdash\chi impliziert Γ⊢ψ∧χΓ⊢ψ∧χ\Gamma\vdash\psi\wedge\chi