Lazi

Changer les règles sur if

Contexte

Avec les règles de déduction actuelles il n'est pas possible de raisonner par tiers exclu sur une condition comme "le calcul se finit".

Question

Peut-on changer les règles pour qu'il soit possible de raisonner par tiers exclu sur une condition comme "le calcul se finit" ?

Étude

Essai 1

On peut ne pas définir de valeur 0b, et avoir la règle que if x y z = z si x est calculable en autre chose que 1b.
Par exemple if equal y z = z, ou if (equal 1b) y z = z.

Le problème est qu'il faut définir la notion de calcul.

Réponse