Lazi

Comment la fondation mathématique Lazi est définie

On peut résumer une fondation mathématique à deux fonctions:

  • Une fonction définissant ce qu'est une preuve.
  • Une fonction prenant en argument une preuve et retourant l'objet de la preuve (la phrase mathématique démontrée par la preuve).

On construit ces fonctions par étapes, comme par exemple la définition des symboles utilisés, les différentes règles de déductions etc. Nous verrons plus loins quels sont ces étapes pour Lazi.

Mais cela ne suffit pas, il est aussi nécessaire que les vérités mathématiques (les objets des preuves) expriment toutes les vérités, et seulement les vérités, détachées de tout contexte. Le sens commun de ce dernier critère fait concensus et nous n'y ajouterons qu'un point que l'on peut résumer par "autonomie".

Autonomie

Quelle est la place de la notion de vérité et des mathématiques dans notre esprit ? Et dans notre univers ?

À ces questions, nous les singes fraichement sortis de la forêt que nous sommes, donnons des réponses, plus par confort que par intérêt réel. Ainsi on plaçait la terre au centre parce que c'est rassurant, n'autait-on pas les même motivations pour les mathématiques ? Bien des personnes considèrent les mathématiques comme un simple outil d'esprit, une invention humaine, Un autre postulat serait que ces questions n'auraient pas de conséquences pratiques.

Nous allons ici gentiment contredire cette vision des mathématiques à la manière de Galilée : nous allons montrer que les choses fonctionnent beaucoup mieux en faisant autrement. Nous allons ici placer les mathématiques au centre et les voir comme une réalité, au même titre que l'existance de notre univers. Comme Galillée nous inviterons nos lecteurs à voir cette hypothèse comme purement théorique et seulement nécessaires aux besoins de la construction de Lazi.

Cela a pour conséquence des exigences supplémentaires sur les fondations mathématiques, que nous détaillons ci-dessous.

Application du principe du rasoir d'Ockham

Comme toute représentation de la réalité, le principe du rasoir d'Ockham s'applique. Donc nous ne cherchons pas ici une fondation pratique pour faire des mathématiques mais :

  • dont la définition est la plus simple possible
  • dont l'utilisation est la plus puissante possible : permetant d'exprimer sans limite tout raisonnement valide sous toute forme possible

Simplicité de la définition

Cela passe par la définition d'une base très petite, permetant à la fois:

  • de ne pas douter de la cohérence des règles
  • de servire de formalisme de base à la définion de la suite des fondations.

Ainsi mis à part cette petite base, Lazi est défini de manière complètement formel, sous forme de sources dont les fonctions sont calculables par l'interpréteur Lazi.

Puissance d'utilisation

On pourrait imaginer que l'on ne peut pas définir une notion de puissance pour une fondation mathématique. Mais nous devons ici regarder la mathématique comme une chose séparée de l'esprit humain. La fondation mathématique étant isolée, elle doit pouvoir être la base de toute invention mathématique à venir, même s'il s'agit de nouvaux formalismes et de nouveux types de raisonnements. On peut alors se poser la question suivante: "À partir d'un raisonnement dans un certain formalisme et suivant certaines règles de déductions, puis-je l'exprimer simplement dans la fondation mathématique ?"

On peut voir que les fondations mathématiques utilisées actuellement ne répondent pas à ce critère car il est impossible de produire des vérités en passant par exemple par l'analyse non standard ou encore la théorie des cathétories.

Pour pouvoir utiliser d'autres formes de raisonnement dans une fondation mathématique il faut une règle supplémentaire, qui n'existe pas dans les fondations classiques, et qui permet sous certaines conditions de validités, d'intégrer des vérités provenant d'une preuve d'une autre fondation mathématique. Cette capacité à utiliser d'autres formalismes sera nomé l'extensibilité.

C'est ce que nous ferons en Lazi. Grâce à cette propriété d'extensibilité, nous pourrons partir d'un noyau très petit puisqu'il ne contient ni les quantificateurs ni les variables (pourtant à la base du lambda calcul). Ces notions seront définies par la suite en Lazi.1, par des Lexique:extensions.

Les extensions nous permetrons aussi de définir des notations qui seront, à partir de Lazi.1, intégrée à la mathématique.

Les étapes

La base : Lazi.0.0

Nous définissons le langage mathématique, ce qu'est une règle de déduction, comment déduire des vérités à partir de ces règles et 6 règles de déductions.

Ces règles permettent de calculer des expressions, c'est ainsi que le logiciel lazi-compute permet d'exécuter ces calculs. Il s'agit de calculs mathématique, c'est à dire qu'il est possible de produire une preuve Lazi des égalités prouvées.

Notations externes : Lazi.0-n

Lazi.0.0 est pénible à utiliser sans notation, qui ne peuvent pas à cette étape être vue comme des objets mathématiques. Nous définissons donc des notations au sens traditionnel des mathématiques.

Compléter Lazi.0

Afin de rendre Lazi extensible il est nécessaire d'ajouter 3 règles, deux pour généraliser les raisonnements et une pour l'extensibilité.

Les deux règles permetant de généraliser les raisonnements sont des versions (faibles par rapport au standard) de raisonnement par récurrence et de tiers exclu.

Ces 3 règles n'ajoutent pas de mots clés et sont traduisibles en Lazi.0.0. Ce qui fait qu'elles sont intégrées à la fondation, et non des extensions, est qu'elles sont nécessaire à la preuve et l'utilisation des extensions.

@todo : à relire et éventuellement enlever, voir "vue générale de la définition de lazi"