Was bedeutet "beweisen"?

Sep 08 2020

Ich verwende die folgenden Beispiele, um die allgemeinen Fälle zu verstehen. Ich weiß nicht, wie ich meine Fragen im allgemeinen Fall artikulieren soll. Ich habe mich gefragt, auf welchen Ebenen die folgenden Aussagen gemacht werden, wie die folgenden formuliert sind und welche Unterschiede und Beziehungen zwischen ihnen bestehen:

Beweisen Sie eine Formel $p$. Bedeutet es zu beweisen$ \vdash p$ (oder $\models p$?) und konvertieren Sie daher die Aufgabe in 3 unten? (Ich habe dies möglicherweise in einem Kommentar gefragt, und jemand hat möglicherweise auf diesen Beweis geantwortet$p$ bedeutet zu beweisen $\vdash p$, aber ich kann die Kommentare nicht finden.)
Beweisen Sie, ob $\phi$, dann $\psi$. Was bedeutet es zu beweisen:$\phi \to \psi$, $\phi \vdash \psi$, oder $\phi \models \psi$, und konvertieren Sie daher die Aufgabe in 1 oben oder 3 unten?
Beweisen $\phi \vdash \psi$.
- Bedeutet es abzuleiten $\phi \vdash \psi$durch Verwendung der Inferenzregeln und Axiome in einem gegebenen Beweissystem (z. B. sequentielle Berechnung)?
- Oder behandelt es $\phi \vdash \psi$ als Formel in einer Sprache auf einer höheren Ebene als die Sprache, die enthält $\phi$ und $\psi$und beweisen $\vdash (\phi \vdash \psi)$ durch Anwenden eines gegebenen Beweissystems (z. B. sequentieller Kalkül) auf diese übergeordnete Sprache?
Beweisen Sie, ob $\phi' \vdash \psi'$, dann $\phi \vdash \psi$.
- Bedeutet es abzuleiten $\phi \vdash \psi$, durch die Nutzung $\phi' \vdash \psi'$und die Inferenzregeln und Axiome in einem gegebenen Beweissystem (z. B. sequentielle Berechnung)?
- Oder behandelt es $\phi' \vdash \psi'$ und $\phi \vdash \psi$ als Formeln in einer Sprache auf einer höheren Ebene als der Sprache, die enthält $\phi$, $\psi$, $\phi'$ und $\psi'$und beweisen $(\phi' \vdash \psi') \vdash (\phi \vdash \psi)$ durch Anwenden eines gegebenen Beweissystems (z. B. sequentieller Kalkül) auf diese übergeordnete Sprache?
und 6. Erwägen Sie das Ersetzen $\vdash$ mit $\models$ in 3 und 4

Etwas verwandtes: Ich fragte :

Gilt "beweisbar" oder "widerlegbar" nur für Formeln, nicht für "eine Folgerung" oder "Ableitung" wie z $∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$? Können wir umschreiben?$∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$ als Formel, so dass es (fast) genau dann ableitbar ist, wenn die entsprechende Formel nachweisbar ist?

Lemontree antwortete :

"Nachweisbar" bedeutet "ableitbar ohne Prämissen", dh die Nachweisbarkeit ist eine Eigenschaft von Formeln, während die Ableitbarkeit eine Eigenschaft von Schlussfolgerungen im Allgemeinen ist. Was Sie suchen, ist wahrscheinlich der Abzugssatz, auch bekannt als Import-Export-Satz, der dies besagt$𝐴_1,…,𝐴_𝑛⊢𝐵$ dann und nur dann, wenn $⊢(𝐴_1∧…∧𝐴_𝑛)→𝐵$. Also mit$∃𝑥𝑅(𝑥)⊬∀𝑦𝑅(𝑦)$ wir haben das $⊬∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$das heißt, die Formel $∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$ ist nicht nachweisbar.

Ich denke, meine obigen Fragen sind eine Metasprache oder eine Beweistheorie, und ich weiß wenig darüber. Gleichzeitig habe ich mich auch gefragt, wie Beweisverfahren in der mathematischen Logik formuliert sind. , was könnte Teil der Beweistheorie sein?

Vielen Dank.

Antworten

