Problem Detail: In
Practical Foundations for Programming Languages, Robert Harper says
If for a proposition to be true means to have a proof of it, what does it mean for a proposition to be false? It means that we have a refutation of it, showing that it cannot be proved. That is, a proposition is false if we can show that the assumption that it is true (has a proof) contradicts known facts.
But then, this begs the question- what is a contradiction in constructive/intuitionistic logic? Is this meant in the sense of deriving $(bottext{ true})$ somehow? How would this happen in a sensible way? Would a judgment of the form $(A supset bot text{ true})$ need to be introduced? Alternatively, is it perhaps meant in the sense of the reader using their discretion to informally label something as contradictory? For example, interpreting $a = b$ and $a neq b$ as conflicting propositions.
Asked By : afsmi
It is immaterial whether we speak about constructive or classical logic in this situation. If you read your questions again, you will see that they apply to boths kinds. The only difference that we need to take notice of is the presentation of negation $lnot A$. It can be presented in several ways classically, but intuitionistically it is best to use it as an abbreviation for $A Rightarrow bot$ (which is precisely what Bob Harper is hinting at in the quoted paragraph). But let us not confuse negations and contradictions. In both cases, a contradiction is a situation in which we have managed to prove falsity $bot$. How could we derive $bot$ in a sensible way? Well, from an inconsistent set of hypotheses, that wold be a sensible way to do it. You have no discretion to “declare” a contradiction. You must prove that a given set of hypotheses is contradictory by deriving $bot$. For instance, if $a = b$ and $lnot (a = b)$ then we may use the fact that $lnot (a = b)$ is an abbreviation for $(a = b) Rightarrow bot$ and conclude $bot$ by modus ponens.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/67135
Related
