Études-Mathématique/Extension par règle simple

From Lazi wiki
Jump to: navigation, search

Question

Un contexte mathématique étendue à des variables globales permet de déduire une règle simple : la règle simple est constituée des variables globales ajoutées et des conditions et de la conclusion d'une déduction.

Comment créer et utiliser une extension permettant d'ajouter ces règles simples déduites ?

Étude

L'utiliser avant la preuve de la validité de l'extension

Pour l'utiliser avant de prouver la validité de l'extension il suffit de définir une traduction des déductions de l'extension en déduction Lazi1.

Changer le contexte mathématique pour chaque règle simple ajoutée

L'idée est de mettre les règles simples déduites dans le contexte mathématique. Il faut donc que l'instance de la règle d'ajout d'une règle simple soit les données d'ajout d'une règle simple plus d'une déduction.

Sans changer le contexte mathématique ? (non retenu)

Si l'ajout d'une règle simple ne change pas le contexte mathématique cela signifie que la règle simple est ajoutée dans les vérités. Hors les vérités sont des formules, il faut donc exprimer la règle simple par une formule, ce qui implique l'ajout de mots clés (comme ∀). C'est trop compliqué pour l'instant.

Réponse

C'est possible et pratique, voir l'étude.