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 https://lazi.bobu.eu/wiki_old/index.php/%C3%89tudes-Math%C3%A9matique/R%C3%A8gles_de_d%C3%A9duction/Extensibilit%C3%A9

Question

Quelles sont les propriétés que doivent avoir les fondations et quelles règles de déduction sont nécessaires ?

Étude

Erreurs passées

J'avais ajouté le tiers exclu et la récurrence à lazi.1.0 pour pouvoir déduire des propriétés mais il me semble que ça ne suffit pas pour pouvoir appliquer des vérités d'une extension à la mathématique de base de manière simple (sans avoir à vérifier une longue preuve).
En effet, pour pouvoir déduire des vérités à partir d'une abstraction de preuve on a plusieurs cas :

  • la vérité provenant de la preuve doit être déduite dans une autre mathématique que celle en contexte : il n'y a alors pas besoin de règle particulière.
  • la vérité preuvenant de la preuve doit être déduite dans la mathématique en contexte : il faut tuiliser
la règle de la descente. Si l'abstraction de preuve demande une traduction (car elle représente une preuve utilisant d'autre règles que celle de la mathématique courante), alors on a deux manière de procéder :
  • par une fonction qui fait directement les calculs
  • en utilisant des vérités universelles (donc par une formule utilisant des quantificateurs et implications).

C'est pour ce dernier cas que j'avait ajouté les règles du tiers exclu, mais il faut aussi d'autres règles. Donc il vaut mieux découper autrement les mathémtiques définies :

  • une mathématique très simple servant de base au définitions et calculs lazi.0
  • une mathématique de base définie formèlement (lazi.1)
  • une mathématique comprenant les quantificateurs, implications etc.

Définitions

Une ctruth est une liste de formules formant les conditions (les prémisses) et une formule conclusion (la vérité déduite)

Une mathématique est un type de déduction, les objets de ces déductions sont les ctruths déduites. Une mathématique doit aussi comporter le champs "formulaT" qui est le type des formules de cette mathématique.

Une mathématique est extensible ssi toute vérité démontrable peut se déduire à partir de représentations internes de déductions.

Une mathématique est complètement extensible si elle est extensible et que en plus elle est assez expressive pour pouvoir déduire que toute vérité traduisible d'une extension se traduit en vérité.

Usage de la règle de la descente

La règle de la descente permet de déduire une vérité à partir de la représentation d'une déduction dans la mathématique en cours. Les déductions de cette règle son traduisible : on traduit une telle déduction par la déduction représentée.

Si on n'a pas la règle de la descente alors il est nécessaire de faire de la métamathématique (c'est à dire de sortir du contexte mathématique dans lequel on est) pour utiliser une autre mathématique.
Par exemple si on a un logiciel qui vérifie les preuves dans une certaine mathématique M, avec la règle de la descente il est possible d'utiliser toutes les abstractions que l'on souhaite (dont des mathématiques différentes de M) pour déduire des vérités de M.

Si la mathématique n'est pas construtive alors une déduction provenant de la règle de la descente n'a pas forcément de traduction car il devient possible de prouver que quelque chose existe sans pouvoir l'explicité. Or il est nécessaire d'explicité la représentation de la preuve en condition de la règle pour pouvoir la traduire.

Dans quelles mathématiques ajouter la règle de la descente

À prioris il faut ajouter cette règle à chaque mathématique qui est utilisée pour raisonner sur des preuves utilisant la mathématique elle-même. Mais si on fait les déductions dans une mathématique parent alors il n'y a pas besoin de la règle de la descente, même dans la mathématique parent. Car la règle de la descente n'est utile que pour raisonner sur la mathématique que l'on utilise pour faire le raisonnement.

Donc à partir du moment où une mathématique parent possède le type de formule nécessaire à l'expression des propriétés que l'on veut démontrer sur une mathématique enfant, la règle de descente n'est plus nécessaire. Elle peut quand même être ajoutée pour pouvoir raisonner avec la mathématique en cours.

Il me parait possible de créer une fonction qui cré, à partir d'une mathématique M1, une mathématique M2 qui est M1 avec la règle de la descente en plus.

Imbrication et désimbrication des extensions

Quand on cré des extensions, on le fait à partir d'une certaine mathématique M1. Puis l'ensemble des extensions servent à définir une mathématique M2. On peut par la suite de la même manière définir M3 à partir de M2 etc.

En supposant que l'on ne dispose que d'un logiciel vérifiant les preuves M1, on peut se demander si pour vérifier une preuve en M8 il est nécessaire de par toutes les mathématiques parents. Cela dépend, il peut être possible de réduire la filiation. En pratique un logiciel de vérification de preuves Lazi aura des systèmes pour faciliter l'utilisation des extensions de sorte qu'il sera aussi pratique d'utiliser M8 que M1.

Réorganisation de la construction de lazi

On définit chaque mathématique ci-dessous par le type des déductions. Celui-ci comprend le type des formules que l'on explicitera aussi si nécessaire.

lazi.0.0

Présentation

C'est une mathématique minimale pour réaliser les calculs sur les formules. Elles ne permettent pas de déduire toutes les vérités lazi.1 sur les formules. Il y a peu de liberté dans le calcul des formules.

Le type des déductions

Une déduction est une liste de déduction simple. Pour quelle soit valide il faut que chaque condition de déduction simple soit prouvée auparavant. L'objet d'une déduction est l'objet de la dernière déduction simple.

Les règles de déduction simples

if 1b x y = x
if 0b x y = y
si x = y alors x z = y z
si x = y alors if x = if y
distribute x y z = (x z) (y z)
si x = y et y = z alors x = z

lazi.0.n

C'est lazi.0 auquel on ajoute des notations. Ces notations sont définies dans la langue naturelle. On peut les traduire pour obtenir une définition de lazi.1 sans notation, mais cela rendrait la lecture très pénible.

lazi.1.0

Présentation

Défini en lazi.0.n, le type des formules est celui de lazi.0, on étend un peu les règles.

En lazi.1, l'objet d'une déduction n'est pas une formule mais une ctruth : une liste de formules formant les conditions plus la formule conclusion.

Langage de définition

Lazi.0.n

Type des formules

Ce sont les mêmes formules que lazi.0

Le type des déductions

C'est l'union des types de déduction suivant :

Les règles simples
if 1b x y = x
if 0b x y = y
si x = y alors x z = y z
si x = y alors z x = z y
distribute x y z = (x z) (y z)
si x et x = y alors y

La règle de la preuve
On déduit une ctruth à partir d'une liste de déduction.

lazi.1.1

Présentation

C'est lazi.1.0 plus la règle de la descente qui permet d'utiliser des représentations de déduction pour déduire des vérités.

Langage de définition

Lazi.0.n

Type des formules

Ce sont les mêmes formules que lazi.0

Le type des déductions

C'est l'union du type des déductions lazi.1.0 avec la règle de la descente.

La règle de la descente
Si x est une déduction lazi.1.0 alors on déduit la traduction de l'objet de x.

lazi.2

Présentation

On ajoute des règles pour avoir une mathématique complètement extensible (quantificateur, implication etc).

Faut-il ajouter la règle de la descente ?

Si on ne l'ajoute pas alors si on veut déduire des vérités provenant d'extension il est nécessaire de passer par lazi.1 et une fonction de traduction. Si on l'ajoute on peut alors juste appliquer un théorème.

Réponse

@todo