Études-Mathématique/Application de la règle de la descente

From Lazi wiki
Jump to: navigation, search

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.