Études-Mathématique/Application de la règle de la descente
Contents
Question
La règle de déduction de la descente stipule que si d est une représentation d'une déduction Lazi-1, alors la traduction des représentations des conditions et conclusions de d sont vraies : c'est à dire que si les conditions sont vraies on déduit la conclusion.
Lazi-0 ne comprend pas de constantes globales. Est-ce un problème ?
Étude
Constantes globales dans les représentations
Si nous avons une certaine représentation d d'une déduction et une fonction f Lazi-0 définissant "être une représentation de déduction Lazi-1. Nous devons montrer "f d". d contient des constantes globales, c'est une notation. Il me semble qu'il n'y a pas de problème.
Constantes globales dans la formule déduite
Il faut pouvoir traduire la représentation d'une constante globale en constante globale.
Réponse
Ça ne me semble pas un problème.