À propos des quantificateurs

De mon téléphone: j'abrege quelque soit par la lettre majuscule A

Si Ax(AyR(x,y)) alors AyR(t,y) donc R(t,u).

Comme on n'a rien supposé sur t, on considère qu'on peut affirmer [AxR(x,u)]

Comme pour en arriver là on n'a rien supposé sur u on se sent sûr que Ay[AxR(x,y)]

Bon d'un téléphone c'est une horreur de rédaction. Pardon. Mais tu as l'essentiel de la démarche formelle.

Écoute, Dom, les arguments de Cc relèvent du bon sens. Y a-t-il quelque chose dedans dont tu doutes, franchement ? Si oui, quoi ?

Maintenant, ces arguments se formalisent aussi tout à fait, par exemple dans le calcul des séquents (intuitionniste ou classique, pas d'importance ici).

On part de l'axiome :
$$R(x,y)\vdash R(x,y)$$
(contexte : $\{x,y\}\cup V$ où $V$ est l'ensemble des autres variables libres de la formule $R(x,y)$).
Par la règle d'introduction du $\forall$ à gauche :
$$\forall y\ R(x,y)\vdash R(x,y)$$
(contexte : toujours $\{x,y\}\cup V$).
Encore par la règle d'introduction du $\forall$ à gauche :
$$\forall x\ \forall y\ R(x,y)\vdash R(x,y)$$
(contexte : toujours $\{x,y\}\cup V$).
Puisque la variable $x$ n'a pas d'occurrence libre à gauche du séquent, on peut appliquer la règle d'introduction du $\forall$ à droite, avec élimination de $x$ du contexte :
$$\forall x\ \forall y\ R(x,y)\vdash \forall x\ R(x,y)$$
(contexte : $\{y\}\cup V$).
Puisque la variable $y$ n'a pas d'occurrence libre à gauche du séquent, on peut appliquer la règle d'introduction du $\forall$ à droite, avec élimination de $y$ du contexte :
$$\forall x\ \forall y\ R(x,y)\vdash \forall y\ \forall x\ R(x,y)$$
(contexte : $V$).

Voila une preuve entièrement formalisée. Tu es bien avancé, et Nemya aussi, sans doute ?

( entre parenthèse pour ne pas dévier la question)

Il faut faire attention au symbole $\exists !$ on n'a pas l'équivalence $(\exists!x)(\exists!y)P(x,y)\Leftrightarrow(\exists!y)(\exists!x)P(x,y)$
"j'avais payé les frais"

C'est bien pour ça qu'il vaut mieux en rester à des arguments de bon sens relevant de la sémantique :
Dire que $$\forall x\in A\ \ \forall y\in B\ \ R(x,y)$$ est vrai, c'est dire en bon français que quel que soit l'élément $a$ de $A$ et quel que soit l'élément $b$ de $B$, $R(a,b)$ est vrai.
Dire que $$\forall y\in B\ \ \forall x\in A\ \ R(x,y)$$ est vrai, c'est dire en bon français que quel que soit l'élément $b$ de $B$ et quel que soit l'élément $a$ de $A$, $R(a,b)$ est vrai.
N'est-il pas évident pour toi que les deux sont synonymes ? Et toujours synonyme avec "quel que soit le couple $(a,b)$ dans $A\times B$, $R(a,b)$ est vrai" ?

@cc
Es-tu d'accord avec http://www.les-mathematiques.net/phorum/read.php?16,1693310,1693378#msg-1693378

Pourquoi j 'ai posé la question à cc et non pas à toi gabu ?
J ' ai un contre exemple mais cc m'impressionne des fois avec ces contres exotiques. Je maintiens ma question @cc

:-D je suis sur un téléphone et il n'y a rien de pire que de taper un contre exemple surtout pour un truc aussi bateau dont tu dis que tu en as un gebrane. Il n'y a qu'un seul (si on commence à 1) deuxième mais pas d'avant dernier dans IN.

Ha ! Je vais essayer...

Je tente de traduire avec l'idée suivante :

1) il existe un élément qui satisfait la propriété (l'existence)
$\qquad$ et
2) s'il en existe un autre, alors ils sont égaux (l'unicité)

