déduction de calcul

Contexte

Pour une mathématique lazi, on veut définir un type particulier : une déduction prenant en argument une formule x (dans le domaine des formules pouvant être calculées par cette déduction) et déduit une égalité où x est le membre de gauche.

Définition de "type (ou règle) de déduction de calcul"

Soit M une mathématique lazi et td un type de déduction de M. On dit que td est un type de déduction de calcul si td prend en argument une formule x et si la vérité déduite est de la forme x = y.

Définition de "déduction de calcul"

On dit que d est une déduction de calcul si son type est un type de déduction de calcul.