Lazi

Vue générale de la définition de lazi

Introduction

Ce texte ne présente pas l'intérêt de lazi ni ses propriétés, il n'est pas non plus la définition de la fondation mathématique lazi.
Il chercher à donner une vue synthétique de la fondation mathématique lazi.

Remarque : lazi a des points communs avec le lambda calcul et par exemple "dom p" signifie "dom(p)" en mathématiques classiques.

Plan général de la définition de la fondation mathématique lazi

Le plan général est :

  1. Définition en langage usuel d'une mathématique très simple : lazi.0.0.
  2. Définition en langage usuel d'un système de notations (pour rendre humainement agréable le langage lazi.0.0). lazi.0.0 plus les notations s'appelle lazi.0.1
  3. Définition en lazi.0.1 de la mathématique lazi.1.0

Nous détaillerons plus bas ces 3 parties.

Changement de paradigme

Les mots lazi.0.0 n'ont qu'un seul type (en mathématique classique on a les quantificateurs, les connecteurs logiques, les variables etc).
La sémantique lazi.0.0 et lazi.1.0 n'a aussi qu'un seul type : les choses (en mathématique classique on a les vérités et les ensembles).

Ce changement induit une propriété nouvelle et fondamentale : il est naturel d'exprimer "le sens de la phrase x est vrai". Alors qu'en mathématique classique on peut certe représenter une phrase mathématique par des ensembles, mais certainement pas lui appliquer une fonction qui calcule son sens.

Cette habilité supplémentaire sera utilisée pour représenter et utiliser une mathématique à l'intérieur d'une autre. Cela débloquera toute limitation d'expressivité syntaxiques ou sémentiques puisqu'en définissant de nouvelles mathématiques on peut par exemple ajouter des notations, des nouvelles formes de preuves etc.

Les imbrications des mathématiques Lazi

