Lectures on Constructive Set Theory

(Padua, Spring 1998)

Lecture 6: 20th May (16.30 - 18.00)

The Semantics of Intuitionistic Logic

In lecture 5 we were concerned with the formal rules of deduction for intuitionistic logic (and classical logic). This was a matter of syntax; i.e. the rules are explained purely in terms of the syntactic forms of the logical formulae and not in terms of their meaning. We introduce some notation.

Formal Deduction

Recall that the (logical) formulae of propositional logic are built up from variables and 0,1, using the connectives, ->,&,v. We will write

A1,...,An |- B

if B can be deduced from zero, one or more of A1,...,An as assumptions, using the rules of inference of intuitionistic logic (or sometimes classical logic, depending on the context). Note the special case when n=0.

We now want to consider the question:

In what sense are the rules of deduction correct/sound?

This question is a matter of semantics; i.e. it concerns the possible meaning of the logical formulae.

We will first briefly consider the standard classical answer which is in terms of truth values

The classical standard semantics

The rules of deduction are intended to preserve truth under any interpretration, so that whenever A1,...,An|-B, using the rules of inference of classical logic, then in any interpretation where all the premisses A1,...,An are true the conclusion B will also be true.

What do we mean by an interpretation here?

A standard classical interpretation is an assignment of a truth value, true or false (abbreviated T or F) to each logical formula so that 1, 0 get the values T,F and the truth value of a compound formula (A&B), (AvB), (A->B) is determined by the truth values of A,B using the standard truth tables.

                ---------------------------
               | A  B  ||  A->B  AvB   A&B |
               |-------||------------------|
               | T  T  ||   T     T     T  |
               | T  F  ||   F     T     F  |
               | F  T  ||   T     T     F  |
               | F  F  ||   T     F     F  |
                ---------------------------

Note that once truth values have been assigned to the variables of a formula of propositional logic then a truth value can easily be computed for the formula.

For formulae involving quantifiers an interpretation has to specify a non-empty set D for the variables to range over, called the domain of the interpretation. Also, only formal sentences that do not depend on any (free) occurences of variables, are to be assigned a truth value, but such sentences may contain names for the elements of D. The truth values of the sentences (forall x)P(x) and (exists x)P(x) are then determined in terms of the truth values of the sentences P(a) for elements a:D (more precisely a is to be a name of an element of D, but we will ignore this distinction here.) The procedure for determining the truth values of the quantified sentences is specified by the following table.

             ---------------------------------------------
            |....P(a)...|| (forall x)P(x)   (exists x)P(x)|
            |---------------------------------------------| 
            |...all T...||        T                T      |
            |---------------------------------------------|    
            | not all T ||                                |
            |    and    ||        F                T      |
            | not all F ||                                |
            |---------------------------------------------|    
            |...all F...||        F                F      |
             ---------------------------------------------

Note that if D is a finite set {a1,...,an} then

(forall x)P(x) behaves like P(a1)&...&P(an)

and

(exists x)P(x) behaves like P(a1)v...vP(an).

But when D is an infinite set then we cannot generally expect to be able to compute the truth values of the quantified sentences, even when we know the truth value of each P(a) for a:D. Moreover, in constructive mathematics the truth value of the quantified sentences is not even determined in general.

Classical propositional logic also can be given a semantics in any Boolean algebra, each formula A being assigned a value in the Boolean algebra so that certain conditions hold. This generalises the two valued semantics from the two element Boolean algebra on {T,F} to any Boolean algebra. To be able to deal with the quantifiers it is sufficient that the Boolean algebra is complete. We will not go into the details here. For us the main point is that this semantics carries over to an algebraic semantics for Intuitionistic logic which we examine next.

Non-standard semantics for Intuitionistic Propositional Logic

Interpretations in Heyting algebras

Let H=(H,<=,&,v,0,1,->) be a Heyting algebra; i.e. (H,<=) is a partially ordered set, with binary meet and join operations, &,v, top and bottom elements, 0,1, and a pseudo-complement operation, ->.

Note: A Heyting algebra is complete if every subset has a join and a meet, not just the finite subsets. (This definition is the usual one in classical mathematics, but will have to be refined in constructive set theory. But it will do for now.)

