Fix intuitionistic equivalent of LEM

[PeepNSheep]

By the BHK interpretation, $\lnot \varphi$ is a shorthand for $\varphi \implies \perp$. The original statement was just the definition of negation in intuitionistic logic, not the LEM.

[rzach]

You're right that the first one makes no sense. But your replacement isn't a well-formed formula. I think you meant (\not !A \lif \lfalse) \lif !A.

[PeepNSheep]

You're right that the first one makes no sense. But your replacement isn't a well-formed formula. I think you meant (\not !A \lif \lfalse) \lif !A.

Good catch. I just fixed the typo.

[rzach]

Thanks!