Nous venons de voir que nous définissons d'abord une mathématique en langage usuel et qu'à partir de là nous définissons dans cette mathématique une autre mathématique Lazi (lazi.1.0).
En lazi il est possible d'utiliser une mathématique à l'intérieur d'une autre. Quand on fait de la mathématique lazi.1.0, c'est à l'intérieur de la mathématique lazi.0.2. Pour cela en résumer on utilisera des formules lazi.0.0 qui représenterons des formules lazi.1.0, des preuves etc.
Par exemple la formule Lexique:Lazi ▶:lazi.0.1 ci-dessous représente une preuve lazi.1.0 de x = x ($T[...] : un uple, $L[ ... ] : une liste, $F[...] : une 1-formule (une représentation d'une formule), 'aaa : un nom, $D[...] : une structure (un dictionnaire).
La preuve ci-dessous se lit ainsi : une preuve dont la liste de déductions comprend en première place une déduction "ifOnOne" où l'on remplace la variable x par "x" et la variable y par "0b" etc

$T[ 'proof, $L[
    $T[ 'ifOnOne, $D[ x = $F[x] , y = $F[0b] ] ], // if 1b x 0b = x
    $T[ 'equalArgs, $D[ x = $F[if 1b x 0b] , y = $F[x], z = $F[equal] ] ], // equal (if 1b x 0b) = equal x
    $T[ 'equalFuncs,  $D[ x = $F[equal (if 1b x 0b)] , y = $F[equal x], z = $F[x] ] ], // (if 1b x 0b = x) = (x = x)
    $T[ 'equalityAndTruth, $D[ x = $F[if 1b x 0b = x] , y = $F[x = x] ] ] // x = x
  ]
]

1 Définition en langage usuel d'une mathématique très simple : lazi.0.0.

Nous définissons d'abord la syntaxe, puis ce qu'est une règle de déduction, puis ce qu'est une preuve, puis ce qu'est une vérité.

Les règles de déductions sont des formules lazi.0.1 augmentées de noms vues comme des variables (toujours x,y et z) remplaçables par n'importe quelle formule. Une règle de déduction comprend une liste de phrases conditions et une phrase conclusion.
Par exemple :

x, x = y
--------
   y

est la règle signifiant que si x et x = y sont vrais alors y est vrai.

Une preuve lazi.0.2 est une liste finie de déductions. Une déduction est une structure comprenant le nom de la règle et les valeurs des variables de la règle.
Pour qu'une preuve soit valide il faut que chaque déduction soit valide. Pour qu'une déduction soit valide il faut que les conditions soient des conclusions des déductions précédantes de la preuve.

x est une vérité lazi.0.2 s'il existe une preuve valide où x est la conclusion de la dernière déduction.

2 Définition en langage usuel d'un système de notations

Ces notations permetrons de représenter des fonctions à variables, des uples etc. Toute formule avec notation (c'est à dire lazi.0.1) se traduit de manière univoque en formule lazi.0.0.

3 Définition en lazi.0.1 de la mathématique lazi.1.0

Les règles de déductions lazi.0.0 sont composées de 6 règles très simples et d'une septième signifiant que si une preuve lazi.1.0 sans hypothèse (les preuves lazi.1.0 peuvent contenir des hypothèses) déduit x, alors on déduit le sens de x.

Remarquez que l'on ne déduit pas x : x est une formule lazi.0.0 représentant une formule, et pour passer de la représentation d'une formule à son sens il nous faut appliquer une fonction.

Au premier abord il peut sembler complexe de naviguer dans les représentations de formules, de preuves, de mathématiques etc. En pratique cela est transparent et on l'oublie, de même que quand on écrit un texte à l'ordinateur nous ne sommes pas obligés d'avoir conscience qu'il s'agit de tables de caractières unicodes elles-mêmes codées d'une certaine manière.

Les extensions mathématiques

Résumer :

Nous allons voir que nous pouvons créer et utiliser de nouvelles mathématiques du moment qu'une partie "naturelle" des preuves est traduisible. Nous pourrons utiliser toutes ces mathématiques en nous passant d'imbrications récursives.

Supposons que l'on définisse en lazi.0.1

  • une nouvelle mathématique M1
  • une fonction de traduction tr
  • un domaine dom
tels que
  • pour toute preuve p dans M1, si on a dom p alors tr p est une preuve dans lazi.1.0
  • toute preuve p de M1 sans conditions et prouvant une formule qui a un sens en lazi.1.0 vérifie dom p

Peut-on alors utiliser M1 pour faire des mathématiques sans pour autant passer par un raisonnement méta-mathématique (étape nécessaire en mathématique classique si on veut utiliser une extension comme par exemple l'analyse non standard) ?

Supposons que l'on ait une preuve p dans M1 vérifiant dom p. tr p est alors une preuve dans lazi.1.0 et notre septième règle déduit en lazi.0.0 le sens de la 1-formule déduite par tr p.
Par exemple si M1 était incohérente alors lazi.0.0 serait incohérente.
La réponse est donc affirmative.
M1 peut être définie en lazi.0.1, et il est donc inutile de faire des mathématiques M1 en lazi.1. On voit que l'on n'a pas d'escalade d'imbrications quand on cré des extensions.

Regardons maintenant le cas général : Nous avons 3 mathématiques M0, M1 et M2, où M1 est définie en M0 et M2 en M1. Nous voulons utiliser dans M1 une preuve dans M2 traduisible en preuve de M1. Pour cela nous utilisons M0 pour prouver que la traduction est une preuve de M1 et donc nous pouvons utiliser le résultat de la preuve dans M2 dans M1.

Nous n'avons traité ici que les extensions traduisibles. Et par exemple je pense qu'il est impossible que la théorie des ensembles soit vue comme une extension du fait de propriétés fondamentalement différentes. Mais il me parait claire que cette limitation est en fait plus un guide de bonne conduite ne limitant en rien la construction des abstractions qui nous sont utiles.

Et après ?

Lazi.1.0 ne comprend pas de quantificateurs, ni de variables, ni la possibilité de définition. Mais toutes les caractéristiques des mathématiques usuelles seront définies par des extensions (y compris des notations).