Problem Detail: If a type system can assign a type to λ x . x x, or to the non-terminating (λx . x x) (λ x . x x), then is that system inconsistent as a consequence? Is every type under that system inhabited? Can you prove false?
Asked By : MaiaVictor
Answered By : cody
Certainly, assigning a type to $lambda x. x x$ is not enough for inconsistency: in system $F$, we can derive $$ lambda x.x x:(forall X.X)rightarrow (forall X.X)$$ in a pretty straightforward way (this is a good exercise!). However, $(lambda x.x x)(lambda x.x x)$ cannot be well typed in this system, assuming $omega$-consistency of 2nd order arithmetic, as this implies that all such well-typed terms are normalizing. Furthermore, system $F$ is consistent. This follows from either normalization, as one can show that any term of type $forall X.X$ cannot have a normal form, or a much simpler argument, in which each type is assigned a set, either $varnothing$ or ${varnothing}$ and it can be shown that all derivable types are assigned ${varnothing}$, and $forall X.X$ is assigned $varnothing$ (and is therefore not derivable). The latter argument can be carried out in first-order arithmetic. The fact that $lambda x.x x$ can be well-typed in a consistent system can be seen as somewhat disturbing, and is a consequence of the systems’ impredicativity. It shouldn’t come as a surprise that some people question the trustworthiness of impredicative systems of logic. However, no inconsistencies have been found so far in such systems. On the other hand, to be able to make the more general assertion that $(lambda x.x x)(lambda x.x x)$ cannot be well-typed in a consistent system, you need to have enough “logical structure” in your type system to be able to clearly define consistency. Then you need to show that a term without a head normal form (like the one above) can have any type, which is also not obvious! More details can be found in my answer to a related question: http://cstheory.stackexchange.com/a/31321/3984
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/65003