Symbole implication dans certaines définitions

geo

Bonjour.

Pourquoi dans certaines définitions les auteurs ne mettent pas le symbole implication ni même le mot alors?

Par exemple dans la définition d'une suite de fonctions qui converge uniformément.

Dans  au moins  quatre ouvrages je lis:

Soit $f_{n}$ définie sur $\mathcal{D}$ à valeur dans un EVN $E$ 

Si $f_{n}$  a une limite simple sur $\mathcal{D}$ que l'on note $f$

On dit que $f_{n}$ converge uniformément vers $f$ lorsque:
$$\forall \epsilon>0,\ \exists n_{\epsilon} \in\mathbb{N},\ \forall n >n_{\epsilon},\ \forall x\in \mathcal{D},\quad |f_{n}(x) -f(x)|<\epsilon$$
Or moi je noterais :
$$\forall \epsilon>0,\ \exists n_{\epsilon} \in\mathbb{N},\ \forall n >n_{\epsilon}, \ \Longrightarrow\ \forall x\in \mathcal{D},\ |f_{n}(x) -f(x)|<\epsilon.$$
Pouvez-vous m'éclairer svp ?

Merci

Dom

Ta dernière phrase quantifiée contient-elle une coquille où justement tu trouves vraiment que ça devrait être écrit comme ça ?

Le symbole « => » dans l’expression « A => B » peut se lire « Si A alors B ». Et là, je ne comprends pas ce que signifierait « si quel que soit $\varepsilon >0$, il existe il entier $n_\varepsilon$ tel que pour tout $n>n_\varepsilon$ ». 

Par contre on voit parfois :
« …., $\forall n\in \mathbb N$, $n>n_\varepsilon \Rightarrow \forall x \in …$ ». 

Médiat_Suprème

En fait l'écriture $\forall x \in A(P(x))$ est une abréviation (mal formée du point de vue de la logique) qui cache une implication.

Homo Topi

@geo en plus de ce qui a déjà été dit au-dessus, à savoir qu'il y a bien une implication dans les définitions quand on les écrit proprement, il faut aller un cran plus loin. Une définition, c'est une équivalence entre une phrase en français et une formule mathématique. Lorsqu'une suite de fonctions vérifie [...], on dit qu'elle converge uniformément, et quand on choisit d'introduire une suite de fonctions converge uniformément dans un raisonnement, c'est bien parce qu'elle vérifie [...] et qu'on veut s'en servir. Sinon ça ne servirait jamais à rien d'écrire "soit $(f_n)$ une suite de fonctions qui converge uniformément vers $f$" dans un raisonnement, chose qu'on fait tout le temps.

[Utilisateur supprimé]

Non @Homo Topi, totalement non.
Définir c'est donner un nom, tu mélanges des trucs sans rapport là.

Homo Topi

Je ne suis pas d'accord.

[Utilisateur supprimé]

Tu seras d'accord quand tu auras fait un peu de logique.

Homo Topi

Oui, puisque je n'en ai jamais fait de ma vie, évidemment. Le concept de définition, en logique, il existe ? C'est quoi alors, une définition, en logique ?

Foys

Une définition n'est qu'une déclaration d'abréviation: "désormais (.........) s'appellera f dans la suite du propos pour faire plus court".

gerard0

Je ne suis pas sûr que la logique permette de départager entre celui qui appelle "définition" une phrase du genre "... s'appelle ..." (Le rapport entre le périmètre d'un cercle et son diamètre s'appelle $\pi$) et celui qui parle de définitions d'expressions complexes comme "série uniformément convergente", qui n'est pas un nom, mais un groupe nominal avec introduction d'un adjectif qualificatif pour en modifier le sens.

Vous ne traitez pas des même problèmes ! Et au fond, vous n'êtes pas en contradiction !!
Cordialement.

[Utilisateur supprimé]

@Homo Topi j'ai dit 

cohomologies a dit :

Tu seras d'accord quand tu auras fait un peu de logique.

C'est tout ce que j'ai dit, et je répondais à ta phrase incohérente plus haut. Il m'est déjà arrivé de m'aventurer dans un domaine où je ne connaissais rien car j'avais confondu avec autre chose (c'était un truc en théorie de la mesure), donc je peux te comprendre, mais le mieux c'est d'éviter d'expliquer des choses qu'on ne comprends pas soit même.

Homo Topi

Vu qu'on parle de syntaxe et de sémantique dans le sous-forum de Logique : il me semble qu'on avait conclu que la "logique" s'occupe purement de syntaxe, la sémantique étant à part. Il me semble que de donner un nom à un objet n'est pas syntaxique, donc que le concept de "définition" soit juste séparé du fonctionnement de la logique.

