The class of primitive recursive functions may be defined as the closure of certain initial functions, namely the zero, successor and identity functions, under two schemes, namely composition (sometimes called “substitution”) and recursion. For a detailed definition the reader is referred to any standard work, for instance p. 219 of [2], by Kleene.

We define a notion of realizability, based on a new assignment of formulas, which does not care for precise witnesses of existential statements, but only for bounds for them. The novel form of realizability supports a very general form of the FAN theorem, refutes Markov's principle but meshes well with some classical principles, including the lesser limited principle of omniscience and weak König's lemma. We discuss some applications, as well as some previous results in the literature.

We provide partial answers to the following problem: Is the class of Borel linear orders well-quasi-ordered under embeddability? We show that it is indeed the case for those Borel orders which are embeddable in Rω, with the lexicographic ordering. For Borel orders embeddable in R2, our proof works in ZFC, but it uses projective determinacy for Borel orders embeddable in some Rn, n < ω, and hyperprojective determinacy for the general case.

Scientific inquiry is represented as a process of rational hypothesis revision in the face of data. For the concept of rationality, we rely on the theory of belief dynamics as developed in [5, 9]. Among other things, it is shown that if belief states are left unclosed under deductive logic then scientific theories can be expanded in a uniform, consistent fashion that allows inquiry to proceed by any method of hypothesis revision based on “kernel” contraction. In contrast, if belief states are closed under logic, then no such expansion is possible.

The modal logic S5 has been formulated in Gentzen-style by several authors such as Ohnishi and Matsumoto [4], Kanger [2], Mints [3] and Sato [5]. The system by Ohnishi and Matsumoto is natural, but the cut-elimination theorem in it fails to hold. Kanger's system enjoys cut-elimination theorem, but, strictly speaking, it is not a Gentzen-type system since each formula in a sequent is indexed by a natural number. The system S5+ of Mints is also cut-free, and its cut-elimination theorem is proved constructively via the cut-elimination theorem of Gentzen's LK. However, one of his rules does not have the so-called subformula property, which is desirable from the proof-theoretic point of view. Our system in [5] also enjoys the cut-elimination theorem. However, it is also not a Gentzen-type system in the strict sense, since each sequent in this system consists of a pair of sequents in the usual sense.

In the present paper, we give a Gentzen-type system for S5 and prove the cut-elimination theorem in a constructive way. A decision procedure for S5 can be obtained as a by-product.

The author wishes to thank the referee for pointing out some errors in the first version of the paper as well as for his suggestions which improved the readability of the paper.

In this note, we show that the theory of tracial von Neumann algebras does not have a model companion. This will follow from the fact that the theory of any locally universal, McDuff II1 factor does not have quantifier elimination. We also show how a positive solution to the Connes Embedding Problem implies that there can be no model-complete theory of II1 factors.

We prove that a (recursively) enumerable degree is contiguous iff it is locally distributive. This settles a twenty-year old question going back to Ladner and Sasso. We also prove that strong contiguity and contiguity coincide, settling a question of the first author, and prove that no m-topped degree is contiguous, settling a question of the first author and Carl Jockusch [11]. Finally, we prove some results concerning local distributivity and relativized weak truth table reducibility.

A pair of r.e. sets A1, A2 are said to split an r.e. set A (written A1 Δ A2 = A) if A1 ∩ A2 = ∅ and A1 ∪ A2 = A. In the literature there are various results asserting certain splitting properties hold for all r.e. sets. For example Sacks' splitting theorem (cf. [So]) asserts that an r.e. nonrecursive set A may be split into a pair of Turing incomparable r.e. sets A1, A2, and Lachlan's splitting theorem [La5] asserts that A may be split into a pair of r.e. sets A1, A2 for which there exists an r.e. set B with B ⊕ A1, B ⊕ A2 <TA and with the infinum of the Turing degrees of B ⊕ A1 and B ⊕ A2 existing in the upper semilattice of r.e. degrees.

Two of the earliest observations establishing that splitting properties possessed by some r.e. sets are not possessed by others, are Lachlan's nondiamond theorem [La1] (and so, in particular, no complete r.e. set can be split nontrivially with degree theoretic inf 0) and the Yates-Lachlan construction of a minimal pair (a pair of nonzero r.e. degrees with inf 0). Other examples of this phenomenon, which are not obtained by interpreting degree theoretic results in the r.e. sets, are Lachlan's construction of nonmitotic r.e. sets [La2] (sets which cannot be split into a pair of r.e. sets of the same degree) and, later, Ladner's [Ld1, 2] and Ingrassia's [In] analysis of their degrees.

Profinite groups are Galois groups. The effective study of infinite Galois groups was initiated by Metakides and Nerode [8] and further developed by LaRoche [5]. In this paper we study profinite groups without considering Galois extensions of fields. The Artin method of representing a finite group as a Galois group has been generalized (effectively!) by Waterhouse [14] to profinite groups. Thus, there is no loss of relevance in our approach.

The fundamental notions of a co-r.e. profinite group, recursively profinite group, and the degree of a co-r.e. profinite group are defined in §1. In this section we prove that every co-r.e. profinite group can be effectively represented as an inverse limit of finite groups. The degree invariant is shown to behave very well with respect to open subgroups and quotients. The work done in this section is basic to the rest of the paper.

The commutator subgroup, the Frattini subgroup, the p-Sylow subgroups, and the center of a profinite group are essential in the study of profinite groups. It is only natural to ask if these subgroups are effective. The following question exemplifies our approach to this problem: Is the center a co-r.e. profinite group? Theorem 2 provides a general method for answering this type of question negatively. Examples 3,4 and 5 are all applications of this theorem.

In [5], Metakides and Nerode introduced the study of recursively enumerable (r.e.) substructures of a recursively presented structure. The main line of study presented in [5] is to examine the effective content of certain algebraic structures. In [6], Metakides and Nerode studied the lattice of r.e. subspaces of a recursively presented vector space. This lattice was later studied by Kalantari, Remmel, Retzlaff and Shore. Similar studies have been done by Metakides and Nerode [7] for algebraically closed fields, by Remmel [10] for Boolean algebras and by Metakides and Remmel [8] and [9] for orderings. Kalantari and Retzlaff [4] introduced and studied the lattice of r.e. subsets of a recursively presented topological space. Kalantari and Retzlaff considered X, a topological space with ⊿, a countable basis. This basis is coded into integers and with the help of this coding, r.e. subsets of ω give rise to r.e. subsets of X. The notion of “recursiveness” of a topological space is the natural next step which gives rise to the question of what should be the “degree” of an r.e. open subset of X? It turns out that any r.e. open set partitions ⊿; into four sets whose Turing degrees become central in answering the question raised above.

In this paper we show that the degrees of the elements of the partition of ⊿ imposed by an r.e. open set can be “controlled independently” in a sense to be made precise in the body of the paper. In [4], Kalantari and Retzlaff showed that given A any r.e. set and any r.e. open subset of X, there exists an r.e. open set ℋ which is a subset of and is dense in (in a topological sense) and in which A is coded. This shows that modulo a nowhere dense set, an r.e. open set can become as complicated as desired. After giving the general technical and notational machinery in §1, and giving the particulars of our needs in §2, in §3 we prove that the set ℋ described above could be made to be precisely of degree of A. We then go on and establish various results (both existential and universal) on the mentioned partitioning of ⊿. One of the surprising results is that there are r.e. open sets such that every element of partitioning of ⊿ is of a different degree. Since the exact wording of the results uses the technical definitions of these partitioning elements, we do not summarize the results here and ask the reader to examine §3 after browsing through §§1 and 2.

Lewis and Langford state, “… it appears that the relation of strict implication expresses precisely that relation which holds when valid deduction is possible. It fails to hold when valid deduction is not possible. In that sense, the system of strict implication may be said to provide that canon and critique of deductive inference which is the desideratum of logical investigation.” Neglecting for the present other possible criticisms of this assertion, it is plausible to maintain that if strict implication is intended to systematize the familiar concept of deducibility or entailment, then some form of the deduction theorem should hold for it. The purpose of this paper is to analyze and extend some results previously established which bear on the problem.

We will begin with a rough statement of some relevent considerations. Let the system S contain among its connectives an implication connective ‘I’ and a conjunction connective ‘&’. Let A1, A2, …, An ⊦ B abbreviate that B is provable on the hypotheses A1, A2, …, An for a suitable definition of “proof on hypotheses”, where A1, A2, …, An, B are well-formed expressions of S.

We describe which subdirectly irreducible flat algebras arise in the variety generated by an arbitrary class of flat algebras with absorbing bottom element. This is used to give an elementary translation of the universal Horn logic of algebras, partial algebras, and more generally still, partial structures into the equational logic of conventional algebras. A number of examples and corollaries follow. For example, the problem of deciding which finite algebras of some fixed type have a finite basis for their quasi-identities is shown to be equivalent to the finite identity basis problem for the finite members of a finiteiy based variety with definable principal congruences.

We study the relative complexity of equivalence relations and preorders from computability theory and complexity theory. Given binary relations R, S, a componentwise reducibility is defined by

R ≤ S ⇔ ∃f ∀x, y [x R y ↔ f (x) S f (y)].

Here, f is taken from a suitable class of effective functions. For us the relations will be on natural numbers, and f must be computable. We show that there is a ${\rm{\Pi }}_1^0$-complete equivalence relation, but no ${\rm{\Pi }}_k^0$-complete for k ≥ 2. We show that ${\rm{\Sigma }}_k^0$ preorders arising naturally in the above-mentioned areas are ${\rm{\Sigma }}_k^0$-complete. This includes polynomial time m-reducibility on exponential time sets, which is ${\rm{\Sigma }}_2^0$, almost inclusion on r.e. sets, which is ${\rm{\Sigma }}_3^0$, and Turing reducibility on r.e. sets, which is ${\rm{\Sigma }}_4^0$.

