Consistent Higher-order IG
Abram Demski
Hi all,
Russel, Luke and I have talked about systems IXI and IG in the past. Recently I've had some reason to think about them again. The following proposal stems from my thoughts on the semantics of these systems... as such, I think I know how to prove that it's consistent, though obviously it's not a proof until I work through the details.
The proposal may be of limited interest, because it essentially re-introduces types. However, the result still allows all the untyped reasoning allowed in IG...
The idea: these systems cannot handle 2nd-order quantification because they can only restrict quantification to well-defined sets. Syntactically, this just means a set S needs to satisfy the build-in predicate L before we can deduce Xi S Q for any Q. Semantically, my interpretation is that S needs to have a definite truth value for all arguments. (The Russel set "the set of all sets which do not contain themselves", to take a famous example, cannot.) Xi plays the role of the restricted quantification: "all S satisfy Q". The naive way of trying to do 2nd-order quantification is to use L itself, reading L as "is a predicate" or "is a well-defined predicate"; ie, we restrict our quantification to predicates: Xi L Q. This fails because L is not always-defined; it *needs* to be undefined for certain cases, to avoid paradox. Hence, my approach is to provide a "less powerful" predicate than L which can be used as a substitute for 2nd-order quantification: call it Zeta.
Whereas L includes *all* well-defined predicates, and so must be non-well-defined itself, Zeta will compromise and only include *many* well-defined predicates, so that it can still be well-defined (and hence can be used in restricted quantifications). Different definitions of Zeta will result in more or less powerful systems, depending on how close Zeta comes to L.
To have a reasonably wide Zeta, it seems reasonable to copy the strategy of simple type theory. My suggestion for doing this is to define Zeta over a sub-language which does not contain talk about types. Specifically, we define Zeta to be false for any terms whose normal forms contain typing constants or which lack normal forms. (The second constraint sadly excludes things like the Y-combinator, but is necessary to make Zeta well-defined.) This means it can be true only of statements which have a normal form and are composed only of Xi, lambda calculus, and any nonlogical constants we add to the system. Of these statements, define Zeta to be true and false just when L is.
If this works, then "Xi Zeta" would provide a sort of second-order quantifier: it wouldn't quantify over *all* predicates, but it would at least quantify over all predicates which would be available in simply-typed lambda calculus.
A curious feature of this solution is that we could have Xi A B and Xi B A, ie "A and B are extensionally equivalent," but also have Zeta A without having Zeta B. This could happen when A was written in a way that used type-theoretic talk, but B was not. For example, if A is \x.P where P is some true statement which can be stated without discussing types, but B is \x.Q where Q is a statement which does need type theory, then A and B are both ways of stating the trivial predicate which always returns "true"; however, Zeta is true of one and false of the other. This doesn't obviously create any contradictions, since IG does not reason about equality or allow substitution of equals for equals. However, it's a rejection of the principle of extensionality, which will likely raise a few eyebrows. (I think the principle of extensionality *should* be rejected, but that's another story.)
--
Abram Demski
http://lo-tho.blogspot.com/
http://groups.google.com/group/one-logic