À propos du "Ageron"

@JL: je te donne des précisions un peu plus formelles. Pour les affirmations mathématiques, tu peux essayer de les prouver.

1/ à isomorphisme, on obtient tous les ensembles ordonnés sous la forme $(X,\subset)$ avec $X,E$ bien choisis tels que $X\subset P(E)$.

2/ Le clivage ne se situe pas du tout au niveau classique VS intuitionnisme, qui font à peu près la même chose, même s'il passionne les gens d'en étudier les différences.

3/ Tous les cas, quand tu as un ensemble ordonné, mis sous la forme de (1), le $X$ engendre une topologie et elle donne tous les connecteurs logiques. Par exemple $non(A)$ est le plus grand $B$ tel que $A$ et $B$ sont incompatibles, etc.

4/ Du coup pour CES DEUX LOGIQUES, tu peux voir les éléments de $E$ comme des mondes et les éléments de $X$ comme des "précisions acceptables" de "dans quels mondes" (au pluriel) on sait qu'on parle.

5/ L'inconfort pour les platoniciens classiques, c'est juste un malentendu qui est qu'ils voudraient que $X$ ressemble trop à $P(E)$. Ca ne va pas plus loin que ça.

6/ Les développements, surtout algébriques, de ça proviennent de certaines formes de "passages dans des composantes connexes"

7/ Le vrai clivage se situe en fait à un aute niveau "strictement sous" la logique intuitionniste. C'est le moment où on ne peut plus voir "et" comme la borne inf, ou si tu préfères, le moment où on ne peut plus dire que

