In this thesis, we study the least fixed point principle in a constructive setting. A constructive theory of functions and sets has been developed by Feferman. This theory deals both with sets and with functions over sets as independent notions. In the language of Feferman's theory, we are able to formulate the least fixed point principle for monotone inductive definitions as: every operation on classes to classes which satisfies the monotonicity condition has a least fixed point. This is called the (...) principle of monotone inductive definition. Furthermore, we may formulate this principle in a uniform way as: there is an operation which maps a monotone operation to its least fixed point. This is called the principle of uniform monotone inductive definition. Feferman raised the question of the strength of the principle of monotone inductive definition when adjoined to his theory . This question is our primary concern in this thesis. ;Our main results are the consistency of both the principle of monotone inductive definition and the principle of uniform monotone inductive definition adjoined to his theory, and the proof theoretical equivalence between the principle of monotone inductive definition with Feferman's system without the inductive generation axiom and the system of the Pi-one-one Comprehension Axiom. Determination of the proof-theoretical strength of the principle of monotone inductive definition adjoined to Feferman's theory still remains open. ;The consistency of both the principle of monotone inductive definition and the principle of uniform monotone inductive definition with Feferman's theory will be achieved by constructing their models in set theoretical sense. The proof theoretical equivalence between the principle of monotone inductive definition with Feferman's system without the inductive generation axiom and the system of the Pi-one-one Comprehension Axiom can be obtained by a careful examination of the model construction for the principle of monotone inductive definition with Feferman's system without the inductive generation axiom, which is parallel to the model construction for the principle of monotone inductive definition with his theory. (shrink)

Starting with D. Scott's work on the mathematical foundations of programming language semantics, interest in topology has grown up in theoretical computer science, under the slogan `open sets are semidecidable properties'. But whereas on effectively given Scott domains all such properties are also open, this is no longer true in general. In this paper a characterization of effectively given topological spaces is presented that says which semidecidable sets are open. This result has important consequences. Not only follows the classical Rice-Shapiro (...) Theorem and its generalization to effectively given Scott domains, but also a recursion theoretic characterization of the canonical topology of effectively given metric spaces. Moreover, it implies some well known theorems on the effective continuity of effective operators such as P. Young and the author's general result which in its turn entails the theorems by Myhill-Shepherdson, Kreisel-Lacombe-Shoenfield and Ceĭtin-Moschovakis, and a result by Eršov and Berger which says that the hereditarily effective operations coincide with the hereditarily effective total continuous functionals on the natural numbers. (shrink)

If one wants to compute with infinite objects like real numbers or data streams, continuity is a necessary requirement: better and better (finite) approximations of the input are transformed into better and better (finite) approximations of the output. In case the objects are constructively generated, they can be represented by a finite description of the generating procedure. By effectively transforming such descriptions for the generation of the input (respectively, their codes) into (the code of) a description for the generation of (...) the output another type of computable operation is obtained. Such operations are also called effective. The relationship of both classes of operations has always been a question of great interest. In this paper the setting is extended to the case of multifunctions. Various ways of coding (indexing) sets are discussed and their relationship is investigated. Moreover, effective versions of several continuity notions for multifunctions are introduced. For each of these notions an indexing system for sets is exhibited so that the multifunctions that are effective with respect to this indexing system are exactly the multifunction which are effectively continuous with respect to the continuity notion under consideration. Mostly, in addition to being effective the multifunctions need also possess certain witnessing functions. Important special cases are discussed where such witnessing functions always exist. (shrink)

This little gem is stated unbilled and proved in the last two lines of §2 of the short note Kleene [1938]. In modern notation, with all the hypotheses stated explicitly and in a strong form, it reads as follows:Second Recursion Theorem. Fix a set V ⊆ ℕ, and suppose that for each natural number n ϵ ℕ = {0, 1, 2, …}, φn: ℕ1+n ⇀ V is a recursive partial function of arguments with values in V so that the standard (...) assumptions and hold with. Every n-ary recursive partial function with values in V is for some e. For all m, n, there is a recursive function : Nm+1 → ℕ such that.Then, for every recursive, partial function f of arguments with values in V, there is a total recursive function of m arguments such thatProof. Fix e ϵ ℕ such that and let.We will abuse notation and write ž; rather than ž() when m = 0, so that takes the simpler formin this case ). (shrink)

A type-structure of partial effective functionals over the natural numbers, based on a canonical enumeration of the partial recursive functions, is developed. These partial functionals, defined by a direct elementary technique, turn out to be the computable elements of the hereditary continuous partial objects; moreover, there is a commutative system of enumerations of any given type by any type below (relative numberings). By this and by results in [1] and [2], the Kleene-Kreisel countable functionals and the hereditary effective operations (HEO) (...) are easily characterized. (shrink)

Every acceptable numbering of an effective domain is complete. Hence every effective domain admits the 2nd recursion theorem of Eršov[1]. On the other hand for every effective domain, the 1st recursion theorem holds. In this note, we establish that for effective domains, the 2nd recursion theorem is strictly more general than the 1st recursion theorem, a generalization of an important result in recursive function theory.

We reconsider some classical natural semantics of integers in the perspective of Kolmogorov complexity. To each such semantics one can attach a simple representation of integers that we suitably effectivize in order to develop an associated Kolmogorov theory. Such effectivizations are particular instances of a general notion of “self-enumerated system” that we introduce in this paper. Our main result asserts that, with such effectivizations, Kolmogorov theory allows to quantitatively distinguish the underlying semantics. We characterize the families obtained by such effectivizations (...) and prove that the associated Kolmogorov complexities constitute a hierarchy which coincides with that of Kolmogorov complexities defined via jump oracles and/or infinite computations . This contrasts with the well-known fact that usual Kolmogorov complexity does not depend on the chosen arithmetic representation of integers, let it be in any base n ≥ 2 or in unary. Also, in a conceptual point of view, our result can be seen as a mean to measure the degree of abstraction of these diverse semantics. (shrink)

In this paper we specialize the notion of abstract computational procedure previously introduced for intensionally presented structures to those which are extensionally given. This is provided by a form of generalized recursion theory which uses schemata for explicit definition, conditional definition and least fixed point recursion in functional of type level 2 over any appropriate structure. It is applied here to the case of potentially infinite streams as an abstract data type.

This chapter presents a new semantics for inductive empirical knowledge. The epistemic agent is represented concretely as a learner who processes new inputs through time and who forms new beliefs from those inputs by means of a concrete, computable learning program. The agent’s belief state is represented hyper-intensionally as a set of time-indexed sentences. Knowledge is interpreted as avoidance of error in the limit and as having converged to true belief from the present time onward. Familiar topics are re-examined within (...) the semantics, such as inductive skepticism, the logic of discovery, Duhem’s problem, the articulation of theories by auxiliary hypotheses, the role of serendipity in scientific knowledge, Fitch’s paradox, deductive closure of knowability, whether one can know inductively that one knows inductively, whether one can know inductively that one does not know inductively, and whether expert instruction can spread common inductive knowledge—as opposed to mere, true belief—through a community of gullible pupils. (shrink)