Mathematical definability
Theodore A. Slaman · 1998
Abstract One might fairly say that the mathematical analysis of definability began in 1931, with the appearance of Gödel’s Incompleteness Theorem (Gödel 1931). Gödel showed that, for sufficiently strong formal systems T, there exist undecidable statements φ such that there is no proof of φ or of φ within T. This theorem pointed to an intrinsic incompleteness within the formal notion of proof. The method of computation by algorithm is more general than that of verification by formal proof. It too was shown to be incomplete, but it took some time to develop the technical apparatus needed to state this incompleteness correctly. (Kleene 1987), in his biographical memoir of Gödel, recalls this development and we summarize some of his remarks. Kleene describes the intuitive notion of an algorithm as follows.