Implication en logique classique
Réponses
-
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.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
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.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
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 ?
-
\bot, \top qui donnent $\bot$, $\top$
-
Merci AD.
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.2K Toutes les catégories
- 9 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 53 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 65 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 69 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 314 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 773 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres