Minimal intuitionistic logic as a setting for logical counterfactuals
post by Quinn · 2015-07-30T18:06:18.000Z · LW · GW · 4 commentsThis is a link post for https://www.overleaf.com/read/tpprrdczvfkp
Contents
4 comments
4 comments
Comments sorted by top scores.
comment by SamEisenstat · 2015-07-30T21:38:25.000Z · LW(p) · GW(p)
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.
Replies from: Quinn↑ comment by Quinn · 2015-08-03T00:36:17.000Z · LW(p) · GW(p)
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.
comment by orthonormal · 2015-07-30T18:15:20.000Z · LW(p) · GW(p)
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?
Replies from: Quinn