$$ (A\to = \{x\mid \forall y\in A\forall z: [(z\leq x\ et\ z\leq y) \Rightarrow z\in B ] \}$$


8/ On peut dire la même chose autrement, c'est le moment où avoir deux garanties de $A$ n'est plus la même chose que n'en avoir qu'une. Et ça marche même dans les deux sens à savoir que avoir deux garanties de $A$ ne permet pas de passer à la force d'un déteneur d'1 garantie de $A$, car rien n'indique que la deuxième ne l'encombre pas (s'il ne dispose pas de poubelle pour s'en débarasser)

9/ Tout ceci amène à la définition "définitive" de ce que signifie $A\to B$:

$$ (A\to := \{x\mid \forall y\in A: x*y \in B\} $$

avec une opération $*$ à préciser, et surtout sans obligation que ce soit l'opération "inf".

10/ Voilà en gros les choses.

11/ Ta vision platonicienne se promenait dans 1-6 sans même soupçonner que 7-9 existent et te rendait les choses difficiles. En fait, ce qu'il faut bien comprendre, c'est que pour "bien aborder" la logique intuitionniste, il faut ... y renoncer (sauf éventuellement en algèbre), car elle est le premier pas, le plus maladroit, vers le changement de paradigme

[size=x-large]$$ inf \longrightarrow * $$[/size]

même si pour ce qui est de la LI, elle garde inf comme opération $*$, mais se naufrage dans une assymétrie qui lui retire une partie de son intérêt.

12/ Et pour ça il faut bien comprendre à quel moment la science divorce sans consentement mutuel de la philosophie et devient "domaine d'ingénierie, réparatrice d'ascenseurs, productrices de médicaments" et non plus "quête des caprices de Dieu"


13/ Les preuves scientifiques garantissent aux ascenseurs de ne pas chuter et non aux adeptes de la morale de mieux comprendre le droit ou aux croyants d'importer des discours fumeux basés sur les failles du langage pour renforcer leur rhétorique en faveur du divin.

14/ On n'a donc pas $A=(A^\infty)$, ni même $A=A^2$, ni même $A^2\leq A$, où $A$ est l'ensemble des garanties de $A$, $A^2$ est l'ensemble des paires de garanties de $A$ et $A^\infty$ est l'ensemble des cartes navigo pour garantir $A$.

15/ Et de ce fait, la confusion entre $A$ et $A^\infty$ ayant disparu, plus personne ne s'étonne que $[A^\infty $ ou $(nonA)^\infty]$ ne soit pas un théorème scientifique une fois qu'on a accepté de bien parler, et ce sans renoncer à $[A$ ou $(nonA)]$ qui n'est rien d'autre que $A\to A$, mais à la condition de bien restatuter les "et" et les "ou" de l'armada langagière qu'on utilisera

16/ S'il n'y a qu'une chose à retenir c'est que $(A\to := \{x\mid \forall y\in A: x*y\in B\}$ et que $*$ n'a pas de propriété a priori connues par principe. Si tu retiens ça tu comprends tout. Tu as:

16.1/ deux "et-like" qui sont

16.1.1/ $A$ $et_1$et $ B:=\{x*y\mid x\in A$ et $y\in B\}$
16.1.2/ $A$ $et_2$ $B:= A\cap B$

16.2/ L'implication, qui est centrale et il n'y en a qu'une: $A\to B := \{x\mid \forall y\in A: x*y\in B\}$

16.3/ deux "ou-like" qui sont:

16.3.1/ $A$ $ou_1$ $B:=[(nonA)\to B]$
16.3.2/ $A$ $ou_2$ $B:=A\cup B$

16.4/ Deux "non".
16.4.1/ L'un primitif qui marche comme le signe moins pour les nombres, il est involutif et décroissant.
16.4.2/ Le "non" habituel des matheux qui est $non(A^\infty)$

etc....

Le fait que le RPA ne soit pas "donné" et qu'il y ait deux logiques "classiques", la vraie classique et l'intuitionniste, ce n'est rien de plus que le fait que c'est réellement difficile de déduire $A$ de $non([non(A^\infty)]^\infty )$ et rien de plus. C'est une des raisons pour lesquelles d'ailleurs je suis souvent intervenu pour rappeler qu'un "vrai" RPA va cloner des hypothèses, sinon, il est "vide" de force et n'a pas de raison autre de ne pas être éliminable que scripturales.

17/ Comme j'imagine que ça va te saouler que $*$ soit inconnue, je te donne la "presque idéale" opération qui elle est définie et qui permet de comprendre: c'est l'application d'une fonction à son argument. Par contre, attention, avec la nuance que tu dois te débarasser des ensembles de définition (ce que tu peux faire en envoyant sur l'ensemble vide au lieu de UNDEFINED en première approximation)

18/ A ce niveau, il faut noter qu'il y a en fait 3 "et" et 3 "ou", mais je ne t'embête pas avec ça, la recherche ne s'en est pas encore "bien" aperçu, je te les décris vite fait:

18.1/ Le "et" gloutons consistant à disposer de deux garanties, une de A et une de B
18.2/ Le "et" borne inf consistant à disposer d'une seule garantie que tu peux commuer en garantie de A, ou en garantie de B selon tes désirs
18.3/ Le "et" oublié des chercheurs (il y a une raison à ça, mais ce serait le sujet d'un autre fil) consistant à disposer d'une garantie qui, sans métamorphose est aussi bien une garantie de A qu'une garantie de B.

Ensemblistement, ça te donne les 3 opérations suivantes, bien distinctes:

18.1bis/ Glouton (A et est "le produit tensoriel de A par B", ie l'intersection quand $X$ varie des $[A\to (B\to X] \to X$

18.2/ Navigo $(A$ $et_2$ $B) := A\times B$

18.3/ Méprisé $(A$ $et_3$ $B) := A\cap B$

19/ Mais attention, seuls certains ensembles de garanties étant "autorisés", je ne te donne ça que pour te montrer qu'il existe un domaine "sympatique". Ce qui n'est pas limité (ie on on ne demande pas que seuls certains ensembles soient autorisés), ce sont les ensembles d'agresseurs. En effet, la science ne peut pas se permettre de penser que la Nature lui fait des promesses. Tu as donc deux notions:

19.1/ Les ensembles "tout court", et la notion "être un élément de"
19.2/ Une sorte de cloture qui est qu'un élément pas dans $A$ peut tout de même garantir $A$

Voilà. Et je te le répète, je t'ai raconté tout ça pour que tu vois à quel moment on quitte Nietzche et on rejoint Carnot, c'est à dire à quel moment on plonge dans la façon dont on va pouvoir faire des procès très concrets à réalisations de non A alors qu'on a prouvé A avec des hypothèses. Et que tu vois qu'on ne va pas seulement forcément se sentir obligé de rejeter UNE hypothèse, mais étudier aussi tout l'arbre des garanties et les répétitions d'une même hypothèses, ainsi que les boucles, etc. Parce que si un avion s'écraser alors qu'il était basé sur une hypothèse H faite une fois, mais utilisée 4187 fois dans la preuves qu'elle implique un truc, ce n'est pas sa fausseté qui en cause mais sa non-absoluité.

Merci Christophe, Foys et Alesha.
Je ne dirai pas que j'ai tout compris, mais une petite lumière vient de s'allumer. La proposition d'Alesha ressemble quand même bougrement au TE, non? En fait toute ma vie (où je faisais des maths pour le plaisir mais non pour le boulot), je n'ai connu qu'à une logique, la classique. J'ai découvert l'intuitionnisme grâce à Ageron et maintenant j'ai beaucoup de retard à rattraper. Mais c'est intéressant en tout cas.
Merci.

Jean-Louis a écrit:

La proposition d'Alesha ressemble quand même bougrement au TE, non?

Non. C'est d'ailleurs parce qu'il m'avait semblé (je n'en étais pas sûr) que tu croyais que la proposition que j'ai énoncée nécessitait le TE que j'ai fait cette remarque. Compare:
$$
(\forall a \in \mathbb{R}) (((a = 0 \vee a = 1) \wedge a \not= 0) \Rightarrow a = 1)

$$ et $$

(\forall a \in \mathbb{R}) (a = 0 \vee a \not= 0).

$$ La première ne nécessite pas le TE, la seconde oui.

@Jean-Louis : P. Ageron a écrit un livre supposé avoir un regard sur la mathématique intuitionniste, alors que 80% (au minimum) des résultats qu'il propose reposent sur le principe du tiers-exclu (TE). J'ai rapidement été déçu par son ouvrage. Peut-être convient-il à des Philosophes.

Pour les gens qui se morfondent à ne pas retrouver qui est l'ordre dans un anneau de Boole, je vous le redonne:

si vous adoptez le point de vue "vrai:=1", c'est $(x\leq y):=(xy=x)$

si vous adoptez le point de vue "vrai:=0", c'est $(x\leq y):=(xy=y)$

Réciproquement, à partir d'une algèbre de Boole (donc juste de l'ordre) et en notant $non(x)$ le plus grand des $y$ tel que $\inf(x,y)=LeMinimum$, vous avez un anneau de Boole avec:

$(a\times b) := \inf(a,b)$

$(a+b) := \sup(\inf(a,non(b)),\inf(b,non(a)))$

christophe c a écrit:

A noter que la tradition a mal fait les choses puisque dans 95% des cas les gens adoptent comme des moutons la convention $vrai := 1$

C'est la convention que j'adopte aussi et j'en suis très satisfait B-)

Ca dépend un peu des posts, disons que je voyais ça comme collectif, je postais pour toi, mais avec l'idée que si tu as des questions précises, plein d'autres pourraient rebondir. Sur les derniers coups, un niveau de juste fin de prepa GE maths + 1 an devrait suffire (avec toujours ce problème que les gens ont tendance à se compliquer la vie avec l'approche ensembliste, et ce, pour rien)

Par exemple, pour voir (compte-tenu juste de mon dernier post) que A ou nonA n'est pas un théorème intuitionniste, tu prends $\R$ et $A:=]-\infty,0[$. Comme $non(A)$ vaut alors $]0,+\infty[$, tu n'as pas $A\vee nonA = vrai(=\R)$.

Bonjour,

@Jean-Louis : je t'invite à jeter un œil à ceci, où tu auras soin de relever notamment ceci qui lève presque tout mystère sur la logique intuitionniste :

Il est très remarquable que cette logique [intuitionniste] ait été inventée par un fameux topologue, Brouwer, et qu’avec un peu de recul, elle s’impose naturellement en vertu du fait que l’intérieur de l’adhérence d’un ensemble ouvert ne lui est pas égal. (p. 21 du document, deuxième paragraphe)

Dans son ouvrage intitulé "Topos theory", P. T. Johnstone précise qu'une algèbre de Heyting se nomme également un treillis brouwerien de Brouwer. (page 137, définition 5.12).

Cf. également ceci. La contribution de Ga? est, comme d'habitude, extraordinaire.

PS : il est impossible, même pour CC, de "construire" tout ces concepts ex nihilo.

.

@Jean-Louis : l’apparition de la logique intuitionniste est loin d'être fortuite. C'est Brouwer, topologue, qui en est le père. Qu'il y ait donc une possibilité de construire un modèle [i.e. une interprétation] $\mathfrak{M}_{\text{LI}}$ de cette logique sur la base des éléments d'une topologie (par exemple celle des ouverts de $\R$ pour sa topologie usuelle), ne me semble encore moins fortuit.

Je reviens vers mes premières amours.

Un grand merci à AD!