C'est bien beau de me dire que je ne comprends pas de quoi je parle, tant que tu ne me le prouves pas de manière irréfutable (fais-le syntaxiquement si tu préfères) je n'en ai juste rien à cirer de ton avis. Peut-être qu'on ne se comprend pas parce que nous n'utilisons pas les mêmes mots de la même manière, mais il n'existe pas de loi qui décrète qu'un mot ne peut pas changer de signification d'un auteur à l'autre (la preuve, ça arrive tout le temps, cf anneau/anneau unitaire ou corps gauche/corps non commutatif). Donc soit tu me dis sur le sens de quel mot tu n'es pas d'accord avec moi et pourquoi, soit tu me démontres que ce que je raconte ne peut pas être cohérent, soit tu la boucles. Le manque de respect a ses limites. Bordel !

[Utilisateur supprimé]

Homo Topi a dit :

Une définition, c'est une équivalence entre une phrase en français et une formule mathématique. 

Aucun sens.

Poirot

La sémantique fait évidemment partie de la logique enfin !!! Le lien entre syntaxe et sémantique est donné par le théorème de complétude (de la logique du premier ordre).

@Homo Topi tu devrais vraiment te plonger dans un cours de théorie des modèles. Je t'ai recommandé plusieurs fois le livre de Dehornoy. Si tu n'y as pas accès immédiatement, il partageait en ligne ses notes de cours à l'ENS qui ont constitué la base pour son livre. Par exemple, son chapitre sur la logique du premier ordre devrait t'aider à y voir plus clair. C'est parfois fastidieux, comme tout cours de logique, mais ça en vaut la peine pour comprendre de quoi on parle.

Foys

gerard0 a dit :

Je ne suis pas sûr que la logique permette de départager entre celui qui appelle "définition" une phrase du genre "... s'appelle ..." (Le rapport entre le périmètre d'un cercle et son diamètre s'appelle $\pi$) et celui qui parle de définitions d'expressions complexes comme "série uniformément convergente", qui n'est pas un nom, mais un groupe nominal avec introduction d'un adjectif qualificatif pour en modifier le sens.

Vous ne traitez pas des même problèmes ! Et au fond, vous n'êtes pas en contradiction !!

Cordialement.

Dans le langage bourbakiste certaines expressions abrègent des termes (par exemple $\pi$ va être une abréviation de $\tau_x\left (x\in \R \wedge x > 0 \wedge \cos(x)=0 \wedge \forall y\in \R, y>0 \Rightarrow \cos(y)=0 \Rightarrow  x \leq y \right) $). Et d'autres expressions abrègent des formules de logique, par exemple "$x$ est une suite de fonctions de $y$ dans $\R$ dont la série est uniformément convergente" est une abréviation de $\exists z \in \R^y ,\forall e>0, \exists n\in \N, \forall t\in E, \forall k\in \N, k\geq n \Rightarrow |z(t) - \sum_{i=0}^k x(i)(t)|\leq e$.

En théorie des ensembles ordinaire il n'y a plus d'opérateur de description indéfinie $\tau$ ce qui complique un peu la tâche. Mais en fait comme tous les objets envisagés sont des ensembles on peut considérer que toutes les notions envisagées (objets comme propriétés) sont des abréviations de couples (syntaxiques) $\{x\mid P\}$ où $x$ est une lettre et $P$ une formule de logique. Si $a$ est une lettre, la notation $a \in \{x \mid P \}$ désignant $P[x:=a]$ (remplacement de $x$ par $a$ dans $P$ avec les précautions usuelles sur les lettres muettes). Appelons alors "terme" une lettre ou un couple comme ci-dessus. Si $B,C$ sont des termes, $B\subseteq C$ abrège $\forall x, x \in B \Rightarrow x \in C$; $B = C$ abrège $B \subseteq C \wedge C \subseteq B$; $\{y \mid Q\} \in B$ abrège $\exists z (z = \{y \mid Q\} \wedge z \in B )$. Les notations $\in$, $=$ ont été étendues à tout les termes. La formule $\exists z, z = B$ se lit "$B$ est un ensemble". $\{x \mid \neg (x \in x)\}$ n'est pas un  ensemble (quels que soient les axiomes rajoutés à la logique ambiante: classique ou même simplement intuitionniste). $\pi$ est une abréviation d'un terme (géant) $\{t \mid R\}$ désignant un ensemble (une partie de l'ensemble des suites de Cauchy de $\Q$ par exemple, partie des $t$ vérifiant la propriété $R$).

Foys

La sémantique est un ensemble de thèmes étudiés en logique et la théorie des modèles est l'un d'entre eux.

1) La sémantique n'est indispensable ni à la caractérisation des textes comme démonstrations mathématiques ou non, ni à la fondation des mathématiques.

2) La sémantique apporte beaucoup d'éclairages conceptuels.

3) Les phrases 1) et 2) ne sont pas contradictoires entre elles (à moins que vous ne croyiez que tout ce qui n'est pas obligatoire est interdit mais alors votre problème ne relève pas des mathématiques).

Homo Topi

@cohomologies je veux connaitre ta définition du mot "définition".

Quand j'écris dans un cours sur les groupes (j'évite le mot "théorie" maintenant) "Définition : $G$ est un groupe lorsque ['axiomes' qui définissent un groupe]". J'ai un énoncé mathématique type (énoncé 1)$\wedge...\wedge$(énoncé $n$) contenant la lettre $G$ comme une variable libre. Dans cette formulation*, j'ai écrit "$($énoncés sur $G) \Longrightarrow (G$ est un groupe$)$". Sauf si...

