We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics (i.e., which part is equiconsistent with $\textbf {PRA}$ or consistent provably in $\textbf {PRA}$ ) already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: (i) fan theorem for decidable fans but arbitrary bars; (ii) continuity principle and the axiom of choice both for arbitrary formulae; and (iii) $\Sigma _2$ induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO (except the choice along functions); but that limited principle of omniscience LPO makes the situation completely classical.

We introduce the framework of AECats (abstract elementary categories), generalizing both the category of models of some first-order theory and the category of subsets of models. Any AEC and any compact abstract theory (“cat”, as introduced by Ben-Yaacov) forms an AECat. In particular, we find applications in positive logic and continuous logic: the category of (subsets of) models of a positive or continuous theory is an AECat. The Kim–Pillay theorem for first-order logic characterizes simple theories by the properties dividing independence has. We prove a version of the Kim–Pillay theorem for AECats with the amalgamation property, generalizing the first-order version and existing versions for positive logic.

We construct a stable one-based, trivial theory with a reduct which is not trivial. This answers a question of John B. Goode. Using this, we construct a stable theory which is n-ample for all natural numbers n, and does not interpret an infinite group.

The initial event, in the series which led to the establishing of the Journal of Symbolic Logic and of the Association for Symbolic Logic, was a conversation early in 1934 between C. J. Ducasse and C. A. Baylis at Brown University in room 112, Rhode Island Hall. Ducasse, in the Graduate School at Harvard in 1911, had had work in Symbolic logic with Josiah Royce, and had become much impressed with the potential importance of the subject. Baylis, years before at the University of Washington, had been the outstanding student in the logic course Ducasse was conducting there, and eventually joined Ducasse on the staff of the Philosophy Department at Brown.

Elementary (first-order) and nonelementary (set-theoretic) aspects of the largest bisimulation are considered with a view toward analyzing operational semantics from the perspective of predicate logic. The notion of a bisimulation is employed in two distinct ways: (i) as an extensional notion of equivalence on programs (or processes) generalizing input/output equivalence (at a cost exceeding over certain transition predicates computable in log space), and (ii) as a tool for analyzing the dependence of transitions on data (which can be shown to be elementary or nonelementary, depending on the formulation of the transitions).

We show that under Dickson’s conjecture about the distribution of primes in the natural numbers, the theory Th (ℤ , +, 1, 0, Pr) where Pr is a predicate for the prime numbers and their negations is decidable, unstable, and supersimple. This is in contrast with Th (ℤ , +, 0, Pr, <) which is known to be undecidable by the works of Jockusch, Bateman, and Woods.

Assume ZF + AD + V = L(ℝ) and let κ < Θ be an uncountable cardinal. We show that κ is Jónsson, and that if cof (κ) = ω then κ is Rowbottom. We also establish some other partition properties.

We define a complete theory SHFe of separably closed fields of finite invariant e (=degree of imperfection) which carry an infinite stack of Hasse-derivations. We show that SHFe has quantifier elimination and eliminates imaginaries.

Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate way which still serves to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is $\Pi _2$ -conservative over intuitionistic arithmetic.

We use model-theoretic methods described in [3] to obtain ordinal analyses of a number of theories of first- and second-order arithmetic, whose proof-theoretic ordinals are less than or equal to Γ0.

In 2001, the algebraico-tree-theoretic simplicity hierarchical structure of J. H. Conway’s ordered field ${\mathbf {No}}$ of surreal numbers was brought to the fore by the first author and employed to provide necessary and sufficient conditions for an ordered field (ordered $K$ -vector space) to be isomorphic to an initial subfield ( $K$ -subspace) of ${\mathbf {No}}$ , i.e. a subfield ( $K$ -subspace) of ${\mathbf {No}}$ that is an initial subtree of ${\mathbf {No}}$ . In this sequel, analogous results are established for ordered exponential fields, making use of a slight generalization of Schmeling’s conception of a transseries field. It is further shown that a wide range of ordered exponential fields are isomorphic to initial exponential subfields of $({\mathbf {No}}, \exp )$ . These include all models of $T({\mathbb R}_W, e^x)$ , where ${\mathbb R}_W$ is the reals expanded by a convergent Weierstrass system W. Of these, those we call trigonometric-exponential fields are given particular attention. It is shown that the exponential functions on the initial trigonometric-exponential subfields of ${\mathbf {No}}$ , which includes ${\mathbf {No}}$ itself, extend to canonical exponential functions on their surcomplex counterparts. The image of the canonical map of the ordered exponential field ${\mathbb T}^{LE}$ of logarithmic-exponential transseries into ${\mathbf {No}}$ is shown to be initial, as are the ordered exponential fields ${\mathbb R}((\omega ))^{EL}$ and ${\mathbb R}\langle \langle \omega \rangle \rangle $ .

In this note we show:

Theorem 1.1. Let G be a Polish group and X a Polish G-space with the induced orbit equivalence relation EG Borel as a subset of X × X. Then exactly one of the following:

(I) There is a countable languageℒand a Borel function

such that for all x1, x2 ∈ X

or

(II) there is a turbulent Polish G-space Y and a continuous G-embedding

There are various bows and ribbons which can be woven into these statements. We can strengthen (I) by asking that θ also admit a Borel orbit inverse, that is to say some Borel function

for some Borel set B ⊂ Mod(ℒ), such that for all x ∈ X

and then after having passed to this strengthened version of (I) we still obtain the exact same dichotomy theorem, and hence the conclusion that the two competing versions of (I) are equivalent. Similarly (II) can be relaxed to just asking that τ be a Borel G-embedding, or even simply a Borel reduction of the relevant orbit equivalence relations. It is in fact a consequence of 1.1 that all the plausible weakenings and strengthenings of (I) and (II) are respectively equivalent to one another.