2 MauroALLEGRANZA Sep 08 2020 at 21:44

In der Mathematik „beweisen“ bedeutet, einen Beweis für eine Aussage im Kontext einer mathematischen Theorie zu schreiben. Ein Beweis ist ein "Argument", das von den Axiomen der Theorie und den zuvor nachgewiesenen Ergebnissen ausgeht und mit der zu beweisenden Aussage endet, die logische "korrekte" deduktive Schritte verwendet (dh ein gültiges Argument).

In der Logik haben wir das Konzept der Ableitung, dh das formale mathematische Modell eines Beweises im Kontext eines logischen Kalküls, z . B. Natural Deduction .

Die logischen deduktiven Schritte werden normalerweise durch Inferenzregeln formalisiert , die die Grundbausteine des Beweissystems sind , auch bekannt als "logischer Kalkül".

Der Versuch, Ebbinghaus 'Lehrbuch, dem Symbol, zu folgen $\vDash$ist ein metasprachlicher Ausdruck, der im semantischen Kontext mit unterschiedlichen Verwendungen verwendet wird: rechts flankiert von einer Formel, die mit „es ist gültig“ abgekürzt wird (Seite 35); zwischen dem Namen einer Reihe von Formeln und einer Formel wird „es ist eine Folge von“ abgekürzt (Seite 33).

Schließlich, flankiert vom Namen einer Interpretation und einer Formel, wird "es ist wahr unter der Interpretation" abgekürzt.

Es ist nicht Teil der formalen Sprache des Kalküls: Es wird verwendet, um Eigenschaften der Formeln des Kalküls auszudrücken; im Kontext der Aussagenrechnung lesen wir Ausdruck "$⊨ A ∨ ¬A$"als" Formel ... ist eine Tautologie ", dh es ist eine gültige Formel der Satzrechnung.

Wir können (in der Meta-Theorie) diese Formel beweisen $A ∨ ¬A$ist eine Tautologie unter Verwendung der Wahrheitstabellenmethode (dieser "Beweis" ist ein mathematischer Beweis und keine Ableitung im Kalkül).

Ähnliches gilt für das Symbol $\vdash$ (siehe Definition Seite 61).

Nach Ebbinghaus, $\varphi \to \varphi$ ist eine Formel, dh ein Ausdruck der formalen Sprache, die wir lesen: „if $\varphi$, dann $\varphi$”.

Wir können es leicht im Beweissystem ableiten und symbolisieren die Existenz einer solchen Ableitung mit $\vdash \varphi \to \varphi$ Dies ist wiederum keine Formel der formalen Sprache, sondern ein Ausdruck der Metasprache, die die Aussage abkürzt: „Es gibt eine Ableitung von ....“, und wir lesen sie (gemäß der Antwort auf Ihren vorherigen Beitrag): „Formel. .. ist ableitbar (im Kalkül) ".

Leider ist in einigen Formulierungen von ND und Sequent Calculus das Symbol $\vdash$ist Teil der formalen Sprache. In diesem Fall können wir Probleme haben, sie auch in der Metatheorie zu verwenden .

Schließlich müssen wir den Satz von Solidität und Vollständigkeit betrachten , einen Metasatz, der sowohl für die Aussagenrechnung als auch für das Prädikat (siehe Seite 70 und Seite 75) gilt und auf den Punkt gebracht heißt:

„$\vdash \text { iff } \vDash$”.

Dieser Satz drückt eine Eigenschaft des Kalküls und seiner Semantik aus. Wir beweisen es auf eine "normale" mathematische Weise.

Wie oben gesagt, können wir die Wahrheitstabelle verwenden, um dies zu beweisen $A ∨ ¬A$ ist eine Tautologie ($⊨ A ∨ ¬A$) und verwenden Sie dann Vollständigkeit, um zu beweisen $⊢ A ∨ ¬A$.

Auf diese Weise verwenden wir ein Argument (Wahrheitstabelle), um eine "semantische" Eigenschaft einer bestimmten Formel zu beweisen, und verwenden dann einen Metasatz (Vollständigkeit), um eine zweite Eigenschaft derselben Formel zu beweisen: das Vorhandensein einer Ableitung in der entsprechendes Beweissystem.