Lazi

1 Théorème de non incohérence de lazi.0.0

Contexte

Lazi.0.0 peut être vu comme des règles de calculs. Il parait donc logique, avec de bonnes règles de calculs, d'arriver à montrer qu'elles sont cohérentes, c'est à dire que l'on ne peut pas prouver 1b = 0b.

Énoncé

Conclusion

Il est absurde que Lazi.0.0 soit incohérente.

Preuve

Soit v une vérité lazi.0.0, par exemple if 1b 1b 1b = 1b.
Supposons que 1b = 0b soit démontrable en lazi.0.0.

On a if 0b 0b v = if 1b 0b v. Comme v est vrai, if 0b 0b v est vrai, donc if 1b 0b v est vrai, donc 0b est vrai. Le théorème "toute vérité se calcule en une égalité" prouve que 0b se univocal-calcul en une égalité, ce qui est absurde.
Donc il est absurde que 1b = 0b soit démontrable en lazi.0.0.
Donc il est absurde que lazi.0.0 soit incohérente.

@theorem