Lazi

Sous-mathématique et équivalence

Contexte

Pour définir les calculs et les interpréteurs, il est nécessaire de voir si on peut tout ramener à lazi.1.0 ce qui simplifierait et permetrait de comparer.

Question

Si M1 est définie dans la mathématique M0, si M2 est une extension de M1 définie dans M1, peut-on trouver un équivalent définie dans M0 ?

Étude

Définissabilité dans M0

Question : Une formule M2 dans M1 est une formule M1. Dans M1 il existe une propriété p définissant les formules M2, existe-t-il une propriété q de M0 définissant les formules M1 qui représente des formules M2 ?

Soit f une formule M1, si on calcule p f alors on a 0b ou 1b de M1 en résultat.

Calculer dans M0 une formule M1

Soit f une formule M1, comment la calculer ?

Il n'y a pas forcément de calcul possible, par exemple si la formule commence par "∀...". Donc la bonne question est :
Soit f une formule calculable pour M1, comment la calculer dans M0 ?

On peut remarquer que f peut contenir des élément lexicaux propres à M1, comme par exemple des noms définis. Prenons ce cas en exemple, il faut alors récupérer les valeurs des noms pour calculer la formule. On peut avoir des règles de déductions effectuant cette tâche mais ce n'est pas obligé. On peut avoir la fonction de traduction qui effectue cette tâche mais on est juste sûr de l'existance des traductions quand la conclusion est une formule M0, et encore pour cela il faut fournir la preuve correspondant au calcul, ce que l'on n'a pas automatiquement.

On voit donc que l'on a besoin d'une fonction "calculator" (que j'appelais avant "interpréteur") associé à une mathématique de sorte de pouvoir calculer les formules.

Définir une fonction "calculator" par mathématique ?

Remarquons que l'on a besoin aussi de prouver que la fonction fournie des formules égales. Une telle fonction devrait avoir les propriétés suivantes :

  • prendre en argument une formule
  • retourner une formule
  • il devrait exister une fonction qui prend en argument la formule de départ et retourne une déduction prouvant l'égalité calculée.

Mais alors pourquoi ne pas directement demander à l'existance d'une fonction qui prend en argument une formule et retourne la déduction prouvant un calcul élémentaire ?
Dans ce cas on a toutes les informations nécessaires mais on pert l'efficacité car cette fonction doit calculer bien plus.
On peut aussi demander l'existance d'une fonction retournant un couple (résultat, déduction).

Étudier la notion d'extension définie en interne

J'ai déjà définie ce qu'est une extension, mais définie en lazi.1.0, mais je n'ai pas définie ou étudier la notion d'extension définie en interne. Il me semble nécessaire de faire cette étude.

Si dans le contexte M0 on définie une mathématique M1 et que dans le contexte M1 on définie une mathématique M2, alors pour utiliser M2 dans le contexte M0/M1 il est nécessaire de calculer les fonctions

Réponse

Non, car on peut avoir des règles déduction de M2 qui prouvent des vérités n'ayant pas de sens en M1.

Par ailleurs cette étude a montré que nous devons, au moins dans le cadre des calculs, ajouter à la définition d'une mathématique une règle de calcul simplifiante pour pouvoir calculer les fonctions de la nouvelle mathématique. Ainsi, si nous y définissons par exemple une autre mathématique, nous avons alors une manière d'utiliser cette nouvelle mathématique puisque l'on peut calculer les fonctions qui la définisse.

@todo