This post is about double negation in constructive type theory. Suppose you know that is true; i.e., (writing for false). In classical logic, you then know that is true. But of course, you are allowed no such conclusion in intuitionistic logic. So far, so familiar. But let us look at this now from the perspective of realizability. Realizability semantics gives the meaning of a type as a set of some kind of realizers. Let us consider untyped lambda calculus terms (or combinators) as realizers for purposes of this discussion. Then the crucial clauses of the semantics for our purposes are
- , and
Let us work through, then, when according to this definition:
So this is saying that if is nonempty, then is universal (contains all terms); and otherwise (if is empty), is empty.
So if you have a function , say, realizing for some , what this means is that can make use of the fact that is true, but not how it is true. If were simply given a proof of , then it could compute with this proof. But here, with , the proof of is hidden behind an existential quantifier (as we deduced above), and so it cannot be used. Only if someone is reasoning at the metalevel about , they can make use of the fact that is true when checking that the body of realizes .
So semantically, is news you can’t use: we know is true, but we have no access to how it is true. For example, if is a disjunction, you cannot case split, within the type theory, on the disjuncts. Only at the metalevel are you entitled to consider the behavior of a term in light of the fact that one or the other of the disjuncts must hold.