Fri, 23 Sep 2016 18:35:42 GMT

And again, a talk for the
best mathematics club of the multiverse. This time, I thought I'd
have a slightly more abstract topic, namely Kripke models. As always,
**this is not a scientific talk**, and it focuses on breadth rather
than depth, and neglects formality in favour of comprehensibility. Its
audience will mainly consist of young students who will probably not
have experience in mathematical logic for the largest part.

Anyway, feel free to drop a comment if you notice any mistakes.

The *lambda calculus* is the prototype of all functional programming
languages. We will give a short informal introduction to it.

A *lambda term* is inductively defined as

- There are
*variables*, as the ones known from programming languages. Every*variable*is a lambda-term. Thus, is a lambda-term. - If are lambda-terms, then the
*application*is a lambda-term. It regards as a function, and as its first argument. A more usual notation would be , but there are reasons why is preferred. - If is a lambda-term and is a variable, then the
*abstraction*is a lambda-term. The variable will usually occur in . The intuition is that is the function that maps to some value the term , where every occurence of in is replaced by . For example, if , then . Another notation that is more common in some other parts of mathematics would be .

The idea of the untyped lambda calculus is that everything is a function. Functions map functions to functions. Lambda terms are the only objects one talks about.

A problem that arises from the above definition is that you might have a lambda term . If we just replaced , we would have , which is obviously not what we want. Actually, the inner is bound by the inner , and will not be replaced. It is possible to define this formally, but for this talk we just forbid that this occurs.

Another problem arises when we substitute with a term that itself contains a variable. Say, we have . This is obviously not intended, and we forbid this to happen, instead of handling it formally.

A variable is *bound* in a term, when it is captured by some
lambda. It is *free* otherwise. A term is *closed* when it does not
contain free variables. For example, contains
freely, while is a closed term.

As for most functional programming languages, we can assign *types* to
terms. In the *simply-typed lambda calculus*, there are *atomic* types
and *arrow types*, which are of the form
, where are
types. Variables will be assigned a type. We write to denote that the term has the type . The intuition is that this term is a function from objects of
type to objects of type . We therefore define the
typing rule . Furthermore, we only allow
applications when the types fit, that is,
. Of course, we can leave
out type annotations when they are clear or not important. This is a
very simple type system, but most other type systems are based on
this.

We now ask ourselves the question whether there is a closed term of type . Well, of course there is none, otherwise we wouldn't ask. Kripke models are a way of answering this kind of questions.

We are given a rooted tree , where is the set of nodes, and is the "is parent" relation for this tree. The tree need not be finite.

Now, for every atomic type , let a monotone function be given, that is, .

A triple is called a *Kripke model* (well, at least a
very simple form of a Kripke model). We now define a so-called
*forcing relation* (where
is the set of simple types).

We define

- if and only if .
- if and only if for all , implies .

We say that (" models ") if and only if .

**Lemma (Monotonicity):** Let be a Kripke model, and
with , and be some type. If
, then .

**Proof:** We prove this by structural induction on . If
for some atomic type , this holds by the
monotonicity of .

Now Let , and assume , that is, for all , implies . But then the same holds especially forall , hence .

Q.E.D.

**Lemma (Correctness):** Let a closed simply-typed lambda term
exist. Then every model satisfies
.

**Proof:** We slightly generalize the Lemma. We actually prove: If
there exists a term with free variables , then for every ,
if we have for all , we also
have . We prove this by structural
induction.

Our induction hypothesis is that the current entailment holds for
*all* Kripke models. Notice that if , then is (trivially) also a Kripke model.

Obviously, it holds for variables .

Assume , where has the free variables and has the free variables (notice that both sets of free variables need not be disjoint). Assume that for all we have . Then by induction, we have and . But means that implies . Hence, the claim follows.

Assume , and
. Besides , let
have the free variables , and
let again for all . We now
have to show that implies
for all . By our monotonicity
lemma, implies . By our induction hypothesis for is that this
holds for *all* Kripke models, especially for . Hence, for all ,
implies . Therefore, , and therefore, .

Q.E.D.

Now that we have shown correctness, we can answer our above question.

**Lemma:** There is no closed simply-typed lambda term of type
.

**Proof:** Consider the tree of words matching the regular expression
`0*1?`

. Define ,
and . That is:

⋮ P→1 Q→0 001 000 P→0 Q→0 \ / P→1 Q→0 01 00 P→0 Q→0 \ / 0 P→0 Q→0

Let for some node . That means that implies . For every , there is some such that but , and therefore , and therefore, . So for all , , and therefore, for all , regardles of whether or not . But then again, if , we have , so does not imply . Therefore, our Kripke model does not force . According to our correctness lemma, there cannot be a closed lambda term with this type.

Q.E.D.

This example is called the *Peirce formula*. You might wonder why this
is interesting. In fact, it is just an introductory example. However,
if you know functional programming languages, especially Scheme,
you might be familiar with the concept of *continuations*. The type of
`call/cc`

is the Peirce formula. In Haskell's standard library,
there is also a `callCC`

routine with a similar type. However,
this routine has a slightly different type: It uses the
continuation translation of (see the type constructor
`cont`

). The reason is that Haskell is pure, and in a pure setting, it
is not possible to derive the Peirce formula, which can be shown in a
similar way as we just did.

So far, our lambda terms only have atomic types and arrow types. We add a few new type constructors:

- If and are types, then so is
, the
*product type*(or*pair type*). - If and are types, then so is
, the
*sum type*(or*union type*– it corresponds to unions in programming languages like C++). - There is a distinguished type , the
*empty type*or*falsum*. It must be impossible to create a closed term with this type.

There are additional *axiomatic* lambda terms for all types
:

