Nouvelles fondations

Bonjour


Je viens d'écrire un article sur des nouvelles fondations, totalement différentes de la théorie des ensembles.

Voici une présentation:

Le paradoxe de Russel a été solutionné en réduisant les possibilités de construction des ensembles. Cette nouvelle théorie résout le problème d'une autre manière: en considérant plus de choses de manière à pouvoir déduire quels sont les constructions problématiques.

La théorie des ensembles correspond à une vision: le langage mathématique est un outils pour étudier "les ensembles", il y a d'un côté le monde des idées et des textes, de l'autre l'univers des ensembles. La nouvelle construction correspond à une autre vision: il n'existe qu'une chose: le langage mathématique, qui s'étudie lui-même. Le résultat est une construction extrêmement concise et (à mon goût) esthétique.

Pour lire l'article: http://fr.neardeep.org/ml/

cordialement

Réponses

  • Bonjour Emmanuel,

    Pourrait-on obtenir de vous un exposé un peu plus explicite de votre conviction ?

    Quand vous dites : " il n'existe qu'une chose ; le langage mathématique... " je ne sais pas quel cadre vous donnez à cette proposition.

    Cordialement
  • il n'existe qu'une chose: le langage mathématique, qui s'étudie lui-même.

    Position formaliste extrême alors ?
  • Bonjour

    Arg, je n'ai pas mis le lien!: http://fr.neardeep.org/ml/

    > quel cadre
    Une réponse précise serait de lire l'article.
  • é bé, je l'ai parcouru, ça m'a bien fait mal à la tête...

    Ce qui me semble un peu un obstacle à partager ton travail est la difficulté résultant du fait que tu cherches à l'expliquer à tous les publics en même tps.

    On trouve des paragraphes "pédagogiques" destinés à tout public, mélangés à des paragraphes pour les cultures "informatiques", et aussi des paragrapahes à sous-entendus "dissidents" (dans les préliminaires). On s'épuise à les lire et on arrive fatigués aux suivants.

    Ne peux-tu pas proposer une synthèse (ici) destinée uniquement, dans un 1er tps, à un public homogène de matheux, ça facilitera peut-être la transmission...
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Je te conseille de changer le nom de ton langage. ML est déjà pris...
  • J'ai regardé en vitesse et il me semble qu'il n'y a rien de nouveau dans le fond, ce qui n'est pas nécessairement important...
    Tu définis une théorie types calcul des constructions, mais d'une manière très compliquée. Je n'ai pas forcement le temps, ni l'envie, mais il me semble que l'on puisse résumer et alléger considérablement ce que tu proposes. J'ai juste la crainte que l'on retombe du coup sur quelque chose de clairement connu ou de clairement inconsistant.
    Quelques remarques sur la forme : 208 axiomes c'est trop. Tes axiomes n'en sont pas vraiment en plus puisque tu définis ce que tu poses comme axiomes. Tu ne donnes pas d'exemple, il est absolument nécessaire d'isoler le noyau de ton langage ainsi que ses règles de déduction, puis de l'illustrer par des constructions exemples. Tu as sûrement l'impression d'avoir hiérarchisé ton travail, mais tu n'as pas fait le bon découpage. Dans l'idéal il faudrait que la définition de ton langage tienne sur un demi page et les règles de réduction ou déduction sur une autre demi-page. Force toi à raffiner, cela sera très payant.
    Ta typographie et ton usage de concepts me fait penser que tu as une certaine érudition mathématico-informatique. Or, ton texte est absent de toutes références alors qu'il fait penser à beaucoup d'autres choses du même type. C'est à toi de faire l'effort de faire les références et de rapprocher explicitement lorsque c'est pertinent tes définitions d'autres travaux. Par exemple, ta définition de vrai donne clairement l'impression que tu connais le lambda-calcul où vrai est le terme $\lambda x. \lambda y. x$ et faux $\lambda x. \lambda y. y$.
    Petite remarque autre, utilise $\emptyset$ à la place de $\otimes$. Ce dernier est pour tout le monde un connecteur binaire. Les notations ça compte. Il n'est pas raisonnable par exemple de définir deux opérations $+$ et $\times$ où la première distribue sur la seconde.
    J'espère ne pas donner l'impression que je te dénigre, ce n'est pas du tout le cas. Je te donne juste des conseils.
    Quel est ton but ? Définir ta petite théorie en dilettante ou aboutir à une publication scientifique ? Dans le second cas tes rapporteurs ne seront pas vraiment cléments.
  • En fait je viens de lire ton texte Préliminaires et il est apparent que tu n'as qu'une idée très superficielle de la notion de fondations en mathématiques. Je t'encourage volontiers à lire sur le sujet. Tu vas sûrement me répondre que tu l'as déjà fait, et je te répondrais de relire plus profondément. Ton paragraphe sur les entiers naturels montre que tu ne vois pas ce que sont fondationnellement les entiers, c'est-à-dire le support du raisonnement inductif.
  • deufeufeu écrivait:
    > J'ai regardé en vitesse et il me semble qu'il n'y
    > a rien de nouveau dans le fond, ce qui n'est pas
    > nécessairement important...
    > Tu définis une théorie types calcul des
    > constructions, mais d'une manière très compliquée.
    > Je n'ai pas forcement le temps, ni l'envie, mais
    > il me semble que l'on puisse résumer et alléger
    > considérablement ce que tu proposes. J'ai juste la
    > crainte que l'on retombe du coup sur quelque chose
    > de clairement connu ou de clairement
    > inconsistant.

    Je défini des fondations des mathématiques, même s'il y a des ressemblances avec le Lamba-calcul, ce n'est pas la même chose. Sinon je ne peux rien te répondre puisque tu donnes ton impression de manière subjective.


    > Quelques remarques sur la forme : 208 axiomes
    > c'est trop.

    Les fondations des mathématiques actuelles sont divisées en deux parties: définition du langage mathématique puis les axiomes (ZFC). Le découpage que je fais est différent: des règles de base très simples et beaucoup d'axiomes, mais ces axiomes définissent le langage mathématique. S'il y a beaucoup d'axiomes, ce n'est pas que la théorie est plus compliquée, c'est qu'elle part d'un mécanisme plus petit et que les axiomes décrivent le langage. Le résultat est qu'en ML l'implication est un objet mathématique, alors qu'en théorie des ensembles l'implication est un élément du langage mathématique mais n'est pas un ensemble. Cette modélisation du langage mathématique dès le début donne une souplesse et une cohérence bien plus grande.

    > Tes axiomes n'en sont pas vraiment en
    > plus puisque tu définis ce que tu poses comme
    > axiomes.

    On ne peut considérer des phrases mathématiques comme vraies que de deux manières: par démonstration ou par ajout d'un axiome. Tant qu'il n'y a pas de manière de définir un terme on ne peut qu'àjouter des axiomes pour ajouter une définition.

    > Tu ne donnes pas d'exemple, il est
    > absolument nécessaire d'isoler le noyau de ton
    > langage ainsi que ses règles de déduction, puis de
    > l'illustrer par des constructions exemples. Tu as
    > sûrement l'impression d'avoir hiérarchisé ton
    > travail, mais tu n'as pas fait le bon découpage.
    > Dans l'idéal il faudrait que la définition de ton
    > langage tienne sur un demi page et les règles de
    > réduction ou déduction sur une autre demi-page.
    > Force toi à raffiner, cela sera très payant.

    La première partie "Base" est le noyau du langage. Je peu résumer, mais ça ne sera plus des mathématiques. Pour les exemples: il y en a peu, c'est un style personnel. Depuis très jeune j'aime bien les démonstrations de théorèmes, les exemples ça m'ennuie, je me construit les miens pour réfléchir mais je trouve que chacun peu se construire ses exemples. À force de prémâcher le travail on retire tout esprit de recherche. En mathématique il faut attendre bac+5 pour avoir accès à de la recherche alors que l'esprit de recherche devrait être à la base des maths. Bon c'est un autre sujet...


    > Ta typographie et ton usage de concepts me fait
    > penser que tu as une certaine érudition
    > mathématico-informatique. Or, ton texte est absent
    > de toutes références alors qu'il fait penser à
    > beaucoup d'autres choses du même type. C'est à toi
    > de faire l'effort de faire les références et de
    > rapprocher explicitement lorsque c'est pertinent
    > tes définitions d'autres travaux.

    Ça ressemble, mais ce n'est pas, par exemple la définition de `vrai' est différente du lambda calcul, même si ça y fait un peu penser. Je ne vois pas en quoi ça serait éclairant de donner des références.

    > Par exemple, ta
    > définition de vrai donne clairement l'impression
    > que tu connais le lambda-calcul où vrai est le
    > terme $\lambda x. \lambda y. x$ et faux $\lambda
    > x. \lambda y. y$.
    > Petite remarque autre, utilise $\emptyset$ à la
    > place de $\otimes$. Ce dernier est pour tout le
    > monde un connecteur binaire.

    Ok pour $ \otimes$, je n'utiliserai pas $ \emptyset$ car je l'utilise déjà dans son sens habituel, mais je vais chercher autre chose. Le problème est que les symboles LaTeX existant ont tous un sens déjà défini, mais bon je vais chercher autre chose...

    > J'espère ne pas donner l'impression que je te
    > dénigre, ce n'est pas du tout le cas. Je te donne
    > juste des conseils.

    Ok. Merci chaleureusement pour le temps que tu as passé à regarder mon texte, ça m'aide à l'améliorer, même si on n'est pas toujours d'accord j'en tire quand même des informations.

    > Quel est ton but ? Définir ta petite théorie en
    > dilettante ou aboutir à une publication
    > scientifique ? Dans le second cas tes rapporteurs
    > ne seront pas vraiment cléments.

    Ni l'un ni l'autre. J'aime les mathématiques, j'aime chercher, et je pense que l'intérêt de la science n'est pas seulement dans la construction de téléphones portables et autre, mais aussi dans la construction de soit. J'ai envie de partager quelque chose que je trouve beau.

    > En fait je viens de lire ton texte Préliminaires et il est apparent
    > que tu n'as qu'une idée très superficielle de la notion de fondations en
    > mathématiques. Je t'encourage volontiers à lire sur le sujet. Tu vas sûrement me
    > répondre que tu l'as déjà fait, et je te répondrais de relire plus profondément. Ton
    > paragraphe sur les entiers naturels montre que tu ne vois pas ce que sont
    > fondationnellement les entiers, c'est-à-dire le support du raisonnement inductif.

    Les entiers sont le support du raisonnement inductif dans la théorie des ensembles. Mais existe-t-il d'autres fondements des mathématiques où les entiers ne sont pas ce support ? Si je te comprend bien tu réponds non, et tu dis que celui qui n'est pas d'accord avec toi n'a pas compris "ce que sont fondationnellement les entiers".

    Comme tu parles de support je suppose que tu entends par là que le raisonnement par induction ne peut pas être défini sans les entiers. Dans ce cas on n'est pas d'accord. Dans les fondations que je défini la récurrence se définie (en dehors des axiomes) sans les entiers (qui eux aussi ne sont pas définis dans les axiomes).

    cordialement
  • Je ne vois pas en quoi ça serait éclairant de donner des références.
    C'est tout simplement parce que ce n'est pas à toi de voir mais aux autres qu'il faut en donner. On a toujours soi-même l'impression que tout est clair, mais ce n'est pas le cas de quelqu'un qui entre par hasard dans ton travail. Les références permettent de replacer ton travail dans un cadre connu. D'ailleurs tu sembles penser être le premier à avoir donné une construction différente de la théorie des ensembles pour les fondations. C'est faux, et pourtant répété de nombreuses fois dans ton document ainsi que dans tes messages précédents, au point que tu donnes l'impression que c'est une croyance de ta part. Je faisais non pas référence au lambda-calcul mais au calcul des constructions plus haut, c'est un cadre très différent de la théorie des ensembles qui permet de reconstruire les mathématiques.
  • Bon j'ai lu en détails les 30 premières pages et j'ai plusieurs critiques plus appuyées. Je les numérote pour que tu puisses y répondre point par point.
    1) Que supposes-tu, que ne supposes-tu pas ? Tu veux faire des fondations, et j'ai donc l'impression que tu t'interdis d'utiliser la théorie des ensembles pour définir tes objets, même si tu l'utilises sans le dire car ce n'est pas en définissant des chaines de caractères que tu l'évites. Mais tu t'intéresses ensuite à une validité extérieure de tes expressions. Or, tu ne donnes aucune règle de déduction. J'en déduis donc que tu supposes acquis un monde déductif extérieur. Et là c'est assez spécieux : tu t'interdis la théorie des ensembles mais tu t'autorises de la logique non triviale sans broncher. Notamment il te semble clair que tu as le modus ponens : si "A -> B" et "A" alors "B". Mais tu dois en parler !
    2) Ta construction se fait en deux temps : un ensemble de phrases pures, ne correspondant à rien en toute généralité et un sous-ensemble d'expressions qui font sens. En ce sens tu définis le type de tes expressions. Pourquoi alors ne pas directement passer à des jugements de type plutôt ?
    3) De manière plus générale, tu es un informaticien, cela se voit. Cela se voit d'autant plus à ta remarque sur l'association mot-clef -> arbre, que tu trouves trop triviale pour être explicitée. On sens la personne qui sais faire des tables de hachage. Mais ce n'est pas le propos ici ! Si on veut pouvoir expliciter cette association c'est pour savoir dans quel monde elle vit ! Tu donnes l'impression qu'il existe un bureaucrate omniscient et extérieur qui réaliserait un gros bottin de définitions. Présupposer ce genre de choses ce n'est pas faire des fondations.
    4) Je vois, imho, ce que tu cherches à faire et je te dis que cela a déjà été fait en beaucoup mieux et plus propre par la théorie des types. Tout d'abord celle de Martin-Lof et plus récemment son enrichissement par Coquand-Huet dans le calcul des constructions. Fait joujou avec coq.inria.fr pour voir. Je t'assure que je ne dis pas cela pour t'embêter.
  • Bon j'ai lu en détails les 30 premières pages et j'ai plusieurs critiques plus appuyées

    Bin tu peux remercie Deufeufeu, parce que moi, je ne le ferai pas c'est sûr. Je suis trop faignant pour me taper une truc pareil. Je ne te le dis pas du tout pour être méchant, mais pour te permettre de mesurer les risques de solitude qui t'attendent dans ces cas-là... Un H averti en vaut 2

    Par contre, tu devrais peut-être t'intéresser de plus près à ce que tu crois être la théorie des ensembles, parce que tu as l'air de l'accuser d'êter compliquée ou subjective (en ce sens qu'elle emmène les maths dans une direction qui en cache d'autres) et (sur le plan théorique!) c'est une erreur

    De plus, les fondations des maths ne sont pas ZFC. La seule vraie avancée "fondationnelle" des maths c'est d'être FORMEL, et la logique.

    De plus, les théorèmes de logique classiques établissent que finalement on peut se passer d'axiomes et donc difficile de trouver plus simple comme fondement. ZF constitue juste la liste des axiomes qu'on n'écrit pas quand on enregistre une démonstration à "l'écadémie des sciences"

    MAIS: il faut que tu saches que ce n'est pas grave pour 2 raisons:

    1) ils sont sous-entendus comme hypothèses

    2) ils n'y a aucun risque qu'ils soient cachées ou perdues, puisque JUSTEMENT ils sont UTILISES dans la démonstration (donc se voit là où ils le sont) (ils ne sont juste pas rappelés dans le préambule (ie dans l'énoncé du théorème, pour éviter les "si .. et si.. et si .."
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Tu n'es ni le premier ni le dernier qui s'engage et prend du tps de sa vie pour ces activités.

    Je te préviens que c'est ingrat et une "erreur" pour des raisons profondes (et là il faut blamer les philosophes et épistémologues qui se la pètent et écrivent des délires sur la "crise des fondements" etc (Godel, et cie)

    Contrairment à un préjugé on ne fait pas des maths avec des axiomes: ce que je veux dire c'est que ZF est non pas une théorie, mais "dispensant". Les gens s'en donnent à coeur joie pour trouver des trucs (les prouver) et seulement à la fin, quand ils ont fini, ils regardent quelles hypothèses ils voudraient ne pas "poser là" et cherchent à les "prouver" via ZF pour publication (mais ce n'est jamais là le problème, c'est du secrétariat)

    Si une ou plusieurs hyp résistent, ils ne publient pas B; mais A--->B et ça ne change rien à leur travail (A devient une conjecture ou une jolie question pas triviale)

    Si A a quelque chose de "transcendantal" (je cherchais un mot) la personne qui le conjecture, au lieu de le conjecturer va l'appeler "axiome de grand cardinal" (c'est presque purement juridique) et charge à elle ensuite de faire accepter cette appelation aux autres...

    L'apparent "langage" n'est qu'une illusion: il n'est pas limitatif (c'est pas parce qu'il y a le mot "appartient"...)

    Bcp "s'usent" à ne pas comprendre ça... (catégorie, topoi, etc) et quand ils finissent par accoucher de quelque chose, et bien ça donne des jolies théorèmes tout à fait classiques et exprimables parfaitement en terme d'ensembles
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Un exemple simple est le système d'axiomes de Quine (je crois) appelé... "new fundation" lol

    il s'étudie comme un problème de maths à part entière (parfaitement exprimable ds ZF) et d'ailleurs je crois que sa consistance est encore un problème ouvert
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • deufeufeu écrivait:

    > C'est tout simplement parce que ce n'est pas à toi de voir mais aux autres qu'il faut en donner.
    > On a toujours soi-même l'impression que tout est clair, mais ce n'est pas le cas de quelqu'un
    > qui entre par hasard dans ton travail.

    Oui, c'est clair :-)

    > Les références permettent de replacer ton travail dans un cadre connu. D'ailleurs tu sembles
    > penser être le premier à avoir donné une construction différente de la théorie des ensembles
    > pour les fondations.

    J'ai l'impression qu'il y a un gros quiproquo: je propose une alternative à la théorie des ensembles, et non une "construction différente de la théorie des ensembles".

    > C'est faux, et pourtant répété de nombreuses fois dans ton document ainsi que dans tes
    > messages précédents, au point que tu donnes l'impression que c'est une croyance de ta part.
    > Je faisais non pas référence au lambda-calcul mais au calcul des constructions plus haut,
    > c'est un cadre très différent de la théorie des ensembles qui permet de reconstruire les
    > mathématiques.

    De ce que j'ai compris du calcul des constructions, c'est une modélisation du langage mathématique, mais pour faire des mathématiques il faut y ajouter des axiomes, par exemple ceux de la théorie des ensembles.
    Mon article défini en même temps une modélisation et des axiomes qui permettent de faire des mathématiques sans autres axiomes.

    > Bon j'ai lu en détails les 30 premières pages et j'ai plusieurs critiques plus appuyées.
    > Je les numérote pour que tu puisses y répondre point par point.
    > 1) Que supposes-tu, que ne supposes-tu pas ? Tu veux faire des fondations, et j'ai donc l'impression que

    > tu t'interdis d'utiliser la théorie des ensembles pour définir tes objets,
    oui


    > même si tu l'utilises sans le dire car ce n'est pas en définissant des chaines de caractères que tu l'évites.

    Pour faire des fondations, on part forcément de quelque chose, qui est forcément modélisable en théorie des ensembles ou alors c'est quelque chose d'extrèmement flou. Donc on peut toujours dire qu'une fondation "utilise" la théorie des ensembles.

    > Mais tu t'intéresses ensuite à une validité extérieure de tes expressions. Or, tu ne donnes aucune règle de déduction.

    La définition de ML (modélisation du langage et autres axiomes) sont fournis en ML. Je donne en première partie une traduction de quelques termes ML de manière à comprendre la définition fournie (en ML). (je simplifie ici en passant sous silence MLN)
    La définition des règles de déduction n'apparaît que tard: page 55, dans "règles de déduction dans les sous-contextes".

    > J'en déduis donc que tu supposes acquis un monde déductif extérieur. Et là c'est assez spécieux :
    > tu t'interdis la théorie des ensembles mais tu t'autorises de la logique non triviale sans broncher.
    > Notamment il te semble clair que tu as le modus ponens : si "A -> B" et "A" alors "B". Mais tu dois
    > en parler !

    page 55

    >2) Ta construction se fait en deux temps : un ensemble de phrases pures, ne correspondant à
    > rien en toute généralité et un sous-ensemble d'expressions qui font sens. En ce sens tu définis
    > le type de tes expressions. Pourquoi alors ne pas directement passer à des jugements de type
    > plutôt ?

    Le cadre minimal dont je part:
    -les arbres ML
    -la traduction de deux expressions MLN
    ne me permet pas de faire des choses sophistiquées. J'ai l'impression que le cadre est tellement petit qu'il n'est pas clair que le choix est très réduit. Les deux expressions MLN (hypothèse et remplacement) sont définies dans notre langage courant, mais ce sont des expressions traduites (par la suite) en ML, ce qui fait qu'elles sont définies très précisément par la suite.

    Cette "contrainte" d'un cadre minimal n'en est pas une réelle, car elle contraint à faire une définition puissante des mathématiques. De même que dans la vie, respecter les contraintes du raisonnement logiques est agréable.


    > 3) De manière plus générale, tu es un informaticien, cela se voit. Cela se voit d'autant plus
    > à ta remarque sur l'association mot-clef -> arbre, que tu trouves trop triviale pour être
    > explicitée. On sens la personne qui sais faire des tables de hachage. Mais ce n'est pas
    > le propos ici ! Si on veut pouvoir expliciter cette association c'est pour savoir dans
    > quel monde elle vit ! Tu donnes l'impression qu'il existe un bureaucrate omniscient
    > et extérieur qui réaliserait un gros bottin de définitions. Présupposer ce genre
    > de choses ce n'est pas faire des fondations.

    Je fais des fondations pour le langage ML. J'utilise et je défini un langage MLN qui est un outils (au même titre que les notations en mathématiques permettent de simplifier l'expression), mais qui n'est pas partie intégrante aux fondations. Je défini MLN suffisamment pour qu'il soit clair dans l'esprit du lecteur qu'il peut traduire de manière univoque MLN en ML. La correspondance avec les arbres fait partie de la traduction de MLN vers ML, c'est pourquoi je n'ai pas besoin de la définir explicitement, du moment que le lecteur comprend qu'il existe une telle traduction. Je trouve clair qu'il existe une injection entre tout mot de notre langue et les arbres binaires utilisés en ML, parce que les deux ensembles sont dénombrables. Je ne vois pas quel publique peut être intéressé à expliciter cette injection: car les personnes qui ne voient pas que l'injection est constructible sont (à mon avis) assez peut pointilleuses pour s'arrêter à ça. Mais si je vois que je me trompe je définirai cette correspondance dans une annexe.

    > 4) Je vois, imho, ce que tu cherches à faire et je te dis que cela a déjà été fait en beaucoup
    > mieux et plus propre par la théorie des types. Tout d'abord celle de Martin-Lof et plus
    > récemment son enrichissement par Coquand-Huet dans le calcul des constructions. Fait joujou
    > avec coq.inria.fr pour voir.

    Je comprends que comparé à une modélisation comme coq mon texte parait mal foutu. Mais ce n'est pas pareil : coq est une modélisation qui n'a pas pour objectif de partir d'un minimum de présupposés. Là il s'agit d'une fondation aux présupposés très réduits. On ne peut pas partir de plus simple que d'arbres binaires n'ayant qu'un type de nœuds, et même les règles de déductions sont définies par le langage lui-même (après une définition dans notre langage afin de pouvoir interpréter ML).


    > Je t'assure que je ne dis pas cela pour t'embêter.
    Ok, je comprends, ça va. Pour moi c'est très fructueux.
  • christophe chalons écrivait:
    > Tu n'es ni le premier ni le dernier qui s'engage
    > et prend du tps de sa vie pour ces activités.
    ...
    > Bcp "s'usent" à ne pas comprendre ça...
    > (catégorie, topoi, etc) et quand ils finissent par
    > accoucher de quelque chose, et bien ça donne des
    > jolies théorèmes tout à fait classiques et
    > exprimables parfaitement en terme d'ensembles

    Je ne comprend pas pourquoi tu viens sur un forum sur les fondations si les fondations ne sont pas intéressantes pour toi. J'ai l'impression de retrouver un style très "phylo" dans tes contributions, avec des affirmations et sans questionnement. Je répond sur un point quand même:

    Tout est exprimable en théorie des ensembles, mais il est intéressant d'avoir un langage le plus simple et puissant possible: ça facilite la communication et la pensée.
  • Tout d'abord pour fixer les idées et pour que tu vois que ce ne sont pas des critiques de quelqu'un extérieur à tout cela, laisse moi te dire que je suis responsable d'un cours de Logique en L3 où j'ai également fait un chapitre sur les fondations.

    Il ne sert à rien de se fixer une contrainte sur ce que l'on a droit d'utiliser pour définir des fondations. La seule chose que l'on pourrait comprendre c'est que d'un point vue idéologique tu te fixes des contraintes. A ce moment là définis-les précisément en préambule à la manière d'un ouvrage de l'Oulipo.
    De plus il te semble clair que l'on puisse admettre la construction qui à un alphabet $\Sigma$ associe l'ensemble des mots $\Sigma^*$. Or, ce n'est pas le cas et en plus tu t'en sers pour définir le magma non associatif des arbres qui est pourtant plus primitif. Voilà une définition qui a le mérite d'être claire : les mots purs de ML sont les éléments du magma librement engendré par $\otimes$. On note $[x,y] = x \times y$ où $\times$ est la loi de composition du magma.

    Ta définition de MLN a besoin d'être précise. Tu as voulu définir un langage de macro type $\TeX$ cela se comprend. Maintenant il manque beaucoup de détails par à rapport à ton objectif. "Qui" effectue les substitutions ? Que se passe-t-il quand on fait [MLNCompose [notation | "A" = "B"] [notation | "B" = "A"]] ?
    Je trouve clair qu'il existe une injection entre tout mot de notre langue et les arbres binaires utilisés en ML, parce que les deux ensembles sont dénombrables. Je ne vois pas quel publique peut être intéressé à expliciter cette injection: car les personnes qui ne voient pas que l'injection est constructible sont (à mon avis) assez peut pointilleuses pour s'arrêter à ça. Mais si je vois que je me trompe je définirai cette correspondance dans une annexe.
    Et tu n'as pas l'impression d'avoir utilisé beaucoup de théorie des ensembles au passage ?
    De ce que j'ai compris du calcul des constructions, c'est une modélisation du langage mathématique, mais pour faire des mathématiques il faut y ajouter des axiomes, par exemple ceux de la théorie des ensembles.
    Mon article défini en même temps une modélisation et des axiomes qui permettent de faire des mathématiques sans autres axiomes.
    Au niveau du calcul des constructions tu te trompes. Il fournit le tout et de manière bien plus puissante que tes axiomes à toi. Par exemple dans CCI (I=Inductives) qui est une extension équivalente de CC on peut définir les entiers comme cela :
    $Nat = Zero : Nat | Succ : Nat -> Nat$
    et obtient automatiquement le schéma de récurrence $\forall P : Nat \rightarrow Prop, (P Zero) \rightarrow (\forall x : Nat, P x \rightarrow P (Succ x)) \rightarrow \forall x: Nat, P x$.
    Rien de tout cela n'est un axiome. Les axiomes ont été définis avant sur les constructions et la possibilité de cette construction en découle. Ce qui fait que ces axiomes bien moins nombreux que les tiens sont plus puissants.
    Là c'est moi qui te montre que tu te trompes, mais dans le monde scientifique on ne procède pas comme cela. Tu te dois d'étudier les autres propositions, particulièrement celles que tes lecteurs t'ont proposées et de ne t'arrêter qu'à partir du moment où tu sais dire soit qu'effectivement c'est similaire soit que cela diffère très précisément en tel et tel points. Pour que ton texte soit lisible tu dois faire ce travail pénible mais indispensable.

    Au sujet des références et de l'historique des fondations, tu peux lire cela : http://iml.univ-mrs.fr/\~{}girard/bsl.pdf.gz
    Lis particulièrement l'intro, et essaie d'argumenter autant. Regarde le passage sur les entiers et compare le au tien par exemple.

    [Correction du lien. AD]

  • (1)Je ne comprend pas pourquoi tu viens sur un forum sur les fondations si les fondations ne sont pas intéressantes pour toi.

    (2)J'ai l'impression de retrouver un style très "phylo" dans tes contributions, avec des affirmations et sans questionnement. Je répond sur un point quand même:

    (3)Tout est exprimable en théorie des ensembles, mais il est intéressant d'avoir un langage le plus simple et puissant possible: ça facilite la communication et la pensée.

    1) Oups, malentendu: je ne dis pas ça, je voulais t'aider à savoir dans quelle aventure tu t'engages, c'est tout. Elles sont passionnantes pour moi, je prétendais juste que la problématique qu'elle pose est (presque*) résolue et je pense (certes en résumé) t'avoir dit pourquoi
    * Et l'exploration du "presque" me parait justifier que tu sois averti (sur le plan humain). Cantor, Godel, Turing, etc se sont "presque" suicidés à force d'essayer de trouver la clé (je veux dire que ça fait souffrir pas mal quand on ouvre les yeux après longtemps sans forcément avoir gd chose à se mettre sous la dent

    2) je ne comprends pas "phylo"? Tu voulais surement dire "philo": rassure-toi, je suis technicien plus que philo et très méfiant justement à l'égard des obscessions fondationnelles non accompagnées d'une bonne appréhension technique de ce qui est déjà connu

    3) oui, d'accord: ton but peut-il être précisé, parce qu'avec "appartient" ; "quelque soit" et "implique" on a réussi à tout exprimer en 3 mots et 3 "axiomes" (extensionnalité, choix et propriété"="ensemble) et sans supposer le tiers-exclus (qui est un théorème prouvé). De plus le 3e axiome se type avec l'identité (autrement dit "rien")

    Difficile de faire plus simple. Après peut-être que par "simple" et "puissant", tu inclus d'autres exigences (popularité, accessibilité, etc?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Je ne vois pas quel publique peut être intéressé à expliciter cette injection: car les personnes qui ne voient pas que l'injection est constructible sont (à mon avis) assez peut pointilleuses pour s'arrêter à ça

    Là tu commets une erreur déontologique: La science n'est pas pointilleuse à cause du plaisr qu'elle éprouve à enculer les mouches, mais parce qu'à empiler les "intuitions" de ce type elle prend des risques inacceptables.

    Rappelle-toi que les axiomes ne sont pas vrais!!!!!!

    Ils sont sont attaqués par la science, c'est à dire conçus pour que si une preuve n'utilisant qu'eux conduit à une conradiction, on puisse immédiatement obtenir en contre-partie de cette preuve un graal qui compense cet "apparent" écroulement.

    C'est pourquoi, quand tu utilises un axiome et que tu "discoures" comme dans la citation pour justifier que tu ne le justifieras pas, le seul engagement que tu prends est qu'au cas où un jour ton axiome serait la pièce principal menant à une contradiction, cadire le paradis, il faudrait trouver dans ton discours ce qu'on gagne à ce que l'axiome que tu fondes par lui soit faux. Or dire "tlm convient que A, sauf les violeurs de mouches", bin le jour où A se manifeste faux, la seule chose gagnée est que les gens que tu qualifies de non violeurs de mouches se sont trompés: c'est peu

    C'est pourquoi deufeufeu te fait remarque "qu'heureusement" ton "A" est déjà prouvé par ailleurs donc n'a pas besoin d'être un axiome
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Là tu commets une erreur déontologique : La science n'est pas pointilleuse à cause du plaisir qu'elle éprouve à enculer les mouches, mais parce qu'à empiler les "intuitions" e ce type elle prend des risques inacceptables.

    On est tout à fait d'accord sur la nécessité de démontrer. Le quiproquo vient du fait que je définis un langage MLN et que toi et deufeufeu prenez MLN comme faisant partie des fondations que je définis. Mais je définis ML, MLN est un outil, au même titre que j'utilise le français pour écrire mes fondations, ce n'est pas une raison pour que j'ai à définir le langage "français". Pour mettre les points sur les i : je pourrais traduire tout mon texte pour que MLN n'apparaisse plus car tout texte MLN est traduisible en ML. Et le résultat serait toujours la définition de fondations mathématiques. Si je ne le fais pas c'est parce que ça serait complètement incommode à lire. Si la définition de MLN n'est pas claire alors là c'est un problème, et il faut peut-être que j'utilise un langage de définition déjà connu dans ce cas, mais si la définition de MLN est claire alors je n'ai pas à le définir mathématiquement.

    Cordialement
  • Rappelle-toi que les axiomes ne sont pas vrais!!!!!!

    Ca dépend. Un platonicien, pour qui les objets mathématiques existent véritablement et indépendamment de l'esprit humain, se fonde sur son intuition pour découvrir des évidences premières, les axiomes, qui sont dès lors admis comme vrais. Sinon la quête de Gödel qui était profondément platonicien, découvrir de nouveaux axiomes de la théorie des ensembles, accessibles à l'intuition et qui permettraient de fixer l'hypothèse du continu (entre autres), n'aurait pas eu de sens. (Je dis bien, accessibles à l'intuition, pour éviter toute polémique !)
  • Difficile de faire plus simple. Après peut-être que par "simple" et "puissant", tu inclus d'autres exigences (popularité, accessibilité, etc?

    Quand je parle de fondations, j'y inclus la définition d'un langage mathématique, pas seulement les axiomes de ZFC.
    Simplicité: ZFC comporte un schéma d'axiomes, autrement dit une infinité d'axiomes, ça fait beaucoup. De plus la notion de "tout" n'y existe pas (car elle amène à une contradiction), je trouve ça pas simple.

    Puissance: je n'ai pas de démonstration. C'est une intuition qui vient de la simplicité des présupposés de base et de l'aspect "auto-construit". Je pense qu'il est reconnu en science qu'entre deux modèles ayant l'air de refléter la réalité, celui basé sur des mécanismes très primitifs a plus de chance de refléter la réalité. Je comprend bien qu'il s'agit d'un critère intuitif.

    cordialement
  • GG a écrit:
    Ca dépend. Un platonicien, pour qui les objets mathématiques existent véritablement et indépendamment de l'esprit humain, se fonde sur son intuition pour découvrir des évidences premières, les axiomes, qui sont dès lors admis comme vrais. Sinon la quête de Gödel qui était profondément platonicien, découvrir de nouveaux axiomes de la théorie des ensembles, accessibles à l'intuition et qui permettraient de fixer l'hypothèse du continu

    Bon c'est clair je suis devenu complètement platonicien en développant ML, par expérience donc très convaincu. Mon expérience est que je suis parti de quelques chose d'assez éloigné, avec comme idée de base d'un langage mathématique qui dès la base a une représentation de lui-même. Et que petit à petit j'ai convergé vers les fondations que je propose là, et que cette convergence m'a donné l'impression très forte d'une exploration dans un univers préexistant, et pas du tout d'une création de ma part.

    De plus, et là c'est très personnel et étant le créateur je reconnais que ce n'est pas forcément partagé: en créant ces fondations j'ai l'impression que mon esprit (ie ma conscience) a grandement changé en utilisant cette simplicité. En fait c'est quelque chose que l'on a tous connu en découvrant les mathématiques: cela nous permet de mieux réfléchir dans beaucoup d'autres domaines. C'est un changement qui en général est assez continu pour qu'il ne soit pas marquant si on ne s'est pas penché dessus. Mais là j'ai vécu des changements très forts et rapides. Mais bon, ça peut être lié aussi au fait de me remettre à chercher, je ne prétend pas que c'est forcément partagé.

    cordialement
  • Je trouve la démarche très salutaire. Les conseils prodigués très sérieusement plus haut t'aideront , je l'espère à rendre ton travail intelligible à un plus large public.

    Salut!
  • deufeufeu a écrit:
    Il ne sert à rien de se fixer une contrainte sur ce que l'on a droit d'utiliser pour définir des fondations. La seule chose que l'on pourrait comprendre c'est que d'un point vue idéologique tu te fixes des contraintes.

    D'accord avec toi si tu inclus dans "idéologie" la démarche consistant à "isoler les concepts de base permettant de modéliser un système". C'est une démarche habituelle en science et qui me semble à la base de la démarche scientifique: isoler les paramètres important. Je pense comprendre ton point de vue, notre divergence vient de la vision différente des mathématiques: je ne vois pas de coupure nette entre la physique et les mathématiques, pour moi un objet mathématique a autant d'existence qu'un verre d'eau, le verre d'eau est localisé à un endroit précis, pas l'objet mathématique, mais ça n'en fait pas quelque chose de "moins existant". J'explore les mathématiques à la manière des physiciens: je cherche les "particules élémentaires" des mathématiques. J'ai l'impression que tu vois plus les mathématiques comme un outils construit, et dans ce cadre je conçois que ma démarche paraisse étrange.
    deufeufeu a écrit:
    A ce moment là définis-les précisément en préambule à la manière d'un ouvrage de l'Oulipo.

    Oui, merci de la remarque, je pense travailler ça.
    deufeufeu a écrit:
    De plus il te semble clair que l'on puisse admettre la construction qui à un alphabet $ \Sigma$ associe l'ensemble des mots $ \Sigma^*$.
    Or, ce n'est pas le cas et en plus tu t'en sers pour définir le magma non associatif des arbres qui est pourtant plus primitif. Voilà une définition qui a le mérite d'être claire : les mots purs de ML sont les éléments du magma librement engendré par $ \otimes$. On note $ [x,y] = x \times y$ où $ \times$ est la loi de composition du magma.

    MLN est un outil permettant de clarifier le document, mais il est possible de traduire toutes les expressions MLN de manière à ne laisser que la définition de ML. Ce serait monstrueux à lire, mais c'est tout à fait faisable. C'est pourquoi je ne vois pas pourquoi je devrais définir mathématiquement MLN. Le langage MLN est utilisé dans un nombre fini de cas dans le document, je ne prétend pas que ce langage soit utilisé par d'autres. Pour prétendre cela il faudrait que je le définisse mathématiquement. C'est possible que ce soit fait par la suite mais ce n'est pas le sujet des fondations de ML.
    deufeufeu a écrit:
    "Qui" effectue les substitutions ?

    Veux-tu dire par là qu'il faudrait que je décrive une procédure de traduction automatique de MLN en ML ?
    deufeufeu a écrit:
    Que se passe-t-il quand on fait [MLNCompose [notation | "A" = "B"] [notation | "B" = "A"]] ?

    Je ne prétend pas que MLN soit entièrement défini, je l'utilise pour un nombre fini de phrases dans lesquels ces ambiguïtés n'existent pas.


    deufeufeu a écrit:
    Et tu n'as pas l'impression d'avoir utilisé beaucoup de théorie des ensembles au passage ?

    Oui, mais c'est pour définir MLN, ça serait pour ML ça me dérangerait beaucoup.

    deufeufeu a écrit:
    Au niveau du calcul des constructions tu te trompes. Il fournit le tout et de manière bien plus puissante que tes axiomes à toi. Par exemple dans CCI (I=Inductives) qui est une extension équivalente de CC on peut définir les entiers comme cela :
    $ Nat = Zero : Nat \vert Succ : Nat -> Nat$
    et obtient automatiquement le schéma de récurrence $ \forall P : Nat \rightarrow Prop, (P Zero) \rightarrow (\forall x : Nat, P x \rightarrow P (Succ x)) \rightarrow \forall x: Nat, P x$.
    Rien de tout cela n'est un axiome. Les axiomes ont été définis avant sur les constructions et la possibilité de cette construction en découle. Ce qui fait que ces axiomes bien moins nombreux que les tiens sont plus puissants.

    Ok, tu veux dire qu'il existe des fondations mathématiques (CCI ?) qui sont très différentes de la théorie des ensembles, et qui, par exemple, n'ont pas de schéma d'axiomes, résolvent le paradoxe de Russel autrement que par une réduction de l'univers conduisant à ne pas avoir la notion de "tout" ? Dans ce cas CCI m'intéresse beaucoup. Cette théorie a-t-elle aussi un abord différent de l'axiome du choix ?

    Une réponse à cette question m'intéresse beaucoup beaucoup.

    deufeufeu a écrit:
    Là c'est moi qui te montre que tu te trompes, mais dans le monde scientifique on ne procède pas comme cela. Tu te dois d'étudier les autres propositions, particulièrement celles que tes lecteurs t'ont proposées et de ne t'arrêter qu'à partir du moment où tu sais dire soit qu'effectivement c'est similaire soit que cela diffère très précisément en tel et tel points. Pour que ton texte soit lisible tu dois faire ce travail pénible mais indispensable.

    Cette démarche me parait naturelle et non un devoir. Cela dit je me paye le luxe, la liberté, le plaisir, de faire les choses quand je suis convaincu et non par devoir. Je n'ai pas forcément besoin d'une démonstration, ni que l'autre travaille beaucoup à me convaincre, je ne me prétend pas supérieur ni inférieur, je ne veux pas que l'autre fasse le travaille à ma place. Simplement la compréhension est mon carburant.
    deufeufeu a écrit:
    Au sujet des références et de l'historique des fondations, tu peux lire cela : [iml.univ-mrs.fr]
    Lis particulièrement l'intro, et essaie d'argumenter autant.

    Merci pour la référence, et pour toutes ces remarques dont je vais tenir compte car il est clair que mon texte n'est pas clair!
    deufeufeu a écrit:
    Regarde le passage sur les entiers et compare le au tien par exemple.
    Les entiers sont utilisés par MLN uniquement, mon passage sur les entiers veut signifier que je n'utilise que les entiers entre disons 1 et 100 et que du coup je n'ai pas besoin de récurrence sur les entiers.

    Mais du fait de la correspondance entre MLN et les arbres ML, j'utilise les entiers, donc je vais retirer cette partie qui est fausse. Par contre je pourrais ajouter que je n'utilise pas la notion d'entier pour définir ML.

    Tu pourrais objecter que la définition récursives des arbres ML utilise la récursivité et donc les entiers. Mais il faut voir que la définition des arbres ML faite dans la partie "Base" n'est qu'une présentation, la véritable définition des arbres ML est faite en ML, dans les premiers axiomes.


    cordialement
  • Le concept important pour comprendre CCI c'est l'imprédicativité, qui est en à la base du paradoxe de Russel. Une propriété est dite imprédicative ssi elle s'auto-référence dans sa définition.
    Là où CCI (en fait CCI + Set predicatif) est fin c'est qu'il y a d'un côté un type $Prop$ qui correspond naïvement aux valeurs de vérité. L'axiome $\forall P: Prop, \forall p, q : P, p = q$ est admissible et il dit en gros qu'il n'existe qu'une preuve de $P$, on peut donc y faire de la logique classique. $Prop$ est imprédicatif, c'est-à-dire qu'on a par exemple $\forall P: Prop, P$ qui est également de type $Prop$.
    Et de l'autre côté une hiérarchie $Set = Type_0 : Type_1 : Type_2 : ...$ avec $Set$ prédicatif. Une formule $P : Set$ définis un ensemble d'éléments. La prédicativité entraîne que $\forall P: Set, P$, a.k.a. l'ensemble de tous les ensembles, se type dans $Type_1$ et pas dans $Set$.
    Du coup, on a d'un côté le monde des propriétés sur lesquelles on peut raisonner de manière d'autant plus puissante que l'on n'en construit rien. D'un autre côté le monde des constructions où de chaque preuve d'une formule typé par $Set$ on peut extraire un témoin de preuve, un programme, qui effectue explicitement la construction.
    L'axiome du choix est prouvable avec une quantification sur Set mais incohérent sur Prop B-)-.

    J'espère en avoir dit assez, mais je ne veux pas sur-polluer ton post.
  • en créant ces fondations j'ai l'impression que mon esprit (ie ma conscience) a grandement changé en utilisant cette simplicité. En fait c'est quelque chose que l'on a tous connu en découvrant les mathématiques: cela nous permet de mieux réfléchir dans beaucoup d'autres domaines. C'est un changement qui en général est assez continu pour qu'il ne soit pas marquant si on ne s'est pas penché dessus. Mais là j'ai vécu des changements très forts et rapides

    D'où mes recommandations ci-dessus et une invitation à prendre connaissance des histoires personnelles des logiciens célèbres (c'est un grand chelem de pétages de plomb)

    Selon toute vraisemblance, on "ressent" qu'en jouant avec l'infini et le langage il doit y avoir une contradiction (hélas peut-être trop subtile pour être déjà apercevable) dans toutes les théories riches (y compris ZF)

    Ce n'est pas un fait clamé très publiquement, mais je t'assure qu'il est partagé, même par les autorités les plus incontestées, c'est pourquoi la création de langages nouveaux auxquels on n'est peu habitués est dangereux d'un point de vue personnel: tu travailles, tu travailles, et puis hop tu tombes sur une contradiction. Tu entres dans un état d'excitation et tu risques ensuite de passer 20 ans à juste vérifier où est l'hypothèse sulfureuse et une fois que tu es assuré que tout est solide, tu l'envoies à des spécialistes qui... ne lisent pas parce que trop peu habitués à ta nouvelle syntaxe...

    C'est ingrat. C'est le seul avantage d'avoir ZF: c'est que si tu trouves un truc tu seras lu, car tu annonceras quelque chose de lisible (une contradiction ou un résultat, ou le cassage d'un grand cardinal). Il n'y en a pas d'autres.

    Dans ZF tu peux largement raisonner dans des contextes où tu "créées" des "ensembles" de tous les ensembles sans avoir besoin de fioriture

    D'une manière générale, tu disposes aussi de la théorie contradictoire contenant un seul schéma d'axiomes:

    il existe a tel que pour tout x x est dans a ssi R(x) (***)

    Chaque fois que tu y prouves quelque chose, tu ne te sers que d'une liste finie précise de "R(x)", liste à laquelle restreindre (***) n'est pas génant, ni forcément contradictoire. Et ta preuve se type parfaitement chaque fois avec un terme du lambda calcul, dont l'étude te permet de voir au juste où tu as été audacieux (si le terme boucle trop, etc: en termes savants "n'est pas normalisable, ou pas fortement normalisable")


    Les new fundations de Quine sont aussi très simple, elles consistent à restreindre (***) aux R(x) dans les lesquelles on peut associer à chaque variable un numéro de sorte que quand une occurence de u \in v apparait, le numéro associé à v est le successeur du numéro associé à v.

    Dans NF on peut parler de l'ensemble de tous les ensembles, de l'ensemble de toutes les fonctions, etc
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Réponse à GG:

    certes, mais c'est de la psychologie, puisque le mot vrai est le mot le moins défini qu'on puisse imaginer en maths. Par ailleurs sa seule définition ne précise pas son sens, mais précise "l'utilisation du MOT lui-même"

    Moi aussi je suis platonicien, mais pas besoin de référence au mot "vrai" pour ça

    Effectivement tu rappelles l'histoire, mais cependant l'activité mathématique est parfaitement symétrique: chercher des preuves de théorèmes, c'est chercher des contradictions des théories. Il n'y a rien d'autre que nous faisons, et prétendre rechercher des axiomes consistants (ou pire: vrais) est une mauvaise formulation de ce que font ou ont fait des gens comme Godel.

    Les axiomes sont des hypohtèses dont on "ressent" que si on prouve leur négation on obtiendra encore plus de "jouissance" et "compréhension" platonicienne, sans parler des applications.

    Et à les utiliser constamment, on passe notre temps à les attaquer. (tenter de prouver A--->B, c'est "agresser" A)

    Quand certains (ce qui est rare) s'amuse à chercher à prouver un axiome, en général c'est dans un contexte très précis et pour "l'économiser" (et d'ailleurs today, on n'y arrive pas, je veux dire, il y a bien lgtps qu'on a éliminé les redondances) ou pour le "réaliser" (notion récente de lambda calcul) ie obtenir une preuve essnetiellement que pour toute preuve p qui l'utilise il existe une preuve q qui ne l'utilise pas (ce qui permet de le considérer comme "sûr")
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Merci pour les infos, très intéressant. Est-ce que tu as des références de livres ou articles pour quelqu'un qui a un dea (bac+5) de logique mais qui n'a pas fait de lambda calcul, en français ou anglais.
  • EmmanuelCh : tu t'adresses à qui ? Si c'est à moi tu peux regarder le cours du dea mpri http://logical.inria.fr/mpri/ mais seul le début et la fin des notes vont t'intéresser. Sinon il y a le cours du dea de lyon http://perso.ens-lyon.fr/alexandre.miquel/enseignement/ . C'est Alexandre Miquel qui le fait alors la moitié parle de réalisabilité plus que de démonstration standard. C'est dommage qu'il n'y ai pas des cours filmés parce qu'il est très pédagogue.
  • Salut deufeufeu,

    deufeufeu a écrit:
    CCI est une extension équivalente de CC

    Pour quelle notion d'"équivalence" ??

    deufeufeu a écrit:
    L'axiome du choix est prouvable avec une quantification sur Set mais incohérent sur Prop.

    Ça, ça n'est pas vrai. L'axiome du choix avec une quantification sur Set est consistant, mais pas prouvable.
    Quelque soit d'ailleurs le sens raisonnable qu'on donne à la proposition "axiome du choix" (même l'axiome des choix uniques est consistant mais non prouvable).
  • Est-ce que tu as des références de livres ou articles pour quelqu'un qui a un dea (bac+5) de logique mais qui n'a pas fait de lambda calcul, en français ou anglais.

    Le livre de Krivine "lambda calcul typé" est assez complet, mais très formel (mais apparemment le formel et toi, ça va bien donc...)

    Sinon, en étant un peu patient tu peux faire des recherches avec lambda calcul, logique combinatoire sur google


    Sinon, en 2 mots (enfin j'exagère):

    tu transforme toute preuve en "terme" de la manière suivante:

    quand tu viens de prouver P avec un modus ponens sur A--->P et A et si tu supposes que tu as déjà fabriqué un terme u pour la preuve de A---->P et v pour celle de A qui ont précédé, tu "déclares" que le terme u.v est associé à la preuve P

    Ca te permet de mettre en mémoire la preuve.

    Si tu viens de prouver P en utilisant l'hypothèse A (et que tu annonces à l'assistance que tu viens de prouver A--->P, sans utiliser A) tu prends le terme t que tu as fabriqué pour la preuve de P (dedans, il y a des occurences qui correspondent à l'hypothèse A (que tu as juste affirmée donc t'as juste mis une "lettre" x qui signifie (ça c'est le cadeau de A qu'on me fait)) et tu déclares que [lambda x:(t)] est le terme associé à ta preuve de A--->P

    tu prends soin dans la construction de tes termes de toujours bien renommer les variables liées, et de noter sous chaque occurence la conclusion de la preuve (par exemple) au premier cas, quand tu as fait u.v, tu notes sous u la phrase A--->P et tu notes sous v la phrase A

    (lol, faut de la place)

    Voilà à une preuve t'as associé un terme.

    Ce qu'il y a de "magique" et désopilant, c'est

    1) que le terme de redonne ta preuve (ie tu pourrais l'utiliser pour prouver ton truc sans réfléchir:

    voyant u.v tu proposes au sceptique un mod pon et voyant lambda x t, tu dis "je prends l'hypothèse A"

    2) que ton terme est un "programme": tu peux l'exécuter autrement.

    Pour exécuter des pas tu prends une occurence dans u de la forme (lambda x:t).v et tu la changes en t', où t' est le terme obtenu à partir de t en remplaçant chaque occurence libre de x par v (ca le rallonge)

    Le nouveau terme u' ainsi obtenu EST ENCORE une preuve de ton truc

    S'il n'y a rien à exécuter dans u (ie aucune occurence dans u de la forme (lambda x:t).v ) c'est une preuve "idéale" (appelée preuve sans coupure) et les gros gros théorèmes de logique disent que dans toutes les preuves dans des bonnes théories chaque terme u obtenu est tel que qu'on ne peut en exécuter des pas qu'un nombre fini de fois

    Comme il y a toujours plus de généralisations de ce procédé, il y a à chaque fois plusieurs nouveau théorèmes, mais le fil est toujours le même, au point même que dans les théories où ça marche pas, ça donne un critère pour dire qu'elles sentent le souffre
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • CCI n'est pas équivalent à CC, ok. Je voulais dire équivalente dans le sens de rapprocher ce qu'il a fait avec CCI plutôt que CC. Mea Culpa.

    Pour (AC) je n'en sais pas grand chose, mais j'avais lu cela :
    Axiome du choix
    L'axiome du choix (forme fonctionnelle) est dérivable si l'existentielle (notée alors comme un Σ-type) est dans Set ou dans Type :
    (∀ x:X.Σ y:Y. P(x,y))→ Σ f:X→ Y.∀ x:X. P(x,fx)
    Si l'existentielle est dans Prop et Y dans Set, l'axiome est incohérent en présence de la logique classique dans Prop, car alors, on peut injecter Prop dans bool et encoder le système U-.
    ∀ X:Type. ∀ A:Set. (∀ x:X.∃ a:A. P(x,y))→ ∃ f:X→ A.∀ x:X. P(x,fx)
    En fait, une forme beaucoup plus faible de l'axiome du choix (bien que plus compliquée à exprimer), à savoir l'axiome de description suffit à obtenir cette contradiction.

    Remarque: Si Y est dans Type, du fait du sous-typage Set ⊂ Type, la contradiction avec la logique classique persiste.
    dérivable pour moi c'est prouvable pas admissible.

    (En fait, à titre personnel j'ai plutôt fait mumuse avec COQ que du CCI, à regret.)
  • C'est volontaire les smileys?
  • A mon avis oui. C'est pour bien montrer que la logique, c'est :X:X:X:X:X ou à la rigueur :S:S:S (:D
  • Les smileys n'ont pas été prévu pour le typage... x:X lire x : X
  • Ok deufeufeu.

    Je n'avais pas compris. Je pensais que tu distinguais suivant que la quantification se faisait sur Set ou Prop, mais tu distinguais suivant que la quantification se fait à valeurs dans Set ou Prop.

    Cependant, je ne trouve pas pertinent d'appeler "axiome du choix" un énoncé avec des sigma-types plutôt que des existentielles (et ça n'engage que moi !).

    Je pense ne suis quand même pas d'accord avec deuxième partie du propos que tu cites, du moins si celle-ci consiste à dire (parce que c'est vrai qu'avec tous ces smileys :P) : "l'énoncé ∀ A : Set, ∀ B : Set, ∀ P : A→B→Prop, (∀ x : A, ∃ y : B, P(x,y)) → (∃ f : A → B, ∀ x : A, P(x,f x)) est réfutable sous l'axiome ∀ P : Prop, P \/ ~P". En fait je pense que ta citation date du temps où Set était imprédicatif (ou bien je ne l'ai pas comprise).

    J'avoue qu'on dévie grave du sujet, mais c'est tellement rare de pouvoir discuter avec d'autres utilisateurs de Coq sur ce forum que je m'en voudrais de ne pas en profiter :D.
Connectez-vous ou Inscrivez-vous pour répondre.