Expression A :
$\big( \exists !u, P(u) \big) \Leftrightarrow \big( (\exists u, P(u))$ et $(\exists u, P(u), \forall v, (P(v) \Rightarrow u=v)) \big) \qquad$ (A confirmer !)

Hum, les experts confirmeront 8-)

J'ai eu envie dans un premier temps d'écrire cela :

Expression B :
$\big( \exists !u, P(u) \big) \Leftrightarrow \big( (\exists u, P(u))$ et $((\exists v, P(v)) \Rightarrow (u=v)) \big) \qquad$ (Confirmer que ce n'est pas correct)
mais il me semble qu'il y a un problème pour le $u$ qui n'est pas présenté après le "et" (est-ce cela les problèmes de variables liées/libres ?).

On a $\exists ! x : \exists y : P(x,y)$ qui entraîne $\exists y : \exists ! x : P(x,y)$ (mais pas réciproquement).

Est-ce que ce quantificateur $\exists !$ a une bonne interprétation en "logique d'un point de vue catégorique", de la même manière que $\forall$ et $\exists$ peuvent être vus comme des adjoints (j'ai essayé mais $\exists !$ ne semble pas se prêter au même jeu). (@GaBuZoMeu je crois que tu t'y connais en ce genre de choses.)

La négation: $$\exists\; x\in \mathbb{R},\;\exists\; (n_1\neq n_2)\in {\mathbb{N}}^2,(n_1\leq x\lt n_1 + 1)\;\text{et}\;(n_2\leq x\lt n_2 + 1)$$

Oh la la ! Panique à bord pour l'utilisation des quantificateurs. $\exists! x\ A(x)$ abrège :
$$\exists x\ \big(A(x)\text{ et } \forall y (A(y) \Rightarrow y=x)\big)\;.$$
C'est ce qu'a écrit Kramer, sauf que j'ai mis des parenthèses pour qu'il n'y ait pas d'ambigüité sur la portée des quantificateurs.
Par exemple
$$\forall x\in \mathbb{R}\ \exists! n\in\mathbb{N}\ n\leq x<n+1$$
abrège
$$\begin{aligned}
&\forall x\in \mathbb{R}\ \exists n\in\mathbb{N}\\
&\hspace{3cm} \left(n\leq x \text{ et } x<n+1\text{ et }\forall p\in \mathbb N\ \left((p\leq x \text{ et } x<p+1)\Rightarrow p=n\right)\right)
\end{aligned}$$
Pour nier, il n'y a qu'à suivre les règles habituelles.

@Champ-Pot-Lion : Le $\exists!$ ne traduit pas une adjonction (pas comme le $\exists_f$ et le $\forall_f$ adjoints respectivement à gauche et à droite du $f^*$).
On voit quelquefois apparaître un $\exists!$ pour les théories définissables par limites projectives finies, mais ça ne correspond pas à l'usage habituel du $\exists !$ : c'est en fait un $\exists$ ordinaire, mais qu'on a le droit d'écrire uniquement quand on a démontré l'unicité de ce qu'on quantifie (par exemple, comme $\exists y\ xy=1$ dans la théorie des anneaux commutatifs).

Il n'y a pas de règles spéciales pour le parenthésage, hors les règles de bon sens qui s'appliquent de manière générale pour indiquer la priorité des opérations (puisqu'on écrit en ligne et pas sous forme d'arbre) et qui permettent par exemple distinguer entre $(\forall x\ A) \vee B$ et $\forall x\ (A\vee $.

@Dom :
$$\exists u, P(u),\color{red}{?}\forall v, (P(v) \Rightarrow u=v)$$
Ta formule ne passe pas l'analyseur syntaxique au ?.
Que veulent dire tes virgules ? Sont elles uniquement décoratives ? Ou alors faut-il les voir comme tantôt décoratives, tantôt signifiant "et" ? Fallait-il lire comme suit ?
$$\exists u\ \left(P(u) \text{ et }\forall v\ (P(v) \Rightarrow u=v)\right)$$

gebrane a écrit:

j'ai lu cette discussion WIKIPEDIA qui stipule que $\exists !$ n'est pas un quantificateur et n'a pas une traduction unique ! quelle belle surprise !

Toute ensemble $Q$ de parties de $E$ est un quantificateur sur $E$, qui fournit l'abréviation suivante:

$$ [QxR(x)] := \{x \in E \mid R(x) \} \in Q $$

Le quantificateur $\forall$ n'est autre que $\{E\}$ et le quantificateur $\exists $ n'est autre que $P(E) \setminus \{\emptyset\}$

wikipedia est génial mais à lire avec un esprit critique car je ne t'apprends rien, si tu y regardes bien. (je n'ai d'ailleurs jamais appris ce que je suis en train de te raconter)

Le quantificateur $\exists !$ est $\{ X\subset E\mid card(X)=1 \}$.

Concernant les parenthèses, il est effectivement désolant que la convention internationale ou nationale n'ait pas fixé des pratiques convergentes. Le plus important en tout cas c'est de bien comprendre que quand $Q_1,Q_2$ sont des quantificateurs, $[Q_1xQ_2y P]$ est une abréviation de $[Q_1x(Q_2y P)]$

Merci GaBuZoMeu. J'ai trouvé cette unique référence : https://perso.univ-rennes1.fr/michel.coste/publis/limfinies.pdf (Une approche logique des théories définissables par limites projectives finies).

Merci à tous.

Ne manque-t-il pas un "et" dans ta phrase à haute voix ?

Non.
Ce n'est pourtant pas difficile. Les formules sont
1) Les formules atomiques
2) Les $A \vee B$, $A \wedge B$, $A \Rightarrow B$, $\neg A$ où $A$ et $B$ sont des formules
3) Les $\forall x A$ et $\exists x A$ où $x$ est une variable et $A$ une formule.

