Un ensemble ?

L'éclairer en quoi? (Je n'ai pas cliqué sur les liens)

Je peux ôter l'abus de langage s'il te gène, mais c'est tout (je cliquerai pour voir votre problème), mais plus tard, je dois sortir.

Votre ensemble est (je fais comme si j'étais un ordinateur automatique):

$$ \{(x,y) \mid x\in ]0, +\infty[ \wedge y\in \R^+\wedge y^2 = 1-x\}$$

l'abus de langage $[a=\sqrt{b}]$ étant une abréviation de $((a\geq 0)$ et $(a^2 =b$))

Salut gai requin,

(je ne suis pas logicien :-D - je commence mon message par être aussi tranché que Christophe, mais je vais ensuite soulever deux subtilités - il sera certainement d'accord avec l'une des deux et pas l'autre ;-) )

$y=\sqrt{1-x}$ est définie par $(y^2 = 1-x)\land y \geq 0$ : c'est une abréviation. En particulier, cet ensemble a un sens, et sa projection sur la première coordonnée est exactement $]0,1]$ (et sur la deuxième coordonnée, $[0,1[$. Cet ensemble est une fonction (ou le graphe d'une fonction, selon tes préférences), de domaine $]0,1]$.

Bon j'exagère un petit peu en mettant une réponse aussi tranchée, parce qu'il y a deux subtilités possibles : 1- est-ce qu'on met des $\exists$ ou des $\forall$ quand on a le choix; et 2- est-ce qu'on pense uniquement à ZF/logique du premier ordre.

Je commence par la première subtilité. Supposons que tu as une propriété $P$ telle que pour tout $x\in A$, il y a un unique $y\in G_x$ ($(G_x)$ une famille d'ensembles indexées par les $x\in A$) tel que $P(y)$. Bon ben dans ce cas-là, on peut être très sloppy et mettre un $\forall$ ou un $\exists$ pour parler de ce $y$.
Plus précisément : si tu veux énoncer une propriété $Q$ sur le $y$ qui dépend de $x$, tu peux dire ou bien "$\exists y \in G_x, Q(y)$" ou bien "$\forall y\in G_x, Q(y)$". Lorsque $x$ est dans $A$, il n'y a aucune confusion possible, et du coup (disons que j'appelle $y_x$ le fameux $y$), la propriété $Q(y_x)$ est définie par l'une de ces deux formules.
Sauf que parfois, il y a des chenapants qui voient une formule du type "$Q(y_x)$" et se disent "est-elle vraie pour $z$ ?" où $z$ n'est pas dans $A$ !! Dans ce cas-là, la réponse n'est pas claire : $Q(y_x)$ est une abréviation de l'une des deux formules plus haut, et selon qui est $z$, s'il n'est pas dans $A$, il se peut très fortement que les deux ne soient pas équivalentes. Du coup la réponse dépend du choix qu'on a fait.

Ici, on pourrait dire que $y=\sqrt x$ n'est pas une abréviation pour $(y^2= x)\land (y\geq 0)$, mais pour "$y = f(x)$" où $f$ est la fonction racine carrée. Sauf que $f(x)$ c'est une abréviation pour "l'unique $z$ tel que $(x,z)$ est dans le graphe de $f$"; et donc ici on voit très clairement le lien avec ce que je viens de dire au-dessus : $y=\sqrt x$ peut vouloir dire "$\forall z, z$ blabla implique que $y=z$" ou "il existe $z$ tel que blabla et tel que $y=z$". Naturellement, lorsque $x$ est négatif, les deux ne sont pas équivalents.

Il y a plusieurs manières de régler ce problème : l'une est par exemple de faire une convention éternelle au début des maths où on décide qu'on mettra toujours un $\exists$, ou toujours un $\forall$; une autre serait de rajouter un "$(x\in A)\land$" à la définition de $Q(y_x)$", de sorte à ce que la réponse soit toujours "non" pour $z\notin A$" (le problème est que ça complique les trucs où on change de domaine...); et la troisième (celle qui est en général choisie je dirais) : ne pas répondre à cette "objection" et simplement ne jamais considérer des expressions où il y a un tel doute, c'est-à-dire ne jamais demander "est-ce que $Q(y_z)$ ? " lorsque $z\notin A$.
Cette troisième solution (ma préférée, et celle que tout le monde utilise en pratique) ressemble à du typage non admis : on "interdit" de considérer certaines formules, parce qu'elles sont mal "typées" ($z\notin A$). Cela fait donc une belle transition vers la deuxième subtilité que je voulais mentionner, qui est d'admettre qu'en pratique on fait des maths typées.