Question honnête : quand on fait une démonstration sur un groupe, quand on écrit "donc" (par exemple "$x \in G$ et $G$ est un groupe donc $x$ admet un inverse dans $G$") on représente ça très très très souvent comme une implication. Est-ce que c'est incorrect ? Y a-t-il à ce stade une différence fondamentale (et importante) entre "de '$x \in G$' et '$G$ est un groupe' je déduis '$x$ admet un inverse dans $G$'" et "$(x \in G) \wedge G$ est un groupe $\Longrightarrow \exists y \in G (y = x^{-1})$" ?

*autre formulation : $\forall G (G$ est un groupe$)\Longleftrightarrow($ axiomes qui définissent un groupe$)$. Mon équivalence avec une phrase en français est ici. "$G$ est un groupe" est une phrase en français.

Si une définition c'est autre chose que ça, j'aimerais qu'on m'explique. Sauf si c'est aussi dans le Dehornoy

[Utilisateur supprimé]

gerard0 a dit :

 qui n'est pas un nom, mais un groupe nominal avec introduction d'un adjectif qualificatif pour en modifier le sens

Ou « expression idiomatique ».

Médiat_Suprème

@Homo Topi $\forall G(G$ est un groupe)⟺()⟺( axiomes qui définissent un groupe)

Cette phrase est une abomination : mélange de langage naturel et de langage formel, et on ne sait pas ce que parcours ce quantificateur (même dans les axiomes, on le sait : ce sont les éléments des modèles).

[Utilisateur supprimé]

Je connais 3 façons de définir les groupes (il y en a sans doutes beaucoup d'autres).
1) par la théorie des modèles: on appelle groupe tout modèle de la théorie des groupes

2) dans un univers (de ZF), "être un groupe" devient ici une relation définissable.
3) la façon que tous ceux qui ont fait des études en mathématiques connaissent: on appelle groupe tout triplet $(G,\star, e)$ tel que ...

Médiat_Suprème

La 1) est ma préférée, devinez pourquoi 

[Utilisateur supprimé]

Aussi @Homo Topi, un énoncé ça n'a pas de variables libre

Homo Topi

Médiat_Suprème a dit :

@Homo Topi $\forall G(G$ est un groupe)⟺()⟺( axiomes qui définissent un groupe)

Cette phrase est une abomination : mélange de langage naturel et de langage formel, et on ne sait pas ce que parcours ce quantificateur (même dans les axiomes, on le sait : ce sont les éléments des modèles).

Je ne suis pas entièrement d'accord. Quand j'écris "$\forall G$", $G$ est un ensemble puisque dans les maths que j'écris (construites sur ZFC disons) tout est un ensemble, et dans ce cadre-là, les formules $\forall x(...)$ ou $\exists y(...)$ sont définies, même certains axiomes de ZFC sont formulés avec ça. L'axiome de l'ensemble vide "$\exists V, \forall x, \neg(x \in V)$" contient un $\forall$ et un $\exists$ qui ne "parcourt rien", et pourtant, c'est licite. Donc je ne comprends pas ta critique.

Je ne comprends pas en quoi je mélange quelque chose qui ne peut pas être mélangé. Pourquoi est-il interdit de déclarer que les énoncés "$G$ est un groupe" et "[liste d'énoncés portant sur $G$ qui définissent la structure de groupe]" ? J'aimerais qu'on m'explique ça avec des vrais arguments, "je trouve ça moche" ça ne compte pas.

cohomologies a dit :

Aussi @Homo Topi, un énoncé ça n'a pas de variables libre

D'où mon autre formulation.

[Utilisateur supprimé]

Homo Topi a dit :

.. J'ai un énoncé mathématique type (énoncé 1)$\wedge...\wedge$(énoncé $n$) contenant la lettre $G$ comme une variable libre...

*autre formulation : $\forall G (G$ est un groupe$)\Longleftrightarrow($ axiomes qui définissent un groupe$)$. 

Donc tu as reformulé ta phrase incohérente avec une autre phrase incohérente...
Ta mauvaise foi n'a pas d'égal, on te dit depuis des jours qu'il faut que tu ailles lire des livres de logique, mais tu préfère venir partager ton expertise sur un domaine qui ne t'est pas familier...

Homo Topi

Tu n'expliques en rien en quoi ce que je dis est incohérent, alors tes commentaires sur une prétendue mauvaise foi de ma part, je m'en contrefiche.

Rédige-moi une définition purement syntaxique, correcte et cohérente, de "$G$ est un groupe". Parce que si ce que j'écris est n'importe quoi, alors je ne sais pas le faire. Sois enseignant plutôt que condescendant : montre-moi.

Foys