We call a logic regular for a semantics when the satisfaction predicate for at least one of its nontheorems is closed under double negation. Such intuitionistic theories as second-order Heyting arithmetic HAS and the intuitionistic set theory IZF prove completeness for no regular logics, no matter how simple or complicated. Any extensions of those theories proving completeness for regular logics are classical, i.e., they derive the tertium non datur. When an intuitionistic metatheory features anticlassical principles or recognizes that a logic regular for a semantics is nonclassical, it proves explicitly that the logic is incomplete with respect to that semantics. Logics regular relative to Tarski, Beth and Kripke semantics form a large collection that includes propositional and predicate intuitionistic, intermediate and classical logics. These results are corollaries of a single theorem. A variant of its proof yields a generalization of the Gödel-Kreisel Theorem linking weak completeness for intuitionistic predicate logic to Markov's Principle.

The axiomatization of algebras of functions or partial functions under various operations has been studied by several authors. Menger [2] deals with the problem of axiomatizing the algebraic properties of 1-ary functions from the reals to the reals. He considers algebras with one of three binary operations corresponding to addition, multiplication or composition. This study is furthered by Schweizer and Sklar in [3]–[6]. In addition to the operations mentioned above they also introduce a partial ordering which corresponds to restriction of functions. In the second of these papers they give a set of axioms such that any system satisfying these axioms is order isomorphic to a concrete system of partial functions under composition and ordered by restriction. In [7] Schweizer and Sklar extend their work to the algebra of multiplace vector-valued functions. In [8] Whitlock studies abstract multiplaced function systems given by super-associative laws and shows that these systems are isomorphically embeddable in a concrete system of multiplaced functions where the operation on the functions is substitution of an m-ary function in an n-ary function.

In this paper we consider the set of functions from Uα, the set of α-sequences, to U where a is an infinite ordinal. As opposed to the composition operations studied in the above works, we consider the composition operations *κ, for κ < α, in a narrow sense—the substitution of one function in the κth place of another. The algebras studied have the form ‹A, *κ, Vκ› κ<α where Vκ are the projection (selector) functions on the κth place. In particular, the polynomials over an algebra form such an algebra called a polynomial substitution algebra. In §6 we show that a first-order axiom system and a condition of local finiteness, given by Pinter in a talk at Berkeley in 1972 to characterize term substitution abgebras, also characterize these polynomial substitution algebras.

We formalise the notion of those infinite binary sequences z that admit a single program P which expresses the entire algorithmical structure of z. Such a program P minimizes the information which must be used in a relative computation for z. We propose two concepts with different strength for this notion, the learnable and the super-learnable sequences. We establish three different equivalent characterizations of learnable (super-learnable, resp.) sequences. In particular, we prove that a sequence z is learnable (super-learnable, resp.) if and only if there is a computable probability measure p such that p is Schnorr (Martin-Löf, resp.) p-random. There is a recursively enumerable sequence which is not learnable. The learnable sequences are invariant with respect to all total and effective transformations of infinite binary sequences.

A generic computation of a subset A of ℕ consists of a computation that correctly computes most of the bits of A, and never incorrectly computes any bits of A, but which does not necessarily give an answer for every input. The motivation for this concept comes from group theory and complexity theory, but the purely recursion theoretic analysis proves to be interesting, and often counterintuitive. The primary result of this paper is that there are no minimal pairs for generic computability, answering a question of Jockusch and Schupp.

Computability logic (CL) is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, “truth” means existence of an algorithmic solution, and proofs encode such solutions. Within the line of research devoted to finding axiomatizations for ever more expressive fragments of CL, the present paper introduces a new deductive system CL12 and proves its soundness and completeness with respect to the semantics of CL. Conservatively extending classical predicate calculus and offering considerable additional expressive and deductive power, CL12 presents a reasonable, computationally meaningful, constructive alternative to classical logic as a basis for applied theories. To obtain a model example of such theories, this paper rebuilds the traditional, classical-logicbased Peano arithmetic into a computability-logic-based counterpart. Among the purposes of the present contribution is to provide a starting point for what, as the author wishes to hope, might become a new line of research with a potential of interesting findings—an exploration of the presumably quite unusual metatheory of CL-based arithmetic and other CL-based applied systems.

The interpretation of the ZF set theory reported in this paper is, actually, part of a wider effort, namely, a new approach to the foundation of mathematics, which is referred to as The Cybernetic Foundation. A detailed exposition of the Cybernetic Foundation will be published elsewhere. Our approach leads to a full acceptance of the formalism of the classical set theory, but interprets it using only the idea of potential, but not actual (completed) infinity, and dealing only with finite objects that can actually be constructed. Thus we have a finitist proof of the consistency of ZF. This becomes possible because we set forth a metatheory of mathematics which goes beyond the classical logic and set theory and, of course, cannot be formalized in ZF, yet yields proofs which are as convincing—at least, from the author's viewpoint—as any mathematical proof can be.

Our metatheory is based on the following two ideas. Firstly, we define the semantics of the mathematical language using the cybernetical concept of knowledge. According to this concept, to say that a cybernetic system (a human being, in particular) has some knowledge is to say that it has some models of reality. In the Cybernetic Foundation we consider mathematics as the art of constructing linguistic models of reality.