Haskell doesn't actually let you do this as far as I can tell, but the natural computational way to implement a function $B o t - > A$ is with a case expression with no cases. This is sensible because $B o t$ has no constructors, so it should be possible to pattern match it with such an expression. Another way of thinking of this is that we can use pattern matching on sum types and $B o t$ is just the $0$ -ary sum type.

[-]Quinn10y00

Thanks for pointing that out. My feeling is still "well yes, that's technically true, but it still seems unnatural, and explosion is still the odd axiom out".

Coq, for example, allows empty case expressions (for empty types), and I expect that other languages which double as proof assistants would support them as well... for the very purpose of satisfying explosion. General purpose languages like Haskell (and I just checked OCaml too) can seemingly overlook explosion/empty cases with few if any practical problems.

[-]orthonormal10yΩ000

Interesting! Can you make a specific model of a 5-and-10 failure in minimal logic, using something similar to the "malicious proof search ordering" 5-and-10 failure in classical logic?

[-]Quinn10yΩ120

Thanks for the suggestion, Patrick. I've now adapted Tsvi's formal argument to the reframed "5-equals-10 problem" and added it into the last section of my writeup.

Moderation Log

LESSWRONG
LW

LESSWRONG
LW

4

Minimal intuitionistic logic as a setting for logical counterfactuals

4

Ω 2

4

Ω 2