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

Question

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

Logik
Mathematik
Intuitionistische Logik
Aussagenkalkül

konewka

Ich erhalte das folgende System im Hilbert-Stil (für die intuitionistische Aussagenlogik):

Axiomenschemata :

$\phi\vee\phi\rightarrow\phi$
$\phi\rightarrow\phi\wedge\phi$
$\phi\rightarrow\phi\vee\psi$
$\phi\wedge\psi\rightarrow\phi$
$\phi\vee\psi\rightarrow\psi\vee\phi$
$\phi\wedge\psi\rightarrow\psi\vee\phi$
$\bot\rightarrow\phi$

Inferenzregeln :

$\phi$ Und $\phi\rightarrow\psi$ implizieren $\psi$
$\phi\rightarrow\psi$ Und $\psi\rightarrow\chi$ implizieren $\phi\rightarrow \chi$
$\phi\wedge\psi\rightarrow\chi$ impliziert $\phi\rightarrow(\psi\rightarrow\chi)$
$\phi\rightarrow(\psi\rightarrow\chi)$ impliziert $\phi\wedge\psi\rightarrow\chi$
$\phi\rightarrow\psi$ impliziert $\phi\vee\chi\rightarrow\psi\vee\chi$

Wir definieren für eine Menge $\Gamma$ von Aussageformeln und einer Formel $\phi$ , wir definieren $\Gamma\vdash_{IL}\phi$ als ''In diesem Beweissystem im Hilbert-Stil (für die intuitionistische Logik) existiert ein Beweis von $\phi$ aus $\Gamma$ .

Ich soll nun beweisen (im Wesentlichen ist die eigentliche Frage umfassender):

Wenn Γ ⊢_{ICH L} ψ Und Γ ⊢_{ICH L} χ, Dann Γ ⊢_{ICH L} ψ \land χ

$\text{if }\Gamma\vdash_{IL}\psi\text{ and }\Gamma\vdash_{IL}\chi\text{, then }\Gamma\vdash_{IL}\psi\wedge\chi$ In einem Beweissystem wie der natürlichen Deduktion würde dies durch eine Konjunktionseinführung bewiesen, aber mit den obigen Hilbert-Regeln konnte ich in keiner Weise eine Art Konjunktionseinführung erhalten. Zum Beispiel hat mich die Verwendung von Axiomenschema 2 nicht weitergebracht, wir könnten an eine Ersetzung denken

(ψ \land χ)

$(\psi\wedge\chi)$ für

ϕ

$\phi$ , oder einfach ersetzen

ψ

$\psi$ für

ϕ

$\phi$ , aber keine Inferenzregel wird uns dann zu dem gewünschten Ergebnis führen.

Lässt sich die Aussage mit diesem Hilbert-System beweisen?

hmakholm hat Monica übrig gelassen

Das ist nicht wirklich ein Hilbert-System. In einem System vom Hilbert-Typ ist Modus Ponens die einzige Folgerungsregel, und der gesamte Rest der Logik ist als Axiome kodiert.

konewka

@HenningMakholm okay, so hat es zumindest mein Professor formuliert. Er machte tatsächlich die Bemerkung, dass dieses System konstruiert wurde, um die Idee einer Deduktion in einem Hilbert-Stil-System zu unterrichten, aber vielleicht hätte er den Hilbert-Teil nicht verwenden und es einfach einen anderen Beweiskalkül irgendwo zwischen natürlicher Deduktion und Hilbert- Stilsysteme. Wäre es unter Berücksichtigung der oben gegebenen Regeln jedoch möglich, diese Aussage zu beweisen?

hmakholm hat Monica übrig gelassen

Es sieht für mich tatsächlich ziemlich unkonventionell aus – zum Beispiel, um sich zu beweisen

ϕ \to ϕ

$\phi\to\phi$ man müsste entweder über beide gehen

ϕ \land ϕ

$\phi\land\phi$ oder

ϕ \lor ϕ

$\phi\lor\phi$ .

konewka

Ich stimme Ihnen zu, dieses Beweissystem ist meiner Meinung nach ziemlich künstlich

Doug Spoonwood

@HenningMakholm Ich bin anderer Meinung. Dies qualifiziert sich immer noch als "Hilbert" ... ähm Frege ... Typsystem. Ein System vom Frege-Typ zeichnet sich dadurch aus, dass jeder Schritt in Beweisen entweder Axiome oder Ableitungen von vorherigen Schritten sind. en.wikipedia.org/wiki/Hilbert_system Nicods System zum Beispiel qualifiziert sich als Frege-System, verwendet aber keinen Modus Ponens. Andere wurden auch schon früher in der Literatur beschrieben.

Antworten (2)

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

