Implikation Einleitung als Theorem formuliert?

Die zwei verschiedenen Symbole auf der Seite, auf die Sie verlinken, sind tatsächlich unterschiedlich. Das erste ist das Drehkreuzsymbol Ⱶ, das als „beweist“ gelesen werden kann, während der Pfeil → eine materielle Implikation ist. Diese sind sehr unterschiedlich. Materielle Implikation ist ein Symbol in der Objektsprache, das durch die von Ihnen angegebene Wahrheitstabelle definiert ist, dh T/F/T/T. Turnstile ist ein Symbol in der Metasprache, das gelesen werden kann als P beweist Q oder Q ist ein Theorem über P.

Die Regel der bedingten Einführung kann so verstanden werden, dass wenn Q ein Satz über P ist, dann ist P → Q ein Satz. Allgemeiner könnte man es so schreiben: Wenn Γ eine Menge von Aussagen ist, dann kann man aus Γ,P Ⱶ Q Γ Ⱶ P → Q ableiten. Wenn Γ zusammen mit P Q beweist, dann beweist Γ, dass P materiell impliziert F. Das nennt man das Deduktionstheorem.

In der natürlichen Deduktion können wir die Regel des bedingten Beweises mit dem gleichen Effekt anwenden. Sie können ein beliebiges P annehmen, Q daraus beweisen und dann die Annahme aufheben, um die materielle Implikation P → Q einzuführen.

Was logische Konstanten mit entsprechenden Einführungs- und Eliminierungsregeln betrifft, so ist dies kein Zufall. Im Fitch-System werden die logischen Konstanten durch diese Regeln spezifiziert. Die Idee harmonischer Einführungs- und Eliminierungsregeln wurde von Gerhard Gentzen eingeführt und von verschiedenen anderen aufgegriffen. Die Idee dahinter ist, dass die entsprechenden I- und E-Regeln „umgekehrt“ zueinander sein sollten, um sicherzustellen, dass sie keine widerspenstigen Konsequenzen haben. In einem berühmten Artikel aus dem Jahr 1960 zeigte Arthur Prior ("The Runabout Inference Ticket" Analysis 21: 38-9), dass die Definition logischer Konstanten ohne Einschränkungen es Ihnen ermöglichen könnte, alles zu beweisen.

Diese umgekehrte Beziehung zwischen den I- und E-Regeln wird als logische Harmonie bezeichnet. Michael Dummett argumentierte, dass die klassische Logik keine harmonische Möglichkeit hat, die Regeln für die Negation zu definieren, während dies in der intuitionistischen Logik der Fall ist, obwohl dies umstritten ist. Wenn Sie weitere Informationen über logische Harmonie haben möchten, könnten diese Papiere nützlich sein:

Steinberger, F. (2011) „Was Harmonie sein könnte und was nicht“. Australasian Journal of Philosophy 89: 617-639. Rumfitt, Ian (2016) „Gegen die Harmonie“. Demnächst in Robert Hale, Crispin Wright und Alexander Miller, Hrsg., The Blackwell Companion to the Philosophy of Language, 2. Auflage. Oxford: Blackwell.

Ich glaube, beide Artikel sind auf philpapers.org zu finden.

Was man sich als Implikationseinführung →I vorstellen könnte , wird manchmal als bedingter Beweis oder CP bezeichnet .

Die grundlegende Strategie besteht darin, den Antezedens anzunehmen und die Konsequenz abzuleiten. Sobald die Konsequenz hergeleitet ist, kann die Annahme entladen werden. Hier ist ein Beispiel:

{1} 1. (P ∨ Q) → R Prem.
{2} 2. P Angenommen.
{2} 3. P ∨ Q 2 ∨ I (rechts)
{1,2} 4. R 1,3 MP
{1} 5. P → R 2,4 LP

In Zeile 2 wird der Vordersatz angenommen, in Zeile 4 der Nachsatz abgeleitet. Damit sind die Bedingungen für → Einleitung oder CP in Zeile 5 erfüllt.

Bei diesem besonderen Nachweissystem sind die Abhängigkeitsnummern links aufgeführt. Überall dort, wo die Zahl {2} erscheint, bedeutet dies, dass die entsprechende Zeilennummer von der Annahme in Zeile 2 abhängt. Beachten Sie, dass die Abhängigkeitsnummer für die Annahme gelöscht wird, sobald die Implikation eingeführt wurde. Sie können sehen, dass die Schlussfolgerung nur auf {1} basiert , was die Prämisse ist.

Das andere Symbol:

Der Wikipedia-Artikel lautet:

Die Modus-Ponens-Regel kann in fortlaufender Notation geschrieben werden:

P → Q, P ⊢ Q

wobei ⊢ ein metalogisches Symbol ist, was bedeutet, dass Q eine syntaktische Folge von P → Q und P in einem logischen System ist;

Das andere Symbol ist ein Drehkreuz und funktioniert analog zum Implikationssymbol, aber es gehört zu einem separaten System der Logik oder Metalogik . Das Drehkreuz zeigt an, dass ein angezeigtes Argument stichhaltig ist, und da es wie eine Implikation funktioniert, können alle Prämissen eines Arguments zusammen mit der Schlussfolgerung unter Verwendung der normalen logischen Notation umgeschrieben werden, um eine Tautologie zu bilden.

Wie ich in meinem Kommentar erwähnt habe, ist die durch ((A & (A → B)) → B) ausgedrückte Beziehung das Prinzip, das sowohl die Einführung als auch die Eliminierung regelt, sodass für beide dieselbe Wahrheitstabelle gilt.