Présenter de manière correcte
Bonjour. Lorsque que l'on a une proposition $P(x)$ qui dépend par exemple de $x\in \R$, si l'on veut l'utiliser dans une implication, il faut la quantifier. Mais lorsque l'on résout des systèmes, des équations ou des inéquations, on voit souvent un signe $\Leftrightarrow$ entre les étapes, surtout pour les systèmes. Est-on d'accord que c'est incorrect?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
$$(x-2)^2=x^2 \Leftrightarrow x=1$$
est elle une écriture incorrecte ?
Est-ce que la formule ci-dessus est correctement écrite ? À mon avis, oui.
Est-il correct de dire que la formule est un théorème disons, de la théorie des corps de caractéristique $0$ ? À mon avis, oui (sauf si on insiste dans la définition de théorème pour dire que c'est obligatoirement une formule close).
Pour autant, dès que tu as une formule $P$ et une formule $Q$, tu peux former $P\iff Q$. Ce n'est pas pour autant qu'elle sera vraie, ou prouvable, mais tu as toujours le droit de l'écrire. Non ?
Il faut aussi savoir que $\forall x, (P(x)\iff Q(x))$ n'est pas équivalent à $(\forall x, P(x)) \iff (\forall x, Q(x))$
Si on reprend l'exemple de GBZM, on a bien $(x-2)^2 = x^2 \iff x=1$. Il s'avère que c'est vrai quel que soit $x$ réel, donc tu pourrais rajouter un "$\forall x\in \R$" devant, mais tu imagines bien que si quelque chose est vrai pour tout réel, c'est en particulier vrai pour le réel $x$
(... quel qu'il soit :-D )
Je dis ça parce qu'il a évoqué "les systèmes".
Et dans ce contexte très précis, c'est effectivement une bien méchante entourloupe. Après, il n'y a pas tellement de solutions pédagogiques.
Exemple: tout le monde "voit bien" que je passe de $$
x+y=5 ; \ x+3y = 10
$$ à $$
x+y=5 ; \ 2y = 10 -5
$$ par un donc acceptable, et comme le contexte linéaire fait que les profs de L1,L2 (voire lycée) savent qu'un car aurait été légitime, ils l'acceptent dans les copies.
Soient $x$, $y$ et $z$ des nombres réels. On a
$$ \begin{cases} x+y+z = 0 \\ x+2y+3z=0 \\ x+5y+7z = 0\end{cases} \Longleftrightarrow \cdots \Longleftrightarrow \begin{cases} x= 0 \\ y=0 \\ z=0 \end{cases}$$
donc le système $S$ admet une unique solution $(0,0,0)$.
> GaBuZoMeu : ça ne change pas ma conclusion, il faut à un moment ou un autre dire que $x$
> appartient à un corps de caractéristique 0.
Dans le langage de la théorie des groupes, les variables se promène dans le groupe. Dans le langage des corps, les variables se promènent dans le corps, etc.
D'accord, tu n'es pas logicien. Mais alors au nom de quoi as-tu un avis aussi tranché sur la question ?
$$\forall x\ \Big( (x-2)^2= x^2 \iff x=1 \Big)$$
si on ne précise pas plus les choses, puisque ça peut être faux ou être vrai (ou même indécidable peut-être ?).
Je ne dis pas que la formule en elle-même est incorrecte, mais que quand on veut résoudre des systèmes, des équations, en pratique il faut bien préciser où on cherche les éventuelles solutions!
J'ai l'impression (peut-être que je me trompe), que la question de Boole et Bill était une question plutôt de mathématiques dans la pratique, comment présenter une résolution de système ou d'équation. D'où ma réponse de non logicien mais de mathématicien/prof.
Si on veut écrire correctement les choses, elles doivent être quantifiées. Mais c'est SI on veut les écrire correctement (par exemple, pour présenter une preuve irréfutable qu'un système mécanique pourra être produit en usine sans risque que les avions qui l'incluront se crashent).
Il n'y a pas de "police" qui fait la chasse aux abus de langage ou aux non-maths. Il ne doit donc pas y avoir non plus de gens qui, tout en écrivant incorrectement les choses d'un point de vue mathématique, les revendiquent comme mathématiques.
La PLUPART des choses sont écrites de manière incorrecte pour de simples raisons de PLACE et disgestibilité. Elles ne sont donc pas mathématiquement correcte. Mais les auteurs n'ont pas à s'inquiéter de voir critiquer leur "vertus". L'important n'est pas là, l'important est à quel public on s'adresse. A des pros, les raccourcis et abus de langage sont généralement un cadeau à leur faire, puisque leur fait gagner temps et zenitude.
Ce qui est dramatique, c'est de le faire à des non pros. Autrement dit, la société a eu tendance à inverser les choses, en prétendant qu'il était "dommage" d'abuser" devant des pros et mieux d'abuser devant les enfants.
C'est très EXACTEMENT l'opposé qui devrait être la pratique courante: il est important qu'un élève NE COMPRENNE PAS***, afin d'y revenir, de pouvoir poser des questions, etc, bref, de ne pas se construire des délires astrologico-superstitieux (surtout par les temps de radicalisation un peu gratuite chez les ados qui courent)
Alors que quand un pro ne comprend pas à cause d'une écriture trop correcte, il demandera, exigera des polices plus petites pour certains signes, bref, le pro sait ce qu'il va chercher et où ça se trouve. Pas l'enfant.
Dans le cas des réactions de systèmes (puisque comme je m'en doutais, il s'agit bien de ça, je n'ai pas de réponse sociologique prête à l'emploi. Pour ma part, je ne "reconnais" pas le signe équivalent, donne peu de systèmes à résoudre, et les choisis souvent de déterminant nul, voire non carrés.
Je laisse ensuite les gens s'apercevoir qu'il ont prouvé une inclusion et non une égalité et c'est pas bien grave.
Après je n'enseigne pas dans des BTS ou autres écoles où on fait gros usage de résolutions affines et programmation linéaire non plus. Je plains les gens qui font ça, sans avoir placer ça dans le cadre des matrices (qui font partir comme foys le remarque, la plupart des variables liées, et signes logiques).
[small]*** mon éternel exemple: il vaut mieux exposer au CE2 que
$$\forall a,b: a\times b=b\times a$$
et recevoir des réactions et questions multiples, que d'afficher au tableau
$$ a\times b=b\times a $$
et s'auto-congratuler dans une mièvrerie EN typique des applaudissements et de "j'ai compris" de la classe quand on fait le récit de son héroisme au repas du midi devant les autres instits à la cantine des adultes.[/small]
Tant que le personnel scolaire n'aura pas compris ça, aucune chance de voir les choses s'améliorer. Les abus de langage AIDENT LES PROS! Pas les débutants
Christophe mélange des arguments d'autorité pour décider ce qui est mathématiquement correct ou pas, et des arguments pédagogiques avec l'habituel lot de condescendance pour ceux et celles qui n'ont rien compris.
Héhéhé, Boole et Bill a posté dans le forum "Logique et Fondements".
J’essaye de comprendre.
« Mais une théorie est écrite dans un langage. »
Les termes « théorie » et « langage » sont déjà des termes mathématiques précis et il ne faut pas confondre avec les mots du français courant. J’ai vu ça il y a presque 20 ans alors je suis rouillé et même complètement grippé.
« $(x-2)^2=x^2 \iff x=1$ est une formule du langage des corps (ou des anneaux), et elle est prouvable dans la théorie des corps de caractéristique 0. »
C’est cette histoire de « formule du langage des corps » que je souhaite comprendre quant au débat. La discussion est « faut-il présenter les lettres ou pas ? » si je ne me trompe.
Question : est-ce que je me trompe si je dis « comme on est dans le langage des corps, alors les lettres sont nécessairement des éléments d’un corps ? ». En effet, c’est comme ça que je comprends « formule du langage des corps ».
Merci de m’éclairer.
Cordialement
Dom
Vu le contexte, j'ai préféré essayer d'aider B&B dans sa demande en suggérant une interprétation de sa question pour que les experts qui lui répondent puissent envisager cette aspect. Je ne vais pas me lancer dans un cours de logique pour ce fil de B&B.
@dom: c'est beaucoup plus simple que ça. Les lettres sont des lettres. Un variable libre est le nom propre de quelque chose quand le cerveau humain la lit.
Dans le contexte de GBZM, lesdites n'ont pas reçu d'affectation de valeur, même cachée, car jouent un rôle proche d'indéterminée dans les polynômes. Là, oui à la rigueur on rejoindrait les points sulfureux de désaccord entre GBZM et moi (mais qui sont pas du tout graves et HS ici).
Mais pour être précis, tu peux les voir comme des fonctions (comme quand on écrit $(x,y)$ à la place de $(x_A,y_A)$) qui vont, une fois appliquées associer leurs valeurs aux lettres.
Le point important n'est pas là. Le point important était que pour certaines phrases, quelle que soit l'affectation de valeurs d'un corps de caractéristique 0, la phrase acquièrera la valeur vraie. Attention, il te faut bien aussi comprendre, qu'il n'y a pas que les lettres, mais les signes aussi qui ont le même statut ici. A correctement parler, on devrait écrire:
$$ x \times_K x = 0 \iff x=0_K$$ voire même, puristement:
$$ x_K \times_K x_K = 0 \iff x_K=0_K$$
Mais je ne crois pas que ce soit le sujet du fil. La fonction $x$ est une fonction choix (elle associe à $K$ un de ses éléments), mais la fonction $\times$ est bien connue, elle associe à un corps sa multiplication). Et j'ai utilisé la notation $f_u$ à la place de $f(u)$.
Une formule et les symboles qui y figurent (variables, symboles de fonction, symboles de relation) ne dépendent pas des structures dans lesquelles on les interprète.
Mais en pratique, le fait que cette formule soit vraie, fausse, indécidable, absurde, etc. dépend de la structure!
Je ne comprends donc pas bien, en tant que non logicien, quel est l'intérêt en pratique de considérer la formule $(x-2)^2 = x^2 \iff x=1$ sans préciser aucun contexte. Que peut-on en faire ?
Là, tu mélanges des choses.
Vrai ou faux c'est de la sémantique et ça fait intervenir une structure où on interprète la formule.
Indécidable, c'est syntaxique : on ne peut démontrer ni l'énoncé, ni la négation de l'énoncé.
Mais peut-être ne fais-tu pas de différence entre structure et théorie ?
Il y a effectivement quelque chose qui m'échappe...
Quand tu dis "on peut la démontrer (dans la théorie des corps de caractéristique zéro)" tu es justement en train de mettre un "contexte". J'ai l'impression (je dois me tromper) que ça revient à quantifier...
Je ne vois pas la différence profonde entre dire: "la formule $(x-2)^2=x^2 \iff x=1$ est démontrée dans la théorie des corps de caractéristique zéro" et dire "soit $K$ un corps de caractéristique 0. Alors $\forall x \in K,\ \big( (x-2)^2=x^2 \iff x=1 \big)$".
http://www.les-mathematiques.net/phorum/read.php?16,1982350,1983232#msg-1983232
je répondais à dom sur un statut sémantique, voire philosophique des lettres et symboles. J'ai bien compris que tu souhaites aussi afficher l'importance de la syntaxe, mais j'essaie de m'adapter à la demande.
Du reste la syntaxe est tout de même "au service" de la certitude recherchée pour les réponses mathématiques. On écrit des démonstrations pour prouver des choses.
je crois (et peux me tromper) que dom attend un "lien" entre syntaxe est sémantique plus qu'une explicitation des règles de correction syntaxiques.
> Je ne vois pas la différence profonde entre dire:
> "la formule $(x-2)^2=x^2 \iff x=1$ est démontrée
> dans la théorie des corps de caractéristique
> zéro" et dire "soit $K$ un corps de
> caractéristique 0. Alors $\forall x \in K,\ \big( (x-2)^2=x^2 \iff x=1 \big)$".
La quantification n'est pas essentielle ici : démontrer $(x-2)^2=x^2 \iff x=1$ ou démontrer $\forall x\quad((x-2)^2=x^2 \iff x=1)$, c'est pareil.
Ceci dit :
démontrable entraîne vrai dans tous les modèles : c'est que le système de déduction est correct.
vrai dans tous les modèles entraîne démontrable ; c'est que le système de déduction est complet (théorème de complétude de Gödel).
Version (1). Il faut toujours quantifier. Il faut toujours Kant-ifier. Il faut toujours mettre des impératifs catégoriques, dans tout et n'importe quoi. Même dans un sandwich crabe mayonnaise.
Version (2). Il vaut mieux savoir ce que l'on est en train de faire, et savoir pourquoi on est en train de le faire. C'est ainsi que $$(x-2)^2=x^2 \Leftrightarrow x=1$$ est une formule de bon aloi dans la théorie des corps de caractéristique $0$, mais pas dans la théorie des sandwichs crabe-mayonnaise sur un corps de caractéristique $2$.
En résumé: si on cause des nombres zentiers, cela ne s'applique pas forcément aux propriétés flottatoires des éléphants de mer. Petits zenfants, prenez-en bonne note sur votre tablette confinée: c'était votre ration de logique du jour.
Cordialement, Pierre.
Chaque mot ayant son importance et je n’ai pas le dictionnaire dans ma tête.
Je vais tenter de lire mais aussi il faudrait que je me documente.
J'ai l'impression qu'on "cache" la quantification en se plaçant dans un contexte donné (désolé j'emploie le terme flou de contexte pour ne pas dire de bêtise).
C'est un peu comme dire: dans le contexte des nombres réels positifs, on démontre $x^2 \geq 0 \iff x \geq 0$. Je ne vois pas bien la différence avec écrire $\forall x \in \R_+,\ x^2 \geq 0 \iff x \geq 0$. J'ai vraiment l'impression qu'on cache la quantification en se plaçant dans un contexte qui finalement quantifie $x$.
Toute explication supplémentaire est la bienvenue
Lorsqu'on travaille avec des types, chaque lettre du contexte est accompagnée de son type.
Lorsque $\mathcal C$ est un contexte, $y$ est une lettre (que l'on décrète d'un certain type $T$) n'appartenant pas à $\mathcal C$, $F_1,...,F_n$ des énoncés écrits dans le contexte $\mathcal C$ (donc sans $y$), et $G$ un énoncé du contexte $\mathcal C \cup \{(y:T)\}$ ($y$ peut donc figurer ou non dans $G$):
si on peut démontrer l'énoncé $(F_1\wedge F_2 \wedge ... \wedge F_n) \Rightarrow G$ dans le contexte $\mathcal C\cup \{(y:T)\}$, alors l'énoncé $(F_1\wedge F_2 \wedge ... \wedge F_n) \Rightarrow (\forall y:T, G)$ est également un théorème.
Autrement dit, le fait que $y$ ne figure pas dans les hypothèses $(F_i)_{i=1...n}$ (c'est ce que mes suppositions ci-dessus disent) signifie que $y$ désigne un objet quelconque de type $T$ (si on remplaçait $y$ par n'importe quoi d'explicite le caractère probant de la preuve serait inchangé car les $F_i$ ne seraient pas affectés par cette substitution: $G$ est alors vraie "pour tout objet de type $T$ appelé $y$"). C'est ce qui explique la règle en rouge (si c'est trop formel pour le mathématicien non logicien, je l'invite à regarder à nouveau comment il procède dans sa pratique car c'est bien comme ça qu'on fait couramment).
L'application répétée de cette règle de raisonnement dite "d'introduction du quantificateur universel" fait que dans la pratique courante des maths les contextes changent sans arrêt. En fait les contextes sont effectivement dans un certain sens une manière de rendre les quantifications plus discrètes dans les discours.
Ne t'inquiiète pas, tu as raison de dire qu'il faut quantifier. Le problème est le double niveau de discours. Tu as l'aspect vérité et l'aspect preuve.
Une preuve est une forme et il y a un théorème célèbre qui dit que si tu es capable de prouver que la prouvabilité de A entraine A alors tu es capable de prouver A (et la transformation de la première preuve en la deuxième est automatique et linéaire).
Donc quand tu discutes avec des expérimentés, selon l'angle qu'ils ont envie d'éclairer, tu n'auras pas les réponses forcément correspondant à ce que ton intimité à toi demande.
Précisément ici, (en oubliant l'hypercontextualisation des systèmes et B&B le temps d'un post), tu as "le drame familial" de l'équipe logique du monde qui est qu'au premier ordre (ie quand ce ne sont pas que les phrases qui sont les objets atomiques) on a une règle INCONTOURNABLE en plus du modus ponens qui est:
$$\frac{R(x)}{\forall x: R(x)}$$
(on se fiche du contexte, ce n'est pas important du tout, en fait, par rapport à ce que tu demandes.
Et bé, vue comme ça, c'est sûr que qu'on pourrait paraitre des neuneu (nous les scientifiques) à beaucoup de gens.
Hélas, il y a des preuves que si on veut éviter cette malheureuse apparence LOCALE et "hilbertiser", les preuves arcihvées à l'académie, ce serait vraiment beaucoup, beaucoup plus long.
Donc tout le monde est pour garder cette règle (avec la condition de validité qu'on n'a rien supposé sur le $x$ dont on parle, afin qu'à la fin, la preuve tout entière $P$ devient une fonction qui s'applique comme suit:
$$a\mapsto PreuveObtenueEnRemplacantByDans(x,a,P)$$
C'est le fameux "Soit x". (Les contextes n'ont aucune importance, ils consistent à dire "Soit $x\in CeciCela$"
Pour éviter ces problèmes, personnellement, face à des béotiens, je dis "Je nomme $x$ l'objet choisi par le Démon qui a tout fait pour que la preuve n'existe pas avec ce choix", mais bon, chacun sa life.
Tu as exactement LE PROBLEME DUAL (j'en ai souvent parlé sur le forum) d'ailleurs, mais HEUREUSEMENT de toute ma vie, je n'ai jamais rencontré d'élèves qui m'a fait l'objection (on doit avoir dans les gênes un truc qui masque l'objection). Je me suis toujours demandé comment je ferais pour lui répondre si un jour un petit malin de 15ans me sortait cette objection.
Il consiste en ce que la logique (donc la législature des maths) EXIGE pour qu'un raisonnement aboutissant à R(a) soit valable qu'il soit valable pour convaincre de $\forall x:R(x)$.
Exemple:
Germaine: $5$ est suivi par $6$ qui est pair, donc tous les nombres impairs sont suivis par des nombres pairs.
Prof: ça vous arrive souvent de déduire que votre petit ami mange tous les jours du poisson parce qu'il en a mangé aujourd'hui?
Germaine (jamais arrivé, mais si ça arrivait, que dire): non, pour le poisson ça ne marche pas, là, c'est vous qui généralisez. Vous me faites un reproche d'utiliser un principe que vous appliquez vous-mêmes pour prétendre justifier votre reproche.
$$ \frac{X}{Y}$$
signifie essentiellement que la personne qui prouve va dire $X$ donc $Y$.
Dans des preuves d'enseignants, je pense que tu pratiques souvent le :
soit $x\in E$ blablabla: $R(x)$.
Donc $\forall x\in E: R(x)$
A noter aussi que la précaution "je n'ai rien supposé sur $x$" est une espèce de "toc" de matheux, qui ne change rien: toute preuve s'applique à tout énoncé. Tu peux très bien exécuter la preuve du théorème de Tychonoff sur l'énoncé "Syracuse" et regarder ce qu'il se passe. Ça te générera des axiomes naturels qui impliqueront Syracuse et évidemment ça fera rire les lecteurs tant ils leur paraîtront faux, mais c'est vraiment pas grave.
Par exemple dans une preuve comme:
Soit $x$ un nombre entier. Blablabla. Comme $x\in ]1/3;2/3[$, donc blabla, finalement $x>500$
Donc $\forall x\in \N: x>500$
tu n'auras aucun mal à récupérer les hypothèses utilisées "à tort" comme disent les gens et énoncer "la vraie chose prouvée".
Par contre il y a un truc important mais qui déborde de ce fil, c'est de décider si on considère le $\forall $ comme un produit ou comme une borne inf, autrement dit si :
$$(1): Garanties(\forall xR(x)) = \cap_a \ (Garanties(R(a)))$$
ou plutôt comme :
$$(2): Garanties(\forall xR(x)) = \prod_a \ (Garanties(R(a)))$$
Mais faudra que tu me demandes dans un autre fil si tu veux en savoir plus. IL SE TROUVE qu'on a découvert "récemment" la très grosse erreur qu'il y avait à prendre (2), et qu'en fait en maths, c'est bel et bien (1) qui est utilisé.
Mais ça ne se devine pas au premier coup d'oeil dans la mesure où on a vraiment de chez vraiment :
$$ Garanties(A \ et\
dans toute la communauté scientifique. Et même encore chez énormément de gens qui pourtant "devraient être au courant" que c'est erroné. Mais laissons B&B sans crainte de HS.
On l'a vu d'ailleurs avec les soucis de Bourbaki et aussi des travaux "récent" de la réalisation de l'axiome du choix par Krivine.
Pour Bourbaki, or de question de s'emmerder avec des lettres baladeuses, donc ils ont implémenté le démon à travers un petit truc qu'ils ont appelé $\tau$ et l'axiome:
$$ \forall R [ \forall x: (R(\tau yR(y)) \Rightarrow R(x) )] $$
ce qui t'évite le problème du "soit $x$" devant les étudiants (théoriquement), dans la mesure où, ensuite, avec le jeu des abréviations, tu vas écrire:
$<<$Bjour Msieurs-Dames, je m'en va vous prouver $\forall R(x)$, bon, hein, on est bien d'accord que je vous aurai convaincu quand j'aurai prouvé $R(a)>>$,
où $a$ est $\tau xR(x)$ et où il aura pris soin au commencement, de brieffer les gens là dessus pour ne pas y revenir et où il écrira vraiment la lettre $a$ (et non pas le gros machin $\tau xR(x)$ sur son tableau).
Ainsi, l'honneur était sauf, et la platonicité sémantique conquérante.
Mais tu avais probablement pas mal de gens qui se sentaient chatouillés par cette audace sémantique consistant à "croire au ciel", pour le dire autrement à croire que le témoin (c'est son nom officiel en maths) nous tombe dessus comme ça.
Je te donne un exemple de preuve "Bourbakiste-like" de l'énoncé super important:
$$ [\forall x(R(x)\to S(x))]\to [(\forall xR(x))\to (\forall S(x))]$$
dans ce paradigme. Je crée les abréviations suivantes:
$a:= \tau xR(x)$
$b:= \tau xS(x)$
$c:= \tau x[R(x)\to S(x)]$
[small]Les hypothèses nous donnent $R(c)\to S(c)$ et $R(a)$. On veut prouver $S(b)$
Comme on a $R(c)\to S(c)$, on a donc $R(b)\to S(b)$
Or comme $R(a)$, on a donc $R(b)$, et finalement $S(b)$[/small]
Platoniquement, c'est jouissif, mais "en pratique" c'est pénible.
De plus la science est là pour nous filer des garanties. Faire appel au père Noel, fut-ce modérément pour prouver des choses (ici l'appel est "s'il un truc marche donne-le moi, je ne te demande pas plus, en particulier pas de me donner un truc qui marche s'il n'en existe pas" ) offre une garantie absolue certes (puisque théorème de maths), qu'on va gagner un procès contre le père Noel, puisqu'on aura, au moment d'appliquer la garantie émergeant de la preuve, en cas d'échec, exhibé la preuve que le Père Noel a défailli, à savoir la preuve qu'il existe un truc demandé, et que quand on l'a demandé, le père Noel ne nous l'a pas donné.
C'est bien de gagner des procès, mais comme chacun sait, ça ne mène pas forcément là où on voulait aller.
C'est finalement JLKrivine (sans le savoir, vu que je te donne une CC-description, donc si tu lui demandes, il ne le saura peut-être pas, il présente les choses à sa façon) qui a résolu le problème entre 1990 et 2000, sauf erreur, en remplaçant ça par l'axiome plus faible:
$$ \forall R [ \forall x: ([\forall n\in \mathbb{N} R(\tau_n yR(y))] \Rightarrow R(x) )] $$
qui est par contre lui, inoffensif quand on le transforme en garantie père noelique sur le chantier travail matériel.
Cela provient de ce qu'au moment où tu appliques ta garantie, il n'y a pas de copie (de clonage) du témoin demandé, donc que tu n'es plus confronté au problème de la déception et du procès au père Noel.
En effet, si tu peux prouver qu'il t'a déçu, c'est que tu apportes $X,Y$ avec $X$ un truc qui ne marche pas que le père Noel t'a pourtant donné lors de l'appel, et $Y$ un truc qui marche qu'il aurait pu t'apporter.
Du coup, évidemment, $X\neq Y$, et tu ne peux pas rembobiner l'histoire en disant "bin, au lieu d'envoyer le père noel au tribunal, je n'ai qu'à prendre $Y$ (tu as souvent utilisé $X$, donc faut tout recommencer, tu ne peux pas remplacer $X$ par $Y$ et "garder" le bénéfice des avantages déjà construits sur $X$ (le ciment a coulé et peut-être déjà séché depuis 3 semaines et tu es au troisième étage quand tu t'aperçois de la trahison du père Noel).
Avec l'astuce Krivinienne, d'indexer sur les battements d'une horloge (qui renouvelle donc constamment son numéro), tu es déçu par $\tau_{1803} xR(x)$ qui n'a pas marché, l'horloge ayant tourné jusqu'à $71946$. Mais tu affectes
$$ \tau_{71947} xR(x):= Y$$
comme valeur, non encore jamais considérée, au $Y$ qui marche que le père Noel ne t'a pas donné et dont tu te serais servi au tribunal pour le faire condamner.
Ainsi tu restes tranquilou sur le chantier, termine l'immeuble, et happy end.
Evidemment, depuis longtemps les logiciens avaient INCONSCIEMMENT trouvé la même chose (l'opérateur "new"), et traduit ça dans le raisonnement du premier ordre avec un "soit $x$" qu'on écrit au tableau, devenu le célèbre
"quand $x$ n'est pas libre dans $\Gamma$" dans les manuels académiques à droite de $$
\frac{\Gamma\vdash R(x)}{\Gamma\vdash \forall x R(x)}$$
mais c'était artisanal (ie une production inspirée de philosophie, qui n'a pas tenu contre le godélisme en termes de sécurité, puisqu'on se retrouvait à "accepter" une nouvelle production linguistique, qu'il aurait fallu justifiée).
A noter que l'astuce Krivinienne te redonne le $\tau$, tu n'as rien perdu, via:
$$ \sigma xR(x) := \tau_{f(R)} xR(x)$$
où $f(R):=min(\{n\in \N \mid R(\tau_n xR(x))\}) $ s'il existe $0$ sinon.
Prix à payer: raisonnement par l'absurde. Mais on sait depuis à peu près aussi longtemps que l'axiome du choix entraîne le raisonnement par l'absurde***, donc pas grave.
[small]*** Preuve:
$A:= \{x\mid x=0$ ou ($x=1$ et $P)\} $
$B:=\{x\mid x=1$ ou $(x=0$ et $[P\to Q])\}$
On suppose $(P\to Q)\to P$ (1) et le but est de prouver $P$
Tu prends $f$ choisissant (extensionnellement) un élément dans $A$ et en choisissant un dans $B$.
$a:=f(A)$
$b:=f(B)$
Rappel: $(0=1\to Q)$. De plus $\forall x: [x\in (A\cup
Donc $[(a=b)$ ou $((a=b) \to Q)]$. Exercice: terminer la preuve.[/small]
Voici un exemple plus simple : tu considères la formule $\forall x \forall y, xy=yx$.
Cet énoncé est indécidable dans la théorie des corps, puisqu'il existe des corps commutatifs et des corps non commutatifs. Cela signifie que si tu n'as à ta disposition que les axiomes de la théorie des corps,tu ne peux démontrer ni qu'elle est vraie, ni qu'elle est fausse. (Ce que je raconte a l'air trivial, mais il faut savoir que j'utilise sous-jacemment le théorème de complétude, qui est loin d'être une trivialité).
A noter que certains auteurs préfèrent employer le terme "indépendant de la théorie blabla" plutôt que "indécidable" dans la théorie blabla. Selon Jean-Louis Krivine (avec qui j'avais discuté au gastos il y a de cela quelques siècles), c'est psychologique : le mot "indécidable" fait peur aux non-logiciens.
Enfin, tu peux faire la même chose avec la formule $\exists x, x^2=-1$, qui est fausse dans $\R$ mais vraie dans $\C$.
(Voir la discussion sur les corps gauches « mal nommés » etc.)
Bon on peut changer le mot corps en un autre mot, je ne remets pas en cause l’ensemble.
C’est plutôt à titre de vanne que j’interviens (en rappelant aux lecteurs que dans un concours, « corps » désigne un ensemble notamment dont la deuxième loi est commutative...).
-Le "tau" bourbakiste (en fait le epsilon d'Hilbert) ne résout pas le problème des variables liées (et donc du "soit x ..."; ce problème est évacué autrement dans leur livre, avec des cases reliées par des traits physiques vers le symbole lieur en gros).
-Ledit tau est existentiel: il est choisi de sorte que pour toute formule $P$, tout terme du langage $u$ et toute lettre $y$, $P(y:=u) \Rightarrow P\left [y:= \tau_y(P)\right]$ soit un axiome (et donc $P\left [y:= \tau_y(P) \right ]$ signifie "il existe $y$ tel que $P$" et non pas "pour tout $y$, $P$" même si cette dernière acception est possible via l'utilisation de $P\left [y:= \tau_y(P)\right ] \Rightarrow P(y:=u)$ dans l'axiome ci-dessus). C'est beaucoup moins choquant (même si pareil in fine en passant à la négation): l'univers est non vide de manière assumée et pour chaque propriété il y a quelque part un objet dont le nom mentionne explicitement cette propriété et qui la vérifie à chaque fois qu'elle est vérifiée par au moins un objet.
- le tiers exclu est supposé explicitement. Pas besoin de Diaconescu.
"Soit $x,y$ des réels. on note $a(x,y)$ le réel $x^2+y^2-1$" est la traduction en prose de $a:= x, y\in \R \mapsto x^2+y^2-1$. Donc les contextes sont des outils rédactionnels de déliaison des variables pour décrire une fonction. $\forall x F$ abrège $"toujours [x \mapsto F]"$ au fond. Ils n'indiquent pas nécessairement une quantification. Dans un langage de programmation comme mettons le C,on a des contextes (qui sont des listes de déclarations).
MAIS: avoir le lieur universel $\lambda$ (que tu as noté et je suis aussi pour cette notation) $\mapsto$, permet de virer tous les autres.
Aussi, je trouve dommage de ne pas l'avoir institué plus largement et tôt dans le langage scientifique.
Et :-D même geogebra "délie" alors qu'il est fait pour l'école, ce qui est dommage (mais le point de vue pratique l'emporte). Dans la barre de commande tu écris $f(x)=3x$ et non pas $f=(x\mapsto 3x)$.
Pour caml, ça m'a toujours choqué qu'il le fasse vu son ADN de perfection logique recherchée, mais idem, j'imagine que c'est le pratique qui l'a emporté.
$\forall xR(x)$ devient $[R = Constante(vrai)]$
De même, si vous disposez de $\forall$, vous disposez de $=$ à travers la traduction:
$(x=y):=[$ $\forall z: (z(x)\to z(y))]$
Autrement dit, l'un ou l'autre des concepts $\forall$ ou $=$ permet tout le reste** à condition de disposer de l'opérateur $Constante$ (et des valeurs de vérité et évidemment de l'appartenance (ou de l'espace qui applique une fonction à son argument)).
** (A et
(A=>B) := ((A et
(non(A)) := [$\forall X: $(A=>X)]
Par exemple deux intervalles peuvent être disjoints, leur longueur n'indique rien.
1/ En tant qu'étudiant, tu peux tout simplement voir la négation de $A\to B$ comme $A\setminus B$. Ca va ainsi jusqu'au algèbres de Boole quelconque (la notation peut rester comme si c'étaient des ensembles).
2/ Au delà tu entres dans les algèbres de Heying (pour ce qui est des concepts les plus anciens), c'est à dire les espaces topologique, auquel cas, tous les ensembles n'étant pas des ouverts, la négation de $A\to B$ est l'intérieur de l'adhérence de $A\to B$, qui est la réunion des ouverts dont l'intersection avec $A$ est incluse dans $B$.
3/ Au delà on entre dans des logiques découvertes récemment (linéaire et affine). Dans ce cas, tu peux (et dois complètude sémantique) raisoner avec une opération binaire associative et commutative $*$ et voir $A\to B$ comme étant
$$ \{x\mid \forall x\in A: x*y\in B\} $$
Mais selon que tu es linéaire ou affine, tu n'as plus qu'une seule négation (il y en deux, qui sont égales affinement, mais pas linéairement) ni qu'un seul "et" (il y en a 2 aussi),
- l'un est $A\cap B$
- l'autre est $[A*B] := \{x*y\mid x\in A$ et $y\in B\}$
4/ Dans le monde quantique l'implication est trop rigide pour signifier quelque chose, mais on est très proche des dex dernières logiques
5/ La plupart du temps il est erroné de chercher à probabiliser cela (comme l'ont montré les déboires de l'humanité en enfantant dans la douleur une réaction scientifique saine face aux "surprises" quantiques) du fait que "A et A" ne veut pas dire A et ne devrait pas, stricto sensu avoir la même probabilité, et le succédané de deux tirages successifs indépendant demandant si les couple tiré est dans $A\times A$ n'est qu'hélas un très maigre palliatif.
6/ Ces choses sont naturellement implémentées dans ton cerveau via le fait que tu auras du mal quand tu évaluera la phrase : j'ai acheté 2 croissants et j'ai aussi acheté 1 croissant. (tu auras du mal à savoir si la personne te dit qu'elle a acheté 3 croissants ou qu'elle te t'affirme 2 fois dont une pour rien qu'elle a acheté 2 croissants)
De même que le conditionnel, incompatible avec l'implication
7/ Pour des groupes, tu peux revenir à (1) et ignorer (2) à (4). Tu fais l'ensemble des entiers diviseur de machin qui ne sont pas le cardinal d'un sous-groupe de truc.
Mais je pense que B&B posait la question assez "informellement", il semble le dire lui-même. En toute rigueur les "valeurs de phrases" autres que $vrai; faux$ sont un chapitre entier de logique. J'ai essayé dele faire "triper" sans mentir sur la came ;-)
Evidemment que les scientifiques travaillent en disant "il y a tant de probabilité que A". Mais N'EST PAS et ne peut pas être sa seule proba.