A Simple Proof of the Undecidability of Inhabitation in lambdaP

Abstract

Capsule ReviewIt had been known that the simplest system with dependent types, XP, is undecidable, in that sense that the set {(A,D\3pr\-XP p:A} is non-computable.The proof runs as follows.First, there is an obvious embedding of predicate logic into XP.This is the principle idea of one of the basic members of the AUTOMATH family, AUT-QE, and also later of Edinburgh LF.It can be shown that this embedding is conservative (Berardi; Barendsen and Geuvers).This is not completely obvious, since XP has functions of arbitrarily high type at its disposal.Now it follows from Godel's technique (proving the incompleteness theorems) that arithmetic and even a finitely axiomatizable part of it (Robinson's arithmetic) is essentially undecidable.Therefore XP is also undecidable.This is quite a long path to the result -admittedly quite beautiful, passing along classical details like the Chinese remainder theorem -but almost too much.Fortunately, the authors of this paper have given a very direct argument showing the same result, by a surprisingly straightforward encoding of a register machine.An inhabitation problem in a given Pure Type System (PTS) XS is a pair (F, B) such that, for some sort s, F \-^s B : s.A solution for (F, B) is a term A such that F \~xs A : B. In this note we prove that in the PTS kP it is undecidable whether an inhabitation problem has a solution.This result also follows from Lob's results on embeddings of predicate logic in fragments of intuitionistic logic (Lob, 1976, p. 1, 1. 10) plus the fact that XP is sound and complete with respect to minimal predicate logic (see Geuvers (1993)).The merit of our proof is that it is short, simple and intuitive.Sometimes, inhabitation problems are defined with F the empty context.In IP, however, this makes little sense: the only statement valid in the empty context is * : D. After the proof of our result, we discuss related results concerning the other systems of the ^-cube.For a general introduction to PTSs the reader is referred to Barendregt (1992).