Lecture notes for October 27 Lecture notes for October 27

Introduce function symbol = whose values are of type Boolean.
Introduce two Axioms from Chapter 1 of G-S:
(1.2) |- x = x .
(1.3) |- (x = y) º (y = x) .
We will not introduce (1.4) and (1.5) as these can be proved.
For P, Q of type Boolean note that P = Q is what we write normally as P º Q. For X, Y expressions of type integer we interpret X = Y as ordinary equality of integers, etc.
(3.83) Axiom, Leibniz::
 |- e = f   Þ Eze = Ezf .
Note that where e, f as well as E are Boolean formulas, (3.83) can be proved as follows:
Assume e º f. By the Leibniz inference rule, Eze º Ezf is a theorem. Then by the Deduction Theorem, |- e º f   ÞEze º Ezf . If we only were to use this in the case of Boolean formulas, we would not need to introduce (3.83) as an axiom, since we have a proof of it in our system.
Examples:

a = 1 Þ a2 = 12.

a = b Þ a3+2a +1 = b3+2b+1.
(3.83) and (3.84) which follows from it are used extensively in 2090.
(3.84)(a) Theorem:
 |- (e = f) ÙEze      º (e = f) ÙEzf .
Observe that Eze and Ezf must be of type Boolean.
 (e = f) ÙEze    º   (e = f) ÙEzf
 =

 (3.3)

 (e = f) ÙEze    º   (e = f) ÙEzf    º   true
 =

 (3.3) gives true º (e = f) º (e = f)

 (e = f) ÙEze    º   (e = f) ÙEzf    º   (e = f)    º   (e = f)
 =

 (3.49)

 (e = f) Ù(Eze    º   Ezf)    º   (e = f)
 =

 (3.60)

 (e = f) Þ (Eze º Ezf).
(3.84)(b) Theorem:
 |- (e = f)   Þ Eze      º     (e = f)   Þ Ezf .

 (e = f) Þ Eze
 =

 (3.60)

 (e = f) ÙEze º (e = f)
 =

 (3.84)(a)

 (e = f) ÙEzf º (e = f)
 =

 (3.60)

 (e = f) Þ Ezf
The proof of (3.84)(c)
 |- Q Ù(e = f) Þ Eze    º   Q Ù(e = f) Þ Ezf
is left as an exercise.
Application:
 |- (a = b) Ù(b = c)   Þ  (a = c) .

 (a = b) Ù(b = c)   Þ  (a = c)
 =

 (3.60)

 (a = b) Ù(b = c)Ù(a = c)     º     (a = b) Ù(b = c)
 =

 see below

 (a = b) Ù(b = c)Ù(b = c)     º     (a = b) Ù(b = c)
 =

 (3.38)

 (a = b) Ù(b = c) )     º     (a = b) Ù(b = c)
The justification for the second step is as follows:
(3.84)(a) gives
(a = b) Ù(b = c) Ù(a = c)      º     (a = b) Ù(b = c)Ù(b = c)
where E is the expression
(a = b) Ù(b = c) Ù(x = c).
Then apply Leibniz Inference where E is r º (b = c)Ù(a = b).
Theorem:
 |- (a = 1) Ù(b = 1)  Þ (a = b) .

 (a = 1) Ù(b = 1) Þ (a = b)
 =

 (3.84)(c)

 (a = 1) Ù(b = 1) Þ (a = 1)
 =

 (3.36)

 (b = 1) Ù(a = 1) Þ (a = 1)
 =

 (3.84)(c)

 (b = 1) Ù(a = 1) Þ (1 = 1)
 =

 (1.2), Metatheorem

 (b = 1) Ù(a = 1) Þ true
 =

 (3.72)

 true

File translated from TEX by TTH, version 2.60.
On 26 Oct 2000, 21:31.