I don’t have much time, so here’s just a quick jot. I don’t think System IG can prove this rather obvious proposition:
|- GL(\a. Ga(Ka)) (\a x. x)
Or translated to more conventional notation: (\a x. x) : (a : Type) -> (a -> a), the type of the polymorphic identity function. In order to prove this, we need the axiom LL (conventionally, Type : Type). But that axiom is inconsistent. So I’ve tweaked the rules a bit to allow the above to be proven, without allowing LL. It’s possible that these tweaks are still consistent; they don’t admit Girard’s paradox, at least.
The rules I’m modifying can be found on page 8 of the above paper, in the IG box. My tweak is, changing rule Gi from:
?, Xx |- Yx(Zx) ; ? |- LX ; x not in FV(?,X,Y,Z) => ? |- GXYZ
?, Xx |- Yx(Zx) ; ? |- L(GXY) ; x not in FV(?,X,Y,Z) => ? |- GXYZ
I’m saying that you need to prove that GXY (conventionally, (x:X) -> Y x) is a type before you can say something has that type. Without more modifications, this is equivalent to the original. However, now I add two new rules:
? |- L(GL(KL)) ? |- GL(KL)p => ? |- L(GLp)
These say: (Type -> Type) : Type, and if p : Type -> Type then ((x:Type) -> p x) : Type. The latter one is the one I’ve heard is still consistent, but you can’t really do anything with it without the former. So, it needs further investigation.
Trying to prove the consistency of this new system, I need a semantics for terms. If I can model these semantics in CIC (the calculus used by Coq), then if CIC is consistent, so is this system. My idea for semantics is as follows:
Bare lambda terms don’t really have semantics; they are modeled by their syntax. But typing proofs have the semantics of whatever they are proving as well-typed. If I use [-] as the meaning function, then the semantics of [Lx] is a type (because it is a proof that x is a type). Formally:
[Lx] : Type [Gxyz] : (a:[Lx]) -> [Gx(KL)y] a
Simplified, the latter means that the semantics of a proof that x has type y -> z is a function from y to z. (Rather, it’s the dependent version of that). These semantics motivate the axioms I am adding.
Okay, that’s all the time I have!