Lazi

Caractéristiques des mathématiques lazi

Dans ce contexte : la fondation mathématique Lazi

Interrogeons nous sur son adéquation avec les principes du rasoir d'Occam et d'autonomie "prouvés" ci-dessus.

Remarque : j'invite le lecteur sceptique devant les caractéristiques de Lazi décrites ici à vérifier par lui-même par la lecture de la définition de Lazi.

Critères numériques simples

Composant Mathématiques classiques Lazi
nombre de symboles 8
règles de grammaire nombreuses (notions de termes, variables, quantificateurs,connecteurs logiques) 2
règles de déductions nombreuses, voir Calcul des séquents et Calcul des prédicats 10
nombre d’axiomes 9 plus un shéma d’axiomes (= ∞) 0

D'autres critères

Autonomie

Nous définissons ici la notion d'autonomie d'une fondation mathématique comme sa capacité à ne pas nécessiter d'être changée au cours du temps.

Dans les mathématiques classiques

On ne peut utiliser une extension à la fondation (par exemple comme l'analyse non standard) dans une preuve. En mathématique classique pour utiliser une extension il faut prouver sa cohérence et prendre une décision d'utiliser cette extension. Cette décision ne peut être incorporée à une preuve même si on ajoutait un éventuel axiome d'extension à la fondation car alors l'incorporation de vérités provenant de représentations de preuves mèneraient à une incohérence (voir la démonstration du premier théorème de Gödel).

On peut remarque que ce manque d'autonomie se fait déjà ressentir et a provoqué la naissance de la théorie des catégories.

Les notations ne sont pas intégrées à la fondation mathématique. Un programme de vérification ne peut offrir un traitement des notations plus ouvert (extensible) et solide (basé sur des preuves mathématiques) que les fondations qu'il vérifie car il serait incohérent d'utiliser pour les notations un système plus puissant que les fondations dont on vérifie les preuves.

En Lazi

Il n'y a aucun présupposé fort (comme le tiers exclu en mathématiques classique) orientant la fondation. C'est à dire que l'on ne peut manifestement envisager de règles de déductions plus faibles sans rendre impossible la pratique mathématique.

La règle d'extension permet de définir des notations ou d'autres sortes de mathématiques, tant que l'on peut prouver la traductibilité (ce qui prouve aussi sa cohérence) de l'extension. Il en résulte que l'on peut utiliser Lazi pour pratiquer d'autres mathématiques tant que l'on peut prouver qu'une sous-partie des preuve est traduisible.
Remarque : cela implique que l'on ne peut définir les mathématiques classiques directement comme une extension, néanmoins il me parait quand même possible de récupérer les théorèmes ayant des conséquences pratiques (directes ou non).

Étendue des bases informelles

Cette partie sert à mesurer la simplicité et la fiabilité de la définition d'une fondation. En effet on conçoit bien qu'un texte en langage courant de cent pages faisant appel à divers notions (comme l'infini) est plus fragile qu'un texte comprenant quelques pages utilisant des notions simples et suivi dans pour le reste d'un texte en langage formel.

Nous définissons ici l'étendue des bases informelles comme la quantité de texte nécessaire avant qu'il soit possible de définir formellement la fondation par un formalisme définit dans la définition de la fondation.

Dans les mathématiques classiques

Toute la fondation, sauf quelques lignes, est définie informellement. La quantité de texte nécessaire me parait difficile à évaluer tellement le découpage, le non formalisme et la diversité des approches est grande.

En Lazi

Après environ 15 pages la définition de Lazi est formelle (et d'ailleurs lue par le logiciel de vérification de preuves Lazi). Aucune notion d'infini n'est utilisé.

Unification fondation mathématique / informatique théorique

Le cœur de la fondation mathématique Lazi est un système formel Turing-complet. Les règles de déduction ajoutées à ce système sont minimales afin d'obtenir une fondation mathématique. Si une vérité exprimable dans ce système minimal est déduite avec des règles ajoutées, alors il existe une traduction de la preuve dans le système minimal. Il en résulte par exemple que le quantificateur existentiel est constructif.
De ce fait les théorèmes d'informatique théorique sont directement applicable à Lazi et inversement toute vérité déduite exprimable dans le système formel de base est applicable à l'informatique théorique. On obtient donc une unification de l'informatique théorique avec la mathématique Lazi.