"$G$ est un groupe" est une abréviation de "il existe $H,m$ tels que $(H,m) = G$ et $m$ est une application de $H \times H$ dans $H$ telle que pour tous $x,y,z \in H$, $m(x,m(y,z)) = m(m(x,y),z)$ et telle qu'il existe $e$ dans $H$ tel que pour tout $x$ dans $H$, $m(x,e) = x$ et  $x = m(e,x)$ et pour tout $x$ dans $H$, il existe $y$ dans $H$ tel que $m(x,y) = e$".

geo

hum, hum...

Pour répondre à DOM, je vais rajouter des parenthèses.
$$\forall \epsilon>0,\ \exists n_{\epsilon} \in\mathbb{N},\ \forall n \in\mathbb{N} ,(n >n_{\epsilon}, \ \Longrightarrow\ \forall x\in \mathcal{D},\ |f_{n}(x) -f(x)|<\epsilon).$$
Ça c'est ce que j'ai toujours écrit quand j'étais étudiant. Or dans beaucoup de manuels on retrouve une définition sans symbole implication. De fait, je me dis qu'il ne doit pas être aisé d'utiliser la définition pour montrer qu'une suite de fonction converge ou ne converge pas uniformément. En effet, la négation de cette phrase ne sera pas la même.

C'est un peu comme si on donnait comme définition de limite d'une suite l'expression suivante : $$\forall \epsilon>0,\ \exists n_{\epsilon} \in\mathbb{N},\ \forall n >n_{\epsilon},  |U_{n}(x) -\ell|<\epsilon.$$

PS. Dans le Gostiaux 3, le Dantzer et dans de nombreux documents que l'on trouve sur ne net ce symbole n'y est pas.

Homo Topi

D'accord. D'après cohomologies cependant, ton énoncé n'est pas un énoncé puisque $G$ est une variable qui n'est pas liée à un quantificateur. Donc ta définition est-elle valide ? En tout cas je ne comprends pas comment la lettre $G$ pourrait être muette dans la définition de "$G$ est un groupe"...

Je ne comprends honnêtement pas, hein. Je ne suis pas d'aussi mauvaise foi que ça, même si certains ici essaient de prétendre le contraire.

Médiat_Suprème

geo a dit :

En effet, la négation de cette phrase ne sera pas la même.

$\forall \varepsilon >0 P(\varepsilon)$ est une formule mal formée du strict point de vue logique, donc on ne peut pas lui appliquer les règles valides pour les formules bien formées (comme la négation)

Foys

$\forall \varepsilon>0 P(\varepsilon)$ est une abréviation inoffensive et complètement transparente de $\forall \varepsilon, \varepsilon >0 \Rightarrow P(\varepsilon)$.

Médiat_Suprème

Je sais, mais elle est mal formée et donc les règles qui s'appliquent aux formules bien formées ne peuvent pas s'appliquer mécaniquement dessus (et c'est bien la question soulevée par @geo).

Homo Topi

@Foys j'ai oublié de te mentionner dedans mais mon message précédent était pour toi.

Foys

En supposant les formules écrites avec $\neg,\wedge, \exists$, l'implication $A \Rightarrow B$ peut être vue comme une abréviation de $\neg ( A \wedge \neg B ) $ et $\forall x F$ comme une abréviation de $\neg \exists x \neg F$. La négation d'un énoncé comme $\exists x (P \wedge \neg  Q )$ devient alors syntaxiquement $\forall x (P \Rightarrow Q)$. Quand on abrège $\forall x, x \in e \Rightarrow ... $ par $\forall x \in e$ et $\exists x ,x \in e \wedge ...$ par $\exists x \in e$, on se retrouve avec $\forall x\in e, F$ qui est la négation de $\exists x \in e, \neg F$.

Foys

Une phrase qui veut parler d'un objet $G$ se doit de le mentionner explicitement quand même.

Médiat_Suprème

M'enfin, je n'ai pas écrit que la négation n'existait pas, mais que les règles s'appliquant aux formules bien formées ne pouvaient s'appliquer mécaniquement sur la formule mal formée, d'ailleurs, dans votre message, vous êtes revenu à la "bonne" forme pour en prendre la négation

Homo Topi

Justement ! Une phrase, oui. Ton énoncé purement formel n'est pas une phrase. Ton "il existe $H$..." peut être intégralement "symbolisé", tu ne l'as pas fait parce que c'est long pour pas grand-chose, mais si on transformait ça effectivement en syntaxe formelle pure (on peut), le symbole $G$ apparaitrait dedans. Donc, lie-le à un quantificateur, pour former un énoncé valide selon la définition de cohomologies à laquelle j'essaie de me conformer. C'est justement parce que je ne sais pas le faire que j'utilise des équivalences avec des phrases en français.

[Utilisateur supprimé]

😆😆😆A quoi me sert la parole puisque @Homo Topi s'octroie le droit de parler en mon nom.
You can't make this up 😆

[Utilisateur supprimé]

Qui a dit qu'il fallait un énoncé ?
Pour ta gouverne la définition de @Foys c'est ce que j'évoque à la définition "2)". Là tu as une formule à une variable libre, ce n'est pas un énoncé, ça te définit une relation unaire (c'est à dire une classe) dont les éléments sont ce que tu appelles "groupe".
Édit. Énoncé: formule sans variable libre.

