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

Question

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

Logik
Mathematik
Beweistheorie
Informatik
Hilbert-Kalkül
natürlicher Abzug

Tim

Ist es richtig, dass Endertons A Mathematical Introduction to Logic ein System im Hilbert-Stil für die Logik erster Ordnung verwendet?

Auf Seite 110 in ABSCHNITT 2.4 A Deduktiver Kalkül in Kapitel 2: Logik erster Ordnung

Unsere einzige Schlussregel ist traditionell als Modus Ponens bekannt. Üblicherweise heißt es: Aus den Formeln $α$ Und $α → β$ wir können schließen $β$ :
$\frac{a, a \to β}{β} .$ $\frac{α, α → β}{β}.$

Was bedeutet die Regel:

Ein Fall von Beziehung $\vdash$ : $\{α, α → β\} \vdash β$ .
Eine Instanz einer Beziehung zwischen den Instanzen von $\vdash$ : Wenn $\vdash α$ Und $\vdash α → β$ , Dann $\vdash β$ .
Für einen Satz $\Gamma$ von Formeln, wenn $\Gamma \vdash α$ Und $\Gamma \vdash α → β$ , Dann $\Gamma \vdash β$ . Das Zitat bedeutet also zu haben $\Gamma$ aber lässt es weg, weil es denkt, dass seine Leser es automatisch ausfüllen werden. (Siehe auch weiter unten)
Etwas anderes?

Einige Gedanken, Beobachtungen und Fragen:

2 und 3 sind äquivalent, weil 2 durch das deduktive Theorem 3 impliziert (oder ich liege falsch, weil das deduktive Theorem aus den Inferenzregeln und Axiomen abgeleitet wird, also nicht vor den Inferenzregeln und Axiomen existiert?).
Was mich dazu bringt, 3 über 2 zu unterstützen, ist, dass ich in Wikipedia gesehen habe , dass der deduktive Satz als erweiterte Inferenzregel angesehen wird.

Da Systeme im Hilbert-Stil nur sehr wenige Abzugsregeln haben, ist es üblich, Metatheoreme zu beweisen, die zeigen, dass zusätzliche Abzugsregeln keine Abzugskraft hinzufügen, in dem Sinne, dass ein Abzug unter Verwendung der neuen Abzugsregeln in einen Abzug umgewandelt werden kann, der nur den ursprünglichen Abzug verwendet Regeln.

Einige gebräuchliche Metatheoreme dieser Form sind: Der Abzugssatz, ...

und in Endertons Buch auf S. 118

SCHLUSSSATZ Wenn $\Gamma; \gamma \vdash ϕ$ , Dann $\Gamma \vdash ( γ → ϕ )$ .
Bedeuten Inferenzregeln in einem Hilbert-System dasselbe wie in einem natürlichen deduktiven System? Nr. 3 oben ist ähnlich wie 3.5 "Modus ponens" auf p65 in IV Sequent Calculus (eigentlich ein natürliches Deduktionssystem) in Ebbinghuas' Mathematical Logic . Bedeuten die horizontalen Linien, die in beiden erscheinen, "wenn ... dann ..." auf der Ebene der Metasprache?
Die Antwort auf eine verwandte Frage besagt, dass Inferenzregeln auf Formeln wirken können, wenn sie nicht explizit so geschrieben sind, dass sie auf Sequenzen wirken (dh Instanzen von $\vdash$ ). Ist das falsch? Inferenzregeln arbeiten immer auf der Instanz von $\vdash$ , auch wenn sie in einer Form geschrieben sind, die aussieht, als würden sie direkt mit Formeln arbeiten?

Danke.

Tim

Danke. Was meinst du mit "sie sind die Menge Γ in der Definition der Deduktion von 𝜑 von Γ"?

Antworten (1)

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

Danke. Was meinst du mit "sie sind die Menge Γ in der Definition der Deduktion von 𝜑 von Γ"?

Mauro ALLEGRANZA · Answer 1

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

JA.

Siehe Folgerungsregel . Die "kanonische" Darstellung ist ziemlich üblich, aber es ist nur eine durchsichtige symbolische Darstellung.

Wir können es in Worten beschreiben: In der Regel handelt es sich um eine „Prozedur“, die als Eingabe eine oder zwei Formeln einer bestimmten Form nimmt und als Ausgabe eine neue Formel erzeugt.

Sie arbeiten also nach Formeln . Und was relevant ist, ist nicht die „typografische Form“, die wir verwenden, um sie darzustellen, sondern die Tatsache, dass sie „formal“ ist.

Die Modus-Ponens-Regel wird im Zusammenhang mit der Definition von „formaler Deduktion“ angegeben, die dazu gedacht ist, „(in unserem Modell des deduktiven Denkens) die Beweise des arbeitenden Mathematikers zu spiegeln“ [siehe gestrigen Beitrag ] .

Eine formale Deduktion ist eine Folge von Formeln: In jeder Phase können wir eine Annahme, ein logisches Axiom schreiben oder eine Formel unter Verwendung der MP-Schlussregel hinzufügen, die die "Ausgabe" -Formel aus zwei zuvor geschriebenen Formeln der Folge erzeugt.

