Questions sur intuitionnisme.

Je t'expliquerai d'un PC. Là je sors du film Papicha que je recommande.

Bonjour Jean-Louis,
Je peux te répondre partiellement sur le point 1).
Comme P implique non non P est toujours vraie et que non non P implique P ne l'est pas en général, la propriété non non P est plus faible que P. Ça, c'est facile à comprendre.
Quant aux valeurs de vérité intermédiaires, je pense qu'Ageron a sorti ça de son chapeau, genre comme un outil pédagogique pour expliquer qu'on n'a pas toujours soit P, soit non P.
A ma connaissance la logique intuitionniste n'utilise pas de valeurs de vérité autres que 0 ou 1. Il existe des logiques à plusieurs valeurs de vérité, voire des logiques floues (à valeurs dans [0,1] ou dans une algèbre de Boole), mais ça n'a a priori rien à voir avec l'intuitionnisme.
Pour le point 2), je pense que tu fais l'erreur d'appliquer sans précautions les lois de de Morgan.
Dire que( P et non P) implique le faux peut aussi s'écrire non(P et non P).
Or, justement (voir le haut de la page 6), la loi de de Morgan non(P et Q) implique (non P ou non Q) est la seule qui soit fausse, en général, en intuitionnisme.
Et même si elle est vraie, tu en déduis que non (P et non P) implique non P ou non non P, mais tu n'es pas plus avancé : comme non non P n'implique pas forcément P, tu ne peux pas en déduire le tiers exclu.
Pour le point 3) je ne sais pas. La seule chose que je peux te dire c'est que les intuitionnistes sont inflexibles sur le TE, même dans les cas triviaux. La meilleure des preuves en est (comme tu as pu le lire) qu'ils font la différence entre ensembles non vides et ensembles habités. Or, en théorie des ensembles être vide c'est bien la même chose qu'être nul, non ?
En espérant avoir pu t'aider, Christophe confirmera ou infirmera.
J'ai moi-même du mal avec ces trucs, parfois je pense avoir enfin compris, et puis à chaque fois que j'essaye de rédiger un truc proprement je me dis que je suis loin de tout maîtriser.

1) La sémantique habituelle du calcul propositionnel classique se contente de 0 et de 1, autrement dit de "Faux" et "Vrai". Tu connais peut-être les tables de vérité ?
La sémantique du calcul propositionnel intuitionniste utilise souvent l'algèbre des ouverts d'un espace topologique. Le "et" et le "ou" correspondent à l'intersection et à l'union, pas de souci. Mais le "non" correspond à l'intérieur du complémentaire, et donc "non non" à l'intérieur de l'adhérence. Le "faux" est le vide, le "vrai" l'espace tout entier.

2) Non, ce n'est pas ça le tiers exclus. Le tiers exclus, c'est "P ou non P".
Reprenons la sémantique topologique de l'intuitionnisme que je t'ai indiquée plus haut :
"P et non P" s'interprète comme l'intersection d'un ouvert et de l'intérieur de son complémentaire, c'est toujours le vide.
"P ou non P" s'interprète comme la réunion d'un ouvert et de l'intérieur de son complémentaire. C'est rarement l'espace tout entier (prends par exemple l'ouvert $]0,1[$ dans $\mathbb R$).

3) Ben oui, en arithmétique intuitionniste on a "$n=p$ ou non $n=p$". Ça se démontre. Ça n'a rien d'exceptions arbitraires à la règle. Tu as cette impression à cause d'incompréhensions. Mais ça va s'arranger au fur et à mesure que tu rentreras dans le sujet, si bien sûr ça t'intéresse.

(tu) Martial ;-)

Édit : j’ai répondu sans voir le dernier message de Martial.

Si, si c’est « un exercice pour traduire le langage ». Pardon si c’est mal dit.
Il faut le faire. (Pas eu le temps d’approfondir...)
Je comprends ça comme « rendre concret la logique avec la topologie ».

Bon c’est peut-être trop vulgarisé, voire à côté de la plaque.


Reprenons : il faudrait retrouver le lien (du forum) où tout l’exercice est bien posé.

Oui, Martial, on a le niveau pour ça je pense.
Des connaissances L2 voire L1 doivent suffire.

Pardon mais je pose une question très naïve...puisque je n'y connais absolument rien, mais je suis curieux.
C'est effrayant de découvrir qu'il "existe une logique" où P et non(non P) ne sont pas équivalents.
Pour un néophyte, est-ce que quelqu'un peut m'expliquer quelle "logique" utilise-t-on dans les raisonnements mathématiques disons "classiques"?
J'espère qu'on me comprendra, je ne suis pas capable de rendre la question plus claire...
Autre question, qui est certainement une conséquence de la première, quand on parle d'une théorie, on parle aussi de sa consistance.
Mais la consistance est liée à la logique...
Pour moi la logique préexistait, et était indépendante de toute théorie...elle est naturelle, canonique...bref.
Mais ce qui semble aussi étrange, c'est qu'on bâtit d'autres logiques (en utilisant des notions topologiques), mais la topologie elle-même se fonde sur "la logique"...