I will not closely examine these possible variations here. The equivalences alluded to above follow from our main theorem and the results of [3]. That monograph had previously shown that (I) and (II) are incompatible, and proved a barbaric forerunner of 1.1, and gone on to conjecture the dichotomy result above.

The canonicity and compactness of the KM system are problems historically important in the development of our understanding of intensional logic (as explained in Goldblatt's paper, The McKinsey axiom is not canonical). The problems, however, were unsolved for years in modal logic. In the beginning of 1990, Goldblatt showed that KM is not canonical in The McKinsey axiom is not canonical. The remaining task is to solve the problem of the compactness of KM. In this paper we present a proof showing that the KM system is not compact.

The symbols of the language of propositional modal logic are as follows:

1. A denumerably infinite set of sentence letters, for example, {p0, P1, p2, …};

2. The Boolean connectives &, ⋁, ¬, →, ↔ and parentheses;

3. The modal operators L and M where M is defined as ¬L¬.

The formation rules of well-formed propositional modal formulae are the formation rules of formulae in classic propositional logic plus the following rule:

If A is a well-formed formula, so is LA.

A normal modal system is a set of formulae that contains all tautologies and the formula

and is closed under the following transformation rules:

Uniform substitution. If A is a theorem, so is every substitution-instance of A.

Modus ponens. If A and A → B are theorems, so is B.

Necessitation. If A is a theorem, so is LA.

Let L be a normal system. Then a set S of formulae is L-consistent if and only if for any formula B, which is the conjunction of some formulae in S, B is not included in L. A set S of formulae is maximal if and only if for every formula A, S either contains A or contains ¬A. A set S of formulae is maximal L-consistent if and only if it is both maximal and L-consistent.

We investigate small theories of Boolean ordered o-minimal structures. We prove that such theories are ℵ0-categorical. We give a complete characterization of their models up to bi-interpretability of the language. We investigate types over finite sets, formulas and the notions of definable and algebraic closure.

An arithmetical interpretation of dynamic propositional logic (DPL) is a mapping ƒ satisfying the following: (1) ƒ associates with each formula A of DPL a sentence ƒ(A) of Peano arithmetic (PA) and with each program α a formula ƒ(α) of PA with one free variable describing formally a supertheory of PA; (2) ƒ commutes with logical connectives; (3) ƒ([α]A) is the sentence saying that ƒ(A) is provable in the theory ƒ(α); (4) for each axiom A of DPL, ƒ(A) is provable in PA (and consequently, for each A provable in DPL, ƒ(A) is provable in PA). The arithmetical completeness theorem is proved saying that a formula A of DPL is provable in DPL iff for each arithmetical interpretation ƒ, ƒ(A) is provable in PA. Various modifications of this result are considered.

In recent years higher recursion theory has experienced a deep interaction with other areas of logic, particularly set theory (fine structure, forcing, and combinatorics) and infinitary model theory. In this paper we wish to illustrate this interaction by surveying the progress that has been made in two areas: the global theory of the κ-degrees and the study of closure ordinals.

A large number of formal systems based on combinatory logic or λ-calculus have been extended to include first order predicate calculus. Several of these however have been shown to be inconsistent, all, as far as the author knows, in the strong sense that all well formed formulas (which here include all strings of symbols) are provable. We will call the corresponding consistency notion—an arbitrary wff ⊥ is provable—weak consistency. We will say that a system is strongly consistent if no formula and its negation are provable.

Now for some systems, such as that of Kuzichev [11], the strong and weak consistency notions are equivalent, but in the systems of [5] and [6], which we will be considering, they are not. Each of these systems is strong enough to have all of ZF set theory, except Grounding and Choice, interpretable in it, and the system of [5] can also encompass first order arithmetic (see [7]). It therefore seems unlikely that a strong consistency result could be proved for these systems using elementary methods. In this paper however, we prove the weak consistency of both these systems by means that could be formulated, at least within the theory of [5]. The method also applies to the typed systems of Curry, Hindley and Seldin [10] and to Seldin's generalised types [12].

Nous considérons des théories d'anneaux locaux reliées aux corps p-adiques, p un nombre premier. Dans le §1 nous établissons les axiomatisations données dans [B1], ainsi qu'une autre axiomatisation des anneaux apparaissant dans [R1]. Il s'agit d'anneaux locaux henséliens dont le corps résiduel est élémentairement équivalent à une extension finie d'un corps p-adique. Nous les appelons anneaux locaux p-adiquement clos. Dans le contexte de [R1] et [B1] ils apparaissent comme fibres du faisceau structural (aussi appelé faisceau de Nash dans [BS]) accompagnant les spectres p-adiques. L'intérêt de nos axiomatisations provient de la simplicité des axiomes qui rendent compte des propriétés henséliennes. Dans le §2 nous donnons une axiomatisation d'une théorie d'anneaux locaux qui apparaît naturellement dans le contexte de la théorie des modèles des corps valués, et se trouve être une complétion d'une théorie du §1. Nous appelons ces anneaux, anneaux intègres p-adiquement clos.

Dans le §3 nous utilisons §2 pour montrer que les anneaux intègres p-adiquement clos apparaissent aussi comme anneaux quotients d'anneaux de fonctions continues définissables sur les courbes affines p-adiques. Nous représentons alors un idéal premier comme le noyau d'un morphisme d'évaluation en un point non-standard de la courbe. Le spectre p-adique fournit un outil commode qui permet de décrire la situation de façon concise.