Lazi

Simplicité de Lazi

La simplicité d'une fondation mathématique peut s'appréhender par plusieurs aspects :

  • La réduction des ambiguïtés
  • La réduction des notions de base nécessaires à la définition
  • La réduction de la complexité de la construction nécessaire à la définition
  • La réduction de la complexité des règles définissant la fondation (par exemple les règles définissant les phrases mathématiquement correcte ou encore les règles de déduction)

Les ambiguïtés

La définitions de la fondation Lazi commence par la définition en quelques pages d'une fondation très petite et simple, permettant uniquement de faire des calculs. Tout ce qui suit cette fondation minimale est entièrement formel et donc sans ambiguïté. La fondation Lazi est donc minimale point de vue ambiguïté.

Notions de base nécessaires

Lazi n'utilise pas d'objet complexes (telle qu'une autre fondation mathématique) pour sa définition. Les structures utilisées sont les arbres binaires finis et les listes finies. Les fonctions utilisées sont des fonctions simples comme celles de constructions par assemblage.

Complexité de la construction nécessaire à la définition

Quelques pages de définitions son nécessaires pour construire par exemple une notion liste ou encore de type informatique. Ce sont des notions standards nécessaire à tout traitement de données. Vérifier une preuve et donc définir ce qu'est une preuve est un traitement de données. Ces constructions seraient nécessaire à tout système formel définissant une fondation mathématique complète.

Complexité des règles

Les règles pour la partie syntaxe et grammaire du langage sont particulièrement simples, il n'y a même pas à définir la notion de variable car elle est définie plus tard dans des extensions.

Lazi comprend 6 règles de déductions de base, toutes triviales, l'une des règles est par exemple "if 1b x y = x". Toutes les autres règles de déduction n'ajoutent pas de vérité supplémentaire aux vérités exprimables dans le langage de base. Toute preuve aboutissant à une vérité exprimable dans le langage de base est traduisible en une preuve n'utilisant que les 6 règles élémentaires.

Remarquons toutefois que la preuve démontrant cette dernière affirmation utilise des règles qui ne sont pas dans les 6 règles de base (par exemple la règle de récurrence). On possède une fonction explicite de traduction, mais la preuve de ses propriété nécessite (on s'en doute) des règles plus sophistiquées comme la récurrence. Toutefois les règles supplémentaires pour prouver cette propriété sont minimaliste et il me parait impossible qu'une mathématique digne de ce nom (c'est à dire capable de prouver des propriétés générales) en ait de moins fortes.

Lazi comprend 0 axiomes (à comparer à l'infinité d'axiomes — dit autrement "shéma d'axiomes" — de ZFC).