En effet ça c'est le point de vue ZF/logique du premier ordre. Tu peux aussi imaginer un système typé, où chaque terme vient avec un type qui lui est intrinsèque, et en particulier, l'expression $Q(y_x)$ ne serait alors définie (syntaxiquement correcte) que si $x\in A$.
Avec un tel système, ton ensemble $F$serait alors mal typé (puisque $\sqrt{} : \mathbb R_{\geq 0}\to \mathbb R_{\geq 0}$ est typée de cette manière, et donc ne peut pas prendre en entrée un réel négatif), et donc la question devient une question de grammaire : ce n'est plus "qui est dans $F$" qui est un problème, mais "qu'est-ce que $F$".

Je ne sais pas si c'est plus éclairant, mais tu pourras notamment jeter un oeil ici, où à peu près la même explication est donnée (la question est un poil plus subtile : c'est "est-ce que $f(0) = f(0)$, si $f$ n'est pas définie en $0$ ?")

GR a écrit:

gai requin écrivait:

---

> @Max : Merci !
>
> Je suis ok sur le fait que mon $F$ est mal typé. On se place dans ZFC. Imaginons que je souhaite que mes élèves lycéens en l'occurrence) calculent des ensembles de définition.

C'est un peu la connerie du siècle. La seule chose que les réformes ont fait de sensé, c'était de les supprimer. Je sais qu'il y a dans les bahuts quelques "doctes" collègues parlant haut qui aiment les revendiquer. Mais c'est juste une manière de dire que tout fout le camp (ça leur sert d'exemple). Hélas ce n'en est pas un, puisque cette notion n'a rien à voir avec les maths d'une part et d'autre part conduit à des lésions graves (confusion entre passage par nom et passage par valeur), produisant des OShine 10ans plus tard.

GR a écrit:

@cc : Quelle est ta position dans le débat $18 = \sqrt{1-60}\in\{V,F\}$ ?

Qu'elle (cette phrase) entraine $18^2 = (-59)$ :-D (je te fais une GR-réponse ;-) )

Non, Max a raison, et il connait et s'y est intéressé, de te renseigner sur l'existence du typage.

Mais attention, le typage "recherche" (qui en gros fait papoter catégoriciens d'un côté et génère COQ de l'autre) et le typage "scolaire" recommandé cache un peu que c'est ABSOLUMENT DANGEREUX ET MISSION IMPOSSIBLE que de demander à des lycéens de typer (typer est 3 fois plus dur que faire des maths, jusqu'à un stade critique où ça s'inverse, bien au delà du lycée).

Après pour ma part, je l'ai souvent dit, mais c'est personnel, je suis contre "on invente les maths". Pour moi, on les découvre. Multiplier les "interdits" ne fera jamais partie de ma démarche. (Le typage est un développement d'une mentalité HYPERTABOUISANTE dédiée à renvoyer dans le "non accepté comme sensé" tout ce qui chatouille un peu, autrement dit, ça rejette en gros toutes les preuves fines de logique sur l'indécidabilité, l'infini, le procédé diagonal, etc et les bijections tordues de l'analyse).

Mais comme toute spécialité, cette activité développe une communauté et des experts entrainés qui en font quelque chose et personne ne peut dire qu'il n'en sortira rien. Par exemple, pour Max, il semble qu'il ait trouvé (ce qui est raconté depuis des décennies dans les bouquins sans que j'aie jamais vraiment cherché à comprendre) à sa guise cette activité pour avancer en topologie algbébrique. Le seul bouquin que j'ai (ou avais) commence par faire tout un tas de déclarations typantes très nombreuses et produire plein de diagrammes et à la fin on a .. Brouwer (et je n'ai jamais vraiment trouvé à quel endroit on triche, sans pour autant trouver que les passages étaient continus). Donc oui, il semble que ce soit efficace.

Mais ce n'est pas le typage qu'on "attend des lycéens", il ne faut pas s'y tromper.

Superkarl : Non, "est défini" n'est pas quelque chose qu'on peut dire dans le langage.

Christophe est partisan de "tout est défini", c'est-à-dire que n'importe quelle expression qu'on peut écrire a un sens. Ce n'est pas l'usage le plus commun (même s'il n'est pas d'accord avec l'usage le plus commun, Christophe pourra au moins reconnaître ça ;-) ), dans lequel il y a des règles de formation de phrases, qui s'apparentent à du typage.