Homo Topi

Donc "un énoncé" et "une définition" ça n'a aucun rapport ? Contrairement à toi qui te moques ouvertement de moi, moi j'essaie juste de comprendre des trucs en déchiffrant ce qu'on me raconte. Je fais avec ce qu'on me donne.

Pour toi, "énoncé" c'est quoi ? Un truc comme un axiome ou un théorème, une formule syntaxique valide ? Un truc auquel une sémantique pourrait accorder une valeur de vérité ? Dans ce cas-là, oui, une définition c'est autre chose, une définition n'est jamais vraie ou fausse, sur ça on est d'accord.

Je veux revenir sur ça.

cohomologies a dit :

Je connais 3 façons de définir les groupes (il y en a sans doutes beaucoup d'autres).
1) par la théorie des modèles: on appelle groupe tout modèle de la théorie des groupes

2) dans un univers (de ZF), "être un groupe" devient ici une relation définissable.
3) la façon que tous ceux qui ont fait des études en mathématiques connaissent: on appelle groupe tout triplet $(G,\star, e)$ tel que ...

Si je comprends bien les choses que tu dis depuis le début à travers les différents fils de discussion récents en Logique. Qu'un truc soit un axiome ou un théorème, c'est un énoncé qui peut exister à part entière sous forme purement syntaxique. Et une démonstration d'un théorème, faite à partir des axiomes et/ou d'autres théorèmes, pareil, ça peut exister à part entière sous forme purement syntaxique. Donc on peut considérer la théorie $\mathfrak{G}$ des groupes, qui contient comme énoncés tous les théorèmes qu'on veut sur la théorie des groupes. Si j'ai bien suivi, et corrige-moi si j'ai tort parce que je m'embrouille avec tout le bazar, $\mathfrak{G}$ contient* donc une liste d'énoncés.

Question subsidiaire : $\mathfrak{G}$ contient*-elle un ensemble d'énoncés ? "Ensembles" au sens de ZFC. Peut-on parler d'ensembles ici ? L'ensemble "énoncé 1, énoncé 2,..." quelque chose comme ça ?

*Je dis "contient" et pas "est" pour l'instant parce que j'ai un problème avec ce concept de "définition". Et que je ne veux pas dire plus de choses fausses si je peux éviter, vu la vitesse avec laquelle on prend les gens de haut dans ce sous-forum. Prenons comme définition de groupe la définition de Foys :

Foys a dit :

"$G$ est un groupe" est une abréviation de "il existe $H,m$ tels que $(H,m) = G$ et $m$ est une application de $H \times H$ dans $H$ telle que pour tous $x,y,z \in H$, $m(x,m(y,z)) = m(m(x,y),z)$ et telle qu'il existe $e$ dans $H$ tel que pour tout $x$ dans $H$, $m(x,e) = x$ et  $x = m(e,x)$ et pour tout $x$ dans $H$, il existe $y$ dans $H$ tel que $m(x,y) = e$".

Admettons que tout ce qu'il a mis après "abréviation de" soit une formule mathématique entièrement symbolisée. Aucun mot de français dedans, syntaxe pure. Sa définition est alors : "$G$ est un groupe signifie [formule qui se rapporte au symbole $G$]". Dans cette définition, il reste du français, il reste "est un groupe signifie". Ce que je demande, c'est

1) Peut-on se passer intégralement de langage français pour donner une définition de "groupe", et si oui, comment ?

2) La définition de "groupe" est-elle dans la théorie $\mathfrak{G}$ ? Au sens où $\mathfrak{G}$ serait un ensemble et une définition serait un élément de cet ensemble-là. D'où ma question subsidiaire ci-dessus.

[Utilisateur supprimé]

Je ne sais pas ce que tu ne comprends pas dans "prends un livre de logique". 

Homo Topi

Si tu me dis ça, c'est que tu connais un livre précis qui répond à mes questions précises. Tu pourrais au moins me donner un titre. Ou le budget d'acheter un livre après l'autre jusqu'à en trouver un qui répond exactement aux questions que j'ai.

Je fais un gros effort de préciser de plus en plus ce que je ne comprends pas, pour qu'on puisse soit me donner une réponse simple, soit une référence précise qui répond exactement à mes questions. Si ta réponse aux questions finit toujours par être juste "cherche dans un bouquin", je ne comprends pas ce que tu fais sur un forum. Que je peux tout trouver en passant des années et des années à lire des bouquins de logique jusqu'à être capable à faire moi-même un cours de logique, je n'ai pas besoin qu'on me le dise. Qu'on me dise "ce bouquin, dans ce chapitre, explique le détail qui te pose problème", ça ça serait utile, mais ce n'est pas ce que tu fais.

