If ZFC is consistent, then the collection of countable computably saturated models of ZFC satisfies all of the Multiverse Axioms of Hamkins.

We investigate the notion of definability with respect to a full satisfaction class σ for a model M of Peano arithmetic. It is shown that the σ-definable subsets of M always include a class which provides a satisfaction definition for standard formulas. Such a class is necessarily proper, therefore there exist recursively saturated models with no full satisfaction classes. Nonstandard extensions of overspill and recursive saturation are utilized in developing a criterion for nonstandard definability. Finally, these techniques yield some information (...) concerning the extendibility of full satisfaction classes from one model to another. (shrink)

Dependence logic, introduced in Väänänen [11], cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized, and this is what we shall do in this paper. We give an explicit axiomatization and prove the respective Completeness Theorem.

We expand the notion of resplendency to theories of the kind T + p", where T is a fi rst-order theory and p" expresses that the type p is omitted. We investigate two di erent formulations and prove necessary and sucient conditions for countable recursively saturated models of PA. Some of the results in this paper can be found in one of the author's doctoral thesis [3].

Ajtai’s completeness theorem roughly states that a countable structure A coded in a model of arithmetic can be end-extended and expanded to a model of a given theory G if and only if a contradiction cannot be derived by a proof from G plus the diagram of A, provided that the proof is definable in A and contains only formulas of a standard length. The existence of such model extensions is closely related to questions in complexity theory. In this paper (...) we give a new proof of Ajtai’s theorem using basic techniques of model theory. (shrink)

§0. Introduction. In [16], Barwise described his graduate study at Stanford. He told of his interactions with Kreisel and Scott, and said how he chose Feferman as his advisor. He began working on admissible fragments of infinitary logic after reading and giving seminar talks on two Ph.D. theses which had recently been completed: that of Lopez-Escobar, at Berkeley, on infinitary logic [46], and that of Platek [58], at Stanford, on admissible sets.Barwise's work on infinitary logic and admissible sets is described (...) in his thesis [4], the book [13], and papers [5]—[16]. We do not try to give a systematic review of these papers. Instead, our goal is to give a coherent introduction to infinitary logic and admissible sets. We describe results of Barwise, of course, because he did so much. In addition, we mention some more recent work, to indicate the current importance of Barwise's ideas. Many of the central results are stated without proof, but occasionally we sketch a proof, to indicate how the ideas fit together.Chapters 1 and 2 describe infinitary logic and admissible sets at the time Barwise began his work, circa 1965. From Chapter 3 on, we survey the developments that took place after Barwise appeared on the scene.§1. Background on infinitary logic. In this chapter, we describe the situation in infinitary logic at the time that Barwise began his work. We need some terminology. By a vocabulary, we mean a set L of constant symbols, and relation and operation symbols with finitely many argument places. As usual, by an L-structureM, we mean a universe set M with an interpretation for each symbol of L. (shrink)

Mancosu, P., Generalizing classical and effective model theory in theories of operations and classes, Annas of Pure and Applied Logic 52 249-308 . In this paper I propose a family of theories of operations and classes with the aim of developing abstract versions of model-theoretic results. The systems are closely related to those introduced and already used by Feferman for developing his program of ‘explicit mathematics’. The theories in question are two-sorted, with one kind of variable for individuals and the (...) other for classes. The individual variables range over a domain closed under pairing and containing, among other things, natural numbers and operations.All the theories used assume a common group of axioms that insure that the individuals in the domain satisfy the conditions for a partial combinatory algebra with pairing. We also assume a class of natural numbers and a class induction axiom on . Finally there are various class existence axioms. I work mainly with three theories, FMT0, FMT and FMTΩ, which differ from each other both in their class existence axioms as well as in some further applicative axioms.These theories have various interpretations in which every object is explicitly presented by some means of definition as well as classical, or ‘standard’, set-theoretical interpretation. The systems are formulated in a flexible general language which can be used to prove abstract theorems of mathematics , thereby generalizing recursive, hyperarithmetic and admissible versions of classical mathematics.The aim of my work is to give an abstract development of portions of model theory in the afore-mentioned theories, in a way to look as much as possible like classical mathematics. Thus, FMT0 generalizes portions of countable and recursive model theory; FMT further generalizes portions of countable and hyperarithmetical model theory and finally FMTΩ provides a generalization of the classical L-completeness theorem and of an admissible version of L-completeness due to Bruce and Keisler. This continues the development of the program mentioned above, originating with Feferman. (shrink)

Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed‐point logic. Inclusion logic is not axiomatisable in full, but its first order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first order consequences in inclusion logic.

D’Aquino et al. (J Symb Log 75(1):1–11, 2010) have recently shown that every real-closed field with an integer part satisfying the arithmetic theory IΣ4 is recursively saturated, and that this theorem fails if IΣ4 is replaced by IΔ0. We prove that the theorem holds if IΣ4 is replaced by weak subtheories of Buss’ bounded arithmetic: PV or $${\Sigma^b_1-IND^{|x|_k}}$$. It also holds for IΔ0 (and even its subtheory IE 2) under a rather mild assumption on cofinality. On the other hand, it (...) fails for the extension of IOpen by an axiom expressing the Bézout property, even under the same assumption on cofinality. (shrink)

We give a valuation theoretic characterization for a real closed field to be recursively saturated. This builds on work in [9], where the authors gave such a characterization forκ-saturation, for a cardinal$\kappa \ge \aleph _0 $. Our result extends the characterization of Harnik and Ressayre [7] for a divisible ordered abelian group to be recursively saturated.

We prove that (additive) ordered group reducts of nonstandard models of the bounded arithmetical theory are recursively saturated in a rich language with predicates expressing the integers, rationals, and logarithmically bounded numbers. Combined with our previous results on the construction of the real exponential function on completions of models of, we show that every countable model of is an exponential integer part of a real‐closed exponential field.

In this note we study a counterpart in predicate logic of the notion of logical friendliness, introduced into propositional logic in [15]. The result is a new consequence relation for predicate languages with equality using first-order models. While compactness, interpolation and axiomatizability fail dramatically, several other properties are preserved from the propositional case. Divergence is diminished when the language does not contain equality with its standard interpretation.