Independence results in computer science?

摘要

The adequacy of weak theories of arithmetic as axiomatic bases for Computer Science is investigated. The formal system studied in Lipton (in “Proceedings, 19th Symposium of the Foundations of Computer Science,” pp. 193–200, 1978) is shown to be inadequate for Computer Science in the sense that it has a model with the following defects: (i) finite (i.e., bounded) sets may be undecidable in the model, (ii) standard recursively enumerable sets which are undecidable may have linear time decision procedures in the model, and (iii) programs which simply loop a bounded number of times may not terminate in the model (demonstrating the inadequacy of the formal system for proving program termination).