Foys

Un truc au sujet de ces histoires de lettres quantifiées/non quantifiées.

On appelle contexte une liste de lettres distinctes.

Une formule de calcul des prédicats sur un contexte $\ell$ est alors:

-une formule atomique (au sens usuel) dont toutes les variables sont dans $\ell$

-$\top$ et $\bot$ sont des formules du contexte $\ell$

-$F \Box G$ où $\Box$ est l'un des symboles $\Rightarrow,\Leftrightarrow, \vee, \wedge$ et $F,G$ sont des formules du contexte $\ell$

-$\neg F$ où $F$ est une formule du contexte $\ell$

-$\mathbf Q \delta H$ où $\mathbf Q$ est l'un des symboles $\forall, \exists$: où $\delta$ est une lettre n'apparaissant pas dans $\ell$ et où $H$ est une formule du contexte $(\delta :: \ell)$ (le "::" voulant dire bien sûr l'ajout d'un item à une liste).

Cette notion est d'invention tardive (les vieux manuels de logique ne la mentionnent pas) mais correspond mieux à la pratique courante des maths où un contexte est toujours déclaré: l'incantation "soit $E$ un $\R$ espace vectoriel" indique que le mathématicien s'apprête à s'exprimer dans le contexte $\{E\}$ (liste à un élément) et avec l'axiome $P(E)$ qui dit formellement que $E$ est un $\R$-ev.

La phrase "toutes les variables doivent être quantifiées" est une formulation maladroite de "le contexte doit toujours être déclaré".

Dans la définition de groupe plus haut, le contexte est $\{G\}$

Un énoncé mathématique ne parle pas des lettres qui ne figurent pas dans son contexte.

Au cours d'une démonstration mathématique le contexte peut changer. Etant donné un contexte $\ell$ et des énoncés $A_1,...,A_n, B$ du contexte $\ell$, on écrit $A_1,...,A_n \vdash_{\ell} B$ pour "$B$ est prouvable dans le contexte $\ell$ à partir des hypothèses $A_1,...,A_n$".

Alors par exemple on a la règle suivante (dite "d'introduction du quantificateur universel") Soit $\ell$ un contexte, $A_1,...,A_n$ des énoncés de $\ell$, $u$ une lettre ne figurant pas dans $\ell$ et $F$ un énoncé du contexte $(u :: \ell)$. Si $A_1,...,A_n \vdash_{u :: \ell } F$ alors $A_1,...,A_n \vdash_{\ell} \forall u F$. La non-apparition de $u$ dans le contexte des $A_1,...,A_n$ veut dire que $u$ désigne un objet quelconque au regard de ces axiomes.

raoul.S

Homo Topi a dit :

Qu'un truc soit un axiome ou un théorème, c'est un énoncé qui peut exister à part entière sous forme purement syntaxique.

Un énoncé est une formule close (même si dans le Krivine ce n'est pas le cas...) ce qui veut dire que c'est une chaîne de caractère écrite dans le langage considéré, par exemple celui de la théorie des ensembles, syntaxiquement valide (voir un bouquin de logique pour la définition rigoureuse) et sans variable libres.

Homo Topi a dit :

Question subsidiaire : $\mathfrak{G}$ contient*-elle un ensemble d'énoncés ? "Ensembles" au sens de ZFC.

Ça dépend à quel niveau tu te places. Si tu fais de la logique dans ZFC alors oui. Sinon non, dans ce dernier cas c'est un ensemble "intuitif"...

Homo Topi a dit :

Ce que je demande, c'est

1) Peut-on se passer intégralement de langage français pour donner une définition de "groupe", et si oui, comment ?

2) La définition de "groupe" est-elle dans la théorie $\mathfrak{G}$ ? Au sens où $\mathfrak{G}$ serait un ensemble et une définition serait un élément de cet ensemble-là. D'où ma question subsidiaire ci-dessus.

1) Oui. Tu écris ce qu'à dit Foys "il existe $H,m$ tels que $(H,m)=G$... etc." dans le langage de la théorie des ensembles, ça te donne une formule à une variable libre qui est $G$. Tu peux noter $R(G)$ l'abréviation de cette longue longue formule. C'est ce qu'on nomme une relation unaire. Au sens intuitif (en interprétant) $R(G)$ te dis : "oui $G$ est un groupe" ou "non $G$ n'est pas un groupe". Enfin dire que $G$ est un groupe s’écrit formellement $R(G)$ tout simplement. C'est une chaîne de caractère quoi.

2) Disons que dans ZFC, chaque fois que tu voudras écrire un théorème de la théorie des groupes il faudra ressortir la formule $R(G)$. Par exemple pour dire qu'un groupe $G$ contient un unique élément neutre il faudra écrire un truc du style $\forall G,\forall H,\forall m, ((G=(H,m))\wedge R(G))\Rightarrow \left(\forall g\in H \forall e\in H ((\forall x\in H, m(g,x)=x\wedge m(x,g)=x) \wedge (\forall x\in H, m(e,x)=x\wedge m(x,e)=x))\Rightarrow g=e\right)$. Avant le premier $\Rightarrow$ on spécifie que $G$ est un groupe. Bref ça devient vite un cauchemar.

