     Next: Predicate Logic Up: Examples from Introductory Previous: Constructive Propositional Logic

## Classical Propositional Logic

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

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995