Implication en logique classique

marco · November 2021

Bonjour,

Comment montre-t-on $\mathrm{non}(\forall x, P(x)) \implies \exists x , \mathrm{non} P(x)$ en logique classique ? Car il me semble que c'est faux en logique intuitioniste ?

Est-ce qu'en logique intuitionniste $\mathrm{non}( A)$ est par définition $A \implies \mathrm{Faux}$ ?

Merci d'avance.

Foys · November 2021

La réponse va fortement dépendre du système d'axiomes utilisé (même en logique classique il y a plusieurs jeux d'axiomes différents quoiqu'équivalents). En logique intuitionniste on peut prendre un espace topologique et interpréter les phrases comme des ouverts avec les conventions suivantes:

$A \wedge B:= A \cap B$

$A \vee B := A \cup B$

$\perp := \emptyset$

$A \Rightarrow B := \text{intérieur de } A^c \cup B$

$\neg A := A \Rightarrow \perp:= \text{intérieur du complémentaire de } A$

$\exists x F(x):= \bigcup_x F(x)$

$\forall x F(x):= \text{intérieur de } \bigcap_x F(x)$.

Lorsque la topologie de l'espace est discrète, le passage à l'intérieur ne fait plus rien et on retrouve une interprétation ensembliste de la logique classique dans l'algèbre de Boole des parties d'un ensemble.

Les théorèmes de logique intuitionniste (sans axiome supplémentaire) sont les formules égales à l'espace tout entier (et d'autre part $ X\Rightarrow Y$ est égal à tout l'espace si et seulement si $X\subseteq Y$), ce qui n'est pas le cas de $\neg (\forall x P(x)) \Rightarrow \exists x \neg P(x)$

Pour la deuxième question, cela dépend des auteurs (dans COQ c'est le cas) mais ces énoncés sont toujours équivalents.

Foys · November 2021

Le théorème suivant est intuitionniste et se démontre avec COQ:

$\left [\neg \left ( \forall x \neg \neg P(x)\right )\right ] \Rightarrow \neg \neg \exists x \neg P(x)$

(*Ce code compile avec coq 8.9*)

Theorem pas_tous_P_un_non_P: forall (T:Type) (P:T ->Prop),
    ~(forall x:T, ~ ~ P x) -> ~ ~ exists x:T, ~ P x.
Proof.
  intros T P hyp1.
  intro hyp2.
  apply hyp1.
  intro w.
  intro hyp3.
  apply hyp2.
  apply ex_intro with (x:=w).
  apply hyp3.
Defined.

(*
Print pas_tous_P_un_non_P.
--->
pas_tous_P_un_non_P = 
fun (T : Type) (P : T -> Prop) (hyp1 : ~ (forall x : T, ~ ~ P x))
  (hyp2 : ~ (exists x : T, ~ P x)) =>
hyp1 (fun (w : T) (hyp3 : ~ P w) => hyp2 (ex_intro (fun x : T => ~ P x) w hyp3))
     : forall (T : Type) (P : T -> Prop),
       ~ (forall x : T, ~ ~ P x) -> ~ ~ (exists x : T, ~ P x)
*)

On a toujours des résultats intuitionnistes, classiquement équivalents à des résultats classiques via des ajouts de double négations dans ce genre. Chercher sur le web les traductions de Kuroda ou de Godel-Gentzen pour plus de précisions.

marco · November 2021

Merci Foys.

En logique classique, est-ce que pour montrer $(\neg \forall x,P(x)) \implies \exists x, \neg P(x)$, on ne raisonne pas par contraposée ? On suppose $\neg \exists x, \neg P(x)$. Ainsi que $\neg P(y)$ ($y$ variable libre). Alors $\exists y, \neg P(y)$. Donc contradiction. Donc $\neg P(y) \implies \mathrm{Faux}$. Donc $P(y)$. Comme $y$ est libre, $\forall y,P(y)$. Donc $\neg \exists x, \neg P(x) \implies \forall x,P(x)$ ce qui est la contraposée.

En logique intuitionniste, si on interprète les énoncés comme des ouverts de $[0,1]$, on choisit $P(n)=[0,\frac{1}{n}[$, alors $\forall n,P(n)=\emptyset$ et $\neg \forall n,P(n)=[0,1]$. Mais $\neg P(n)=]\frac{1}{n},1]$, et $\exists n, \neg P(n)=]0,1]\neq[0,1]$.

Comment fait-on le $T$ à l'endroit pour Vrai et le $T$ à l'envers pour Faux en Latex ?