Brandon S. Allbery KF8NH wrote:
That's not quite what I was trying to say. (p^~p)->q is equivalent to _|_ in the sense that once you derive/compute (respectively) it, the "world" in which it exists breaks. (I don't think formal logic can have a Haskell-like _|_, but deriving (p^~p)->q is close to it in effect.)
Here's a couple of papers you might like... "Fast and Loose Reasoning is Morally Correct" http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.... "Precise Reasoning About Non-strict Functional Programs How to Chase Bottoms, and How to Ignore Them" http://www.cs.chalmers.se/~nad/publications/danielsson-lic.pdf "Total Functional Programming" http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0... Greg Buchholz