Analyse ce que tu as écrit, tu verras que ça ne peut pas se démonter suivant les règles ci-dessus.

Je ressors la définition d'une fonction $f : \mathbb R \to \mathbb R$ majorée :

$\exists M \in \mathbb R, \forall x \in \mathbb R, f(x)<M \qquad$ (Ne me demandez pas pourquoi je mets des virgules !)

Ici, tout est contracté dans peu de notations et on n'a pas de "$et$".
C'est cela je crois qui m'embrouille...

On lit : "Il existe un réel $M$ tel que pour tout réel $x$, $f(x)$ est strictement inférieur à $M$".

Je tente une traduction avec les règles que tu as données en notant "$R(x)$" la formule "$x$ est réel".

$\exists M \, \left( R(M) \wedge \forall x \, \left( R(x) \Rightarrow f(x)<M \right) \right)$

Est-ce juste ?
J'ai l'impression de mettre trop de parenthèses, est-ce le cas ?

Merci :-)

@dom: mot clé "grammaires et langages algébriques". La théorie est très simple d'initiation. Tu pourrais l'acquérir.

Si tu ne taffes pas un peu sérieusement (je t'assure que ce n'est pas long) les langages algébriques je t'assure que tu ne te sentiras.jamais en sécurité pour prouver la NON APPARTENANCE d'une suite de signes à un langage car les connaisseurs ont en fait des réflexes issus de leur pratique.

Acquérir ça te fera plaisir ne te prendra que quelques trentaines de minutes de lectures et au moins tu seras "au propre".

Sinon tu seras oblige d'étudier chaque fois comme s'ils étaient ad hoc les programmes qui inspectent une suite.

@cc
Oui, je sais bien que ce n'est pas long.
Je m'essaye à traduire un truc et surtout je m'interroge : comment en est-on arrivé à écrire un phrase courte et pour moi très claire : $\exists M \in \mathbb R, \forall x \in \mathbb R, f(x)<M \qquad$ ?
Alors qu'avec une "grammaire algébrique" on écrit des phrases "plus dures à lire".
Est-ce une histoire d'implicite ?

@Dom
Un fil qui peut t’intéresser surtout que gabu était présent et tu peux remarquer qu'il n'utilise jamais les "virgules" ou " tel que" https://www.ilemaths.net/sujet-ecrire-en-quantificateurs-500440.html