Homo Topi

Souvent, un message signé @Foys et rempli de $\LaTeX$, c'est "au secours je ne vais rien comprendre", mais là je comprends des choses

Mais... pas tout.

Foys a dit :

 l'incantation "soit $E$ un $\R$ espace vectoriel" indique que le mathématicien s'apprête à s'exprimer dans le contexte $\{E\}$ (liste à un élément) et avec l'axiome $P(E)$ qui dit formellement que $E$ est un $\R$-ev.

 Est-ce que je comprends bien que ce $P(E)$ contiendra la lettre $E$, mais que cette lettre $E$ ne sera effectivement pas quantifiée ?

Mieux : peux-tu me donner la version "purement syntaxique" (avec $\vdash$ etc) de "Soit $E$ un $\R$-ev. Si $\dim(E)=n$, alors $E \simeq \R^n$." en utilisant $P(E)$ comme définition de $\R$-ev et en précisant le contexte ? Histoire de voir sur un exemple comment présenter "au mieux" les choses.

Homo Topi

@raoul.S je n'avais pas vu ton message. Oui ça devient vite lourd et moche, mais, c'est "faisable proprement" du coup. Et par rapport à ce que je viens de demander à Foys, la définition de "machin est un [objet à définir]" va effectivement contenir "machin" comme variable libre, mais

raoul.S a dit :

$\forall G,\forall H,\forall m, ((G=(H,m))\wedge R(G))\Rightarrow \text{charabia}$

ici, tu quantifies ledit "machin". Je lis ça comme "pour tout ensemble $G$, pour tout ensemble $H$, pour tout ensemble $m$, si $G=(H,m)$ et que ça vérifie la définition d'un groupe, alors charabia". Contexte ou pas contexte, ici il n'y a pas de variables libres.

Donc si un "énoncé" ne doit pas contenir de variable libre, une définition n'est pas un énoncé. Du coup je ne sais toujours pas trop où la placer*, ma définition, mais j'avance un peu. Comme quoi, pas besoin des deux clowns.

*étant donné une "formule" $def(X)$ qui définit un objet $X$, je peux lister la "théorie des $X$" qui sera donc une liste d'énoncés de la forme "$\forall X, def(X) \Longrightarrow ($résultat$)$", je simplifie un peu. Mais alors, $def(X)$ en lui-même, si ce n'est pas "un énoncé" de ma théorie, d'un point de vue purement syntaxique et formel, c'est quoi ?

Médiat_Suprème

Pourquoi être insultant ? Pour cacher vos faiblesses ? Dans ce cas "Clown" va vite être insuffisant.

[Utilisateur supprimé]

@Homo Topi vous voulez qu'on ait un texte en langage naturel (qui parle de mathématique mais ca reste de la syntaxe de langage naturel) $\Leftrightarrow$ à une expression logique.
Alors que le symbole $\Leftrightarrow$ sert à relier des expressions logiques et non des phrases en langage naturel avec d'autres en langage mathématique.

Le langage naturel évolue dans un univers avec certaines règles et, les maths dans un autre avec d'autres règles, vous voulez appliquer un symbole du second pour relier des choses hétérogènes, ca n'a pas de sens.

On peut aussi dire que le tennis c'est du football avec une petite balle et seulement deux joueurs et qu'il n'y a pas de but, qu'il faut être le dernier à avoir touché la balle qui rebondira dans l'autre camp, sachant qu'on a rajouté un filet entre les deux camps, qu'on ne peut toucher la balle qu'une fois à la fois... etc...

Et en gros, vous dîtes que vous avez posé les bases permettant à un joueur de football de passer immédiatement automatiquement, au tennis, juste à partir de sa pratique parfaite du football.

Personne ne vous croira ou vous suivra (le temps est bien trop précieux !), On peut seulement faire une reconversion ou un apprentissage mais ca passe uniquement, ben, par jouer au tennis.

raoul.S

Homo Topi a dit :

Mais alors, $def(X)$ en lui-même, si ce n'est pas "un énoncé" de ma théorie, d'un point de vue purement syntaxique et formel, c'est quoi ?

$def(X)$ est une formule ("formule" a une définition précise donnée par Foys ICI) à une variable libre. C'est ce que j'avais noté $R(G)$ où $G$ est la variable libre.

Remarque si tu écris $def(X)$ où $X$ est l'unique variable libre de la formule $def$ alors la formule $\forall X, def(X)$ est une formule close (sans variables libres) donc un énoncé.

Homo Topi

Je pourrais te retourner exactement ce même message...

