Documentation

Logic.IntProp.Kripke.LEM

Counterexample to the Law of Excluded Middle in Intuitionistic Logic #

Theorems #

@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Law of Excluded Middle is not always provable in intuitionistic logic.

    Intuitionistic logic is proper weaker than classical logic.