The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations

E-ISSN： 1943-5886|40|3|321-346

ISSN： 0022-4812

Source： The Journal of Symbolic Logic, Vol.40, Iss.3, 1975-09, pp. : 321-346

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

The primary purpose of this work is to analyze the constructive interpretations of classical theorems concerning the continuity of effective operations. These theorems are the “recursivizations” of the statements that all functions (on various spaces) are continuous. To discuss the question whether these statements are constructively valid, it would be necessary to analyze the notion of “constructively valid,” which is beyond the scope of this paper. We now proceed to describe our results. We deal with two kinds of effective operations: (i) partial operations on indices of partial functions, and (ii) total operations on indices of total functions. The two principal theorems of the subject assert that each such operation is continuous; for (i) this is due to Myhill-Shepherdson [7] and called MS here; for (ii) it is due to Kreisel, Lacombe, and Shoenfield [5] and called KLS. (Explicit formulations of these and other principles mentioned in the introduction will be given in §1 below.)