How can some statements be consistent with intuitionistic logic but not
classical logic, when intuitionistic logic proves not not LEM?
I've heard that some axioms, such as "all functions are continuous" or
"all functions are computable", are compatible with intuitionistic type
theories but not their classical equivalents. But if they aren't
compatible with LEM, shouldn't that mean they prove not LEM? But not LEM
means not (A or not A) which in particular implies not A - but that
implies (A or not A). What's gone wrong here?
No comments:
Post a Comment