As we saw in chapter 3, the operators associated with
classical logic are easily defined in Nuprl
. Now
we will see how
to prove a typical fact about them. The most characteristic fact
about the classical operators is the
``law of the excluded middle,'' which
says that for every proposition P,
, where vel is usually
read as the English ``or''. Recall that in Nuprl
, P
vel P
is defined to mean
~ (P & ~ P).
The following snapshots show how this
proposition is proved. It is interesting to notice that there is not
much computational content to this result;
thus, while it is a true fact in Nuprl
, it is not a very
interesting one.
The next window shows the hypotheses and subgoals after introducing the arbitrary propositional variable.
,------------------------------------------, |EDIT THM t2 | |------------------------------------------| |# top | |>> all P:U1. P vel ~P | | | |BY intro at U2 | | | |1# 1. P:(U1) | | >> (P vel ~P) | | | |2* >> (U1) in U2 | '------------------------------------------'
Next we deal with the first subgoal. (The system has dispatched the second one.) Since P vel P is defined as a negation, and since negation is defined to be an implication, we prove it via an introduction rule. This results in the two subgoals shown below.
,---------------------------------------, |EDIT THM t2 | |---------------------------------------| |# top 1 | |1. P:(U1) | |>> (P vel ~P) | | | |BY intro at U1 | | | |1# 1. P:(U1) | | 2. ~P&~~P | | >> void | | | |2* 1. P:(U1) | | >> ~P&~~P in U1 | '---------------------------------------'
The system has proven the second subgoal here. We handle the first subgoal by first breaking down the conjunction in the hypothesis list.
,-----------------------------------------, |EDIT THM t2 | |-----------------------------------------| |# top 1 1 | |1. P:(U1) | |2. ~P&~~P | |>> void | | | |BY elim 2 | | | |1# 1. P:(U1) | | 2. ~P&~~P | | 3. ~P | | 4. ~~P | | >> void | '-----------------------------------------'
Now we recognize that ~ P is just P=>void, so if we eliminate hypothesis 4 the proof will be complete. The result of this command is displayed in the next snapshot.
,-------------------------------------------, |EDIT THM t2 | |-------------------------------------------| |* top 1 1 1 | |1. P:(U1) | |2. ~P&~~P | |3. ~P | |4. ~~P | |>> void | | | |BY elim 4 | | | |1* 1. P:(U1) | | 2. ~P&~~P | | 3. ~P | | 4. ~~P | | >> ~P | | | |2* 1. P:(U1) | | 2. ~P&~~P | | 3. ~P | | 4. ~~P | | 5. void | | >> void | '-------------------------------------------'