Lazi

2 Théorème de non incohérence de lazi.1.0

Contexte

Les preuves en lazi.1.0 sont traduisiblesen preuves lazi.0.0 (reste à prouver), donc la cohérence de lazi.0.0 se communique à lazi.1.0.

Énoncé

Il est absurde que lazi.1.0 soit incohérente.

Preuve

Supposons que 1b = 0b soit démontrable en lazi.1.0.

Soit p une preuve lazi.0.1 de 1b = 0b. Comme toute preuve lazi.0.1 est traduisible en preuve lazi.0.0 (reste à prouver), il existe une preuve q lazi.0.0 de 1b = 0b. On obtient alors une absurdité par la cohérence de lazi.0.0.

@todo

@theorem