UNPROVABLY INTRACTABLE LANGUAGES.

With respect to a given formal system F, the author investigates the class UI left bracket F right bracket of unprovably intractable languages, i. e. , those whose nonmembership in P is independent of F. It is shown that when F is sufficiently strong, UI left bracket F right bracket (together with P) is closed downward under polynomial-time Turing reducibility. In other senses, however, the boundary between UI left bracket F right bracket and the complementary class PI left bracket F right bracket is shown to be very badly behaved. All results hold when F is Peano arithmetic or any stronger system. The investigations treat two questions of general interest: (1) how strong must a system be to constitute an acceptable formal theory of computation? ; and (2) which theorems in computer science can or cannot be proved constructively?