Parfois il y a des ambiguïtés sur certaines abréviations (ces abréviations "augmentent" en un sens le nombre de phrases qu'on peut former, même si c'est purement psychologique : en principe une abréviation est la phrase qu'elle abrège), et donc cela peut mener à des confusions : ces ambiguïtés sont là parce que la plupart du temps quand on définit des abréviations, on ne les pense que pour l'usage pour lesquels on les définit. C'est un peu tautologique, mais ça explique la situation : $y=\sqrt x$ est une abréviation, et plus généralement, pour une formule $P$ à une variable libre, $P(\sqrt x)$ est une abréviation.

De quoi ? Eh ben cela dépend d'un choix qu'un.e scribe aura fait dans Bourbaki ou je-ne-sais-quel traité "fondationnel". Cela dépend, mais en principe, si les définitions sont bien faites, lorsque $x$ est un réel positif ou nul, cela n'en dépend pas.

C'est ce que j'expliquais plus tôt avec $\forall$ vs $\exists$ : on peut définir $P(\sqrt x)$ comme l'abréviation de "$\forall y, ((y^2 = x)\land y \geq 0)\implies P(y)$" ou de "$\exists y, ((y^2 = x)\land y \geq 0)\land P(y)$. Lorsque $x\geq 0$, les deux sont équivalentes. Lorsque $x < 0$, ce n'est pas le cas a priori.

Du coup pour ton prédicat, avec $P(a) = a\in \R$, la réponse est.... ça dépend. Il est défini sur tout $\R$, mais est-il vrai lorsque $x=0$ ? ça dépend. Je pense que Christophe répondrait que non parce qu'il pencherait pour l'interprétation $\exists$, mais je ne suis pas sûr parce que c'est essentiellement arbitraire (vu que les deux sont "moralement" justifiables, et ont le comportement attendu pour $x\geq 1$)

Quant à l'expression $\sqrt{-1}$, est-ce défini ? La réponse est non, en principe, puisque pour une fonction $f$ (christophe dira n'importe quel ensemble (*), avec une légère modification, mais à nouveau ce n'est pas standard - cela se justifie par son slogan "toute expression a un sens"), $f(x)$ est l'unique $y$ tel que $(x,y)\in f$. Lorsqu'un tel $y$ n'existe pas (i.e. $x$ est "hors du domaine de définition de $f$"), la version christophe ressort $\emptyset$; "ma" version ressort "undefined".

Moi je n'aime pas que ça ressorte $\emptyset$ (mais je n'ai pas de théorème mathématique qui dit "ça ne peut pas être $\emptyset$"); et la manière dont les gens pensent c'est "l'ordi s'arrête et répond 'undefined' ". On peut y voir un inconvénient évidemment, ou un avantage. La version où l'ordi s'arrête et répond 'undefined', c'est du bébé typage, ou encore du typage non assumé.

