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 | '-------------------------------------------'

Thu Sep 14 08:45:18 EDT 1995