Lazi

Égalité par calcul et tiers exclu

Contexte

Pour raisonner à partir d'une hypothèse comportant une égalité par calcul, il nous faut explorer les différents cas signifiés par cette égalité (arguments calculables ou non).
Pour pouvoir explorer les différents cas, il faut que la propriété =c soit un booléen.

Question

Est-il possible que l'égalité "x =c y" soit un booléen ? Et sinon comment faire des preuves à partir d'une hypothèse comportant une égalité par calcul.

Étude

la propriété de calculabilité

Cela revient au teste "être une liste", car une formule incalculable correspond à une liste infinie. Donc on peut retourner 1b pour une formule calculable, mais alors la fonction ne se termine pas si la formule est incalculable.

Si on passe par une expression de la calculabilité de plus haut niveau, alors "être calculable" ne retourne plus un binaire.

Tiers exclu sur du premier ordre

On peut définir un "ou" du premier ordre à partir de l'inférence. Peut-on alors démontrer un théorème de tiers exclu ? Je pense que l'on peut avoir une forme de tiers exclu au premier ordre.

Calculabilité et tiers exclu

Supposons que "calculable" est la propriété sur une formule d'être calculable. C'est une fonction qui, appliquée à une formule, retourne 1b ou boucle. Soit x une 1-formule (donc une représentation de formule) incalculable, comment prouver que (calculable x = 1b) ⇒ ⊥ ? On suppose calculable x = 1b, on utilise la règle d'induction en montrant que l'on a loopStop next x = 1b.

Si "calculable" est la propriété sur une formule d'être calculable, comme la négation du premier ordre est définie par ¬ x = (x ⇒ ⊥), pour x une formule, calculable x ∨ (¬ ( calculable x ) ) est égale à
calculable x ∨ (calculable x ⇒ ⊥) qui est égale à (¬ ( calculable x ) ) ⇒ (¬ ( calculable x ) )

Réponse

On ne peut pas définir =c pour qu'il retourne un binaire, mais à l'aide d'une forme de tiers exclu en logique de niveau 1 il devient alors possible de raisonner sur une hypothèse comportant une égalité par calcul.