(*) for completeness, la version Christophe, si je ne m'abuse (il me corrigera) c'est $a(b) := \{c \mid (b,c) \in a\}$ quels que soient $a$ et $b$.
Lorsque $a$ est effectivement une fonction, disons de domaine $A$ et $b\in A$, cela ressort $a(b) = \{$ ce qu'on aurait communément appelé $a(b)\}$, c'est-à-dire que $a(b)$ est le singleton dont le seul élément est l'image de $b$ par $a$, et lorsque $b\notin A, a(b) = \emptyset$.
Comme je l'ai dit plus haut, ça a ses avantages, mais aussi ses inconvénients.

Au sujet de défini/non défini: Les gens ressentent une confusion devant une tâche où on écrit un terme pour établir si on a bien le droit de l'écrire par la suite.

En fait:

En théorie des types/logique d'ordre supérieur, un symbole de fonction est toujours défini sur la totalité de son type de départ. Autrement dit pour tous types $A,B$, $f:A\to B$ et $x:A$, le terme $f(x):B$ est un objet légitime de la théorie. On ne peut pas vraiment faire autrement (sauf à tenter de résoudre un problème sémantique insoluble au niveau syntaxique).

Lorsqu'on fait de la théorie des corps (et c'est bien se qui se passe dans COQ par exemple), on a donc $/ := x,y \mapsto \frac{x}{y}$ appartenant à $K\to K \to K$ (et donc $/$ est définie sur la totalité de $K^2$). On a des axiomes qui relient le comportement de $/$ aux autres opérations: $D:=\forall a,b:K, b \neq 0 \Rightarrow b \times \frac{a}{b} = a$ par exemple (conjointement à d'autres axiomes disant que $(K,+,\times,0,1)$ est un anneau et mettons, $\forall p,q:K, p+(q - p) = q$).
Avec juste ça, on voit qu'il n'y a jamais de problème puisque -$/$ n'étant connu que via $D$- la preuve de la moindre identité avec $/$ obligera l'auteur à prouver à un moment où à un autre que le dénominateur est non nul. $(3/0 \neq 0) => \frac{3/0}{3/0} = 1$ est un théorème COQ par exemple :-D.

Si on doute de l'absence de scandale avec cette approche, vous pouvez étant donné $\K$ un corps, fixer $e\in K$ comme vous voulez et interpréter $/$ par l'application qui à $p,q\in \K$ fait correspondre lorsque $q$ est non nul, $pz$ où $z$ est l'inverse de $q$, et lorsque $q$ est nul, $e$ (bref une fonction partielle se prolonge toujours en une fonction totale sans problème ...).

#############

La logique du premier ordre peut être vue comme un cas particulier de logique d'ordre supérieur (*). Les mêmes considérations s'appliquent. Si $\varphi$ est un symbole de prédicat à $d$ arguments du langage employé et $a_1,...,a_d$ des termes quelconques, $\varphi(a_1,...,a_d)$ est un terme parfaitement légitime du langage.

Si vous ne me croyez pas, ouvrez votre livre de calculs des prédicats préféré et regardez comment est défini le langage du premier ordre: jamais on ne dit que l'écriture d'un terme peut être rendue impossible en raison des conséquences des axiomes des théories qui seront écrites avec ce langage.

Ainsi, si $\div$ est une abréviation (i.e. un symbole pour un certain ensemble, agrandissant le contexte courant) de $\{(x,y)\in \R^2 \mid xy=1\}$ et $\sqrt{\:} $ est une abréviation de $\{(x,y) \in\R^2 \mid y \geq 0 \text{ et } y^2 = x\}$, $\C \div M_2(\R)$ et $\sqrt{L^2([0,1],\R)}$ sont des ensembles.
Mais la moindre tentative de preuve de ce que $ \left (\C \div M_2(\R) \right )\times \left ( M_2(\R) \div \C \right ) - \sqrt{\Z} \leq 1$ vous obligerait de fait (sauf inconsistence invraisemblable de ZFC :-D), à un moment ou à un autre, à prouver que $M_2(\R) \in \R, \C \in \R, \Z \in \R$ et que les deux premiers sont non nuls et le troisième est positif.

[size=x-small](*)où il n'y a qu'un seul type $U$ à part le type des propositions, les symboles de fonction/prédicat sont limités à des arguments dans $U$ et ou les quantificateurs sont réservés exclusivement à $U$.[/size]

Foys : Ce n'est pas ce qu'il obtient. Il obtient "classical $f(x)$" $\in f(x)$. Enfin je crois. A nouveau, il me corrigera si je me trompe.

Je ne comprends pas ce que tu dis par contre, dans ZFC on ne peut pas "mettre des termes" à la suite, donc comme tu définis $\sqrt{L^2([0,1],\R)}$ par exemple ? Enfin, plus généralement, comment tu définis $A(B)$, tu suis la convention de Christophe ?

Sinon par rapport aux types oui bien sûr, mais dans ce cas-là la question du domaine de définition est "calculable" : il s'agit de déterminer le type $A$ tel que l'expression $f(x)$ est bien typée pour $x:A$ (où encore le type $A$ tel que $f: A\to B$ pour un certain $B$)

Oui, oui, bien que lu en diagonale, je confirme à peu près ce qui a été dit sur ce que je raconte. Nuance: je dis que toute suite de signes DOIT avoir un sens, plutôt que toute suite "en a un". Ou alors ajouter "en a un à découvrir".

Je suis en effet relativement opposé à $undefined = undefined$, qui est faux en général et pour éviter ce problème, d'autant plus violent qu'on est sévère sur l'ensemble des suites "autorisées", j'adopte mon paradigme.

D'autant que le préjugé voulant que l'ensemble vide soit "vraiment vide" est réellement agaçant, puisque sa seule propriété opérationnelle est d'être inclus dans tous les autres, et pour un univers d'être une des fenêtres pour voir l'extérieur. Jusqu'à il y a peu, les rayons du soleil entraient par l'ensemble vide uniquement, c'était lourd, même si des progrès récents les font entrer par plus d'endroits dans l'univers.

Par ailleurs, ça, c'est dans le version platonicienne du "tout donné". Mais in fine, quand on s'attache plus à l'extraction de garanties à partir de preuves, l'ensemble vide est gigantesque puisque contient toutes les fonctions choix (et pour tout $E$, on va naturellement, mais ce n'est pas une inclusion, du Vide dans $E$, via $s\in Vide\mapsto s(E)$. Ce phénomène est important quand on regarde les preuves à la loupe et souhaite la fluidité du spectacle (continuité). Sinon, on a des cassures idiotes qui oblige à raisonner par l'absurde de manière externe pour justifier des choses intuitionnistes basiques en interne

Bon de toute façon, ce n'est pas vraiment le sujet.

@Foys, je n'ai pas trop compris pourquoi tu préfères $a(b):=\{x\mid \exists y: x\in y$ et $(b,y)\in a\}$??? C'est rajouter un étage de plus.

Pour ma part, j'utilise $a(b) := \{x\mid (b,x) \in a\}$ et si "donnée comme boite noire $f$", je prends l'ensemble $\{(x,y) \mid y\in f(x)\}$. Comme tu le rappelles parfaitement bien, un domaine de fonction, c'est RAJOUTE de manière ad hoc et arbitrairement, et ça désigne l'ensemble des $x$ tels qu'on a confiance en le fait que $f(x)$ est ce qu'on veut from $x$.

Autrement dit, la correspondance est "triviale":

$$y\in f_{Classic}(x) \iff y\in [SET_{cc} (f)](x)$$

Tu es en train de me dire que $(x, \{t\mid \exists u: t\in u$ et $(x,u)\in f\} ) \in f$ ?????

Ca ne me saute pas du tout aux yeux, mais je vais y réfléchir... Ce serait beau!

Maxtimax a écrit:

Sinon par rapport aux types oui bien sûr, mais dans ce cas-là la question du domaine de définition est "calculable" : il s'agit de déterminer le type $A$ tel que l'expression $f(x)$ est bien typée pour $x:A$

Ce n'est pas toujours vrai (lorsqu'il y a des types dépendants).
https://cs.stackexchange.com/questions/12691/what-makes-type-inference-for-dependent-types-undecidable

christophe c a écrit:

Après pour ma part, je l'ai souvent dit, mais c'est personnel, je suis contre "on invente les maths". Pour moi, on les découvre. Multiplier les "interdits" ne fera jamais partie de ma démarche.

On invente les règles du jeu d'échec et on découvre les gains forcés dans certaines positions.
En maths c'est pareil, à part l'absence de borne a priori sur la taille de l'arbre ou on bosse.

@christophe c:
l'opération que j'ai définie est totale, et a le bon comportement pour des fonctions.

gai requin a écrit:

@Foys : Qu'entends-tu par opération totale ?

Je veux dire que $a(b)$ est défini pour tous ensembles $a,b$ avec la convention que j'ai introduite (c'est aussi le cas de celle de cc qui n'est pas la même).

@gai requin:
il y a en anglais le livre de Jonathan P. Hindley et J. Roger Seldin: "Lambda calculus and combinators, an introduction" qui est de lecture facile (je trouve).

gai requin a écrit:

Ok Foys.

De plus, avec ta convention, si $x\notin dom(f)$, $f(x)=\emptyset$ et on peut calculer ce que j'aurais dû appeler des domaines de définition. smiling smiley

Attention aux fois où $\emptyset$ est parmi les valeurs prises par $f$ quand même (il peut exister des fonctions $g$ et des $y\in dom(g)$ tels que $g(y)=\emptyset$. Par exemple en théorie des ensembles, où $\N$ est souvent confondu avec le premier ordinal non successeur, $0=\emptyset$).

"Undefined" est le point fixe de toutes les fonctions de l'univers, ce n'est pas "n'importe qui", on a tort de le regarder avec dédain. Max (peut-être inconsciemment) parle d'un point teur vers undefined.

En outre, il n'est pas clair que la vocation du monde de tous les possibles soit de fournir un point fixe commun à toutes les fonctions. A la rigueur d'accord à tout ensemble de fonctions qui commutent 2 à 2, mais TOUTE toute toute, bof bof.

Alors je ne sais pas si c'est ce que christophe veut dire par pointeur, mais effectivement, je ne "veux" pas de "$f(x)=$ undefined", je pensais vraiment à "$f(x)$ undefined".
En théorie des types, si $x$ n'est pas du bon type, $f(x)$ n'est pas $=$ à quoi que ce soit, c'est juste une expression mal formée, comme si en logique du premier ordre j'écrivais $\forall \implies \in a \exists$