Lazi

Extension mathématique définie en interne

Contexte

J'ai déjà défini ce qu'est une extension, mais définie en lazi.1.0, et je n'ai pas définie ou étudier la notion d'extension définie en interne.

Question

Comment définir une extension définie en interne ? C'est à dire qu'une mathématique M1 définit une mathématique M2.

Étude

Le contexte M0/M1/M2

Voir la définition des contextes.

Soit M0 (qui sera normalement lazi.0.2) dans laquelle on définit une mathématique M1 dans laquelle on définit une mathématique M2.

Dans M1, M2 est définie par des propriétés :

  • être une formule.
  • être une déduction.

Les formules M2 sont exprimées en M1 donc du point de vue de M0 ce sont des formules M1 particulières.
Mais si on veut se ratacher à la définition d'extension mathématique définies précédemment et où toutes les mathématiques étaient définies en lazi.1.0, il faut que l'on puisse faire une sorte de traduction de sorte que les élément de lazi.1.0 soient vue comme tel. On ne peut avoir automatiquement une traduction de l'extension car il peut y avoir de nouvelles manières de représenter les déductions.
Il me semble qu'il faut étendre la définition des extensions.

Calculs des formules M1 :

Comme le calcul des propriétés doit aboutir à 0b ou 1b (du M1), on voit qu'il suffirait que M0 puisse calculer les formules de M1 pour avoir une définition de M2. Mais il faudrait aussi pouvoir traduire certaines preuves, mais cela peut aussi se faire si M0 peut calculer les formules de M1.
Si la traduction se fait vers Lazi.1.0/M1/Lazi.1.0 , il faut un moyen de traduire une formule lazi.1.0/M1/lazi.1.0 en lazi.1.0.
Cela est possible par l'application de la fonction "object" "des types formule". Remarquons que cela fonctionne même avec les "dvar".
Mais si par exemple la formule à calculer contient au départ un symbole non traduisible (comme "∀") ?

En résumé :

  • Il nous faut en M0 un calculateur de formules M1
  • Une propriété dans M1 (par exemple pour définir les formules de M2) peut alors, grâce au calculateur, devenir une propriété M0 sur les formules M1.
  • Grâce à la fonction "object", on peut accéder aux sens d'éléments de base comme la structure CTruth.
  • Il faut la preuve que le calculateur produit des égalités.
  • Il me semble que l'on a donc tous les éléments (reste à définir le calculateur) pour que M0 voit, à travers M1, M2 comme une extension de M0, M1 ou d'une autre mathémtaique.

Minimum pour définir une extension mathématique

  • Une propriété p et une fonction tr tq si p x alors tr x une preuve lazi.1.0

Ramener toute mathématique au contexte lazi.1.0

On a vue que l'on doit ajouter une règle de calcul à la définition d'une extension.
L'idéal serait de montrer que si M1 est une extension mathématique définie en lazi.1.0 et si M2 est une extension mathématique de M1 définie en M1, alors M2 peut se définir en lazi.1.0.

Donc les formules pour définir M2 sont dans le contexte H/lazi.1.0/M1.

Ce que l'on a besoin pour définir une mathématique M2 dans le contexte H/lazi.1.0/M1 :

  • une fonction pour calculer les formules de M1
  • la fonction "apply" de M1
  • une fonction pour tester l'égalité à la formule 1b ou 0b
  • M2

Réponse

@todo