THE MAXIMUM CONSISTENT THEORY OF THE SECOND ORDER \beta\eta LAMBDA CALCULUS We prove the existence of the maximum consistent theory Top and that it satisfies the following omega-rules (I write (M Top(o) N) for (Top |- M=N;o), where o is a closed type expression and M and N are closed tems of type o) : i. M Top(V t.o[t]) N iff for all closed type expressions o0 M[o0] Top(o[o0]) N[o0] ii. M Top(o1 --> o2) N iff for all closed terms P of type o1 (M P) Top(o2) (N P). These two properties imply that the following is a model (we use the definition in [Bruce-Meyer 84]) : Notation : \L0(o) is the set of closed terms of type o X/R is the set of equivalence classes w.r.t. R, where R is an equivalence relation on X [P] is the equivalence classes of P w.r.t. Top(o), where P is a closed term of type o DEF. (The maximum consistent closed term model) T = { o | o closed type expression} [T-->T] = {\t.o[t] | o type expression with at most t free} arrow : TxT --> T s.t. arrow(o1,o2) = (o1 --> o2) forall : [T-->T] --> T s.t. forall(\t.o[t]) = (V t.o[t]) D : T --> Set s.t. D(o) = \L0(o) / Top(o) App{o1,o2} : D(arrow(o1,o2))xD(o1) --> D(o2) s.t. App{o1,o2}([M],[N]) = [(M N)] App{\t.o[t]} : D(forall(\t.o[t]) --> ( \Pi o0:T.D(o[o0]) ) s.t. App{\t.o[t]}([M],o0) = [M[o0]] * PROPOSITION (Statman) TOP |- M=N:sigma <=> For all closed F of type sigma -> BOOL \beta\eta |- FM = FN. It's easy to show that TOP is the maximum of CON, but one has to use the PER{_} construction to prove that TOP is a theory * However, the following conjecture is still open: CONJECTURE (Statman) The theory of Coquand's model is the maximum consistent theory (see Coquand's message on the 14th April in the type mail for a description of his model) * DETAILS ----------------------------------------------------------------- DEF. An equation (M = N : o) is WELL-FORMED iff o is a closed type expression and M and N are closed terms of type o REMARK: the definition of well-formed (used here) does not depend on a set of equations between type expressions A THEORY is a set of well-formed equations closed w.r.t. the inference rules for \beta\eta A theory is CONSISTENT iff it is not the set of all well-formed equations A model F is TRIVIAL iff for all types of F the underlying set is of cardinality less than or equal to 1 The THEORY OF A MODEL F is the set of well-formed equations true in F * PROP. A model is non trivial iff its theory does not contain the well-formed equation (True = False : Bool) A theory is consistent iff it does not contain the well-formed equation (True = False : Bool) * PRELIMINARY FACTS: DEF 1. CON (the set of consistent pretheories) is R \in CON iff a. R is a family indexed by closed type expressions o s.t. R(o) is an equivalence relation on the set of closed terms of type o b. R respect \beta\eta-conversion, i.e. \beta\eta |- M = N : o implies M R(o) N c. M1 R(o1 --> o2) M2 and N1 R(o1) N2 implies (M1 N1) R(o2) (M2 N2) M1 R(V t. o[t]) M2 and o0 is a closed type expression implies (M1 [o0]) R(o[o0]) (M2 [o0]) d. R is non trivial i.e. True and False are not related by R(Bool) On CON one can define the following partial order R \leq S iff for all o R(o) is included in S(o) * FACT 2. (Properties of CON) CON has a least element Bot (Bot is the theory of the open term model, see the definition of "Th" below) CON has binary sups, i.e. if R,S \in CON then there exists R+S \in CON s.t. for all T \in Con R,S \leq T iff R+S \leq T CON has a maximum Top * To prove that CON has maximum is crucial that for any R,S \in CON there exists an upper bound of {R,S} in CON Incidentally CON has infs of non empty subsets ----------------------------------------------------------------- Proof of CON has binary sups : Let R,S \in CON and define T as the family of equivalence relations s.t. T(o) = the equivalence relation generated by R(o) \union S(o) If we prove that T is in CON then T is the sup. Notation. if X and Y are relations and n is a natural number, then (XY) is the composition of X with Y X^n is the composition of X with itself for n times * Claim. T(o) is the sup of the omega-chain (R(o)S(o))^n * Claim. T is in CON . Proof. We check that T has the properties a-d (see Def 1) : a. is immediate from the definition b. T respects \beta\eta-conversion, because R respects \beta\eta-conversion and R(o) is included in T(o) c. If M T(o1 --> o2) M' and N T(o1) N', then we must derive (M N) T(o2) (M' N') By the Claim there exists n s.t. M (R(o1 --> o2)S(o1 --> o2))^n M' and N (R(o1)S(o1))^n N' So there are M0 ... M(n+1) and M0' ... Mn' s.t. M = M0 , M' = M(n+1) and Mi R(o1 --> o2) Mi' S(o1 --> o2) M(i+1) for i = 0 ... n Similarly there are N0 ... N(n+1) and N0' ... Nn' s.t. N = N0 , N' = N(n+1) and Ni R(o1) Ni' S(o1) N(i+1) for i = 0 ... n By the property c. for R and S it follows that (Mi Ni) R(o2) (Mi' Ni') S(o2) (M(i+1) N(i+1)) for i = 0 ... n So (M N) (R(o2)S(o2))^n (M' N') By the Claim (M N) T(o2) (M' N') * The corresponding property for polymorphic types is proved in a similar way d. T is non trivial, because R and S are non trivial * ----------------------------------------------------------------- FACT 3. For every non trivial model F we can define an element Th{F} of CON (call it the theory of F): M Th{F}(o) N iff (M = N : o) is true in F * In general not all elements of CON are the theory of a model (but I don't have any counterexample). FACT 4. If R \in CON then there is a non trivial model PER{R} s.t. R \leq Th{PER{R}} * The construction of PER{R} from R is similar to the way Coquand define the closed term model; actually his model is PER{Bot}. In particular all the elements of a closed type in PER{R} are interpretation of closed terms (of that type). ----------------------------------------------------------------- Notation : \L0(o) is the set of closed terms of type o X/R is the set of equivalence classes w.r.t. R, where R is a partial equivalence relation on X [P]{R} is the equivalence classes of P w.r.t. the partial equivalence relation R (and P must be in the domain of R, i.e. P R P) Definition of PER{R} : T = { (o,S) | o closed type expression and S partial equivalence relation on \L0(o) s.t. if M S N and N R(o) P then M S P } [T-->T] = { G:T-->T | exist o[t] and F s.t. if (o0,S0) \in T then G(o0,S0) = (o[o0],F(o0,S0)) } arrow : TxT --> T s.t. arrow((o1,S1),(o2,S2)) = ((o1 --> o2),S), where M S M' iff for all N,N' if N S1 N' then (M N) S2 (M' N') forall : [T-->T] --> T s.t. forall(G) = ((V t.o[t]),S), where M S M' iff for all (o0,S0) \in T M[o0] F(o0,S0) M'[o0] see def of [T-->T] for the meaning of o[t] and F D : T --> Set s.t. D((o,S)) = \L0(o) / S App{(o1,S1),(o2,S2)}([M]{S},[N]{S1}) = [(M N)]{S2} see def of arrow for the meaning of S App{G}([M]{S},(o0,S0)) = [M[o0]]{F(o0,S0)} see def of [T-->T] for the meaning of o[t] and F ----------------------------------------------------------------- Theorem. Top is the maximum consistent theory. Proof. Top is consistent (by definition of CON) Top is a theory because it's the theory of PER{Top} (by definition of Top Th{PER{Top}} \leq Top, by Fact 4 Top \leq Th{PER{Top}}) Top is the maximum consistent theory (by Fact 3 if F is a non trivial model Th{F} \in CON by definition of Top Th{F} \leq Top) * Top satisfies the following omega-rules : i. M Top(V t.o[t]) N iff for all closed type expressions o0 M[o0] Top(o[o0]) N[o0] ii. M Top(o1 --> o2) N iff for all closed terms P of type o1 (M P) Top(o2) (N P). These rules don't seem to be valid in general (but I don't have counterexamples); the general result used to derive them for Top is : PROP. Given R \in CON let S = Th{\PER{R}} \in CON, then i. for all closed type expressions o0 M[o0] R(o[o0]) N[o0] implies M S(V t.o[t]) N implies for all closed type expressions o0 M[o0] S(o[o0]) N[o0] ii. M S(o1 --> o2) N iff for all closed terms P of type o1 (M P) S(o2) (N P). * ----------------------------------------------------------------- A SIMILAR CONSTRUCTION FOR INHABITED MODELS extend the second order lambda calculus by adding a constant 0 of type (V t.t) and the axioms: 0[o1->o2] = \x:o1.0[o2] 0[V t.o[t]] = \t.0[o] from now on we use this extension of the calculus (\inhab\beta\eta) unless otherwise stated. Theorem there is a maximum consistent theory of the \inhab\beta\eta lambda calculus Remark if we drop the two axioms for 0 (but do not remove 0), then there is maximum consistent theory, in fact it is possible to satify the equation \t 0[t->t] = \t.\x:t.x (e.g. in Finitary projection model) but this toghether with the first axiom for inhab implies True = False Open problem: what happens if we do not add 0 to the language? HINT ------------------------------------------------------------ DEF 1. InhabCON (the set of inhabited consistent pretheories) is R \in InhabCON iff a. R is a family indexed by closed type expressions o s.t. R(o) is an equivalence relation on the set of closed terms of type o b. R respect \inhab\beta\eta-conversion, i.e. \inhab\beta\eta |- M = N : o implies M R(o) N c. M1 R(o1 --> o2) M2 and N1 R(o1) N2 implies (M1 N1) R(o2) (M2 N2) M1 R(V t. o[t]) M2 and o0 is a closed type expression implies (M1 [o0]) R(o[o0]) (M2 [o0]) d. R is non trivial i.e. True and False are not related by R(Bool) e. (\x:o1.M) R(o1->o2) (\x:o1.N) iff M R(o2) N FACT 2. InhabCON is a complete lattice. ----------------------------------------------------------------- Definition of InhabPER{R} : Let R be in InhabCON, then: T = { (o,S) | o closed type expression and S partial equivalence relation on \L0(o) s.t. 0[o] S 0[o], if M S N and N R(o) P then M S P } [T-->T] = { G:T-->T | exist o[t] and F s.t. if (o0,S0) \in T then G(o0,S0) = (o[o0],F(o0,S0)) } arrow : TxT --> T s.t. arrow((o1,S1),(o2,S2)) = ((o1 --> o2),S), where M S M' iff for all N,N' if N S1 N' then (M N) S2 (M' N') from 0[o2] S2 0[o2] it follows that 0[o1->o2] S 0[o1->o2] forall : [T-->T] --> T s.t. forall(G) = ((V t.o[t]),S), where M S M' iff for all (o0,S0) \in T M[o0] F(o0,S0) M'[o0] from image of G in T it follows that 0[V t.o] S 0[V t.o] see def of [T-->T] for the meaning of o[t] and F D : T --> Set s.t. D((o,S)) = \L0(o) / S App{(o1,S1),(o2,S2)}([M]{S},[N]{S1}) = [(M N)]{S2} see def of arrow for the meaning of S App{G}([M]{S},(o0,S0)) = [M[o0]]{F(o0,S0)} see def of [T-->T] for the meaning of o[t] and F Proposition InhabPER{R} is a non trivial model of \inhab\beta\eta.