Lazi

Règle du tiers exclu

Contexte

Voir la page parent. On est dans le contexte où l'on traduit une preuve sans hypothèse en traduisant toute déduction ayant aux moins une hypothèse et une sous-preuve.

Définition de la règle : voir excludedMiddleRuleT dans le fichier lazi deductions.def.lazi

Question

Comment traduire cette règle ?

Preuve de traductibilité

Pour traduire la règle, on recherche la valeur de x, et suivant sa valeur (0b ou 1b) on utilise p0 ou p1.

Il faut donc montrer que si une preuve sans hypothèse (une preuve lazi.0.0) déduit $F[if] +f x +f y +f z *=* $F[1b] (ou 0b) alors on peut construire une preuve déduisant la valeur de x dans 0b ou 1b :

Les conditions du théorème "Toute vérité se calcule en une égalité" sont vérifiées car $F[if] +f x +f y +f z *=* $F[1b] est prouvé par une preuve lazi.0.0.
Donc $F[if] +f x +f y +f z =c $F[1b], comme le calcul de $F[1b] est terminé on a $F[if] +f x +f y +f z →c[loose] $F[1b]. D'après le théorème d'égalité des arguments pour un calcul terminé on a $F[if] +f x +f y +f z →c[univocal] $F[1b]. D'après les règles du calcul univoque on a x →c[univocal]= $F[1b] ou x →c[univocal]= $F[0b].
Comme le calcul univoque peut se traduire en preuve, on peut obtenir une preuve de x *=* $F[1b] ou x *=* $F[0b].