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