Abzugssatz - Interpretation
In dem Buch "Eine Tour durch die mathematische Logik" von Robert S. Wolf wird der Abzugssatz wie folgt spezifiziert:
Wenn T. $\cup$ {P} $\vdash$ Q, dann T. $\vdash$ (P. $\to$ Q)
Wobei T eine Theorie erster Ordnung ist und P & Q einige Formeln in der Sprache dieser Theorie erster Ordnung sind. Ist dann die folgende Interpretation des Abzugssatzes richtig?
Wenn Q von T ableitbar / nachweisbar ist $\cup$ {P}, dann kann man sagen, dass - wenn P von T ableitbar ist (dh P ist ein Satz von T), Q auch von T ableitbar ist.
Erfasst diese Interpretation auch die Essenz des Deduktionssatzes?
PS: Eine andere Frage mit dem Titel Deduktionssatz - Intuition scheint sich hauptsächlich auf die syntaktischen Aspekte des Satzes und der Prädikatenrechnung im Allgemeinen zu konzentrieren - und nicht auf seine Semantik.
Antworten
Ist die folgende Interpretation des Abzugssatzes richtig?
Was du schreibst ist
Wenn $T \cup \{P\} \vdash Q$, dann wenn $T \vdash P$, dann $T \vdash Q$.
Dies ist das gleiche wie zu sagen
(1) Wenn $T \cup \{P\} \vdash Q$, dann $T \nvdash P$ oder $T \vdash Q$.
Dies ist aber nicht gleichbedeutend mit
(2) Wenn $T \cup \{P\} \vdash Q$, dann $T \vdash P \to Q$.
Es kann sein, dass $P$ ist nicht nachweisbar, aber $P \to Q$ist auch nicht. Dann "$T \nvdash P$ oder $T \vdash Q$"hält, aber"$T \vdash P \to Q$"nicht. Also (1) $\not \Rightarrow$ (2).
Dies ist, was in den Kommentaren mit "Trivialisierung" gemeint ist: "wenn $T \vdash P$ dann $T \vdash Q$"(= was du geschrieben hast) wird trivial wahr, wenn $T \nvdash P$dh wenn $P$ist nicht beweisbar. Aber "$T \vdash P \to Q$"(= was der Abzugssatz besagt) nicht: Nur weil wir nicht beweisen können $P$ heißt nicht, dass wir beweisen können $P\to Q$- wie du beobachtet hast. Daher warum "$T \vdash P \to Q$"ist eine stärkere Behauptung, dass" If $T \vdash P$ dann $T \vdash Q$".
Das Wesentliche des Abzugssatzes ist, dass Sie zwischen einem Satz, der von einer offenen Annahme abhängt, und dem Nachweis einer bedingten Aussage "Flip-Flop" machen können:
Wenn es einen Beweis dafür gibt$Q$ was immer noch von der Annahme abhängt $P$, dann wird es einen Beweis in der Theorie der Aussage geben $P \to Q$. Dies ist die unmittelbare Wirkung der bedingten Proof- Technik (siehe S. 14).
Und für die umgekehrte Richtung des Abzugssatzes, wenn Sie beweisen können$P \to Q$, dann können Sie beweisen $Q$ unter der Annahme, dass $P$. Dies ist eine Folge der Inferenzregel des Modus ponens (siehe S. 13).
Die beiden Richtungen zusammen, der Abzugssatz rechtfertigt einfach, was wir mit einem Beweis von "$\to$".
Sie weisen zu Recht darauf hin, dass der zentrale Begriff eines formalen Systems eher der Beweis als die Wahrheit ist. Denken Sie jedoch daran, dass wir normalerweise daran interessiert sind, ein "nützliches" Beweissystem zu entwerfen, das dem Begriff der Wahrheit "entspricht": Eine Aussage sollte in einer Theorie genau dann beweisbar sein, wenn sie in allen Modellen der Theorie wahr ist . Schließlich geht es bei einem Beweissystem darum, ein mechanisches Gerät zu haben, um Aussagen, die wir für wahr halten, rigoros zu beweisen. Also während die Vorstellung eines Beweises von$\to$ wird in Form von Inferenzregeln formuliert, die Art und Weise, wie diese Regeln verwendet werden, spiegelt die Wahrheitstabelle für wider $\to$: Ein Beweissystem sollte (und was das in Wolfs Buch vorgestellte Beweissystem betrifft ) in Bezug auf die Semantik solide sein: Was bewiesen werden kann, ist in allen Strukturen wahr (gemäß den Definitionen der Wahrheitstabelle); Das System beweist (hoffentlich) keinen zufälligen Unsinn.