Predicate Logic - Déduction naturelle

Question

L'ensemble des règles d'inférence de la déduction naturelle de Gentzen a-t-il une redondance en ce sens que sans une règle du système, il peut encore être complet?

Mes pensées: je suis tombé sur cette question et je n'ai pas pu former un argument audacieux pour savoir s'il y a redondance dans le système ou non. Notez que spécifiquement, les règles d'inférence de la déduction naturelle de Gentzen incluent$\forall$-intro, $\forall$-elim, $\exists$-intro, $\exists$-elim, $\wedge$-intro, $\wedge$-elim, $\lor$-intro, $\lor$-elim, $\Rightarrow$-intro, $\Rightarrow$-elim, $\neg$-intro, et $\neg$-elim.

Answer 1

Il n'y a pas une telle redondance, et voici une idée comment le prouver.

[EDIT: j'ai reformulé l'argument pour le rendre, espérons-le, plus intuitif.]

Concentrons-nous juste sur le connectif $\land$pour la simplicité. Mettez-vous dans l'esprit de quelqu'un qui ne sait pas ce que l'expression$A\land B$signifie, mais veut le savoir en regardant les règles de déduction naturelle. Une façon de lire les règles d'introduction et d'élimination pour$\land$est qu'ils imposent des limites inférieures et supérieures à la force logique de l'expression$A\land B$. Par exemple,

($\land$-intro) À partir de $A$ et $B$ déduire $A\land B$.

vous dit que $A\land B$est au plus aussi forte que la combinaison de$A$ et $B$, tandis que

($\land$-elim) À partir de $A\land B$ déduire $A$ ou $B$.

vous dit que $A\land B$est au moins aussi fort que les deux$A$ et $B$.

Supposons maintenant que vous omettez la règle ($\land$-intro). Le système résultant ne vous indique aucune limite supérieure sur la force logique de l'expression$A\land B$. Donc intuitivement,$A\land B$pourrait être tout ce qui est au moins aussi fort que$A$ et $B$. Mais alors rien ne t'empêche d'interpréter$A\land B$ dans le système résultant comme l'expression la plus forte possible: une contradiction logique ($\bot$ si cet atome est contenu, ou autrement $p\land\lnot p$ pour une variable fraîche $p$). Notez en particulier qu'en remplaçant$A\land B$ par $\bot$ dans ($\land$-elim), vous obtenez la règle du son

De $\bot$ déduire $A$ ou $B$.

Il s'ensuit que vous ne pouvez rien prouver dans le système qui contredit l'interprétation de$A\land B$comme une contradiction. Par exemple, le théorème$q\rightarrow (q\land q)$ ne sera pas prouvable car $q\rightarrow \bot$ n'est pas valide.

Pour faire de cette intuition un argument formel, considérons une traduction $\pi$ qui remplace toutes les sous-formules $A\land B$ dans une formule par $\bot$. Ensuite, vous pouvez montrer par récurrence sur la longueur de preuve que si une formule$F$ est prouvable en déduction naturelle sans la règle ($\land$-intro), puis $\pi(F)$ est prouvable en déduction naturelle sans ($\land$-intro) ainsi. Il s'ensuit que le théorème$q\rightarrow (q\land q)$ n'est pas prouvable sans ($\land$-intro), comme ce serait alors $\pi(q\rightarrow (q\land q))=q\rightarrow \bot$, ce qui n'est pas valide. D'où la déduction naturelle sans ($\land$-intro) est incomplète.

Un argument similaire peut être trouvé pour l'omission d'autres règles.