Ce dont je suis sûr, c'est que je n'y comprends absolument rien. Au moins, la certitude rassure!

La logique fait partie des mathématiques, elle ne préexiste pas aux mathématiques. C'est une sujet d'étude qui comprend plusieurs branches, dont la théorie de la démonstration. On y étudie divers systèmes de déduction, ça serait trop triste si on n'avait que le système de déduction de la logique classique à se mettre sous la dent. On entend souvent parler sur ce forum de logique intuitionniste, de logique linéaire ...
Il y a des sémantiques intéressantes pour ces systèmes de déduction non classiques (par exemple on entend aussi parler de topos sur ce forum), et les problèmes que se posent recoupent quelquefois des préoccupations d'informatique théorique.

Martial : merci!!!

GBZM: merci beaucoup pour ta réponse!! Bon je vais essayer de dire ce qui me bloque:

On part d’un langage du premier ordre.
Vient ensuite la structure qui permet d’associer une valeur de vérité à un énoncé de ce langage.
Déjà j’ai un premier blocage ici, justement de nature « logique »(je ne sais même pas si j’emploie le bon terme!):
Comment on définit cette valeur de vérité?
Bon, ensuite je crois que vient la « théorie » à proprement parler, les axiomes quoi.
Et c’est là qu’on va avoir besoin d’un « système de déduction » GBZM...il me semble...?
Alors autre blocage chez moi:
Ce système de déduction est issu de quelle « logique » exactement?(purée je suis perdu!!!)
Pire: Tu cites la « théorie de la démonstration », mais comment est-elle construite, ou plus exactement « définie »...justement...?

La suite ne me pose plus de problème(dans « l’ordre »: théorème, modèle,consistance(mais pour autant que je lève mes blocages précédents..), décidabilité.
Encore merci GBZM,

Martial : Je ne le définis pas, j'en prends un. Ce choix fait partie de la distribution de valeurs de vérité.

Amathoue : tu connais la méthode des tables de vérité pour le calcul propositionnel classique ? On choisit des valeurs de vérité 0 ou 1 pour les variables propositionnelles, et on en déduit des valeurs de vérité pour pour toutes les propositions par les règles bien connues pour les connecteurs logiques.
Pour la sémantique topologique du calcul propositionnel intuitionniste, on choisit un espace topologique, on choisit des valeurs de vérité qui sont des ouverts de cet espace pour les variables propositionnelles, et on en déduit des valeurs de vérité pour toutes les propositions, par les règles que j'ai rappelées pour les connecteurs logiques.

Le système de déduction pour le calcul propositionnel intuitionniste (et aussi celui pour le calcul propositionnel classique) se formalise bien dans le calcul des séquents inventé pas Gentzen, un des "pères fondateurs" de la théorie de la démonstration (branche de la logique mathématique qui s'intéresse aux propriétés des démonstrations dand tel ou tel système de déduction).

JL a écrit:

GBZM, pour mon point 3, tu dis que la décidabilité de l'égalité dans N en logique intuitionnisme se démontre.Mais alors je trouve un peu trompeur le propos de P.Ageron qui laisse entendre que c'est "la traduction mathématique d'une pensée philosophique".

Et tu as parfaitement raison. JPA n'a pas sauté assez de lignes, ni statuté assez son changement d'angle.

La phrase $(n=0$ ou $n\neq 0)$ a une preuve par récurrence que tu es tout à fait capable de produire toi-même! Il n'y a même pas besoin de te corriger cet exercice. Et tu verras bien en le faisant qu'à aucun moment tu n'as recours à la partie non intuitionniste des axiomes logiques.

J'en viens aux addictions philosophiques de Jean Louis et Amathoué.

1/ Toute votre perplexité part du fait qu'il préexiste des choses en vous, que je vais tenter de décrire, pour ensuite voir comment en sortir partiellement, et paramétrer.

2/ A vrai dire, c'est vite dit: une phrase habite $\{vrai; faux\}$ (ou ne mérite pas de s'appeler "phrase sensée").

3/ Mais remontons un peu plus en amont.

4/ Les textes de science sont des suites de mots (séparés par des espaces). Parmi eux, on distingue une sorte de suite de mots, appelées "phrases" qui "se suffisent à elles-mêmes" dans la convention lecture-écriture d'un texte de science. Par exemple, on écrit $2+2=50$ pour affirmer que $2+2=50$, mais on n'écrira pas $3+ = 70-$.

5/ Les preuves (j'utilise un théorème à moi, ça simplifiera drastiquement) sont des phrases $p$ telles qu'il existe $a,b$ vérifiant $p=(a\to b)$ et $p$ est une conjonction* d'axiomes et $a$ est un axiome. Le théorème prouvé par $p$ vue comme preuve est alors $b$. Evidemment en pratique on a inventé des usines à gaz racourcissantes, mais ici c'est hors-sujet, puisqu'on ne discute pas de pratique. J'utilise le terme "évidence" au besoin pour abréger "conjonction d'axiomes".

6/ Jusque là pas de souci, mais une remarque. Tout ceci ne dit rien de ce qu'on appelle "un axiome".

7/ Et bien c'est très simple: "axiome" ça ne veut rien dire. Ou plus précisément, ça veut dire "hypothèse pérenne". N'importe qu'elle phrase (qui est une implication) est une preuve, puisque partant d'elle il est facile de recenser ses axiomes et sa conclusion. Pour la plupart des phrases $a\to b$, la liste d'axiomes est $a;a\to b$. Mais il peut arriver que non, et ça a fait exister les maths. Par exemple la phrase $(a\to (b\to c)) \to c$ vue comme une preuve démontre $c$ à partir des axiomes $a;b$; et $a\to (b\to c)$

8/ Autrement dit, l'idée de théorie (ie d'ensemble d'axiomes) n'est ABSOLUMENT PAS CONTRAINT par ce que je viens de raconter de 3 à 7.

9/ Ca s'appelle "la description syntaxique de la science".

10/ La description sémantique de la science est la suivante:

11/ On a des phrases, formant un ensemble, disons $P$. Maintenant je ne parle plus de suites de signes mais de valeurs. Toutes les suites de signes désigneront leur valeur.

12/ Cet ensemble de phrases sera supposé ordonné par un ordore partiel que je note $\leq$. Il contient aussi une phrase, notée $1$. Il est pertinent de traduire un français $x\leq y$ par $<<y$ est un cas particulier de $x>>$

13/ Il est aussi doté d'une opération binaire, notée $\to$ qui est décroissante à gauche et croissant à droite. En outre $(1\to y) = y$ pour toute phrase $y$.

14/ L'ordre est généralement supposé complet (c'est l'ajout d'un platonisme partiel), ce qui permet d'avoir le quantificateur $\forall$ de manière totalement décomplexée: $\forall x\in G: R_x$ est juste une abréviation de $inf(\{p\mid \exists u\in G: p=R_u\})$

15/ Et bien tout ça , ça n'a jamais obligé $P$ à avoir le cardinal $2$.

16/ On peut ajouter des contraintes. On peut demander qu'il existe une application $\neg$ de $P\to P$ qui est involutive et décroissante.

17/ Et bien tout ça n'empêche toujours en rien $P$ de NE PAS AVOIR LE CARDINAL 2

18/ on peut ajouter des tas d'autres contraintes, mais il faut aller très loin pour forcer $P$ à avoir le cardinal $2$ (je vous conseille d'assayer).