Das ist nicht wirklich ein Hilbert-System. In einem System vom Hilbert-Typ ist Modus Ponens die einzige Folgerungsregel, und der gesamte Rest der Logik ist als Axiome kodiert.
@HenningMakholm okay, so hat es zumindest mein Professor formuliert. Er machte tatsächlich die Bemerkung, dass dieses System konstruiert wurde, um die Idee einer Deduktion in einem Hilbert-Stil-System zu unterrichten, aber vielleicht hätte er den Hilbert-Teil nicht verwenden und es einfach einen anderen Beweiskalkül irgendwo zwischen natürlicher Deduktion und Hilbert- Stilsysteme. Wäre es unter Berücksichtigung der oben gegebenen Regeln jedoch möglich, diese Aussage zu beweisen?
Es sieht für mich tatsächlich ziemlich unkonventionell aus – zum Beispiel, um sich zu beweisen $\phi\to\phi$ man müsste entweder über beide gehen $\phi\land\phi$ oder $\phi\lor\phi$ .
Ich stimme Ihnen zu, dieses Beweissystem ist meiner Meinung nach ziemlich künstlich
@HenningMakholm Ich bin anderer Meinung. Dies qualifiziert sich immer noch als "Hilbert" ... ähm Frege ... Typsystem. Ein System vom Frege-Typ zeichnet sich dadurch aus, dass jeder Schritt in Beweisen entweder Axiome oder Ableitungen von vorherigen Schritten sind. en.wikipedia.org/wiki/Hilbert_system Nicods System zum Beispiel qualifiziert sich als Frege-System, verwendet aber keinen Modus Ponens. Andere wurden auch schon früher in der Literatur beschrieben.

hmakholm hat Monica übrig gelassen · Answer 1

Sie können es beweisen

ψ \land χ \to ψ \land χ

$\psi\land \chi \to \psi\land\chi$ indem du durchgehst

(ψ \land χ) \land (ψ \land χ)

$(\psi\land\chi)\land(\psi\land\chi)$ . Wenden Sie jetzt Regel 10 an, um zu erhalten

ψ \to (χ \to ψ \land χ)

$\psi \to (\chi\to\psi\land\chi)$ Dann Ihre angenommenen Ableitungen von

ψ

$\psi$ Und

χ

$\chi$ , plus modus ponens zweimal schließt

ψ \land χ

$\psi\land \chi$ .

Oh, das tut es tatsächlich. Danke für die Einsicht, solche Beweissysteme erfordern wirklich mehr Arbeit, als man bei Verwendung eines anderen Beweissystems erwarten würde, selbst für solche elementaren Aussagen
Ich verstehe nicht, wie Sie den ersten Schritt gemacht haben, aber Sie können zu dem gelangen, was Sie dort haben.

Doug Spoonwood · Answer 2

Ich verwende die polnische Notation. Die Formationsregeln lauten:

Alle Kleinbuchstaben des lateinischen Alphabets und 0 gelten als wohlgeformte Formeln (wffs).
Wenn $\alpha$ Und $\beta$ als wffs qualifizieren, dann auch N $\alpha$ , C $\alpha$ $\beta$ , k $\alpha$ $\beta$ , und ein $\alpha$ $\beta$ .

Die Axiomenschemata sind:

Capp ein Gesetz von Clavius
CpKpp ein Gesetz der K-Tautologie Einführung
Einführung der CpApq-Linksdisjunktion
CKpqp linke Konjunktionseliminierung
CApqAqp A-Kommutation
Die CKpqApq-Konjunktion ist schwächer als die Disjunktion
C0p falsum impliziert jede Aussage

Die Inferenzregeln lauten:

$\alpha$ , C $\alpha$ $\beta$ $\vdash$ $\beta$ Modus ponens
C $\alpha$ $\beta$ , C $\beta$ $\gamma$ $\vdash$ C $\alpha$ $\gamma$ Hypothetischer Syllogismus
CK $\alpha$ $\beta$ $\gamma$ $\vdash$ C $\alpha$ C $\beta$ $\gamma$ Ausfuhr
C $\alpha$ C $\beta$ $\gamma$ $\vdash$ CK $\alpha$ $\beta$ $\gamma$ Einfuhr
C $\alpha$ $\beta$ $\vdash$ CA $\alpha$ $\gamma$ A $\beta$ $\gamma$

Wenn wir nun q durch p (im Folgenden q/p) in 3 ersetzen, erhalten wir

CpApp

Wenn wir den hypothetischen Syllogismus auf 13 und 1 anwenden, erhalten wir somit

Cpp

Durch Ersetzen von p durch Kpq in 14 erhalten wir

CKpqKpq

Wenn wir jetzt den Export auf 15 anwenden, erhalten wir

CpCqKpq

Und ich denke, den Rest schaffst du.

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

konewka

hmakholm hat Monica übrig gelassen

konewka

hmakholm hat Monica übrig gelassen

konewka

Doug Spoonwood

Antworten (2)

hmakholm hat Monica übrig gelassen

konewka

Doug Spoonwood

Doug Spoonwood

Aussagenkalkül und intuitionistische Logik

Benötigen Sie Hilfe bezüglich eines Beweises in First Order Logic

Maximal konsistente Theorien haben vollständige zählbare Teiltheorien in jeder zählbaren Teilsprache.

Beweisen Sie die Richtigkeit der Aussagenlogik ohne Induktion?

Wie kann man wissen, ob A⟹BA⟹BA \impliziert, dass B (eine Implikation) wahr ist, ohne zu wissen, ob BBB (die Konsequenz) wahr ist?

Warum ist „weil“ in der Aussagenlogik keine logische Verknüpfung?

Gültige Form und wahre Prämissen machen ein Argument stichhaltig, aber bedeutet „Prämissen“ P, Q, R, … oder „was den Antezedens umfasst“?

Reihenfolge der Quantoren und Umkehrvariablen

Warum gibt es mehrere Axiomensysteme für die Aussagenlogik?

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