An interpretation (of intuitionistic propositional logic) in H is an assignment of [[A]]:H to each formula A (of intuitionistic propositional logic). such that

[[0]] = 0
[[1]] = 1
[[A&B]] = [[A]] & [[B]]
[[A->B]] = [[A]] -> [[B]]
[[AvB]] = [[A]] v [[B]]

where, on the right hand side of these equations, 0,1:H and &,->,v are the Heyting algebra operations on H.

Soundness Lemma

We assume given an interpretation in a Heyting algebra H.

If A1,...,An |- B then [[A1]]&...&[[An]] <= [[B]].

In particular, when n=0, then

|- B implies [[B]]=1.

This result gives an easy method to show that certain formulae B cannot be proved in intuitionistic logic - it suffices to find an interpetation in a Heyting algebra H, where [[B]] =1 is false. We call such an interpretation a counter-model for B.

The topological examples of complete Heyting algebras.

Recall that a topological space on a set X of points consists of a set of subsets of X, called the open sets of the space, that is closed under the operations of taking unions of arbitrary subsets and intersections of finite subsets, so that in particular the empty set, 0, and the whole set X are both open. (This definition will need to be refined in consructive set theory. But we use it for now.)

The open sets of a topological space on a set X of points form a complete Heyting algebra, when partially ordered by the subset relation. The top and bottom are X,0, the join operation is the set theoretic union operation and the finite meet operation is the set theoretic intersection operation. For the general meet operation of a possibly non-finite set, Y, of open sets we need to use the operation that takes the interior of the intersection of the sets in Y. For open sets Y,Z, the pseudo-complement is given by:-

(Y->Z) = the union of the open sets V such that (V&Y) <= Z.

In some topological spaces the open sets are closed under taking intersections of arbitrary subsets. In constructing countermodels it will be enough to use such spaces determined by a partial ordering.

Kripke Structures for Propositional Logic

Let (K,<=) be a partially ordered set. A subset X of K is upwards closed if whenever k<=k' then [k:X implies k':X].

The upwards closed subsets of K form the open sets of a topological space that is closed under taking arbitrary intersections. An interpretation in K will also be called a Kripke structure on (K,<=).

Examples

(1) Countermodel for --A->A and Av-A:

Partially order the set K = {0,1} with 0<1. Let A be a variable and choose a Kripke model so that [[A]] = {1}. Then [[-A]] is empty and [[--A]] = K, so that

[[--A->A]] = [[Av-A]] = {1}

which is not equal to K.

(2) Countermodel for --Av-A:

This time let K = {0,1,2}, with 0<1, 0<2 only, and let [[A]] = {1} again. Then [[-A]] = {2} so that [[--A]] = {1} and so

[[--Av-A]] = {1,2}

which is not equal to K.

Exercise

Find countermodels to the other `classical' examples of lecture 5.

Kripke structures for Predicate Logic

We shall restrict attention to languages for predicate logic involving only unary predicate symbols P.

Given a partially ordered set (K,<=) and a non-empty set D, a predicate calculus Kripke structure on (K,<=), with domain D, will be assignment of K(d):K to each d:D and [[A]]:K to each formula A (that is a sentence of the formal language for predicate logic that has a name, d, for each element of D) such that the previous conditions hold for 0,1,->,&,v and also the following conditions hold for the quantifiers.

[[(forall x)P(x)]] = Intersect_d:D(K(d)->[[P(d)]])

[[(exists x)P(x)]] = Union_d:D(K(d)&[[P(d)]])

It is not hard to show that the soundness theorem extends to predicate logic, so that the method of counterexamples can be applied to show the non-provability in intuitionistic predicate logic of certain formulae.

Examples

-(forall x)P(x)->(exists x)-P(x):

Let K = {0,1,2} with 0<1 and 0<2 only.

Let D = {0',1',2'} and K(0') = K, K(1') = K(2') = {1,2}.

Let [[P(0')]] = {1,2}, [[P(1')]] = {1} and [[P(2')]] = {2}.

Now check that [[(forall x)P(x)]] is empty, so that [[-(forall x)P(x)]] = K, but [[(exists x)-P(x)]] = {1,2} so that we have a countermodel.

Exercise

Find counterrmodels for the other `classical' predicate logic examples of lecture 5.

See Lecture 7

Draft. Last Revised: 20th May, 1998.