Lazi

Quelles règles pour lazi.1.0

Contexte

En rellisant la "Vue générale de la définition de lazi" je m'intéroge sur l'intérêt d'ajouter la règle du tiers exclu et de la récurrence. Peut être qu'à l'époque je pensais que ces déductions n'était pas traduisibles ? Ou alors est-ce par nécessité de faire certaines démonstration ?

Voir aussi l'ancienne étude.

Question

Quelle est la définition d'une mathématique extensible et comment arriver à définir une mathématique extensible avec Lazi.

Étude

Définition d'une mathématique extensible

Une définition informelle :

Une mathématique est extensible ssi elle n'a pas de limite d'expressivité.

Si dans une mathématique on peut y définir et utiliser (pour prouver des vérités dans la mathématique de base) une autre mathématique alors elle est extensible. En effet, toute création mathématique envisageable peut se faire dans une certaine mathématique, comme cette mathématique est utilisable dans la mathématique extensible, toute création mathématique enfisageable peut être utilisée dans une mathématique extensible.

Si une mathématique n'a pas de limite d'expressivité alors on peut y définir une autre mathématique et l'utiliser (dans la mesure où il y ait un sens et où les preuves sont traduisibles) dans la mathématique de base.

Définition plus formelle :

Supposons que l'on ait un logiciel L qui permette de vérifier les preuves d'une mathématique M. On souhaite ne pas modifier L tout en pouvant faire toute les mathématiques que l'on souhaite. Il faut donc que M permette de définir une mathématique M2 et que les déductions de M2 transposables dans M (il faut que la vérité déduite par M2 ait, après traduction, un sens dans M et que la logique de la démonstration dans M2 soit transposable dans M) puissent être utilisée directement.

L'utilité d'une mathématique extensible est seulement l'éfficacité

La règle d'extension ne permet pas de démontrer de vérité supplémentaire. Le seul avantage est de factoriser les démonstrations en une partie commune qui est une nouvelle mathématique.

Nécessiter d'une règle pour rendre une mathématique extensible

Sans règle spéciale une mathématique n'a pas de "connaissance" de ce qu'elle est, et donc il n'est pas possible qu'une représentation de démonstration puisse servir à déduire une vérité. C'est pourquoi nous allons ajouter une règle.

Soit M une mathématique et M/M la représentation de M dans M.

Soit MD, M où l'on a ajouté la règle D (dite règle de la descente) définie par :

si d est une déduction de M/M alors on déduit l'interprétation de la représentation de vérité déduite par d.
Comme M est une mathématique constructive on peut expliciter d et traduire une déduction de D par l'interprétation de la déduction.

Si M contient les outils usuels des mathématiques classiques (quantificateurs, implication, tiers exclu) alors on peut dans M définir une mathématique N, prouver que pour un certain sous-ensemble de déduction de N, il existe une traduction en déduction M/M et donc déduire ainsi des vérités provenant de N. La règle précédente est donc suffisante (et évidemment nécessaire) pour que la mathématique soit extensible.

Si on n'a pas les outils usuels, il faut une règle minimale, qui permette de généraliser un raisonnement puis de l'appliquer à des cas particuliers. Cette règle sera utile dans une mathématique contenant deux règles nécessaires à la généralisation : le tiers exclu et la récurrence. C'est la règle suivante, dit règle de généralisation primitive, elle correspond à "∀ x; d x ⇒ tr x" :
: paramètre d (le domaine), tr (la traduction),x (la variable), p (la preuve), a (la valeur sur laquelle appliquer la règle) :

  • d,tr,a sont des formules
  • x est une variable
  • p est une preuve où x est une variable déduisant la ctruth de condition "d x" (plus exactement d +f x) et de conclusion "tr x".
Alors on déduit la ctruth :
  • condition : "d a"
  • conclusion : "tr a"

Avec la règle de la généralisation primitive, cela permet d'utiliser des vérités déduites dans une autre mathématiques. On doit à chaque fois fournir la preuve de la validité de cette mathématique, mais cette preuve est identique pour chaque déduction utilisant la même mathématique.

Analyse point de vue efficacité des calculs

Tant que l'on ne peut pas stocker des résultats ce qui impliquer de modifier la mathématique, voir les déductions "évènements", alors l'efficacité des calculs des abstractions — telles que les deux règles ci-dessus — est négative car on cré des abstractions puis on les traduits à chaque fois. Donc du point de vue des mathématiques sans évènement, toutes ces abstractions sont inutiles du point de vue efficacité des calculs ( mais pour nous c'est utile puisque l'on peut copier-coller de grosses parties).

Est-ce un problème de créer dans un premier temps des règles qui n'ont pas d'utilité point de vue calcul ? De toute manière il on est obligé de créer beaucoup de chose avant de pouvoir améliorer l'efficacité. Rien ne dit qu'elle se mesure d'après les mathématiques à la base. On peut voir les mathématiques à la base comme un cadre de définition. Donc ce n'est pas un problème.

Que doit comporter la fondation Lazi ?

La mathématique fondation Lazi doit comprendre, pour être extensible (et donc la fondation), les règles suivantes :

  • les règles de base
  • tiers exclu
  • récurrence
  • généralisation primitive
  • la descente

Pour l'exprimer il faut définir M/M et des propriétés sur des objets de M/M. Ce qui est à première vue laborieux.

Utilité de définir tôt une mathématique extensible ?

Il y a une utilité d'avoir une mathématique extensible simple, car ça sera la fondation mathématique, une fois obtenu il n'y aura plus besoin d'ajouter d'axiomes. Mais "simple" et "tôt" sont différents car on peut définir d'abord des extensions puis une fois acquis suffisamment de puissance on peut définir la mathématique fondation par traduction.

Donc le plus simple est de définir des extensions de Lazi.2 pour finir par définir la version finale de lazi.1 (en ajoutant la règle de la descente) par la suite. Ce n'est pas une définition récursive car Lazi.2 est utilisé comme un moyen de calcul de Lazi.1 et il n'y a pas de référence de Lazi.2 dans Lazi.1.
Concrètement :

Les différentes versions de Lazi.1.*

  • Lazi.1.0 : c'est la mathématique comportant les mêmes règles de déductions que lazi.0.0 plus la règle de la preuve.
  • Lazi.1.1 : ajout du tiers exclu
  • Lazi.1.2 : ajout de la récurrence
  • Lazi.1.3 : ajout de la généralisation primitive
  • Lazi.1.4 : ajout de la descente
Donc Lazi.1 = Lazi.1.4

Les différentes versions de Lazi.2.* nécessaires à la définition de Lazi.1.4

Il faudra ajouter les extensions suivantes :

  • évènements : pour modifier la mathématique
  • Def : pour avoir des définitions
Et toutes les représentations de formules utilisé dans lazi-compute, car pour pouvoir démontrer des propriétés sur lazi.1.4 il faudra passer par ces représentations (fonction, objet etc), pour toutes ces représentations il faudra prouver des propriétés.

Réponse

Voir l'étude. Donc il faut remanier les sources et définitions de lazi.