Différence de définition
Bonjour.
Soient $E$ et $F$ deux ensembles.
Pour définir le fait que $E$ est inclus dans $F$, je vois souvent deux définitions.
1) $\forall x,\ x\in E\Rightarrow x\in F$.
2) $\forall x\in E,\ x\in F$.
La première me semble la plus pratique à utiliser pour les démonstrations. Mais la deuxième, est-elle rigoureuse ?
Soient $E$ et $F$ deux ensembles.
Pour définir le fait que $E$ est inclus dans $F$, je vois souvent deux définitions.
1) $\forall x,\ x\in E\Rightarrow x\in F$.
2) $\forall x\in E,\ x\in F$.
La première me semble la plus pratique à utiliser pour les démonstrations. Mais la deuxième, est-elle rigoureuse ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Merci X:-(
Ce n'est pas une formule bien formée, impossible d'en prendre la négation (syntaxiquement)
Quand "$\forall x\in E, P(x):= \forall x \left (x\in E \Rightarrow P(x) \right)$" apparaît dans les livres, il est suivi ou précédé de "$\exists y \in F, Q(y):= \exists y \left (y \in F \wedge Q(y) \right )$" et on a bien $\neg \forall z \in G, R(z)$ qui équivaut à $\exists z \left (z \in G, \neg R(z) \right )$.
-- Schnoebelen, Philippe
La notion de formule mal formée ne s'applique guère qu'aux objets formels en question et non à leurs abréviations où tout est possible.
Cette notation se réalise trivialement sur des logiciels qui ont des mécanismes d'abréviation comme COQ.
De plus que veut dire "les règles syntaxiques de la négation?" (comme il doit y avoir environ une définition différente de la syntaxe de la logique du premier ordre par auteur cette expression est ambiguë).
La négation de $\forall x( x \in E \Rightarrow P(x))$ est équivalente à $\exists x (x \in E \wedge \neg P(x))$.
Ces formules s'abrègent habituellement, respectivement en $\forall x \in E, P(x)$ et $\exists x \in E, \neg P(x)$.
Il y a des gens qui écrivent $\neg \forall x( x \in E \Rightarrow P(x)) = \exists x \left (x \in E \Rightarrow \neg P(x)\right )$?
Personnellement je n'ai jamais vu personne faire cette faute.
Le prétendu saccage par ledit programme d'une graphie qui n'apparaît qu'aux yeux du programmeur est un non-problème (qui n'existe pas en fait).
Par contre pour moi :
$non(\forall x\in E,\ x\in F)$ ce serait $\exists x\in E,\ x\notin F$
1) j’accepte les règles qu’on m’a enseigné en L1 (le « quel que soit » se nie en « il existe » et vice versa, la négation de $\in$ est $\notin$ et vice versa)
2) j’imagine que ma proposition est aussi mal formée (?).
Bien formé cela devient $\neg(\forall x (x\in E \Rightarrow x \in F))$ et en appliquant les règles de la négation on obtient $\exists x(x\in E \wedge x\notin F)$ (si on ne se souvient pas de la négation de l'implication, il faut se souvenir que $a\Rightarrow b$ estune abréviatoin légitime pour $\neg a \vee b$
Vous remarquerez que dans vos deux "formules" la virgule n'a pas le même sens (ambigü et même gênant)
-- Schnoebelen, Philippe
Je comprends l'anglais donc l'anglais c'est du français : X:-(
Ce que je ne comprends pas c'est qu'il y ait débat : une formule mal formée est mal formée, point barre.
Non parce que ni l’anglais ni le français ne sont des langages mathématiques.
-- Schnoebelen, Philippe
Je répète, au cas où ... une formule mal formée est mal formée !
Je me réserverais donc au gens sérieux comme Dom, par exemple.
On te dit que non, tu l’as prouvé toi-même en la traduisant correctement.
-- Schnoebelen, Philippe
Si j'ironise c'est face aux sophismes, qui d'ailleurs pourraient être drôles dans un autre contexte ;.la seule chose que j'ai dite et qui semble justifier toutes les "réponses" reçues (comme "les règles de la négation syntaxique sont ambigües") est que cette abréviation est plutôt une mauvaise abréviation (pour des raisons déjà citées) alors que $\Rightarrow$ est plutôt une bonne abréviation.
La question de départ est "est elle rigoureuse", la réponse est non : elle est mal formée
On est bien dans le forum "Logique"
(* 24/09/2021 Ce programme compile avec COQ 8.9*) Section main. Variable Letter:Type. Inductive Formula:Type:= |f_belongs: Letter -> Letter -> Formula |f_not_belongs: Letter -> Letter -> Formula |f_equal: Letter -> Letter -> Formula |f_not_equal: Letter -> Letter -> Formula |f_and: Formula -> Formula -> Formula |f_or: Formula -> Formula -> Formula |f_forall: Letter -> Formula -> Formula |f_exists: Letter -> Formula -> Formula. Fixpoint f_negation (p:Formula){struct p}:Formula:= match p with |f_belongs x y => f_not_belongs x y |f_not_belongs x y => f_belongs x y |f_equal x y => f_not_equal x y |f_not_equal x y => f_equal x y |f_and a b => f_or (f_negation a) (f_negation b) |f_or a b => f_and (f_negation a) (f_negation b) |f_forall t q => f_exists t (f_negation q) |f_exists t q => f_forall t (f_negation q) end. Notation f_implies:= (fun a b:Formula => f_or (f_negation a) b). Notation f_forall_in := (fun (x E:Letter) (g:Formula) => f_forall x (f_implies (f_belongs x E) g)). Notation f_exists_in := (fun (x E:Letter) (g:Formula) => f_exists x (f_and (f_belongs x E) g)). Theorem not_exists_in_is_equal_to_forall_in_not: forall (x E:Letter) (p:Formula), f_negation (f_exists_in x E p) = f_forall_in x E (f_negation p). Proof. simpl. intros; reflexivity. Defined. Theorem not_forall_in_is_equal_to_exists_in_not: forall (x E:Letter) (p:Formula), f_negation (f_forall_in x E p) = f_exists_in x E (f_negation p). Proof. simpl. intros; reflexivity. Defined. Theorem f_negation_involution: forall f:Formula, f_negation (f_negation f) = f. Proof. induction f. simpl; reflexivity. simpl; reflexivity. simpl; reflexivity. simpl; reflexivity. simpl; rewrite IHf1; rewrite IHf2; reflexivity. simpl; rewrite IHf1; rewrite IHf2; reflexivity. simpl; rewrite IHf; reflexivity. simpl; rewrite IHf; reflexivity. Defined. End main.Ce sont les mathématiques qui font COQ, pas le contraire
$\in$ n'appartient pas au langage de la logique (FOL), certes on peut l'ajouter,comme on peut ajouter n'importe quoi, mais est-ce que les démonstrations basées sur une récurrence sur les formules bien formées vont continuer de fonctionner ? Oµu est-ce qu'il faut les refaire toutes (avec leurs idiosyncrasies) ?
Encore une fois la question était "est-ce rigoureux ?", la formule n'étant pas wff la réponse est non.
Oui.
Tu connais le langage de programmation BrainFuck ?
-- Schnoebelen, Philippe
Le monde mathématique est encore infesté de pères fouettards de la rigueur, des gens qui prennent d'autres de haut, soit parce qu'ils fantasment sur ce qu'est une démonstration mathématique faute de formation soit parce qu'ils savent et gardent jalousement pour eux-mêmes les règles d'arbitrage des mathématiques.
Personnellement j'ai commencé à déplacer toute mon activité sur des prouveurs formels. Dans tous les cas ces pseudo rigoristes me font mourir de rire (par contre leur attitude peut-être nuisible pour des lecteurs moins avertis, j'essaie de répondre si je peux). Pour ce qui est de la validation des idées, ce que je sais est ce que je sais faire et COQ a de mon point de vue et dans cette optique PRIORITE ABSOLUE sur les jérémiades des profs de maths aigris d'internet.
Je soutiens à fond la formalisation des mathématiques et le projet QED, ne serait-ce que dans l'espoir que cette engeance disparaîtra pour le bien de tous.
Si vous dites "truc est faux" et que mon compilateur dit "truc", ce sera "truc".
En FOL il y a des signatures pour définir les formules atomiques. Ce symbole est parmi ceux souvent employés. Ne dit-on pas que "la théorie des ensembles est une théorie du premier ordre sur la signature (en l'espèce deux symboles de relation à deux variables)$\in,=$ (ou même simplement $\in$ seul)", et c'est bien ce qui est pratiqué du reste.
De plus le sujet du fil parle de $\in$, de formules avec $\in$, je ne l'ai pas choisi.
Ce qu'il n'y a pas en FOL, c'est de négation d'une formule (par induction). Les exos de taupin "écrivez la négation de la formule blabla" ne sont pas des exercices de logique du premier ordre (mais ils seraient traitable par mon programme sous réserve qu'ils soient écrit sur le langage de la théorie des ensembles basique, et ils le sont en général). En FOL on ne livre pas la signature par paires de symboles pour écrire une telle négation.
La négation de $A$ en FOL c'est juste $\neg A$ ou $\neg (A)$ (voir $A \Rightarrow \perp$ s'il n'y a pas de symbole de négation mais un symbole $\perp$), une formule obtenue en rajoutant à la gauche de $A$ un seul symbole (et éventuellement deux parenthèses).
La négation syntaxique de $\forall x\in E, P$ est donc $\neg \left (\forall x\in E, P \right )$. On ne peut pas en faire grand chose ici. D'où ma question "que veut dire la négation syntaxique d'une formule" afin d'avoir un réponse tranchée. Bon en guise de réponse j'ai eu des sarcasmes. OK.
Merci de confirmer ce que je dis depuis le début!
Quand je pense que j'ai eu la faiblesse de vous croire sincère dans votre message d'il y a1 heure, je regrette
Qui croire? (:P)
(Bonus: la négation de ceci serait, selon Lean, $\neg \forall (x : A), x \in E \to x \in E : \mathrm{Prop}$)
PS: D'ailleurs, Foys, je crois que les leaneux sont en recherche constante de gens qui formalisent des théorèmes, ça pourrait t'intéresser.
PPS: À ne pas prendre trop au sérieux, j'avais juste envie de jeter de l'huile sur le feu.
Je pense que Lean a raison!!
C'est bien formé en Lean !
Je ne comprends pas votre négation en Lean,
Pour la négation, mon IDE rend exactement ce que j'ai écrit (bon, il le rend en unicode, mais ça ne passe pas sur le forum), mais c'est probablement du sucre syntaxique, où des parenthésages ont été dégagés pour faciliter la lecture (il faudrait voir l'ordre de précédence de la notation $\neg$ par rapport aux autres symboles).
Il me semble que la négation d'un objet $a$ de type Prop en lean est en fait $a \to \mathrm{false}$. En tout cas, c'est ce qu'indique https://leanprover-community.github.io/mathlib_docs/init/core.html#not. (Edit: c'est bien la définition de la négation, ligne 85 de https://github.com/leanprover-community/lean/blob/a0fb1e8c7ac81dfd2e80ad0de08f4e57ee853d82/library/init/core.lean#L85).
Si j'ai bien compris la négation, dans Lean, de ( ................) est \neg ( ................), c'est pas faux :-D