Lectures on Constructive Set Theory
(Padua, Spring 1998)
Lecture 5: 15th May (16.30 - 18.00)
Intuitionistic Propositional Logic
In these notes we will use the following symbols for the logical
connectives.
-
(A->B) for A implies B
-
(A&B) for A and B
-
(AvB) for A or B (or both)
- -A for not A
We will also use 0 for the canonical false proposition and 1 for the
canonical true proposition.
Methods of Reasoning
- to prove (A->B):
- assume A and deduce B
- to prove (A&B):
- first deduce A
second deduce B
- to prove (AvB)
- first choose one of A,B
second deduce the one chosen
- to prove -A:
- assume A and deduce 0
- to prove 1:
- no need to do anything.
- from (A->B) deduce:
- B from A
- from (A&B) deduce:
- first A
second B
- from (AvB) deduce:
- C after
- first case:
- deduce C assumingA
- second case:
- deduce C assuming B
- from -A deduce:
- 0 from A
- from 0 deduce:
- C
These methods of reasoning can be expressed as rules of inference,
which we present schematically below.
[A] [A]
B A B A B 0
---- ----- ----- ----- --- ---
A->B A&B AvB AvB -A 1
[A] [B]
A->B A A&B A&B AvB C C -A A 0
------- --- --- ---------- ----- ---
B A B C 0 C
Note that [A]
above a premiss indicates that A may be
assumed in the premiss but gets discharged at the inference
step.
The rules for -A can be derived from the rules for -> using the
definition
-A =(def)(A->0)
We will also use the definition
(A<->B) =(def)(A->B)&(B->A)
from which we can get the inference rules having the following
schemes.
[A] [B]
B A A<->B A A<->B B
-------- ---------- ----------
A<->B B A
Examples
- (1) A->--A
| A
| | -A
| | 0
| |___
| --A
|_____
A->--A
- (2) ---A->-A
| ---A
| A->--A, by (1)
| | A
| | --A
| | 0
| |____
| -A
|_______
---A->-A
The classical method of arguing by contradiction
The next example cannot be derived in intuitionistic logic, but
requires the following rule which needs to be added to get the
traditional classical logic.
- to prove A:
- assume -A and deduce 0
- (3)--A->A, classically
|--A
||-A
|| 0
||___
| A
|_____
--A->A
- (4) --(Av-A)
|-(Av-A)
|| A
|| Av-A
|| 0
||_____
| -A
| Av-A
| 0
|_______
--(Av-A)
- (5) (Av-A), classically
- Apply (3) to get
--(Av-A)->(Av-A)
and then (4). This result is the law of excluded middle.
- (6)-(AvB)->(-A&-B)
| -(AvB)
| |A
| |AvB
| |0
| |__
| -A
| |B
| |AvB
| |0
| |__
| -B
| -A&-B
|______________
-(AvB)->(-A&-B)
- (7) (-A&-B)->-(AvB)
|-A&-B
|-A
|-B
|| AvB
|| |A
|| |0
|| |_
||
|| |B
|| |0
|| |_
||
|| 0
||_____
|-(AvB)
|______________
(-A&-B)->-(AvB)
Some Exercises
- (8) -(A&B)->(-Av-B), classically
- (9) -(AvB)->-(A&B)
- (10) (A->B)->(-AvB), classically
- (11) (-AvB)->(A->B)
- (12) -(A->B)<-> (A&-B)
- (13) (A->B)->(-B->-A)
- (14)(-B->-A)->(A->B), classically
- (15) ((A->B)->A)->A, classically
Heyting Algebras
Logical formulae are built up from variiables using the logical
connectives. For logical formulae A,B we write A<=B (i.e. A is less
than or equal to B) if (A->B) can be proved using the rules of
intuitionistic logic. We also write A<=>B if both A<=B and B<=A. Then
<= can easily be seen to be a reflexive transitive relation, so that <=>
is an equivalence relation. It follows that if we work up to
<=> then <= is a partial ordering of the logical formulae. In
fact it is a Heyting algebra; i.e. a lattice, with (A&B) the
meet of A, B and (AvB) the join of A,B< having top, 1, and bottom, 0,
and havoing a pseudo-complement operation mapping A,B to (A->B). This
information can be summarised as follows.
C <= (A&B) iff [C <= A and C <= B]
(AvB) <= C iff [A <= C and B <= C]
0 <= C
C <= 1
C <= (A->B) iff (C&A) <= B
A Heyting Algebra is a Boolean Algebra if --A<=A for all A.
Intuitionistic Predicate Logic
We assume that variables x,y,... range over a fixed set A that is
inhabited (i.e. has an element in - constructively distinct from
`non-empty' which means the same as `not not inhabited'). We
use P(x) and Q(x) for predicates on the set A that depend only on the
variable x. We continue to use A,B,C,... for propositions (that do
not depend on x). We use the following symbols to express the two
quantifiers.
(forall x)P(x) for for all x (in A) P(x)
(exists x)P(x) for for some x (in A) P(x)
Methods of reasoning for the quantifiers
- to prove (forall x)P(x):
- let y:A be arbitrary and deduce P(y)
- to prove (exists x)P(x):
- choose an object a:A and deduce P(a)
- from (forall x)P(x):
- deduce P(a) from a:A
- from (exists x)P(x):
- deduce C if
C can be deduced from y:A such that P(y)
The rules of inference for the quantifiers can be presented
schematically as follows.
[y:A]
P(y) a:A P(a)
-------------- --------------
(forall x)P(x) (exists x)P(x)
[y:A P(a)]
(forall x)P(x) a:A (exists x)P(x) C
-------------------- -------------------------------
P(a) C
Examples
- (1) -(exists x)P(x)->(forall x)-P(x)
|-(exists x)P(x)
| | y:A
| | |P(y)
| | |(exists x)P(x)
| | |0
| | |______________
| | -P(y)
| |_______________
|(forall x)-P(x)
|_______________________________
-(exists x)P(x)->(forall x)-P(x)
- (2) (forall x)-P(x)->-(exists x)P(x)
|(forall x)-P(x)
| | (exists x)P(x)
| | |y:A, P(y)
| | |-P(y)
| | |0
| | |____________
| | 0
| |_______________
|-(exists x)P(x)
|_______________________________
(forall x)-P(x)->-(exists x)P(x)
- (3) (exists x)-P(x)->-(forall x)P(x)
|(exists x)-P(x)
| | (forall x)P(x)
| | |y:A, -P(y)
| | |P(y)
| | |0
| | |____________
| | 0
| |_______________
|-(forall x)P(x)
|_______________________________
(exists x)-P(x)->-(forall x)P(x)
- (4) -(forall x)P(x)->(exists x)-P(x), classically
- Use the propositional laws (3), (13) and (3) above.
- --(forall x)P(x)->(forall x)--P(x)
- Use (1), (3) and the propositional law (13)
Exercises
- (6) (Av-A)->[(A->(exists x)P(x)->(exists x)(A->P(x))]
- (7) -(forall x)-P(x)<->--(exists x)P(x)
- (8) [Av(forall x)P(x)]->(forall x)[AvP(x)]
- (9) (forall x)[AvP(x)]->[Av(forall x)P(x)], classically
- (10) [A->(forall x)P(x)]<->(forall x)[A->P(x)]
- (11) [(exists x)P(x)->A]<->(forall x)[P(x)->A]
-
See Lecture 6
Draft. Last Revised: 18th May, 1998.