A programming language theorem which is independent of Peano Arithmetic
Michael O'Donnell · 1979
Strongly typed programming languages contain a natural subrecursive part consisting of programs with no loops and no explicitly recursive (circular) function definitions. For languages with polymorphic type structure, such as Model, the termination of all loop-free nonrecursive programs is independent of Peano Arithmetic. An attempt to apply the same techniques to prove independence of the [email protected]@@@NP problem can succeed only if NP complete problems have almost polynomial complexity.