Somit führt eine Anwendung der MP-Regel zu folgender Schlussfolgerung: $\{ α, α → β \} ⊢ β$ .

2 ist einfach ein Sonderfall von 3. Das Zitat lässt Annahmen nicht aus: Sie sind die Menge $Γ$ in der Definition des Abzugs von $\varphi$ aus $Γ$ (Seite 111).

Was sind „Annahmen“? Wie bereits gesagt, ist die Definition der formalen Ableitung ein formales Modell der mathematischen Praxis: let $\Gamma$ der Satz von Euklids Elementaxiomen und let $\varphi$ Satz des Pythagoras.

Wir haben $Γ \vdash \varphi$ .

Annektieren

Hier ist Endertons Modus Ponens (Endertons Beweissystem ist ein Hilbert-Stil):

\frac{a, a \to β}{β} .

$\frac{α, α → β}{β}.$

Hier ist die gleiche Regel (Bedingte Eliminierung genannt) aus einem populären Lehrbuch über natürliche Deduktion:

van Dalens Logik und Struktur .

Dieselbe Regel wird "im Kontext" von Ableitungen dargestellt $\mathcal D, \mathcal D'$ .

Aus typografischen Gründen können wir es wie folgt darstellen:

$\frac{D . . . φ D^{'} . . . (φ \to ψ)}{ψ} .$ $\frac{\mathcal D ... \varphi \ \ \ \mathcal D' ... (\varphi \to \psi)}{\psi}.$

Und dann können wir das Ableitungssymbol in folgender Form "umformen" :

Wenn $(Γ \vdash \varphi)$ Und $(Δ \vdash (\varphi → \psi))$ beide richtige Folgen sind, dann die Folge $(Γ \cup \vdash \psi)$ ist richtig.

Der letzte Schritt besteht darin, eine Prämisse über die andere zu setzen, und wir haben Ebbinghaus' Modus Ponens .

Danke. Die Antwort auf eine verwandte Frage besagt, dass Inferenzregeln auf Formeln wirken können, wenn sie nicht explizit so geschrieben sind, dass sie auf Sequenzen wirken (dh Instanzen von $\vdash$ ). Ist das falsch? Inferenzregeln arbeiten immer auf der Instanz von $\vdash$ , auch wenn sie in einer Form geschrieben sind, die aussieht, als würden sie direkt mit Formeln arbeiten?
Ihre Antwort hier stimmt mit Nr. 2 oder 3 überein, was bedeutet, dass eine Inferenzregel auf Instanzen von angewendet wird $\vdash$ , auch wenn es in einem Hilbert-System eine Regel ist und ohne geschrieben wird $\vdash$ wie im ersten Zitat in meinem Beitrag. Ihr Kommentar unter math.stackexchange.com/questions/3819852/… bedeutet, dass eine Regel immer mit Formeln arbeitet. Konsequent oder nicht?
Schlußregeln arbeiten mit Formeln : "wenn $p \to q$ Und $p$ , Dann $q$ " ist eine vollkommen korrekte Verwendung von Modus Ponens, aber $p \to q$ ist keine Tautologie; daher ist es durch Korrektheit nicht ableitbar , indem nur logische Axiome und Regeln verwendet werden, dh $\nvdash p \to q$ . (siehe Beitrag von gestern).
Wie oben gesagt, wenn wir die Regeln einschränken auf " $\vdash$ „Wir können sie nur auf Sätze der reinen Logik (gültige Formel) anwenden und können sie daher nicht verwenden, um Konsequenzen aus Annahmen abzuleiten. Der Schluss: $\forall x P(x) \vdash P(s)$ ist eine gültige Schlussfolgerung von FOL (eine Anwendung der universellen Instanziierung: Aus der Annahme, dass alles ein Philosoph ist, leiten wir korrekt ab, dass Sokrates ein Philosoph ist), aber das haben wir nicht $\vdash \forall x P(x)$ weil es nicht gilt: es ist nicht wahr, dass alles ein Philosoph ist.

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

Tim

Tim

Antworten (1)

Mauro ALLEGRANZA

Tim

Tim

Mauro ALLEGRANZA

Mauro ALLEGRANZA

Mauro ALLEGRANZA

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

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

Unterschied zwischen logischen Axiomen und Schlußregeln

Wie wird die vollständige Semantik von SOL und HOL spezifiziert?

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

Ist eine Turing-Maschine auf einem beliebigen (endlichen) Alphabet äquivalent zu einer auf {0, 1}?

Ist die Formel logisch gültig? (Prädikatenlogik)

Sind Mengen und Symbole die Bausteine der Mathematik?

Was ist die Intuition hinter der Verwendung des Gesetzes der ausgeschlossenen Mitte in der natürlichen Deduktion?

Unter der Curry-Howard-Korrespondenz oder locker "Beweise-als-Programme", haben wir auch "Programme-als-Beweise" und was würde einige Arb. Programm beweisen?