3. False Propositions and Negation
A simple extension of the minimal implication logic allows us to reason about negation, symbolized as ∼P or ¬P for "not P," where P is a proposition. Let us specialize the constant ⊥ to be the constant proposition False. By definition, False is a proposition that has no correct or meaningful evidence. We could also say that any hypothetical evidence for False in a context of assumptions is a mistake. In this case we imagine that some hypothetical combination of ideas that we thought provided evidence for some other proposition P are wrong or mistaken and could be used to show False in the sense of revealing the mistake. We denote this calculus as PC[False, ⇒].
Once we have the False proposition, we can say that there is no evidence for a proposition P by saying (P ⇒ False) has evidence. If there were evidence for P, then (P ⇒ False) would convert it to evidence for False. But since there is no evidence for False, this means there cannot be evidence for P either. Let us define the negation of a proposition this way:
Negation: ∼P means (P ⇒ False).
We just used a very important bit of logical reasoning in our analysis of ∼P. We said that if some proposition P implies the proposition Q, then if we know ∼Q, we must know ∼P. This is called the contrapositive claim. We can already express this in the new calculus with negation. We assert that (P ⇒ Q) ⇒ (∼Q ⇒ ∼P), and we can build the evidence for this as follows. Let pq be hypothetical evidence for (P ⇒ Q), and let nq be hypothetical evidence for ∼Q, an operation to provide evidence for (Q ⇒ False). Now we need evidence for (P ⇒ False) which is an operation from P to False. We build it from the other operations as λ(pq.λ(nq.λ(p.nq(pq(p))))), where p is hypothetical evidence for P. The proof of the contrapositive is shown later as Theorem 6.
A subtle point about this small calculus arises in thinking about what it should mean to assume False. What follows from this assumption? We surely have (False ⇒ False), which is something we have for any constant including ⊥. If we define True to be (False ⇒ False), then we also have (False ⇒ True) using the evidence λ(x.λ(y.y)).
Do we have (False ⇒ P) for any proposition P? There can be no evidence for False, so if we consider evidence of the form λ(x.x) can this be evidence for (False ⇒ P)? It is plausible to say that under the assumption that there is evidence for False, we can prove anything, including that x is evidence for P. In ancient logic this was the "ex falso quod libet" rule that claimed from false anything follows. This simple question has been studied and pondered a great deal, and one working conclusion is that it seems that no great harm is done adopting this rule and using something simple as evidence for P. So we allow a rule that is used by Constructive Type Theory (CTT) and Intuitionistic Type Theory (ITT) that uses the following evidence term for the proposition (False ⇒ P): λ(x.any(x)).
False Elimination Rule:
H, f : False ⊢ G by any(f)
Negation in Nuprl
There are a few things to note about using these new concepts in Nuprl. First, the False elimination rule is applied using the tactic FalseHD i, where i is the index of the assumption of False. Second, in order to use the application rule with ∼P as the operation in Nuprl, we first apply the tactic Unfold 'not' i in order to unfold ∼P to be (P ⇒ False), where i is the index of the hypothesis for ∼P. Otherwise, when decomposing ∼P Nuprl will automatically use the False elimination rule in the extract, which isn't necessarily required. The evidence for the contrapositive claim as described above is an example of this scenario, since we used the application rule with negation but did not require the special "any" evidence.
When negation is the outermost operator in the goal, it is not necessary to unfold the "not" operator before applying the tactic D 0 for the construction rule. However, in the proofs that follow, we have included the unfolding step for clarity, which is applied to the conclusion by using 0 as the index in the tactic, i.e. Unfold 'not' 0.
In the next few theorems we apply these concepts to prove some facts about negation and implication:
We leave the following theorems as exercises:
Table of Contents