19/ Comment fait-on des maths?

20/ Et bien c'est très simple: une fois qu'on a $(P, \leq, \to, 1, \neg)$ et une structure (je prends la signature relation ternaire) $(A,R)$ où $R$ est une application de $A^3$ dans $P$, tous les énoncés clos ont une valeur dans $P$, tous les énoncés à une var libre ont une valeur tacitement (en mettant $[x\mapsto] $ devant) dans $P^A$, tous les énoncés à deux var libres (ordonnées alphabétiquement par exemple) ont une valeur dans $P^{(A^2)}$, etc. Rien de plus trivial.

21/ Ces énoncés sont fabriqués à partir de $R$, $\to$ et $\forall$.

22/ Les $P$-théorèmes sont les éléments $\geq 1$, et si on fait un retour au syntaxique, ce sont les epxressions dont on peut prouver (classiquement) qu'elles sont $\geq 1$.

23/ Bref, en conclusion, calculer des valeurs de phrases, ce n'est pas calculer dans $\{vrai; faux\}$.

24/ D'où viennent du coup, les logiques qui émergent de ça?

25/ Et bien déjà, on n'est jamais descendu en dessus de ne pas admettre que $\forall x,y,z: (x\to (y\to z))=(y\to (x\to z))$ qui exprime la commutativité du "et" qui est défini par $(a\ et\ b) := \forall x\in P: ((a\to (b\to x)) \to x)$. Cela provient du fait que les scientifiques, à la recherche de certitudes absolues et formelles, ne considèrent pas comme intéressant de faire la différence entre les deux suites suivantes:

25.1/ si a alors si b alors c
25.2/ si (a et b) alors c

26/ Ensuite, on considère une auto-réflexion que personne ne peut contester sous la forme :

$$ \forall x,y: ([x\leq y]\iff [1\leq (x\to y)]) $$

C'est là le point qui fait qu'on "est en logique" et pas seulement en maths (maths = branche de la logique = logique appliquée à des choses concrètes). On a une opération qui vient "refléter" un ordre. Le $\iff$ est juste une abréviation du bon vieux "si et seulement si" de vos habitudes, ce n'est pas une opération de $P$.

27/ Du coup, $1$ a tendance à mériter de s'appeler "le vrai" et $0:=\neg(1)$ s'appelle "le faux". Mais ayant admis tout ça, on est encore très loin d'avoir "peu de $P$", et très loin de pouvoir dire que tous les $P$ ainsi ont le cardinal $2$.

28/ Toutes les qualités que je viens d'ajouter ne donnent même pas à $1$ le "grand privilège" d'être le plus grand élément de $P$. Autrement dit, même avec ces contraintes, il existe des phrases dont le vrai n'est pas un cas particulier

