# The things I end up reading late at night: “Therefore, there is a way to go from a proof of 0 = 1 to a proof of any basic arithmetic equality, and thus to a proof of any complex arithmetic proposition. Furthermore, to get this result it was not necessary to invoke the Peano axiom that states that 0 is “not” the successor of any natural number. This makes 0=1 suitable as. in Heyting arithmetic (and the Peano axiom is rewritten 0 = Sn → 0 = S0). This use of 0 = 1 validates the principle of explosion.”

The things I end up reading late at night:

“Therefore, there is a way to go from a proof of 0 = 1 to a proof of any basic arithmetic equality, and thus to a proof of any complex arithmetic proposition. Furthermore, to get this result it was not necessary to invoke the Peano axiom that states that 0 is “not” the successor of any natural number. This makes 0=1 suitable as. in Heyting arithmetic (and the Peano axiom is rewritten 0 = Sn → 0 = S0). This use of 0 = 1 validates the principle of explosion.”

This is the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic. There is no “law of excluded middle” but you _can_ use “absurdity” instead. This puts into the frame of being a value judgement rather than a rootless axiom.