Notions from classical general topology are developed in parallel in a constructive context and in interpretations in sheat models. These include the T0, T1, T2 separation principles, (complete) regularity, normality, compactness and connectedness. Intuitionistic continuity principles are also considered.
I give a class forcing that adds a real which is Pi-1-2 and for which no forcing extension (by a set of conditions) can destroy this definability.
We define recursive models of Martin-Löf's (type or) set theories. These models are a sort of recursive realizability; in fact, we show that for implication-free formulae of HAω, satisfaction in the model coincides with mr-HEO realizability. Using an idea of Aczel, we extend the model to a recursive model of the constructive set theories of Myhill and Friedman. Our models can be described without presupposing any knowledge of Martin-Löf's theories, and may make them seem less mysterious. We use our models to obtain several metamathematical results, for example consistency and independence results concerning continuity of functions on compact metric spaces. On the other hand, Martin-Löfs (latest) theories refute continuity of functions from NN to N, as well as Church's thesis, although a show that all provably well-defined functions are continuous.
Assuming the Continuum Hypothesis we interpret the theory of the cardinal 2ℵ 0 with quantification over the constructible monadic, dyadic, etc. predicates in the monadic (second-order) theory of the real line, in the monadic theory of any other short non-modest chain, in monadic topology of Cantor’s Discontinuum and some other monadic theories. We build monadic sentences defining the real line up to isomorphism under some set-theoretic assumptions. There are some other results.
Our main result is the decidability and ω-stability of free cth nilpotent p-groups of finite exponent (c < p).
The algebraic and recursive structure of countable languages of classical first-order logic with equality is analysed. All languages of finite undecidable similarity type are shown to be algebraically and recursively equivalent in the following sense: their Boolean algebras of formulas are, after trivial involving the one element models of the languages have been excepted, recursively isomorphic by a map which preserves the degree of recursiveness of their models.
In this paper extensions of HA are studied that prove their own completeness, i.e. they prove A → □ A, where □ is interpreted as provability in the theory itself. Motivation is three-fold: (1) these theories are thought to have some intrinsic interest, (2) they are a tool for producing and studying provability principles, (3) they can be used to proved independence results. Work done in the paper connected with these motivations is respectively: 1.(i) A characterization is given of theories proving their own completeness, including an appropriate conservation result.2.(ii) Some new provability principles are produced. The provability logic of HA is not a sublogic of the of PA. A provability logic plus completeness theorem is given for a certain intuitionistic extension of HA. De Jongh's theorem for propositional logic is a corollary.3.(iii) FP-realizability in Beeson's proof that ∦HA KLS is replaced by theories proving their own completeness. New consequences are ∦HA+−MPR KLS, ∦HA+DNS KLS.
If κ is measurable, Prikry's forcing adds a sequence of ordinals of order type ω cofinal in κ. This destroys the regularity of κ but κ does remain uncountable. Magidor has a forcing notion generalizing Prikry's which adds a closed cofinal sequence of ordinals through a large cardinal. The cardinal remains uncountable but uts regularity is still destroyed. We obtain a forcing notion which adds a closed cofinal sequence of ordinals (and more complex objects) through a large cardinal κ, of order type κ, and keeps κ regular. In fact κ remains measurable after the forcing.
The present paper studies the relation between admissibility, reflection and partition properties. After introducing basic notions in Section e, Σn admissible ordinals are characterized using reflection properties (Section 2). Σn partition relations are introduced in Section 3. In Sections 3 and 4 connections are explored between partition properties, admissibility and projecta. Several more characterizations of admissibility are given in Section 5 (using Σn trees) and Section 6 (using Σn compactness). The ideas developed in Section 5 are used in Section 7 to study the partition relation κ → σn (κ)2.
Let Robinson's consistency theorem hold in logic L: then L will satisfy all the usual interpolation and definability properties, together with coutable compactness, provided L is reasonably small. The latter assumption can be weakened ro removed by using special set-theoretical assumptions. Thus, if Robinson's consistency theorem holds in L, then (i) L is countably compact if its Löwenheim number is < μ0 = the smallest uncountable measurable cardinal; (ii) if ω is the only measurable cardinal, L is countably compact, or the theories of L characterize every structure up to isomorphism. As a corollary, a partial answer is given to H. Friedman's third problem, by proving that no logic L strictly between L∞ω and L∞∞ satisfies interpolation (or Robinson's consistency), unless K-elementary equivalence coincides with isomorphism.
A version of Harrington's DELTA3-automorphism technique for the lattice of recursively enumerable sets is introduced and developed by reproving Soare's Extension Theorem. Then this automorphism technique is used to show two technical theorems: the High Extension Theorem I and the High Extension Theorem II. These theorems and other technical theorems are used to show: for all high r.e. degrees h and for all r.e. sets A there is an r.e. set B in h such that these two sets have isomorphic principal filters of r.e. sets. In addition it is shown that for any nonrecursive r.e. set A, there is a high r.e. set B such that A and B are automorphic in the lattice of recursively enumerable sets (this was shown independently by Harrington and Soare). These techniques are also used to show that if A is a coinfinite r.e. set such that ABAR is semi-low2 and A has the outer splitting property then the principal filter formed by A is isomorphic to the lattice of r.e. sets.