29/ Exercice: $1$ est le max de $P$ si et seulement si $\forall x,y: x\leq (y\to x)$. Et bien ça (le fait que $1$ soitl e max de $P$, on peut l'appeler l'axiome des poubelles gratuites. En logique formelle propositionnelle des débuts d'étude de logique, c'est l'axiome écrit sous la forme : A=>(B=>A). Pourquoi ce nom poétique. Et bien parce qu'il dit qu'on peut jeter des hypothèses.

30/ Et là encore on n'a pas grand-chose. Par exemple, en dehors de la complétude de l'ordre, la structure:

30.1/ $P:=\R$
30.2/ $(a\to b) := (b-a)$
30.3/ ordre usuel
30.4/ $\neq := (x\mapsto (-x))$

est une PARFAITEMENT BELLE structure de phrase, dont les théorèmes sont juste les nombres négatifs ou nuls (autrement dit, ceux qu'on peut acheter avec un porte-monnaie vide)

31/ Le truc qui fait tout exploser est tout bête et très platonicien. C'est l'axiome (qu'il ne faut SURTOUT pas ajouter) suivant: $\forall x: (x\ et\ x)=x$

32/ Si vous ajoutez cet axiome, vous n'avez plus rien (enfin vous avez la logique classique, complète pour la représentation "une phrase doit être dans $\{vrai; faux\}$", c'est à dire une algèbre de Boole dont les quotients intègres sont $\{vrai; faux\}$ et son environnement platonico-affectif)

33/ La logique intuitionniste. Pourquoi passe-t-elle à la trape?

34/ Et bien elle ne passe pas à la trappe. Elle émerge juste de deux façons fondamentalement différentes.

34.1/ Ou bien on la découvre "accidentellement", on la subit et on l'étudie (plans non arguésiens)
34.2/ Ou bien on la "voit" bien avant qu'elle ne se manifeste (géométrie projective correcte).

35/ Quand $P$ a les propriétés ci-dessus, on peut ajouter comme hypothèse qu'il existe une application $\Rightarrow$ allant de $P^2$ dans $P$ qui est telle que $\forall x,y: (x\Rightarrow y) = ((x^\infty)\to y)$. Ca c'est l'approche 34.2.

36/ L'approche (peu pertinente et plus difficile) consiste à renoncer à la présence de $\neg$ et à supposer "d'emblée" (ça écrasera presque tout, donc nous rendra aveugles partiellement) que $\forall x: (x\ et\ x)=x$. C'est l'approche 34.1.

37/ Dans cette approche, on se retrouve avec une situation assymétrique "idiote" car on a écrasé les raisons (qui maintenant semblent arbitraires) qui vont provoquer l'assymétrie. On "subit" l'assymétrie. Comme le corpus des matheux fonctionne à coups de crédits, de problèmes ouverts, de résolutions en 150 pages de problèmes difficiles, il est naturel que ce soit cette voie "dangereuse et arbitraire" qui ait été choisie. Car "peu naturelle", elle génère des maths difficiles (c'est tout le mouvement catégories-topos-Grothendieck-degré 0 d'incertitude, donc algèbre)

38/ Dans cette approche, le $P$ obtenu s'appelle "une algèbre de Heyting".

39/ J'en reviens au tout début.

40/ Si vous y regardez de très près, il n'est pas vrai du tout qu'une phrase mathématique a une valeur dans $2:=\{vrai; faux\}$. Donc VOUS NE DEVRIEZ PAS VOUS ETONNER que les valeurs de vérité (ce sont les éléments de $P$ ou du $P$ choisi pour faire des maths) ne soient pas toutes dans cette ensemble. En effet, une phrase de maths courante est une application de $E\to 2$ où $E$ est l'ensemble des modèles de la théorie choisie pour faire des maths. C'est bien une algèbre de Boole, mais elle n'est pas du tout intègre. Car vous ne précisez que rarement dans quel modèle vous êtes (en fait, même vous ne le précisez jamais).

41/ Vous avez DONC TORT de parler trop vite en disant "dans $\{vrai; faux\}$". C'est un parfait abus de langage avachi. Ce que VOUS VOULEZ REELLEMENT EXPRIMER est qu'une fois quotienté par un idéal premier, on se retrouve dans $F_2$. Ce n'est pas du tout pareil. Et bien, ce que je viens de vous dire, c'est que quand on n'est pas dans un anneau de Boole, les quotients par des idéaux premiers ne sont pas forcément $F_2$, ET POURTANT quasiment toutes les règles de déduction y sont valables et on peut faire des maths. Et selon telle ou telle règle qui manque on donne tel ou tel nom à la logique.

42/ La réponse à votre perplexité est donnée de 1 à 21 et le reste précise techniquement la situation.

Merci beaucoup Christophe pour cette explication (détaillée)edit : je t’ai remercié avant d’avoir tout lu bien sûr, eh bien j’attends ton post suivant avec impatience!!!
Merci également à toi Martial pour les références!!

Merci beaucoup Christophe.
J’ai fait une première lecture mais j’ai besoin de relire plusieurs fois.
La fin de la définition de la « description sémantique de la science » m’aide déjà à y voir un peu plus clair.
Tu réponds clairement à l’un de mes blocages: les valeurs de vérité sont définies par récurrence sur les énoncés: c’est ton point 20.
Quant au cardinal de $P$ (dont la conclusion sémantique apparaît au point 17), je dois encore relire pour l’accepter.
J’aime beaucoup 40 et 41, il y a comme un air familier dans ces explications :-).
Encore merci pour t’être donné la peine de nous avoir aidé(enfin je parle pour moi).
Je reviens vers toi prochainement.

Pour te donner un idée de "à quel point" l'intuitionisme a du mal avec le TE, tu prends un espace topologique connexe (il en existe des pelletés :-D ) .

Dès lors que tu as "A ou B" qui est un théorème, il n'est pas possible que "non(A et " en soit un, sauf à considérer que pour cet espace, l'une des deux parmi A,B soit déjà un théorème. Idem avec $\exists$.

Ce truc a fait totalement décoller les gens qui l'ont perçu uniquement syntaxiquement au début du siècle, et ça a généré des passions (et donc des découvertes).

Mais il est souvent perçu à tort en oubliant qu'on parle de théorème sans hypothèse, hélas. Le fait que

$$ (A\ ou\ \to (A\ ou\ $$

ne permet pas de déduire que $(A\ ou\ \to A$ est prouvable ou que $(A\ ou\ \to B$ l'est. En bref, vive l'émotion qui fait visiter les jungles.

A propos de Cohen, je feuillette l'édition de 2009 de "Set Theory and the Continuum Hypothesis".
Au bas de la page 113 on trouve une définition qui commence comme ça :
A "labeling" is a mapping defined in ZF, which assigns to each ordinal $0<\alpha<\alpha_{0}$ a set $S_{\alpha}$, the "label space", etc.

Comment, dans ce contexte, traduire "labeling" et "label" ?
Les mots "étiquetage" et "étiquette" me paraissent fortement inadéquats.

@Christophe : Mouais, pourquoi pas ?
Faut qu'j'voye.

Sinon, tu penses que l'ouvrage de Cohen peut être un bon plan pour essayer de bien comprendre le forcing ?

Comme je suis vraiment une tanche en intuitionnisme je vais poser une question qui renferme tout (comme disait ma grand-mère) : où est-ce qu'on peut trouver, dans la littérature, un ouvrage qui explique ces choses-là de façon compréhensible pour un néophyte ?
Je veux dire : PA nous explique bien comment se passer du TE, du RPA ou de la règle de contraposition, mais quand même, par rapport à la citation de Jean-Louis au sujet de la page 15 : "postuler que l'égalité dans $\N$ est décidable (…) est la traduction mathématique d'une position philosophique", je trouve qu'il se fout un peu de notre gueule (il = PA, pas Jean-Louis, œuf corse). Et ce d'autant plus que si j'ai bien compris, ces choses-là se démontrent, mais à condition de sortir l'artillerie lourde des assertions à valeurs de vérité dans une algèbre de Boole, ou dans l'algèbre des ouverts d'un espace topologique. Or c'est ça qui me manque. PA n'en parle pas, et j'aimerais bien savoir où trouver ça.
En gros, je cherche une référence sérieuse, introductionnelle et pédagogique, pas forcément exhaustive.
Merci d'avance
Martial

Et mreci à toi Poirot!

@Martial: comme je pense savoir ce que tu veux comprendre et comme GBZM et foys ont répondu sur certains points, je produis un post qui je l'espère t'aidera à profiter du leur. Je vais prendre les choses beaucoup plus en amont et corriger les erreurs (parfois heureuses) de l'histoire scientifique du 20ie siècle pour t'éviter d'errer.

1/ L'idée clé, dans ton contexte, c'est la règle du jeu, ou, pourrait-on dire autrement, la syntaxe-grammaire, etc.

2/ Je ne vais donc pas aborder la sémantique (foys vient de le faire par exemple).

3/ Dans un premier temps, je te conseille VIVEMENT de NE PAS tout de suite lire les docs (que je n'ai pas lu, mais je devine) de GBZM où figurent le symbole $\vdash$, qui à lui seul, est une véritable catastrophe, car renferme à la fois des erreurs historiques, des crispations, des changements de sens, etc, le tout nourri à la recherche récente qui n'est accessible qu'à des habitués ayant dû fortement évoluer du platonisme vers l'opératoire quasiment physique.

4/ Prouver quelques chose veut dire écrire un texte qui est lui-même une suite de trucs.

5/ Les trucs sont des phrases.

6/ Initialement ces phrases ont forcément une valeur dans $\{vrai; faux\}$, mais ça c'est très platonicien à cause de la main invisible "qui sait" et qu'on essaie d'imiter.

7/ Cette notion de cardinal 2 doit être absolument comprise en termes opératoires.

7.1/ Quand deux scientifiques se disputent sur une île déserte, il n'ont que 2 choix de jeux (de règle du jeu).

7.2/ Choix1, ils sont d'accord sur qui a la charge de la preuve et dans ce cas, il n'y a STRICTEMENT AUCUN PROBLEME, fin de l'histoire. Tous les devoirs sont du côté du prouveur, le sceptique n'ayant quasiment rien à faire

7.3/ Choix2: il n'y a pas d'accord. Leur désaccord tient alors à la vérité de la phrase: l'un dit qu'elle est fausse, l'autre dit qu'elle est vraie. Ils vont alors jouer non pas à un jeu "prouveur-sceptique" mais à un "jeu de la vérité".

8/ C'est de là que vient qu'une phrase est dans $\{vrai; faux\}$ et que le non est involutif puisqu'il est juste une permutation dans $S_2$ (la seule qui ne soit pas l'identité), en échangeant les 2 rôles.

9/ Comme je l'ai souvent déjà dit, les règles du jeu de la vérité sont très simples:

9.1/ Devant $a\to b$, c'est au défenseur de vrai de choisir entre continuer avec $b$ et continuer avec $non(a)$

9.2/ Devant $non(a)$ les rôles sont échangés et on continue avec $a$

9.3/ devant $\forall xR(x)$, c'est au défenseur de faux de choisir $x$ (il va poser $x:=u$) et on continue avec $R(u)$

9.4/ devant $a\ et\ b$ c'est à faux de jouer (il choisit si on continue avec $a$ ou si on continue avec $b$)

9.5/ etc (il est facile de réglementer les connecteurs).

9.6/ Par exemple: devant $\exists xR(x)$, c'est au défenseur de vrai de choisir $x$ (il va poser $x:=u$) et on continue avec $R(u)$


10/ La partie termine sur une phrase qui tranche et le jeu est terminé, ils se sont mis d'accord.

11/ Ca ne veut pas dire qu'ils ont bien joué, mais c'est la rançon à payer d'habiter sur une ile déserte.

12/ En conclusion de ce préambule, les maths sont symétriques et il n'y a pas lieu de considérer une assymétrie entre vrai et faux.

13/ Une preuve classique est une stratégie automatique pour gagner qui peut être programmée, mais attention, toutes les stratégie automatiques ne sont pas des preuves. Il y a une uniformité comme contrainte de plus pour être une preuve. Par exemple, il existe des tas de stratégies automatiques qui gagnent à $\forall nR(n)$ quand elles défendent le vrai, mais sans pour autant qu'on ait une preuve de $\forall nR(n)$.

14/ Il y a de fortes exigences sur ce que doit être une preuve pour garantir des certitudes formelles absolues qui en font pluss que de simples stratégies. C'est la grande surprise, bien qu'ayant une preuve triviale, qu'a été le théorème de complétude de Godel que de dire que "ça suffit" de ne pas avoir de preuve pour ne pas avoir de "définitivement" de certitude formelle.

15/ Comme tu vas voir les règles du jeu sont très très simples et "acceptables" par tous.

16/ Je vais légèrement modifier le vocabulaire habituel.

17/ J'appelle "assertion" une liste finie de phrases

18/ J'appelle phrase un objet qui peut être, mais ce n'est pas obligé précédé du signe @, ou qui est le mot "BINGO"

19/ Exemple d'assertion: a; b=>c; t; @(u=&gt;k); c=>k; @a

20/ Attention, @a)=a

21/ Moralement, une assertion affirme que telle liste de ressources peuvent être utilisées pour aller au paradis

22/ On peut procéder à des éliminations et certaines contractions évidentes, comme suit:

23/ ....; @BINGO; ..... peut être suivi de ..; X; @X; ...

24/ Tu peux aussi remplacer .....A; @B...... par @(A=&gt;B)

25/ Et enfin la seule chose (avec la coupure) qui te fait passer de DEUX assertions à une seule est la règle suivante:

De $\Gamma; @A$ et $\Delta; $ B passer à $\Gamma; Delta; (A\Rightarrow $

$\Gamma, \Delta$ étant des listes.

26/ Ca, ce sont les règles du jeu "de fond" des garanties scientifiques. Mais à ça, il faut ajouter:

27/ La possibilité de permuter les éléments de la liste

28/ La possibilité d'en rajouter (un supplément de ressources ne change rien à mon accès au paradis)

29/ Et la pire de toutes, littéralement explosive (et qui oblige et permet à la science d'être platonicienne), la CONTRACTION:

le droit de passer de ....; X; X; ..... à ....;X;........

30/ Règle sulfureuse (appelée coupure): passer de $\Gamma; A$ et $\Delta; @A$ à $\Gamma; \Delta$

31/ Et bien sache que le théorème de Godel (qui avec cette présentation est facile à prouver) dit que ces règles suffisent à prouver irréfutablement tout de ce qui est vrai dans tout monde où toutes les phrases vivent dans $\{vrai; faux\}$

32/ Quelques remarques:

32.1/ La règle de coupure est redondante, mais prouver cette redondance a occupé pas mal de logiciens pendant pas mal de temps

32.2/ Tous les autres connecteurs s'obtiennent à partir de =>

32.3/ Avec ces règles, "@ fonctionne un peu comme non". Mais ce n'est pas "non", c'est juste la permutation des deux joueurs

32.4/ L'ajoute des quantificateurs est suffisamment triviale pour que je n'en parle pas

32.5/ La règle de coupure est une erreur historique qu'on a découvert hélas que récemment comme erronée. En effet, la bonne règle est

passer de $\Gamma; A$ et $\Delta; @B$ à $\Gamma; \Delta; (A=>B)$ et une sorte de confiance platonicienne en la réalité de tout ça consiste à dire "mais virez-moi ce (A=>A), vu qu'il est évident.

32.6/ Cette erreur a été découverte (par moi :-D , mais est visiblement ressentie inconsciemment par beaucoup) à cause de l'informatique. Je te la reformules en termes de modus ponens.

32.6.1/ Modus ponens: ayant prouvé A=>B ainsi que A, je peux dire "donc B". Ca c'est une superbe erreur!!! Pourquoi?

32.6.2/ Pour le comprendre il faut d'abord regarder la bonne règle:

32.6.3/ Modus ponens correct: ayant prouvé A=>B ainsi que C, je peux dire "donc (C=>A)=>B". Certes appliqué avec $C=A$, ça donne une conclusion de la forme (A=>A)=>B qui parait du gaspillage d'encre, mais qui ne doit pas être négligée, car l'implémentation des phrases en informatique n'est jamais garantie ni bien fondés (pas de cycle), ni direct (ce sont des pointeurs). Or le MP ne marche pas avec les seuls pointeurs, il faut parfois s'assurer en fouillant une égalité "de fond" que A=A (précisément que deux pointeurs différents décrivent la même phrase).

Or comment marche la procédure de vérification d'égalité conceptuelle? Comme suit:

egal(X,Y):= if feuille(X) then if feuille(Y) then $X=_{physique} Y$ else ... else if egal(hyp(X), hyp(Y)) then egal (conc(X), conc(Y)) else false.

33/ J'arrête là le point 32. Je t'invite à bien t'apercevoir que le modus ponens correct EST DEJA dans la règle du jeu: c'est la règle 25.

34/ Maintenant tu te demandes peut-être où est la logique intuitionniste dans tout ça?

35/ Et bien c'est très simple:

36.1/ Un théorème (classique) de maths est une assertion qu'on peut prouver en partant d'une liste contenant BINGO et en respectant les règles de constructions ci-dessus.

36.2/ Un théorème (au sens intuitionniste) de maths est une assertion qu'on peut prouver en partant d'une liste contenant BINGO et en respectant les règles de constructions ci-dessus PLUSSSSSS la condition très restrictive qu'aucune assertion de la liste ne contienne plus d'une seule fois le symbole @.

37/ C'est cette assymétrie très défavorable aux pointeurs qui a fait accidentellement (un accident heureux car a donné des recherches en territoire montagneux, on s'est offert des randonnées gratuites) émerger la logique intuitionniste.

38/ Tu te demandes peut-être si cette névrose apparait ailleurs dans les maths et l'informatique.

38.1/ Et bien la réponse est oui: en informatique elle apparait de façon spectaculaire via l'obsession pour le mot function. Il n'était strictement nullement nécessaire ne PASCAL par exemple (je pense que tu as du programmer en PASCAL), puisqu'une fonction(x,y,..):z n'est qu'une procédure (x,y,...; var z); qui d'ailleurs en C s'écrit procédure (x,y,...; z);

38.2/ On le voit aussi en maths, où la notion de fonction (univoque) a pris le pas sur celle de relation (ou fonction multivoque).

38.3/ Exercice: trouver plein d'autre endroits où la névrose s'est épanouie.

39/ Maintenant que tu sais tout, exercice :-D : prouver le RPA quand on n'est pas contraint par (36.2)

C9/ La CCH (correspondance de Curry Howard consiste à remarquer que les règles du jeu (lues à l'envers) sont réellement utilisables sans ressources et sans peine dans la vraie vie. et en particulier, utilisées en informatique, traduisent toutes les preuves en programmes garantisseurs de leur spécifications.

C10/ Moins connue, et réciproquement.

C11/ Exception notable: la règle de clonage (passage de X;X à X) n'est pas PHYSIQUEMENT réalisable. La règle de la poubelle gratuite non plus (les déchets prennent de la place).

Exercice concernant C11: retrouve les numéros dans mon post des deux règles que j'évoque en C11. Si tu y parviens ça voudra essentiellement dire que tu as tout compris.

C15/ J'en termine là, après je me déconnecte. Je te raconte le "drame" scientifique tel qu'il a été construit fin 19ie, début du 20ie, avec une sorte de "sortie progressive" en train de se produire depuis quelques décennies.

C16/ On a cherché longtemps des théorie consistantes "définitives". Godel a mis une fin partielle à cette idée, et la CCH l'a définitivement et totalement condamnée de lamanière suivante, qui est très simple et se lit "mot à mot" dans la CCH:

C16.1/ Chercher une théorie consistante c'est comme chercher un OS (opérating system) qui s'arrête. Autrement dit, c'est complètement débile puisque sa vocation est de ne pas s'arrêter (donc d'être une théorie contradictoire).

C16.2/ La conception abstraite des solides n'est pas représentable mathématiquement. Je ne te prends que la dimension1. J'ai deux bloc des glaçons, l'un occupant $[0,1]$ et l'autre occupant $[1,2]$ qui ont le devoir d'être superposable. Et bien ça va pas, car ils ne sont pas assez "solides" pour ne pas partager $1$. Ok, alors essayons l'un occupant $]0,1[$ et l'autre occupant $]1,2[$. Grr, :-X ça va pas non plus puisqu'il y a "l'espace" $1$ entre les deux.

C16.3/ L'ostratisation de $\{x\mid x\in x\to P\}$, qui est littéralement parlant une phrase représentant la moitié de $P$ (autrement dit, s'obtenant avec la moitié des ressources qui permettent d'obtenir $P$), en vue (inconsciente) de conserver le droit de cloner à volonté les garanties scientfiques (une photocopie d'une preuve est une preuve).

C16.4/ La logique intuitionniste (qui n'est qu'une découverte tardive et syntaxique des espaces topologiques connexes), qui a caché longtemps les "bonnes logiques" qui sont un peu plus faibles, etc

C16.5/ L'extensionalité (qui écrase tout, mais donne bcp quand on suppose le père Noel) trop souvent recherchée à être remise artificiellement. (Remarque: sans l'extensionalité, la science est fortement normalisable et tous les OS s'arrêtent ou sont EXPLICITEMENT prévus pour boucler)

C17/ En résumé (vu ta situation de "vacancier"), je pense que tu peux te permettre de passer directement de la logique classique aux logiques faibles et de faire l'impasse sur l'intuitionniste, qui demande, du fait de sa nature accidentelle et usine à gaz, extrêmement dure à étudier. Elle est d'ailleurs, de manière évidente, PSPACE-complète rien qu'avec implique (et indécidable en ajoutant juste $\forall$).

C18/ Le RPA je te rappelle que c'est (je prends l'énoncé le plus monsieur tout le monde) :

$$ ((A\to \to C)\to ((A\to C)\to C)$$

qui moralement dit que si je sais faire C quand on me donne aussi bien que quand on me demande A alors je sais faire C tout court

contient EN LUI MEME la duplication, avec $C:=(A\to $, donc est malsain.

C19/ Je ne conseille pas tout de suite d'aller étudier la spécialité de Girard car il s'est gourré dans ses notatoins en oubliant de passer aux log:

il écrit $A\otimes (B+C) = (A\otimes + (A\otimes C)$
au lieu de
$A + sup(B,C) = sup( (A+B),(A+C))$

ce qui rend la lecture de ses travaux (de lui et de ses potes) particulièrement désagréable, avec des apparences d'arbitraire.

C20/ Mais selon ton évolution, je pourrais de signaler des bouquins.

@Martial, je te décris une autre activité amusante, très parente de ces sujets et qui a le mérite de te placer directement dans l'abîme laissé béant par l'absence de l'axiome du choix.

1/ On va accepter plusieurs signes et pas d'autres:

2/ Les signes $\cap$; $\cup$; $\times$; $\to$.

3/ Petite documentation sur $\to: X\to Y$ voudra dire "ensemble des applications de $X$ dans $Y$.

4/ On se place dans ZF (sans choix). Soit $E$ un ensemble inaccessible et $A$ un expressions utilisant des lettres ($n$ lettres) et ces signes.

5/ On dira que $A$ est "prouvable" quand toi, tu seras capable de prouver dans ZF, qu'il existe une application choix $\phi$ qui à chaque $(\dots)\in E^n : \phi(\dots]\in A$

6/ Exemples:

6.1/ $(A\cap \to A$ est un théorème :-D (pas très dur).

6.2/ $(A\cap \to (A\times $ en est-il un?

6.3/ $(A\to (B\cup C)) \to ((A\to \cup C)$ en est-il un d'après toi?

6.4/ $((A\cup \to C) \to ((A\to C)\times (B\times C))$

6.5/ Et la réciproque de (6.4)?

Et bien ça, tu vois ça te fait une nouvelle logique désopilante. Alors bien sûr, si tu n'utilises que $\to$, c'est la logique intuitionniste (et cette présentation te décrit sans le dire le principe de la CCH). Mais si tu utilises les autres signes, ça te fait une espèce de logique bizarre comme tout, à cause du $\cap$ et du $\cup$, mélangés avec le $\times$.

Toujours à Martial, Amathoué et JL, voici une chtite théorie innocente MAIS passionnante si vous vous intéressez à ces trucs-là.

J'appelle "Terre" un triplet $(E,\leq +,-)$ où $-;+$ sont associatives et commutatives allant de $E^2$ dans $E$, croissantes à droite à et gauche et où $\forall x,a,b: x+(a-b) \leq (x+a)-b$

Et bien ça résume tout (je vous dirai pourquoi plus tard).

Etant données deux expressions $a,b$ prouver que $a\leq b$ dans toute terre est NP-complet (c'est un bel exemple, car on n'a que des déplacements), y compris pour le jeu réduit à une seule lettre autorisée au total dans les 2 expressions.

Vous pouvez vous exercer à ce jeu.