[Prev][Next][Index][Thread]

Kripke lambda models

Date: Sat, 21 Jan 89 15:35:18 PDT
To: meyer@theory.LCS.MIT.EDU, riecke@theory.LCS.MIT.EDU
Cc: types@theory.LCS.MIT.EDU

This is a response to "point 3" of a message about Kripke
lambda models from Jon Riecke and Albert Meyer.
The point they raises was essentially that it followed in the
framework of my paper with Moggi in 1987 LICS (to appear in
J. Pure and Applied Logic one of these days) that
if T is the first-order theory of a class of Kripke lambda models 
(regarded as multi-sorted  first-order structures), then T is the 
theory of a single Kripke model. Here is a summary of some relevant
communication (to bring everyone up to date, and remind Meyer
and Riecke what we were discussing), follows by my current
point of view.

JCM:
   Date: Fri, 6 Jan 89 15:54:44 PDT
   From: John Mitchell <jcm@ra.stanford.edu>

   I can't see why 3. would be true, for much the same
   reasons that it fails for classical models. (We have
   disjunction in first order logic, so a disjunction
   of closed formulas may hold for a class of models
   without either disjunct holding for the entire class.)
   What did I/we say that suggested 3. is true?


RIECKE:
We suspected 3 might hold from an informal statement made on page 313 in your
paper:
      We have shown that every typed lambda theory is the theory of some
      Kripke quotient of a classical lambda model, but that this does not
      carry over to quantified formulas.  

I'm going to be a bit stubborn and try to sketch a proof (?) of 3.  I don't
claim to have mastered all the definitions yet, so please tell me if I'm
confused; I'll go back and study my intuitionistic logic more if I am!
   Proof:  Suppose we have a class of Kripke models SM.  To construct a model 
     for THF(SM), construct the world structure W which is the disjoint union
     of all worlds in SM, ordered by the old orderings.  That is, if A and B
     are models in SM, and w is a world in A, w' a world in B, then in the new
     model, w and w' are not ordered.  This new model is a model of precisely
     THF(SM).

---

Your proof looks right to me, but it raises a subtle issue that we did not 
bring out properly in the paper. The main reason was that I really wasn't
aware of this at the time. Let me try to put things in perspective
by discussing the connection between logical theories and categorical notions.

If we take typed lambda calculus, for example, then it is relatively easy
to see (from the right point of view; I'll try writing this down sometime)
that the natural "algebraic" definition of lambda theory is precisely the
definition of cartesian closed category. So really we have an equivalence
typed lambda theory = ccc; this is well-known to the relevant brand
of category theorist.  For this reason, it is slightly inaccurate to
say that ccc's give us a completeness theorem for typed lambda calculus.
The connection is really too trivial to call it this. A similar equivalence
exists between Church's type theory (when we drop the excluded middle)
and toposes. For this reason category theorists try to find various
representation theorems, or identify special kinds of categories as
"models." 

For type theory, (or any first-order language), two natural properties
we might require of models are the "existence" and "disjunction" 
properties. (This is discussed in Chap 17, Part II of Lambek and Scott.)
These are (i) if a model satisfies Exists x.P(x), then there is some
a (perhaps in an extended language) such that the model satisfies P(a),
(ii) if a model satisfies P or Q, then the model satisfies P or satisfies
Q. If these appeal to your sense of "semantics", then perhaps you'll 
agreee that is makes sense to say a categorical "model" of type theory
is a topos satisfying (i) and (ii). If we now ask whether the proof 
system of type theory is complete, we are asking something less trivial
(or "tautological") than before.

For typed lambda calculus, it is not clear to me what we should require
of models. The main "arguement" in my paper with Phil Scott (this
came out of work in empty types and the paper with Eugenio) is that
"well-pointed-ness" (or "having enough points" or "having 1 as a
generator") seems a bit too strong. The two reasons for this claim
are (a) if we make this restriction, we don't have completeness,
(b) every ccc is "well-pointed" in a natural internal sense, so 
why worry about "well-pointed-ness" anyway. On the other hand, 
accepting all ccc's as models seems too relaxed (even if I am getting 
used to California). I thought at the time we wrote our paper that it
was clear that Kripke models are "models". However, your argument
points out what I would now call a flaw. We should have said
"Kripke models satisfying the existence and disjunction properties
are models." What this boils down to is that we should have proved
completeness for Kripke models having a least world. We in fact
did this, and discussed the existence and disjunction properties
between ourselves at the time, but didn't highlight it in the
write-up. If we restrict our attention to these Kripke models,
then your arguement fails, since the disjoint union of a family
of Kripke models does not have a least world; all of the minimal
worlds are incomparable.

John