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.