Théorème de déduction - Interprétation
Dans le livre "Un tour à travers la logique mathématique" - de Robert S. Wolf, le théorème de déduction est spécifié comme suit:
Si T $\cup$ {P} $\vdash$ Q, puis T $\vdash$ (P $\to$ Q)
Où T est une théorie du premier ordre et P & Q sont des formules, dans le langage de cette théorie du premier ordre. Alors, l'interprétation suivante du théorème de déduction est-elle correcte?
Si Q est dérivable / prouvable de T $\cup$ {P}, alors on peut dire que - si P est dérivable de T (c'est-à-dire que P est un théorème de T) alors Q est également dérivable de T.
De plus, cette interprétation capture-t-elle l'essence du théorème de déduction?
PS: une autre question intitulée Théorème de la déduction - Intuition , semble se concentrer principalement sur les aspects syntaxiques du théorème et du calcul des prédicats en général - plutôt que sur sa sémantique.
Réponses
L'interprétation suivante, du théorème de déduction, est-elle correcte?
Non, ce que vous écrivez est
Si $T \cup \{P\} \vdash Q$, puis si $T \vdash P$, puis $T \vdash Q$.
C'est la même chose que de dire
(1) Si $T \cup \{P\} \vdash Q$, puis $T \nvdash P$ ou $T \vdash Q$.
Mais ce n'est pas équivalent à
(2) Si $T \cup \{P\} \vdash Q$, puis $T \vdash P \to Q$.
Il se peut que $P$ n'est pas prouvable, mais $P \to Q$n'est pas non plus. Ensuite "$T \nvdash P$ ou $T \vdash Q$"tient, mais"$T \vdash P \to Q$"pas. Donc (1) $\not \Rightarrow$ (2).
C'est ce que l'on entend dans les commentaires par "banalisation": "si $T \vdash P$ puis $T \vdash Q$"(= ce que vous avez écrit) devient trivialement vrai si $T \nvdash P$, ie si $P$est indémontrable. Mais "$T \vdash P \to Q$"(= ce que dit le théorème de déduction) ne fait pas: simplement parce que nous ne pouvons pas prouver $P$ ne veut pas dire que nous pouvons prouver $P\to Q$- comme vous l'avez observé. D'où pourquoi "$T \vdash P \to Q$"est une affirmation plus forte que" Si $T \vdash P$ puis $T \vdash Q$".
L'essence du théorème de déduction est que vous pouvez "basculer" entre avoir un théorème dépendant d'une hypothèse ouverte et prouver une déclaration conditionnelle:
s'il existe une preuve de$Q$ qui dépend toujours de l'hypothèse $P$, alors il y aura une preuve dans la théorie de l'énoncé $P \to Q$. C'est l'effet immédiat de la technique de preuve conditionnelle (voir p. 14).
Et pour le sens inverse du théorème de déduction, si vous pouvez prouver$P \to Q$alors tu pourras prouver $Q$ sous l'hypothèse que $P$. C'est une conséquence de la règle d'inférence modus ponens (voir p. 13).
Les deux directions combinées, le théorème de déduction justifie simplement ce que nous entendons par une preuve de "$\to$".
Vous avez tout à fait raison de souligner que la notion centrale d'un système formel est celle de la preuve plutôt que de la vérité. Mais gardez à l'esprit que nous sommes normalement intéressés par la conception d'un système de preuve «utile» qui est «en ligne» avec la notion de vérité: une affirmation doit être prouvable dans une théorie exactement quand elle est vraie dans tous les modèles de la théorie . Après tout, le but d'un système de preuve est d'avoir un dispositif mécanique pour prouver rigoureusement les déclarations que nous considérons vraies. Alors que la notion de preuve de$\to$ est formulé en termes de règles d'inférence, la manière dont ces règles sont utilisées reflète la table de vérité pour $\to$: Un système de preuve devrait être (et comme pour le système de preuve présenté dans le livre de Wolf, est) sain avec la sémantique: Ce qui peut être prouvé est vrai (selon les définitions de la table de vérité) dans toutes les structures; le système (espérons-le) ne prouve pas de non-sens aléatoire.