Il manque quelque chose dans une simple dérivation de la règle de double négation via la règle d'introduction de négation

Nov 19 2020

Je cite l'entrée de Shapiro sur la logique classique (en SEP) où (As) se réfère à une "règle des hypothèses":

(As) Si ϕ est membre de Γ, alors Γ⊢ϕ.

Nos clauses suivantes sont pour le signe de négation, «¬». L'idée sous-jacente est qu'une phrase ψ est incompatible avec sa négation ¬ψ. Ils ne peuvent pas être tous les deux vrais. Nous appelons une paire de phrases ψ, ¬ψ opposées contradictoires. Si l'on peut déduire un tel couple d'une hypothèse θ, alors on peut conclure que θ est faux, ou, en d'autres termes, on peut conclure ¬θ

(¬I) Si Γ1, θ⊢ψ et Γ2, θ⊢¬ψ, alors Γ1, Γ2⊢¬θ

Par (As), nous avons que {A, ¬A} ⊢A et {A, ¬A} ⊢¬A. Donc par ¬I nous avons cela {A} ⊢¬¬A . Cependant, nous n'avons pas encore l'inverse. Intuitivement, ¬¬θ correspond à «ce n'est pas le cas que ce n'est pas le cas que». On pourrait penser que ce dernier équivaut à θ, et nous avons une règle à cet effet ...

Je vois facilement comment les deux $A$ et $\neg A$ sont dérivables par la règle (As) de l'ensemble $\{A, \neg A\}$ , mais je ne vois pas comment il en découle que $\{A\}⊢¬¬A$.

Autrement dit, je ne comprends pas de quelle manière $\{A\}$ joue le rôle de l'union d'ensemble $\Gamma_1, \Gamma_2$dans l'énoncé de la règle juste avant. Je ne comprends même pas ce qui joue le rôle de$\Gamma_1$, ni de $ \Gamma_2$, ni de $ \theta$.

Quelles substitutions faut-il faire pour reconnaître clairement dans cette preuve une instanciation de la règle d'introduction de la négation?

Réponses

1 GrahamKemp Nov 19 2020 at 09:46

Vous cherchez à avoir $\{A\}$être l'union de deux ensembles. Au moins un doit être$\{A\}$, l'autre peut être $\{A\}$ ou alors $\{\}$.

Vous cherchez à dériver $A$ de $\neg A$ et l'un des ensembles ci-dessus (appelez-le $\Gamma_1$). Depuis,$A$ ne peut pas dériver de $\neg A$ et le vide, mais est dérivé trivialement de $\{A\}$, le dernier est ce que sera cet ensemble.$$\{A\}, \neg A\vdash A$$

Vous cherchez également à dériver $\neg A$ de $\neg A$ et l'autre des ensembles ci-dessus (appelez-le $\Gamma_2$); et comme$\{A\}$ ou alors $\{\}$ fonctionne ... nous pouvons utiliser l'un ou l'autre.$$\{\},\neg A\vdash\neg A$$

Alors on y va $$\begin{split}\Gamma_1,\theta&\vdash \varphi\\\Gamma_2,\theta&\vdash \neg \varphi\\\hline \Gamma_1,\Gamma_2&\vdash \neg\theta\end{split}\qquad\begin{split}A,\neg A&\vdash A\\\neg A&\vdash \neg A\\\hline A&\vdash \neg\neg A\end{split}$$