Crossposted from the AI Alignment Forum. May contain more technical jargon than usual.
This is a linkpost for https://www.overleaf.com/read/tpprrdczvfkp
Haskell doesn't actually let you do this as far as I can tell, but the natural computational way to implement a function is with a case expression with no cases. This is sensible because 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 is just the -ary sum type.
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.
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?
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.