Sémantique topologique

Précision: dès lors qu'on remplacé $\{vrai; faux\}$ par une topologie:

U => V est la réunion des ouverts X tels que $U\cap X\subset V$

U et V est $U\cap V$

U ou V est $U\cup V$

faux est $\emptyset$

vrai est l'espace entier

non(U) est (U=> faux)

U égal V est( (U=>V) et (V=>U))

@Poirot de mon téléphone. Figure toi que c'est GBZM qui m'en avait informé, je n'en avais jamais entendu parler avant.

Tu as les 1ers et seond ordre aussi puisque l'ordre inclusion est complet.

Et la complétude n'est pas "si dur". Tu as même la possibilité de fabriquer un seul espace top où SEULS les théorèmes intuitionnistes valent l'espace entier.

Oui (sauf erreur) les ouverts sont les Ap ens des q qui impliquent PROUVABLEMENT p (c'est mon téléphone qui a imposé les majuscules). À vérifier quand même.

@poirot, pardon pour le retard. Je veux aller aux puces assez tôt, donc suis pressé.

J'essaie de te dessiner le paysage global.

1/ La complétude historique est mal connue (enfin je veux dire son intérêt est mal connu) et ne concerne que la logique classique précisément du premier ordre.. En dehors de ça, c'est une trivialité pour une raison simple: on fait exprès de l'avoir en "trichant". J'entre dans les détails.

2/ La complétude propositionnelle c'est juste l'axiome u choix ou le lemme de Zorn (qui sont des théorèmes dans le cas fini). Bref, ça ne dit rien.

3/ La complétude du premier ordre est THE MIRACLE ABSOLU de l'histoire de la science: en temps fini on "peut savoir" que des alternances de $\forall/\exists$ seront ou non acceptables alors qu'on discute de monde infinis. Si tu veux plus de détails, je peux t'en donner, mais ce n'est pas vraiment le sujet. Globalement, c'est la relation efficace des variables liées avec le raisonnement.

4/ Le paysage global est le suivant:

4.1/ Tu as 6 mots importants: complétude, compacité, liberté, génération, beauté, symétrie, et un drame.

4.2/ On a une situation "retenue sous le vocable "complétude" " quand deux conditions sont réunies: compacité + génération

4.3/ Le théorème de complétude concerné est vendu dans les médias scientifiques quand on deux conditions supplémentaires sont vérifiées: symétrie et beauté.

4.4/ Mais "in fine", dans ce champ d'étude dès qu'on a envie d'avoir de la complétude, il SUFFIT de gagner de la compacité. ie "pas de solution pour la liste infinie" => "pas de solution pour au moins une sous-liste finie"

4.5/ Se pose ensuite la question de la génération, ie de trouver des bonnes listes (non redondantes SI POSSIBLE) de montagnes infranchissables afin de pouvoir parler de démonstrations officielles dans tel ou tel système.

4.6/ Le terme de non redondance va rejoindre celui de liberté, etc, etc.

4.7/ j'ai utilisé le mot "génération" comme synonyme de "se préoccuper des bons systèmes de générateurs"

5/ Le drame: tout ce qui est libre et complet est trivial. Il y a donc une quète éternelle dont on sait qu'elle n'aboutira que partiellement

6/ L'importance de la symétrie: pas trop besoin de faire un dessin pour la logique appliquée (ie les maths), mais il y a une "nouvelle" (au sens de "news") dont on ne s'est toujours pas remis et qui rejoint 1+3 ci-dessus: LA SYMETRIE DES VARIABLES LIEES ou des constantes non documentées. On NE PASSE PAS par cette symétrie, purement intuitive, pour prouver le théorème de complétude du premier ordre, mais "on sent bien" que pourtant sans elle, ledit n'existerait pas.

7/ Voilà, en gros le paysage!

8/ Maintenant, "état de l'art médiatisé" dans ce domaine. Et bé, il y a 4 logiques (mais peut en inventer une infinité) qui ont buzzé:

8.1/ La classique évidemment

8.2/ L'intuitionniste (que l'on peut définir comme l'ensemble des formes qui donnent l'espace entier quelque soit la topologie dans laquelle elles sont interprétées

8.3/ La logique affine (définie comme l'ensemble des formes qui contiennent un objet "canonique" (tout bêtement dans lesquelles on peut choisir sans axiome du choix un objet) dans quelques espaces affines où elles sont interprétées (A=>B étant défini comme l'espace des applications affines de A dans )

8.4/ La logique linéaire (définie comme l'ensemble des formes qui contiennent un objet "canonique" non nul (tout bêtement dans lesquelles on peut choisir sans axiome du choix un objetnon nul) dans quelques espaces vectoriel où elles sont interprétées (A=>B étant défini comme étant L(A,B)))

8.5/ Parler ici de "complétude découverte" serait ici une sorte de publicité mensongère. Il est relativement plus fidèle à l'histoire de dire qu'on commence par s'amuser à écrire:

<<msieurs-dames, j'ai décidé d'étudier l'ensemble des formes qui donnent JOKER dans toutes les structures machins>>

puis 10ans plus tard,

<<msieurs-dames, je vous annonce que ledit ensemble est celui des mots tels que blabla-systèmesyntaxique-blabla>>

et je vous demande de me dire si vous le trouvez:

8.5.1/ beau?
8.5.2/ symétrique?
8.5.3/ générationné pertinemment?

8.6/ Pour dire (8.5) en un mot: la sémantique précède la syntaxe.

En espérant que ça te permette de me poser des questions précisées si ce paysage ne t'apporte pas ce que tu voulais savoir.

9/ Humour: et si tu veux une cinquième logique, tu peux prendre celle de tonton christophe, la logique annelée (ens des formes ALL VRAIES quand interprétées dans un anneau commutatif unitaire où les phrases sont des idéaux et où A=>B est défini comme étant l'ens des $x$ tels que $\forall y\in A: xy\in B$. Bon évidemment, on peut faire ça avec n'importe quoi. Mais la taf consiste ensuite à vérifier si c'est compact, puis correctement ou sympathiquement générationné, puis beau/symétrique.

Ok, je reprends (enfin complète).

1/ Classique: le premier ordre est un "miracle"

2/ Evidemment que l'intuitionniste a précédé sa sémantique

3/ A partir de maintenant (années 2000 disons, et même 1970), disons que la sémantique va avoir tendance à précéder.

La compacité c'est juste une condition nécessaire pour qu'il existe une notion de démonstration (qui est finie à tout point de vue).

Oui je le ferai d'un PC pas de souci.

De mon téléphone. Certes mais je pense que tu sais que ces succédanés "ne méritent pas" l'appellation n ieme ordre. Ce sont des simulations, qui reposent essentiellement sur le contenu de fond de ce que peut faire le premier ordre.

Ah oui tu as raison. Si tu as une expression avec des implique et des lettres tu remplaces chaque X=>Y par "espaces des applications affines de X dans Y.

Finalement tu obtiens le nom d'un espace affine mais que tu ne connais puisque les lettres ne sont pas associées à des valeurs (qui devraient être des espaces affines).

Si tu es capable pourtant d'associer à cet espace générique un de ses éléments et bien c'est que ton expression est un théorème de la logique affine (et ça la caractérise).

D'un PC je te donnerai la definition des autres connecteurs.

Plus prosaïquement c'est l'ensemble des théorèmes obtenus avec le calcul des sesuents mais où tu ne t'autorises pas dans les listes à remplacer ...A,A,... par ...A...


De mon téléphone

Poirot, je suis sur un pc, je te réécris ce que j'ai souvent écrit dans divers posts. Il s'agit d'une présentation pour matheux de toutes les logiques.

Mais je ne me rappelle plus comment j'avais décidé de l'appeler, donc j'invente un nom.

Un uplet $(E,\leq , \to , 1, \neg )$ est appelé structure phrasée minimale quand:

0/ $1\in E$ et $\to \in (E^{(E^2)})$

1/ $\leq$ est un ordre sur $E$ qui est complet (ie toute partie de $E$ a une borne inf)

2/ $\forall x: (1\to x)=x$

3/ $\forall a,b,c: (a\to (b\to c) )= (b\to (a\to c))$

4/ $1\leq (a\to b)$ ssi $a\leq b$

5/ $\neg$ est une involution décroissante de $E$ dans $E$.

On appelle "théorème" un élément $\geq 1$.

On appelle "jetable" un élément $\leq 1$.

On note $a\otimes b$ la borne inf des éléments de la forme $(a\to (b\to x))\to x$ quand $x$ parcourt $E$ et $a\wedge b$ la borne inf de l'ensemble $\{a;b\}$.


Avec ça, tu as toutes les logiques actuellement reconnues comme intéressantes et faisant l'objet de recherches payées.

Soit $A$ la plus petite partie de $E$ qui contient tous les $x\to (y\to x)$ et stable par $\otimes$ et $inf$.

Soit $B$ la plus petite partie stable par $\otimes$ de $E$ qui contient $A$ et tous les $x\to (x\otimes x)$

-Une expression dont tu peux prouver qu'elle est $\geq 1$ est un théorème linéaire
-Une expression dont tu peux prouver qu'elle est $\geq inf(A)$ est un théorème affine
-Une expression dont tu peux prouver qu'elle est $\geq inf(B)$ est un théorème classique

Soit $a$ dans $E$. Je note $S(a)$ le plus petit ensemble qui contient $1$ et $a$ et stable par $\otimes$ et $inf$. La borne inf de $S(a)$ est notée $!a$.

Soit $\Rightarrow$ telle que $\forall x,y: ((x\Rightarrow y) = (!x) \to y)$.

Une expression écrite avec juste $\Rightarrow$^dont tu peux prouver qu'elle est $\geq 1$ est un théorème intuitionniste.

Voilà, tu sais tout.

Bon j'ai inventé cette sémantique unifiante pour justement pouvoir répondre en une page aux matheux peu logiciens. La réalité est bien plus bordélique et inachevée. Mais l'approche ci-dessus est saine ne t'inquiète pas.

La complétude de l'ordre te permet de parler à tous les ordres, ce n'est pas limité à la logique propositionnelle. De plus, ça t'éclaire sur la très grande différence entre $\forall $ et $\otimes$ car $(\forall xR(x))$ est par définition la borne inf de l'ensemble des $R(x)$ quand $x$ parcourt L'ensemble d'indices qui te plait. Alors que dans la vie courante, le "et" privilégié est le $\otimes$. Ici tu vois que $\forall$ est apparenté à $\wedge$ et non pas $\otimes$.

Ca se voit très bien dans les preuves. C'est la même preuve (commençant par "soit x") qui prouve tous les $R(x)$ et non pas une preuve $p_x$ par $R(x)$ à prouver.

Alors que quand les gens prouvent $A\otimes B$ (ie ce qu'ils appellent "A et B"), généralement, ils fournissent une preuve de $A$ PLUSSSSSSS une preuve de $B$, le couple formant une preuve de (A et .

La classique est sémantisée par les algèbres de Boole (ie l'ordre sur les bons ouverts d'un esp.topologique (bon ouvert veut dire intérieur de son adhérence)

L'intuitionniste est sémantisé par TOUS les ouverts (pas juste les bons)

La linéaire et l'affine par les espaces vectoriels et affines respectivement.

Pour l'intuitionniste, $non(non(U))$ est l'intérieur de l'adhérence de $U$ et tu retrouves bien l'effet d'appliquer un "non non" pour obtenir des phrases classiques.

Si tu veux taffer directement dans l'affine sans te préoccuper de $inf(B)$, il te suffit de déclarer que tous élément de $E$ est jetable, ce qui équivaut au fait que $1$ est maximum dans $E$ (et du coup $\neg 1$ est minimum, et tu retrouves $faux=Tout$). Seule la logique linéaire fait une différence entre faux et Tout. (Par définition Tout est le minimum de $E$)

De rien.

Je m'aperçois que je n'ai pas répondu à Martial. Je fais ca d'un PC tout à l'heure.