Lazi

Lazi et un tiers exclu sur la finitude d'un calcul

Contexte

Il semble logique que l'on ait que deux cas (et donc une forme de tiers exclu) sur un calcul univocal sur une formule x :

  • le calcul se termine
  • le calcul ne se termine par
Mais comment le montrer ?

Question

Soit x une formule, l'affirmation "il existe une formule y tq x →c[univocal]= y et le calcul de y est terminé" est soit vraie soit fausse ?

Étude

Contre exemple

Nous allons montrer que si on avait un tiers exclu sur "il existe une formule y tq x →c[univocal]= y et le calcul de y est terminé" alors lazi serait incohérent.

Extension "représentation de preuve"

Pour fabriquer le contre exemple, nous montrerons (rapidement) qu'une certaine extension est valide.
Cette extension, à partir d'une représentation dans la mathématique d'une preuve sans condition, déduit l'interprétation de la conclusion de la preuve.
Validité : En traduisant la preuve on a une représentation explicite, et donc on peut l'utiliser comme preuve.

Preuve absurde si on avait un tiers exclu

Soit x une formule qui cherche une preuve (par énumération de toutes les preuves possibles) que le calcul de x ne se termine pas. On peut construire une telle formule car on peut représenter x en elle-même.

Si le calcul de x se termine c'est qu'il existe une preuve qu'il ne se termine pas, on peut utiliser cette preuve (voir l'extension) pour prouver que x ne se termine pas. Donc x ne se termine pas. C'est absurde.

Donc le calcul de x ne se termine pas.

Comme on vient d'expliciter une preuve que le calcul de x ne se termine pas, le calcul de x trouve cette preuve, et donc le calcul de x se termine. Absurde car on vient de prouve que le calcul de x ne se termine pas.

Le calcul de x en Lazi

Si on a pas le tiers exclu, essayons de cherche si le calcul de x se termine.

On a comme ci-dessus que si le calcul de x se termine alors on aboutit à une absurdité.
Mais on ne peut aboutir alors à la conclusion que le calcul ne se termine pas.
Donc en pratique si on calculait x, son calcul ne se terminerait pas (car ce serait absurde).

Si on avait un tiers exclu, on pourrait avoir une preuve que le calcul se termine et donc on aurait une incohérence de la fondation mathématique.

Mais en théorie des ensembles avec tiers exclu, a-t-on un problème de cohérence ?

Réponse

Non, si on suppose qu'elle est soit vraie soit fausse on aboutit à une contradiction (voir l'étude).