- Product type introduction : This term gets two arguments and returns their pair.
- Product type destruction : This term gets a term of the product type, and a term that maps the two elements of this pair to some other type, and returns this type. For example, the projection to the second coordinate of a pair is .
- Sum type introduction and .
- Sum type destruction . This corresponds to
`if … then … else …`

. - Ex falso quodlibet: .

Except for the empty type, all of these are concepts that occur similarily in most modern programming languages, maybe written in a somewhat less intuitive way. We can give terms that do simple stuff like

From that perspective, empty types make no sense: They have no
*computational content*. However, we can as well interpret these types
as *predicates*: The atomic types become atomic predicates,
will mean "or" ,
will mean "implies"
, and will mean "and"
. In this interpretation, is the predicate that
is always wrong, and means "not
". We therefore define the abbrevitation . In this interpretation, closed lambda terms
become *formal proofs*. For example, we can prove the introduction of
contraposition:

However, the other direction cannot be derived. We can show this with a slightly extended definition of Kripke Models: We have to add interpretations for , and :

- not for all .
- if and only if and .
- if and only if or .

The above proof of correctness can be extended, but it is more technical. We will therefore not do this here. In this system, the Peirce formula is not derivable as well, as can be shown by the same Kripke model as above. Also, in the same Kripke model as above, contraposition and the law of excluded middle do not hold (exercise).

We now extend our type system with *objects* and *relations*. We
define a special type of objects. A *relation* is a
"type with object arguments". For example, the set theoretic
-relation is a relation with two object arguments. Remember,
we are in metatheory, the object type is not specified and must be
defined by axioms.

To get the full mathematical strength, we need to introduce *quantors*:

- means "for all objects , holds".
- means "there exists an object , such that holds".

The type is similar to , and is similar to , except that may depend on .

Introducing a universal quantifier is therefore done by abstraction , and it is eliminated by application .

The introduction of an existential quantifier reflects sum introduction: . Its elimination is where must not occur freely in .

We now have the full expressivity of first-order predicate logic. For example, we can prove :

However, as before the type system we just defined only allows for
*intuitionistic* logic. The advantage of intuitionistic logic is that
if you prove the existence of something, you get an algorithm that
calculates it. The disadvantage is that things that cannot be
calculated cannot be shown to exist. The following is the so-called
*Drinker formula* (or Drinker problem, or sometimes Drinker paradox):

It is not derivable in intuitionistic logic. We can show this using a Kripke model, but we first have to extend our semantic:

Firstly, every node gets a *domain* of
objects, such that . The
relation now depends on an *assignment* ,
which is a function from object variables to
elements of the domain of the corresponding node. For every relation
with arguments, now, becomes a
function . This corresponds
to our former function in the sense that predicates become relations
with zero arguments. We then say if and only if
. For
, the definition is
similar to our former definition, where decomposes to and .

For the interpretation of the quantors, we must define , which is , except for the variable , where it is :

- if and only if there exists an such that .
- if for all , for all , .

We again omit the correctness proof. But we show that the Drinker formula cannot be derivable. We set with the canonical ordering. We set and for . (This model is taken from here.)

⋮ 3 D={0,1,2,3} b={0→1,1→1,2→1,3→0} | 2 D={0,1,2} b={0→1,1→1,2→0} | 1 D={0,1} b={0→1,1→0} | 0 D={0} b={0→0}

We set . Obviously, if , then . However, , but . Therefore, .

A similar concept for first-order logic you might see is the concept
of *Beth models*. Their definition is slightly different but similar,
and their properties are similar. See here for example.

There is a generalization of Kripke models, the so-called *presheaf
models*. Here, the domains are given by a *presheaf*
on a
category .

For every relation with arguments and every object from we have an interpretation such that if there is a morphism in , we have . An assignment is, as before, a map from variable symbols into objects. The definition is now similar to the one for Kripke models: For relations, we define . For implications we define if and only if for every morphism , implies .

It is also possible to define this (even more general) in terms of morphisms between classical models instead of explicitly giving interpretations for all relations and domains. You might also find a more intricate version of implication for arrow types, a version that includes computational content, as an interpretation of type theory.

A Kripke model is a special case where is a poset.

The following part is kept very short and only for older
audiences. Paul Joseph Cohen proved that the *continuum
hypothesis* is independent of Zermelo-Fraenckel Set Theory (ZFC). He
uses a concept inspired by Kripke models. We will only look at the
parts related to Kripke models here. For an explanation of the proof
see here, here and here.

This is a relative consistency result, so we can assume that there is a classical transitive countable model of ZFC. (It can be proved that the existence of such a set is unprovable, by Gödel's second incompleteness theorem.)

That is a set for which the ZFC axioms hold when relativizing
all quantors to it (that is, replacing with
, etc). Transitivity means that . This can be proved by the
*Löwenheim-Skolem theorem* and the *Mostowsky collapse lemma*.

We write if the formula holds in
when relativizing all quantors to it. Notice that we already
used the character for Kripke models. It is generally
used for semantic entailment. is a so-called *classical*
model, while Kripke models are *intuitionistic* models.

A *forcing poset* is a triple completely
defined in where is a preorder with the largest
element and the *splitting condition* that for all there exist such that there is no , that is, they form no diamond, that is, the ordering is
similar to a tree.

A -name is, roughly speaking, a set with an element of attached, in which every element itself is a -name. That is, for example, for .

We define , the *valuation map*.

We now define

where is the set of -names in
. We now define a *forcing relation* on elements of
.

- .
- .
- .
- .

One can show that if satisfies some conditions, holds there is a such that .

Show comments (Requires JavaScript, loads external content from Disqus.com)