Intuitionnisme et constructibiité
Je vais radoter une fois de plus, mais essayer d'éclaircir et formaliser certaines "modes" chez les matheux ayant soif de découvrir de nouvelles aventures raisonnementales.
Cependant, je mettrai des liens vers les moult fils que j'ai déjà ouverts sur ce thème de façon à créer un bloc d'infos.
L'ouverture de ce fil m'est inspirée par http://www.les-mathematiques.net/phorum/read.php?11,2047416,2061144#msg-2061144
Il faut savoir qu'en logique ce domaine est totalement exploré depuis longtemps (environ 90ans), je vais essayer de résumer l'état des choses en peu de mots (de toute façon, suis peu dispo), pour commenter ensuite les travaux "faits à la main" comme ceux de Claude et Henri par exemple.
1/ Il y a de nombreuses logiques, mais dans les circonstances qui nous occupent, essentiellement 3.
1.1/ La classique
1.2/ L'intuitionniste
1.3/ L'affine.
Leurs différences sssentielles sont:
En intuitionnisme, on n'a pas le droit d'admettre que $([A\to B]\to
\to (([B\to A]\to A))$ et tout ce qui l'implique de manière générale.
En affine on n'a pas le droit d'admettre que si en utilisant $A$ 2 fois on a prouvé $B$ alors on a prouvé sans rien que $A\to B$. On doit écrire qu'on a prouvé A=>(A=>B)
2/ Ceci est relié à 2 découvertes majeures:
2.1/ Le théorème de complétude (et en fait "les", il y en a un par logique)
2.2/ Qu'un programme ou une preuve c'est pareil.
3/ Tout ceci a fait l'objet de brouilons et recherche avant de finalement se présenter de manière achevée dans diverses phénomènes formels dont je vais parler.
4/ Il faut donc distinguer 6 choses:
4.1/ Preuves classiques avec coupures
4.2/ Preuves classiques sans coupures
4.3/ Preuves intuitionnistes avec coupures
4.4/ Preuves intuitionnistes sans coupures
4.5/ Preuves affines avec coupures
4.6/ Preuves affines sans coupures
5/ Y a-t-il des préjugés qui sont tombés (a) à la suite de ces découvertes? Leur chute est-elle connue (b)?
5.1/ (a) oui, il a été découvert que la logique intuitionniste n'est pas plus constructive que la classique et que le RPA n'introduit aucune non constructivité
5.2/ (b) non, c'est encore trop méconnu des non spécialistes et trop de "savants" ont encore trop tendance à croire que l'intuitionnisme apporte du consrtuctivisme
6/ Que veut dire constructivisme alors?
Réponse: en fait, si on épluche bien les choses et examine les preuves en détails, on s'aperçoit assez vite que sans le vouloir les savants non spé en logique utilisent le mot "constructif" en lieu et place de "sans coupure". Ca n'a rien à voir avec intuitionniste. Mais par une sorte de "serpent de mer culturel", ils continuent de confondre intuitionnisme et constructif.
7/ Est-ce que c'est grave? Réponse: non.
8/ Est-ce que ça induit des pertes de temps?
8.1/ Réponse: un peu oui, même parfois pas mal car on peut voir des gens chercher des heures une preuve intuitionniste à la main en espérant ainsi "constructiviser" la preuve initiale et .. ne pas y parvenir.
8.2/ La raison: il y en a en général 2:
8.2.1/ d'une part une preuve (partiellement, elles sont toutes partiellement seulement intuitionnistes) intuitionniste peut parfaitement n'avoir strictement rien de constructive (un théorème dont la preuve est évidente une fois connue les définitions, appelé "théorème de Statman", dit que la LI est PSPACE complète (autrement bien pire que la classique))
8.2.2/ D'autre part, une preuve classique absolument irréductible à une preuve nituitionniste peut être PARFAITEMENT CONSTRUCTIVE. Exemple: LI (tout jeu fini est déterminé) Exemple LC: 2 est bien ordonné
9/ Y a-t-il besoin d'inventivité?
Réponse importante: NON. C'est là la découverte cruciale de cette branche de la logique. L'algorithme est confluent et archi-connu pour "normaliser" (c'est le nom que ça porte) toute preuve. En particulier, (mais ce n'est qu'une toute petite partie du phènomène), on passe DANS LES 3 LOGIQUES de "avec" à "sans" au sens du point 4 ci-dessus.
10/ Peut-on décrire l'algo à des néophytes?
Réponse oui. Une coupure c'est juste quand vous procédez comme suit à un moment ou un autre de votre preuve:
<< Je veux prouver B. Bon bin, je vais prouver A d'une part et A=>B d'autre part. Je prouve A, blabla, CQFD donc A. Maintenant je prouve A=>B. [large]SUPPOSONS A,[/large] blabla, donc finalement B. Surconclusion: je viens donc de prouver A=>B, et comme j'avais prouvé A, on a donc bien B>>
Si je l'écris en séquents ça donne:
$$ \frac{\frac{B(using:A)}{A\to B} + \frac{\dots}{A}}{B} $$
Voilà, c'est ça une coupure.
En termes de jeu:
jeu tolérant pour prouver B:
option1 le prouveur propose A, le sceptique réponse en choisissant entre A et A=>B, avec quelle phrase on continue
option2 si B est de la forme X=>Y, le prouveur a le dr'oit de dire "je prends X" et on continue avec Y
jeu sans coupure:
en zone verte pareil, sauf que si le sceptique choisit A=>B ci-dessus passage en zone rouge
en zone rouge: l'option2 n'est pas autorisé
11/ Comment éliminer une coupure: bin c'est simple Vous remplacez "je prends A" par "je prouve A", ce qui donne en séquents:
La coupure
$$ \frac{\frac{B(using:A)}{A\to B} + \frac{ArgumentationZ}{A}}{B} $$
saute en remplaçant par
$$ \frac{\frac{ArgumentationZ}{A} + \frac{Feuille}{A\to B} }{B} $$
Autement dit chaque fois que vous utilisez A, vous le prouvez avant dans la partie appelée "feuille"
Attention: ça n'élimine QU'UNE COUPURE. Faut recommancer ad nauseum pour toutes les éliminer.
12/ Est-ce que ça va vite?
Réponse non: on peut prouver que c'est dans le cas le pire de l'ordre de $n\mapsto 2^{2^n}$ en longueur de preuves.
Un être humain peut donc s'amuser à "prendre des raccourcis, jouer de son flair, pour écrire des livres comme ceux de CQ et HL.
Cela dit, c'est aussi amusant de voir ce que donnent "les vraies" preuves sans coupures obtenues, en exécutant un logiciel. Mais ça ferait, par exemple si on avait elicuter de manière automatique les preuves des faits présents dans le livre de CQ et HL, très probablement 150000 pages et non pas 2000 (enfin je crois qu'ils ont ourné à 2000 eux deux)
13/ Constructivité?
Réponse: elle provient de ce que le RPA est un confort humain très usité mais la plupart du temps inutile. ELICUT le fait sauter.
14/ Quand le RPA reste?
Réponse: c'est un RPA constructif évident (c'est un échange de joueur (ie nonA est à la charge de Bob quand A est à la charge de Lea, ça ne compte pas)), qui fait juste boucler "par vocation" (par exemple un OS est un programme tout à fait concret, qui boucle et personne n'aurait l'idée de dire "ah, comme ça boucle, on n'aura pas de résultat à la fin, cet algorithme est un échec". Ce serait stupide de dire ça car on n'attend pas de résultat de Windows autre que de ne s'arrêter que quand on éteint l'ordi).
15/ Pourquoi j'ai évoqué l'affine?
Bin parce que c'est un EXCELLENT exemple où les preuves ne grossissent pas. La preuve sans coupure obtenue est de la même taille (avec la constructivité en plus) que la preuve "gros pacha qui gratte la lampe RPA" initiale (les mecs qui supposent d'office par l'absurde que tout ce qui bouge dans ce qu'ils veulent prouver est faux pour être tranquilles)
(Je me suis forcé, tapé à toute vitesse, n'hésitez pas à me signaler des coquilles).
Cependant, je mettrai des liens vers les moult fils que j'ai déjà ouverts sur ce thème de façon à créer un bloc d'infos.
L'ouverture de ce fil m'est inspirée par http://www.les-mathematiques.net/phorum/read.php?11,2047416,2061144#msg-2061144
Il faut savoir qu'en logique ce domaine est totalement exploré depuis longtemps (environ 90ans), je vais essayer de résumer l'état des choses en peu de mots (de toute façon, suis peu dispo), pour commenter ensuite les travaux "faits à la main" comme ceux de Claude et Henri par exemple.
1/ Il y a de nombreuses logiques, mais dans les circonstances qui nous occupent, essentiellement 3.
1.1/ La classique
1.2/ L'intuitionniste
1.3/ L'affine.
Leurs différences sssentielles sont:
En intuitionnisme, on n'a pas le droit d'admettre que $([A\to B]\to
\to (([B\to A]\to A))$ et tout ce qui l'implique de manière générale.En affine on n'a pas le droit d'admettre que si en utilisant $A$ 2 fois on a prouvé $B$ alors on a prouvé sans rien que $A\to B$. On doit écrire qu'on a prouvé A=>(A=>B)
2/ Ceci est relié à 2 découvertes majeures:
2.1/ Le théorème de complétude (et en fait "les", il y en a un par logique)
2.2/ Qu'un programme ou une preuve c'est pareil.
3/ Tout ceci a fait l'objet de brouilons et recherche avant de finalement se présenter de manière achevée dans diverses phénomènes formels dont je vais parler.
4/ Il faut donc distinguer 6 choses:
4.1/ Preuves classiques avec coupures
4.2/ Preuves classiques sans coupures
4.3/ Preuves intuitionnistes avec coupures
4.4/ Preuves intuitionnistes sans coupures
4.5/ Preuves affines avec coupures
4.6/ Preuves affines sans coupures
5/ Y a-t-il des préjugés qui sont tombés (a) à la suite de ces découvertes? Leur chute est-elle connue (b)?
5.1/ (a) oui, il a été découvert que la logique intuitionniste n'est pas plus constructive que la classique et que le RPA n'introduit aucune non constructivité
5.2/ (b) non, c'est encore trop méconnu des non spécialistes et trop de "savants" ont encore trop tendance à croire que l'intuitionnisme apporte du consrtuctivisme
6/ Que veut dire constructivisme alors?
Réponse: en fait, si on épluche bien les choses et examine les preuves en détails, on s'aperçoit assez vite que sans le vouloir les savants non spé en logique utilisent le mot "constructif" en lieu et place de "sans coupure". Ca n'a rien à voir avec intuitionniste. Mais par une sorte de "serpent de mer culturel", ils continuent de confondre intuitionnisme et constructif.
7/ Est-ce que c'est grave? Réponse: non.
8/ Est-ce que ça induit des pertes de temps?
8.1/ Réponse: un peu oui, même parfois pas mal car on peut voir des gens chercher des heures une preuve intuitionniste à la main en espérant ainsi "constructiviser" la preuve initiale et .. ne pas y parvenir.
8.2/ La raison: il y en a en général 2:
8.2.1/ d'une part une preuve (partiellement, elles sont toutes partiellement seulement intuitionnistes) intuitionniste peut parfaitement n'avoir strictement rien de constructive (un théorème dont la preuve est évidente une fois connue les définitions, appelé "théorème de Statman", dit que la LI est PSPACE complète (autrement bien pire que la classique))
8.2.2/ D'autre part, une preuve classique absolument irréductible à une preuve nituitionniste peut être PARFAITEMENT CONSTRUCTIVE. Exemple: LI (tout jeu fini est déterminé) Exemple LC: 2 est bien ordonné
9/ Y a-t-il besoin d'inventivité?
Réponse importante: NON. C'est là la découverte cruciale de cette branche de la logique. L'algorithme est confluent et archi-connu pour "normaliser" (c'est le nom que ça porte) toute preuve. En particulier, (mais ce n'est qu'une toute petite partie du phènomène), on passe DANS LES 3 LOGIQUES de "avec" à "sans" au sens du point 4 ci-dessus.
10/ Peut-on décrire l'algo à des néophytes?
Réponse oui. Une coupure c'est juste quand vous procédez comme suit à un moment ou un autre de votre preuve:
<< Je veux prouver B. Bon bin, je vais prouver A d'une part et A=>B d'autre part. Je prouve A, blabla, CQFD donc A. Maintenant je prouve A=>B. [large]SUPPOSONS A,[/large] blabla, donc finalement B. Surconclusion: je viens donc de prouver A=>B, et comme j'avais prouvé A, on a donc bien B>>
Si je l'écris en séquents ça donne:
$$ \frac{\frac{B(using:A)}{A\to B} + \frac{\dots}{A}}{B} $$
Voilà, c'est ça une coupure.
En termes de jeu:
jeu tolérant pour prouver B:
option1 le prouveur propose A, le sceptique réponse en choisissant entre A et A=>B, avec quelle phrase on continue
option2 si B est de la forme X=>Y, le prouveur a le dr'oit de dire "je prends X" et on continue avec Y
jeu sans coupure:
en zone verte pareil, sauf que si le sceptique choisit A=>B ci-dessus passage en zone rouge
en zone rouge: l'option2 n'est pas autorisé
11/ Comment éliminer une coupure: bin c'est simple Vous remplacez "je prends A" par "je prouve A", ce qui donne en séquents:
La coupure
$$ \frac{\frac{B(using:A)}{A\to B} + \frac{ArgumentationZ}{A}}{B} $$
saute en remplaçant par
$$ \frac{\frac{ArgumentationZ}{A} + \frac{Feuille}{A\to B} }{B} $$
Autement dit chaque fois que vous utilisez A, vous le prouvez avant dans la partie appelée "feuille"
Attention: ça n'élimine QU'UNE COUPURE. Faut recommancer ad nauseum pour toutes les éliminer.
12/ Est-ce que ça va vite?
Réponse non: on peut prouver que c'est dans le cas le pire de l'ordre de $n\mapsto 2^{2^n}$ en longueur de preuves.
Un être humain peut donc s'amuser à "prendre des raccourcis, jouer de son flair, pour écrire des livres comme ceux de CQ et HL.
Cela dit, c'est aussi amusant de voir ce que donnent "les vraies" preuves sans coupures obtenues, en exécutant un logiciel. Mais ça ferait, par exemple si on avait elicuter de manière automatique les preuves des faits présents dans le livre de CQ et HL, très probablement 150000 pages et non pas 2000 (enfin je crois qu'ils ont ourné à 2000 eux deux)
13/ Constructivité?
Réponse: elle provient de ce que le RPA est un confort humain très usité mais la plupart du temps inutile. ELICUT le fait sauter.
14/ Quand le RPA reste?
Réponse: c'est un RPA constructif évident (c'est un échange de joueur (ie nonA est à la charge de Bob quand A est à la charge de Lea, ça ne compte pas)), qui fait juste boucler "par vocation" (par exemple un OS est un programme tout à fait concret, qui boucle et personne n'aurait l'idée de dire "ah, comme ça boucle, on n'aura pas de résultat à la fin, cet algorithme est un échec". Ce serait stupide de dire ça car on n'attend pas de résultat de Windows autre que de ne s'arrêter que quand on éteint l'ordi).
15/ Pourquoi j'ai évoqué l'affine?
Bin parce que c'est un EXCELLENT exemple où les preuves ne grossissent pas. La preuve sans coupure obtenue est de la même taille (avec la constructivité en plus) que la preuve "gros pacha qui gratte la lampe RPA" initiale (les mecs qui supposent d'office par l'absurde que tout ce qui bouge dans ce qu'ils veulent prouver est faux pour être tranquilles)
(Je me suis forcé, tapé à toute vitesse, n'hésitez pas à me signaler des coquilles).
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Réponses
-
Quelques compléments.
Il y a d'autres préjugés. En voici un:
P1/ "plus il y a des coupures moins c'est constructif" (ou plus c'est mystérieux)
C'est faux. La fonction n'est pas du tout monotone, elle est en cloche. En coupant de plus en plus une preuve (coupée, mais pas trop coupée), vous arrivez non pas à des preuves de plus en plus mystérieuses, mais à des preuves de plus en plus évidentes. Et (sans exception), vous finirez toujours par tomber sur X=>X, dont on ne peut pas dire que ce soit un énoncé "mystérieux" (en fait si mais je ferai un autre post pour dire en quoi il l'est).
P2/ Rappel, donc: un énoncé difficile à prouver L'EST TOUJOURS PARCE QU'IL EST TROP UN CAS PARTICULIER DES EVIDENCES DONT L'EST.
Vous avez donc deux bouts en quelque sorte:
B1/ L'aspect sans coupure (ou une simple lecture quasi-linéaire de la preuve vous indique que la conclusion était affirmée par l'hypothèse)
B2/ L'aspect "totalement surcoupé" où votre théorème est en conclusion d'un énoncé X=>X où toutes les hypothèses sont des truismes dégradés (des trucs de la forme A=>(B=>A, etc)
P3/ En résumé, c'est "au sommet de la cloche" qu'on trouve les preuves les plus "épatantes" au sens qu'on a bien une preuve devant soi et qu'on garde vaguement une sensation que le truc n'est pas prouvé.
P4/ J'explique comment surcouper:
Vous venez décrire
A=>B
B=>C
C=>D
donc A=>D
considérant A=>B;B=>C;C=>D comme évidents.
Vous avez en fait construit $f,g,h$ allant respectivement de $A$ dans $^B$, de $B$ dans $C$ et de $C$ dans $D$ et les avez composé en $h\circ g\circ f$ qui va de $A$ dans $D$.
La personne qui voit A=>D se demande bien quelles preuves peuvent exister de ça. La preuve est coupée, mais pas trop coupe, elle est mystérieuse, car dans le cas général, il faut TROUVER (avec de l'inspiration) B,C
Bon bin, un surcoupage évident vous donne:
((A=>[((B=>C)=>C)])=>[((B=>C)=>C)]) =>D
qui est:
1/ plus général (ie dont A=>D est une conséquence évidente
2/ et évident
Prix payé: c'est pénible à lire.
En outre, au lieu de tarabiscoter pour composer des fonctions inspirées, vous ne faites que prendre les duaux des évidences. De plus, c'est de l'écologie durable. En effet,
Ayant prouvé (par exemple), ((A=>B)=>B)=>C, vous gardez à la vue une fonction $\phi$ bien plus intéressante que celle qui va de A dans C, puisque celle que vous gardez va de (A=>B)=>B dans C ce qui est bien plus général, et ne nécessite pas "de cohérence" (un élément de A est "cohérent" et donne la fonction TRES PARTICULIERE et très belle qui va de A=>B dans A (je parle de $f\mapsto f(a)$)
Mais affirmer A=>C cache complètement qu'en fait vous savez associer un élément de C à n'importe quel élément qui va de A=>B dans B, et pas seulement ) ceux qui sont cohérents (les ultrafiltres) et encore moins pas seulement à ceux qui sont HYPERCOHERENTS (les ultrafiltres principaux.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
On n'est pas d'accord sur le sens du mot constructif alors. En LI, si tu prouves $\exists t, P(t)$, tu peux exhiber un tel $t$ et ce n'est pas le cas en LC (c'est un théorème, non négociable avec des "oui mais en vrai c'est à cause du doublement des hypothèses).
J'appelle ça constructif vs non constructif. Si tu n'es pas d'accord avec ce nom, ok, mais du coup ça déplace la question : c'est comme ça que je (et la plupart des gens que j'ai entendu en parler) l'utilise -
Je ne savais pas qui, mais je me doutais bien que quelqu'un dirait ça :-D
C'est le gros serpent de mer qui a fondé longtemps le préjugé que j'ai décrit. Tout le monde se focalise (parmi les non spé de ces choses) sur ça, je les redis:
M1/ Si $LI\vdash \exists xR(x)$ alors il existe $a$ tel que $LI\vdash R(a)$
M2/ Si $LI\vdash (A$ ou $B)$ alors $LI\vdash A$ ou $LI\vdash B$
Et ça a servi, je pense, longtemps de mascotte comme porte d'entrée au label constructif.
Mais c'est une chimère totale ce truc (enfin quasi-total). Les théorèmes de maths sont de la forme
$$ LI + DesMachinsTerriblementOpportunistes \vdash \forall x\exists y\forall z\dots $$
Idem avec "ou". Le théorème (intuitionniste, affine, linéaire et même linéaro-intuitionniste le plus simple du monde, comme (A ou=>(A ou par exemple, ne vérifie pas [ (A ou =>(A) ] ou [ (A ou =>(B) ]
Maintenant évidemment que dans CERTAINS CAS, c'est UTILE ET PLAISANT à certains d'avoir ce que tu rappelles. Mais ça ne suffit pas à mériter le label "constructif" à mon sens (qui est un mot vague), comme l'exemple suivant le montre:
tu as des tas de preuves de $LI\vdash $ (A ou non(A)), avec par exemple A:="les noirs sgagnent aux échecs", qui vérifient bien que $LI\vdash $ A ou $LI \vdash $ non(A).
Sauf que le deuxième point nécessite de dessiner tout l'arbre du jeu pour trouver lequel est le bon :-D Alors entre "du constructif de principe" et "du contructif concret", faut se positionner.
En logique propositionnel même la logique classique normalise en temps $n\mapsto 2^n$. Il n'y a aucune différence.
Prétendre non constructif une preuve de A ou nonA parce qu'on n'a pas assez d'information pour en tirer qui de A ou de nonA est vrai alors que la LI le permettrait c'est essentiellement une escroquerie (dans un sens non péjoratif). La LI ne permet pas plus de fabriquer des informations manquantes que la classique, elle refuse juste (par connexité) de "faire un pas de plus".
En réalité, c'est surtout sur l'infini, je pense initialement, qu'elle s'était vendue, au sens où par exemple elle ne prouvait pas:
$$ \exists x\forall y: [R(x)\to R(y)] $$
car ne pouvait pas fournir le témoin.
Sauf que pas besoin de la LI pour s'en apercevoir. La LC dit la chose suivante: ce témoin peut être provisoirement pris comme étant $0$. On fait comme si et au premier bug rencontré, cadire quand on a eu tort de croire à $(R(0)\to R(a))$, on a gagné (on a trouvé un VRAI témoin, qui est $a$.
Et là, immédiatement tu vois apparaitre la DUPLICATION. Ce n'est pas rien du tout cette duplication!!!!!
Par exemple, quand j'ai pondu mon article (que je n'ai toujours pas MAJ d'ailleurs :-D ) sur la logique annelée, comment crois-tu que j'ai traité les corps (en logique on ne peut pas se laisser aller à tolérer l'intégrité (au sens celle des anneaux)) ou on demande le truc bizarre :
$$ x=0\ ou \ xy=1$$
qui appelle un traitement par cas. Et bé j'ai dit
$$ x=x^2y$$
et basta (et ça m'a d'ailleurs donné la distinction LC/LI sans preuve, je n'ai trouvé les preuves qu'après)
Je pense sincèrement que la duplication est bien plus importante que la distinction A non(non(A)), mais comme dans les maths on étudie tout ce qu'on trouve, bien évidemment, il est normal, surtout dans ton domaine, que tu apprécies les bienfaits de M1 ("M" pour miracle lol)
D'ailleurs je l'avais signalé dans je ne sais plus quel post, que l'intuitionnisme et les spécialités géométrie algébrique et topologie algébrique avait NATURELLEMENT des verres à boire ensemble, je vais tenter de le retrouver et mettre un lien.
Mais globalement, il ne faut pas confondre l'abstinence anticipée d'un pas et un supposé "pouvoir" supplémentaire de discriminer des cas dont on a prouvé la garantie de la disjonction.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
christophe a écrit:Mais ça ne suffit pas à mériter le label "constructif"
Baaah si :-D En tout cas dans l'esprit des gens qui l'utilisent (à ton exception près, je parle de 100% des gens à qui j'en ai parlé ou que j'ai entendu en parler)
Donc (je n'ai pas tout lu, je ne peux pas savoir ce que tu entends par 'constructif') c'est peut-être à toi de changer de label ;-) (les maths qui sont derrières, elles, ne sont pas à débattre, le nom, lui, si) -
De mon téléphone : on est d'accord sur notre désaccord alors, c'est clair. ;-)Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
Juste une petite question par curiosité, même si je comprends très peu de choses.
Il me semble avoir compris il n’y a pas si longtemps qu’on pouvait « obtenir » toutes logiques à partir d’une seule.
En gros, logique machin+théorie des catégories permet de faire le pont.
Du coup, et pour continuer dans le peu que j’ai capté Christophe, sait-on écrire un énoncé général des théorèmes de complétude dont chacun est un cas particulier de celui-ci? Mais alors, on obtiendrait un théorème de complétude en « dehors » de toute logique, je sais pas, ça me fait bizarre. -
Je te répondrai en détails, mais là, je crève de chaud!! Je ne sais pas ce qui m'arrive, il fait nuit pourtant. Je vais aller cliquer sur meteoAide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.1K Toutes les catégories
- 7 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 53 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 62 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 312 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 772 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres
In this Discussion
Qui est en ligne 12
+9 Invités