Lazi

Indécidabilité, tiers exclu et fondation

Contexte

Le problème de l'arrêt est au cœur de la traduction du tiers exclu du premier ordre quand la méthode de traduction consiste à chercher laquelle des deux conditions est vraie. Car alors pour trouver la condition vraie on recherche parmis toutes les démonstrations pour en trouver une démontrant la condition. Il faut donc pouvoir prouver que ...

Remarque: il faudrait aussi s'interrêter sur l'intérêt de passer par (x ⇒ ⊥) ⇒ y plutôt que par des règles spécifiques sur le "∨".

Question

Étude

Réponse

@todo