C'est facile de me dire que j'ai "des faiblesses" si quand je pose une question, on me répond systématiquement "lis un bouquin" ou "ta question n'a aucun sens". Si le problème est la façon dont je formule les questions, alors il faut expliquer ce que le faux vocabulaire a de faux, et ce un peu mieux qu'en disant "lis un bouquin". Encore une fois, je sais faire pas mal de maths je crois, donc quand je lis un cours et qu'il ne m'a pas l'air complètement incohérent, il n'est probablement pas complètement incohérent, donc si ce que j'ai appris ne correspond pas à ce que tu as appris, ça ne veut en aucun cas dire que je ne sais ni ne comprends rien, chose que vous m'avez crachée dessus à plusieurs reprises. Si vous voulez qu'on vous respecte quand vous apprenez un truc à quelqu'un, faites-le décemment, sinon ne vous étonnez pas qu'on vous traite avec aussi peu de respect en retour.

J'ai posté ce message l'autre jour, en réaction auquel :

1) cohomologies a déclaré que ça ne servait rien d'essayer de me répondre. Je crois pourtant qu'en français, sur un forum, dans un fil de discussion où je pose des questions pour lever mes incompréhensions, "J'ai beaucoup de mal à comprendre comment tout ça est censé fonctionner..." peut être compris comme "expliquez-moi, je vous écoute". Surtout quand on essaie de me faire passer pour l'idiot, ne pas comprendre ça, c'est un comble. En parlant de "je vous écoute" : c'est ce que je fais, je vous interdis purement et simplement d'affirmer le contraire. Je lis les réponses, pose des questions sur ce que je ne comprends pas dedans, pointe du doigt ce qui me parait incohérent dedans et pourquoi (ce qui soulève d'autres incompréhensions de ma part qu'il faut lever). Quand un prof t'expliquait un truc, et que tu ne comprenais pas son explication, tu te disais "oh ben je suis juste con alors" ou bien tu disais "ce que vous avez écrit à l'étape 4 m'a l'air faux pour raison XYZ" et tu laissais le prof démonter ton argument pour montrer que ce qu'il avait écrit avait bien un sens (que tu comprenais au passage) ? Ceux qui estiment qu'on n'a pas le droit de remettre le prof en question, vous devriez être à l'armée, pas sur un forum. Je réagis mal quand on me dit "ce que tu dis est faux/incohérent" mais pas quand on me dit "ce que tu dis est faux/incohérent parce que [...]", du moins quand je comprends le parce que. D'où le fait que je n'accepte pas toujours tout du premier coup, ça veut juste dire qu'il faut expliquer un peu plus. Le forum sert à ça...

2) tu t'énervais que j'avais qualifié un de tes messages de hors-sujet. Et pourtant : je n'ai jamais déclaré vouloir que l'ensemble de tous les ensembles existe. "C'est une façon de ramener la théorie naïve dans ZFC" n'est pas justifié (si c'est justifiable, j'en aurais eu besoin !), "ce qui est contre nature" n'est pas justifié non plus (idem). "C'est peut-être une envie liée au platonisme, et là, je n'ai pas d'argument, à part vous faire remarquer que c'est de la philosophie et pas des mathématiques" ne repose que sur l'hypothèse que je suis un platonicien hardcore (ce que je n'estime n'être pas le cas du tout). "Sinon, appelons cela des chibrückes, et honnêtement, je ne vois pas pourquoi le chibrückes de tous les chibrückes devrait exister" je ne le demande pas, je disais simplement qu'à une époque, j'aurais voulu que ce soit le cas. "Pourquoi ne pas parler du paradoxe des entiers, puisque l'entier plus grand que tous les entiers n'existe pas" aucune idée ce que ça vient faire là, ce paradoxe n'existe pas alors que le paradoxe de Russell existait bel et bien, lui. Donc tu ne répondais rien de concret à quelque chose que j'avais effectivement dit, j'ai qualifié ça de "hors-sujet total". Le mot "total" était un peu fort, surtout à ce moment-là de la discussion. Je peux m'en excuser : je te demande pardon. Cependant, ton message reste à mes yeux plus à côté de la plaque que dans le sujet, et pas vraiment constructif.

Donc les critiques de votre part à tous les deux, franchement, bof. Foys aussi avait déclaré à un moment que je "choisis" quelles réponses j'accepte, je ne suis pas d'accord avec ça, et pourtant il m'a réécrit un pavé de maths, et je ne lui ai pas dit que c'était à mettre à la poubelle à ce que je sache. Donne à l'apprenant quelque chose qu'il peut accepter, et il l'acceptera. Et ce qu'il peut accepter, ça ne dépend pas de lui : il ne comprend que ce qu'on lui a appris à comprendre, et ça c'est l'enseignant qui le fait.

Médiat_Suprème

@Homo Topi : ne vous étonnez pas qu'on vous traite avec aussi peu de respect en retour.

Je vais essayer de me mettre au niveau : c'est celui qui dit qui y est.

PS : relisez-vous et vous constaterez qu'une fois de plus, vous m'attribuez des choses que je n'ai jamais écrites.

[Utilisateur supprimé]

Qui a appris au premier « Homme » ?