Authors:Rob Egrot Pages: 235 - 242 Abstract: Publication date: March 2018 Source:Annals of Pure and Applied Logic, Volume 169, Issue 3 Author(s): Rob Egrot Let m and n be cardinals with 3 ≤ m , n ≤ ω . We show that the class of posets that can be embedded into a distributive lattice via a map preserving all existing meets and joins with cardinalities strictly less than m and n respectively cannot be finitely axiomatized.

Authors:Uri Andrews; Andrea Sorbi Pages: 243 - 259 Abstract: Publication date: March 2018 Source:Annals of Pure and Applied Logic, Volume 169, Issue 3 Author(s): Uri Andrews, Andrea Sorbi We study computably enumerable equivalence relations (or, ceers), under computable reducibility ≤, and the halting jump operation on ceers. We show that every jump is uniform join-irreducible, and thus join-irreducible. Therefore, the uniform join of two incomparable ceers is not equivalent to any jump. On the other hand there exist ceers that are not equivalent to jumps, but are uniform join-irreducible: in fact above any non-universal ceer there is a ceer which is not equivalent to a jump, and is uniform join-irreducible. We also study transfinite iterations of the jump operation. If a is an ordinal notation, and E is a ceer, then let E ( a ) denote the ceer obtained by transfinitely iterating the jump on E along the path of ordinal notations up to a. In contrast with what happens for the Turing jump and Turing reducibility, where if a set X is an upper bound for the A-arithmetical sets then X ( 2 ) computes A ( ω ) , we show that there is a ceer R such that R ≥ Id ( n ) , for every finite ordinal n, but, for all k, R ( k ) ≱ Id ( ω ) (here Id is the identity equivalence relation). We show that if a , b are notations of the same ordinal less than ω 2 , then E ( a ) ≡ E ( b ) , but there are notations a , b of ω 2 such that Id ( a ) and Id ( b ) are incomparable. Moreover, there is no non-universal ceer which is an upper bound for all the ceers of the form Id ( a ) where a is a notation for ω 2 .

Authors:Yurii Khomskii; Giorgio Laguzzi Pages: 1491 - 1506 Abstract: Publication date: August 2017 Source:Annals of Pure and Applied Logic, Volume 168, Issue 8 Author(s): Yurii Khomskii, Giorgio Laguzzi We investigate two closely related partial orders of trees on ω ω : the full-splitting Miller trees and the infinitely often equal trees, as well as their corresponding σ-ideals. The former notion was considered by Newelski and Rosłanowski while the latter involves a correction of a result of Spinas. We consider some Marczewski-style regularity properties based on these trees, which turn out to be closely related to the property of Baire, and look at the dichotomies of Newelski–Rosłanowski and Spinas for higher projective pointclasses. We also provide some insight concerning a question of Fremlin whether one can add an infinitely often equal real without adding a Cohen real, which was recently solved by Zapletal.

Authors:Sonia L'Innocente; Carlo Toffalori; Gena Puninski Pages: 1507 - 1516 Abstract: Publication date: August 2017 Source:Annals of Pure and Applied Logic, Volume 168, Issue 8 Author(s): Sonia L'Innocente, Carlo Toffalori, Gena Puninski We will prove that the theory of all modules over the ring of algebraic integers is decidable.

Authors:Anton Freund Pages: 1361 - 1382 Abstract: Publication date: July 2017 Source:Annals of Pure and Applied Logic, Volume 168, Issue 7 Author(s): Anton Freund As Paris and Harrington have famously shown, Peano Arithmetic does not prove that for all numbers k , m , n there is an N which satisfies the statement PH ( k , m , n , N ) : For any k-coloring of its n-element subsets the set { 0 , … , N − 1 } has a large homogeneous subset of size ≥m. At the same time very weak theories can establish the Σ 1 -statement ∃ N PH ( k ‾ , m ‾ , n ‾ , N ) for any fixed parameters k , m , n . Which theory, then, does it take to formalize natural proofs of these instances? It is known that ∀ m ∃ N PH ( k ‾ , m , n ‾ , N ) has a natural and short proof (relative to n and k) by Σ n − 1 -induction. In contrast, we show that there is an elementary function e such that any proof of ∃ N PH ( e ( n ) ‾ , n + 1 ‾ , n ‾ , N ) by Σ n − 2 -induction is ridiculously long. In order to establish this result on proof lengths we give a computational analysis of slow provability, a notion introduced by Sy-David Friedman, Rathjen and Weiermann. We will see that slow uniform Σ 1 -reflection is related to a function that has a considerably lower growth rate than F ε 0 but dominates all functions F α with α < ε 0 in the fast-growing hierarchy.

Authors:Matthew Harrison-Trainor Pages: 1396 - 1405 Abstract: Publication date: July 2017 Source:Annals of Pure and Applied Logic, Volume 168, Issue 7 Author(s): Matthew Harrison-Trainor A set A is coarsely computable with density r ∈ [ 0 , 1 ] if there is an algorithm for deciding membership in A which always gives a (possibly incorrect) answer, and which gives a correct answer with density at least r. To any Turing degree a we can assign a value Γ T ( a ) : the minimum, over all sets A in a, of the highest density at which A is coarsely computable. The closer Γ T ( a ) is to 1, the closer a is to being computable. Andrews, Cai, Diamondstone, Jockusch, and Lempp noted that Γ T can take on the values 0, 1/2, and 1, but not any values in strictly between 1/2 and 1. They asked whether the value of Γ T can be strictly between 0 and 1/2. This is the Gamma question. Replacing Turing degrees by many-one degrees, we get an analogous question, and the same arguments show that Γ m can take on the values 0, 1/2, and 1, but not any values strictly between 1/2 and 1. We will show that for any r ∈ [ 0 , 1 / 2 ] , there is an m-degree a with Γ m ( a ) = r . Thus the range of Γ m is [ 0 , 1 / 2 ] ∪ { 1 } . Benoit Monin has recently announced a solution to the Gamma question for Turing degrees. Interestingly, his solution gives the opposite answer: the only possible values of Γ T are 0, 1/2, and 1.

Authors:Fan Yang; Jouko Väänänen Pages: 1406 - 1441 Abstract: Publication date: July 2017 Source:Annals of Pure and Applied Logic, Volume 168, Issue 7 Author(s): Fan Yang, Jouko Väänänen We consider team semantics for propositional logic, continuing [34]. In team semantics the truth of a propositional formula is considered in a set of valuations, called a team, rather than in an individual valuation. This offers the possibility to give meaning to concepts such as dependence, independence and inclusion. We associate with every formula ϕ based on finitely many propositional variables the set 〚 ϕ 〛 of teams that satisfy ϕ. We define a maximal propositional team logic in which every set of teams is definable as 〚 ϕ 〛 for suitable ϕ. This requires going beyond the logical operations of classical propositional logic. We exhibit a hierarchy of logics between the smallest, viz. classical propositional logic, and the maximal propositional team logic. We characterize these different logics in several ways: first syntactically by their logical operations, and then semantically by the kind of sets of teams they are capable of defining. In several important cases we are able to find complete axiomatizations for these logics.

Authors:Nick Bezhanishvili; Vincenzo Marra; Daniel McNeill; Andrea Pedrini Abstract: Publication date: Available online 17 December 2017 Source:Annals of Pure and Applied Logic Author(s): Nick Bezhanishvili, Vincenzo Marra, Daniel McNeill, Andrea Pedrini In 1938, Tarski proved that a formula is not intuitionistically valid if, and only if, it has a counter-model in the Heyting algebra of open sets of some topological space. In fact, Tarski showed that any Euclidean space R n with n ⩾ 1 suffices, as does e.g. the Cantor space. In particular, intuitionistic logic cannot detect topological dimension in the Heyting algebra of all open sets of a Euclidean space. By contrast, we consider the lattice of open subpolyhedra of a given compact polyhedron P ⊆ R n , prove that it is a locally finite Heyting subalgebra of the (non-locally-finite) algebra of all open sets of P, and show that intuitionistic logic is able to capture the topological dimension of P through the bounded-depth axiom schemata. Further, we show that intuitionistic logic is precisely the logic of formulæ valid in all Heyting algebras arising from polyhedra in this manner. Thus, our main theorem reconciles through polyhedral geometry two classical results: topological completeness in the style of Tarski, and Jaśkowski's theorem that intuitionistic logic enjoys the finite model property. Several questions of interest remain open. E.g., what is the intermediate logic of all closed triangulable manifolds'

Authors:David Fernández-Duque; Joost J. Joosten Abstract: Publication date: Available online 14 December 2017 Source:Annals of Pure and Applied Logic Author(s): David Fernández-Duque, Joost J. Joosten Given a computable ordinal Λ, the transfinite provability logic GLP Λ has for each ξ < Λ a modality [ ξ ] intended to represent a provability predicate within a chain of increasing strength. One possibility is to read [ ξ ] ϕ as ϕ is provable in T using ω-rules of depth at most ξ, where T is a second-order theory extending ACA 0 . In this paper we will formalize such iterations of ω-rules in second-order arithmetic and show how it is a special case of what we call uniform provability predicates. Uniform provability predicates are similar to Ignatiev's strong provability predicates except that they can be iterated transfinitely. Finally, we show that GLP Λ is sound and complete for any uniform provability predicate.

Authors:Merlin Carl; Philipp Schlicht; Philip Welch Abstract: Publication date: Available online 13 December 2017 Source:Annals of Pure and Applied Logic Author(s): Merlin Carl, Philipp Schlicht, Philip Welch We call a subset of an ordinal λ recognizable if it is the unique subset x of λ for which some Turing machine with ordinal time and tape and an ordinal parameter, that halts for all subsets of λ as input, halts with the final state 0. Equivalently, such a set is the unique subset x which satisfies a given Σ 1 formula in L [ x ] . We further define the recognizable closure for subsets of λ by closing under relative recognizability for subsets of λ. We prove several results about recognizable sets and their variants for other types of machines. Notably, we show the following results from large cardinals. • Recognizable sets of ordinals appear in the hierarchy of inner models at least up to the level Woodin cardinals, while computable sets are elements of L. • A subset of a countable ordinal λ is in the recognizable closure for subsets of λ if and only if it is an element of the inner model M ∞ , which is obtained by iterating the least measure of the least fine structural inner model M 1 with a Woodin cardinal through the ordinals.

Authors:Bruno Dinis; Jaime Gaspar Abstract: Publication date: Available online 12 December 2017 Source:Annals of Pure and Applied Logic Author(s): Bruno Dinis, Jaime Gaspar We present a bounded modified realisability and a bounded functional interpretation of intuitionistic nonstandard arithmetic with nonstandard principles. The functional interpretation is the intuitionistic counterpart of Ferreira and Gaspar's functional interpretation and has similarities with Van den Berg, Briseid and Safarik's functional interpretation but replacing finiteness by majorisability. We give a threefold contribution: constructive content and proof-theoretical properties of nonstandard arithmetic; filling a gap in the literature; being in line with nonstandard methods to analyse compactness arguments.

Authors:Logan Axon Abstract: Publication date: Available online 8 December 2017 Source:Annals of Pure and Applied Logic Author(s): Logan Axon Martin-Löf randomness was originally defined and studied in the context of the Cantor space 2 ω . In [1] probability theoretic random closed sets (RACS) are used as the foundation for the study of Martin-Löf randomness in spaces of closed sets. We use that framework to explore Martin-Löf randomness for the space of closed subsets of R and a particular family of measures on this space, the generalized Poisson processes. This gives a novel class of Martin-Löf random closed subsets of R . We describe some of the properties of these Martin-Löf random closed sets; one result establishes that a real number is Martin-Löf random if and only if it is contained in some Martin-Löf random closed set.

Authors:Antonio Di Nola; Serafina Lapenta; Ioana Leuştean Abstract: Publication date: Available online 31 October 2017 Source:Annals of Pure and Applied Logic Author(s): Antonio Di Nola, Serafina Lapenta, Ioana Leuştean We study Łukasiewicz logic enriched by a scalar multiplication with scalars in [ 0 , 1 ] . Its algebraic models, called Riesz MV-algebras, are, up to isomorphism, unit intervals of Riesz spaces with strong unit endowed with an appropriate structure. When only rational scalars are considered, one gets the class of DMV-algebras and a corresponding logical system. Our research follows two objectives. The first one is to deepen the connections between functional analysis and the logic of Riesz MV-algebras. The second one is to study the finitely presented MV-algebras, DMV-algebras and Riesz MV-algebras, connecting them from logical, algebraic and geometric perspective.

Authors:Raine Abstract: Publication date: Available online 20 October 2017 Source:Annals of Pure and Applied Logic Author(s): Raine Rönnholm In this paper we analyze k-ary inclusion–exclusion logic, INEX[k], which is obtained by extending first order logic with k-ary inclusion and exclusion atoms. We show that every formula of INEX[k] can be expressed with a formula of k-ary existential second order logic, ESO[k]. Conversely, every formula of ESO[k] with at most k-ary free relation variables can be expressed with a formula of INEX[k]. From this it follows that, on the level of sentences, INEX[k] captures the expressive power of ESO[k]. We also introduce several useful operators that can be expressed in INEX[k]. In particular, we define inclusion and exclusion quantifiers and so-called term value preserving disjunction which is essential for the proofs of the main results in this paper. Furthermore, we present a novel method of relativization for team semantics and analyze the duality of inclusion and exclusion atoms.

Authors:Chris Le Sueur Abstract: Publication date: Available online 17 October 2017 Source:Annals of Pure and Applied Logic Author(s): Chris Le Sueur In this paper we develop a technique for proving determinacy of classes of the form ω 2 - Π 1 1 + Γ (a refinement of the difference hierarchy on Π 1 1 lying between ω 2 - Π 1 1 and ( ω 2 + 1 ) - Π 1 1 ) from weak principles, establishing upper bounds for the determinacy-strength of the classes ω 2 - Π 1 1 + Σ α 0 for all computable α and of ω 2 - Π 1 1 + Δ 1 1 . This bridges the gap between previously known hypotheses implying determinacy in this region.

Authors:Tapani Hyttinen; Gianluca Paolini Abstract: Publication date: Available online 17 October 2017 Source:Annals of Pure and Applied Logic Author(s): Tapani Hyttinen, Gianluca Paolini Based on Crapo's theory of one point extensions of combinatorial geometries, we find various classes of geometric lattices that behave very well from the point of view of stability theory. One of them, ( K 3 , ≼ ) , is ω-stable, it has a monster model and an independence calculus that satisfies all the usual properties of non-forking. On the other hand, these classes are rather unusual, e.g. in ( K 3 , ≼ ) the Smoothness Axiom fails, and so ( K 3 , ≼ ) is not an AEC.

Authors:Mohammad Golshani; Rahman Mohammadpour Abstract: Publication date: Available online 14 October 2017 Source:Annals of Pure and Applied Logic Author(s): Mohammad Golshani, Rahman Mohammadpour Assuming the existence of a strong cardinal κ and a measurable cardinal above it, we force a generic extension in which κ is a singular strong limit cardinal of any given cofinality, and such that the tree property holds at κ + + .

Authors:Philipp Hieronymi; Travis Nell; Erik Walsberg Abstract: Publication date: Available online 13 October 2017 Source:Annals of Pure and Applied Logic Author(s): Philipp Hieronymi, Travis Nell, Erik Walsberg Let T be a consistent o-minimal theory extending the theory of densely ordered groups and let T ′ be a consistent theory. Then there is a complete theory T ⁎ extending T such that T is an open core of T ⁎ , but every model of T ⁎ interprets a model of T ′ . If T ′ is NIP, T ⁎ can be chosen to be NIP as well. From this we deduce the existence of an NIP expansion of the real field that has no distal expansion.

Authors:Gunnar Wilken Abstract: Publication date: Available online 21 September 2017 Source:Annals of Pure and Applied Logic Author(s): Gunnar Wilken We provide mutual elementary recursive order isomorphisms between classical ordinal notations, based on Skolem hulling, and notations from pure elementary patterns of resemblance of order 2, showing that the latter characterize the proof-theoretic ordinal 1 ∞ of the fragment Π 1 1 – CA 0 of second order number theory, or equivalently the set theory KP ℓ 0 . As a corollary, we prove that Carlson's result on the well-quasi orderedness of respecting forests of order 2 implies transfinite induction up to the ordinal 1 ∞ . We expect that our approach will facilitate analysis of more powerful systems of patterns.

Authors:S. Barry Cooper; Leo Harrington; Alistair H. Lachlan; Steffen Lempp; Robert I. Soare Abstract: Publication date: Available online 31 July 2017 Source:Annals of Pure and Applied Logic Author(s): S. Barry Cooper, Leo Harrington, Alistair H. Lachlan, Steffen Lempp, Robert I. Soare We indicate how to fix an error in the proof of the main theorem of our original paper, pointed out to us by Yong Liu and Keng Meng Ng.

Authors:Ivan Abstract: Publication date: Available online 26 July 2017 Source:Annals of Pure and Applied Logic Author(s): Ivan Tomašić The theory ACFA admits a primitive recursive quantifier elimination procedure. It is therefore primitive recursively decidable.

Authors:Tommaso Moraschini Abstract: Publication date: Available online 26 July 2017 Source:Annals of Pure and Applied Logic Author(s): Tommaso Moraschini In this paper we consider, from a computational point of view, the problem of classifying logics within the Leibniz and Frege hierarchies typical of abstract algebraic logic. The main result states that, for logics presented syntactically, this problem is in general undecidable. More precisely, we show that there is no algorithm that classifies the logic of a finite consistent Hilbert calculus in the Leibniz and in the Frege hierarchies.

Authors:Jan Dobrowolski; Byunghan Kim; Junguk Lee Abstract: Publication date: Available online 4 July 2017 Source:Annals of Pure and Applied Logic Author(s): Jan Dobrowolski, Byunghan Kim, Junguk Lee Let p be a strong type of an algebraically closed tuple over B = acl eq ( B ) in any theory T. Depending on a ternary relation Image 1 satisfying some basic axioms (there is at least one such, namely the trivial independence in T), the first homology group H 1 ⁎ ( p ) can be introduced, similarly to [3]. We show that there is a canonical surjective homomorphism from the Lascar group over B to H 1 ⁎ ( p ) . We also notice that the map factors naturally via a surjection from the ‘relativised’ Lascar group of the type (which we define in analogy with the Lascar group of the theory) onto the homology group, and we give an explicit description of its kernel. Due to this characterization, it follows that the first homology group of p is independent from the choice of Image 1 , and can be written simply as H 1 ( p ) . As consequences, in any T, we show that H 1 ( p ) ≥ 2 ℵ 0 unless H 1 ( p ) is trivial, and we give a criterion for the equality of stp and Lstp of algebraically closed tuples using the notions of the first homology group and a relativised Lascar group. We also argue how any abelian connected compact group can appear as the first homology group of the type of a model.

Authors:Enrique Casanovas; Luis Jaime Corredor Abstract: Publication date: Available online 30 June 2017 Source:Annals of Pure and Applied Logic Author(s): Enrique Casanovas, Luis Jaime Corredor Let M be the monster model of a complete first-order theory T. If D is a subset of M , following D. Zambella we consider e ( D ) = { D ′ ( M , D ) ≡ ( M , D ′ ) } and o ( D ) = { D ′ ( M , D ) ≅ ( M , D ′ ) } . The general question we ask is when e ( D ) = o ( D ) ' The case where D is A-invariant for some small set A is rather straightforward: it just means that D is definable. We investigate the case where D is not invariant over any small subset. If T is geometric and ( M , D ) is an H-structure (in the sense of A. Berenstein and E. Vassiliev) we get some answers. In the case of SU-rank one, e ( D ) is always different from o ( D ) . In the o-minimal case, everything can happen, depending on the complexity of the definable closure. We also study the case of lovely pairs of geometric theories.

Authors:L.B. Ostrovsky; M.E. Zhukovskii Abstract: Publication date: Available online 21 June 2017 Source:Annals of Pure and Applied Logic Author(s): L.B. Ostrovsky, M.E. Zhukovskii We study asymptotical probabilities of first order and monadic second order properties of Bernoulli random graph G ( n , n − a ) . The random graph obeys FO (MSO) zero-one k-law (k is a positive integer) if, for any first order (monadic second order) formulae with quantifier depth at most k, it is true for G ( n , n − a ) with probability tending to 0 or to 1. Zero-one k-laws are well studied only for the first order language and a < 1 . We obtain new zero-one k-laws (both for first order and monadic second order languages) when a > 1 . Proofs of these results are based on the earlier studies of first order equivalence classes and our study of monadic second order equivalence classes. The respective results are of interest by themselves.

Authors:Anton Freund Abstract: Publication date: Available online 20 June 2017 Source:Annals of Pure and Applied Logic Author(s): Anton Freund We describe a “slow” version of the hierarchy of uniform reflection principles over Peano Arithmetic (PA). These principles are unprovable in Peano Arithmetic (even when extended by usual reflection principles of lower complexity) and introduce a new provably total function. At the same time the consistency of PA plus slow reflection is provable in PA + Con ( PA ) . We deduce a conjecture of S.-D. Friedman, Rathjen and Weiermann: Transfinite iterations of slow consistency generate a hierarchy of precisely ε 0 stages between PA and PA + Con ( PA ) (where Con ( PA ) refers to the usual consistency statement).

Authors:Saskia Chambille; Pablo Cubides Kovacsics; Eva Leenknegt Abstract: Publication date: Available online 9 June 2017 Source:Annals of Pure and Applied Logic Author(s): Saskia Chambille, Pablo Cubides Kovacsics, Eva Leenknegt We prove that in a P-minimal structure, every definable set can be partitioned as a finite union of classical cells and regular clustered cells. This is a generalization of previously known cell decomposition results by Denef and Mourgues, which were dependent on the existence of definable Skolem functions. Clustered cells have the same geometric structure as classical, Denef-type cells, but do not have a definable function as center. Instead, the center is given by a definable set whose fibers are finite unions of balls.

Authors:Ari Meir Brodsky; Assaf Rinot Abstract: Publication date: Available online 8 June 2017 Source:Annals of Pure and Applied Logic Author(s): Ari Meir Brodsky, Assaf Rinot We propose a parameterized proxy principle from which κ-Souslin trees with various additional features can be constructed, regardless of the identity of κ. We then introduce the microscopic approach, which is a simple method for deriving trees from instances of the proxy principle. As a demonstration, we give a construction of a coherent κ-Souslin tree that applies also for κ inaccessible. We then carry out a systematic study of the consistency of instances of the proxy principle, distinguished by the vector of parameters serving as its input. Among other things, it will be shown that all known ⋄-based constructions of κ-Souslin trees may be redirected through this new proxy principle.

Abstract: Publication date: Available online 7 June 2017 Source:Annals of Pure and Applied Logic Author(s): M. Hrušák, D. Meza-Alcántara, E. Thümmel, C. Uzcátegui We study several combinatorial properties of (mostly definable) ideals on countable sets. In several cases, we identify critical ideals for such properties in the Katětov order. In particular, the ideal R generated by the homogeneous subsets of the random graph is critical for the Ramsey property. The question as to whether there is a tall definable Ramsey ideal is raised and studied. It is shown that no tall F σ ideal is Ramsey, while there is a tall co-analytic Ramsey ideal.

Authors:Panagiotis Rouvelas Abstract: Publication date: Available online 26 May 2017 Source:Annals of Pure and Applied Logic Author(s): Panagiotis Rouvelas We introduce the notion of pseudo-increasing sentence, and prove that all such sentences are decidable by a weak subtheory of Simple Type Theory with infinitely many zero-type elements. We then present the consequences of this result to Quine's theory of “New Foundations” (NF). In particular, we prove the decidability of certain universal-existential sentences, and establish the consistency of a subtheory of NF.

Authors:Samuel van; Gool George Metcalfe Constantine Tsinakis Abstract: Publication date: Available online 26 May 2017 Source:Annals of Pure and Applied Logic Author(s): Samuel J. van Gool, George Metcalfe, Constantine Tsinakis Uniform interpolation properties are defined for equational consequence in a variety of algebras and related to properties of compact congruences on first the free and then the finitely presented algebras of the variety. It is also shown, following related results of Ghilardi and Zawadowski, that a combination of these properties provides a sufficient condition for the first-order theory of the variety to admit a model completion.

Authors:Jacob Davis Abstract: Publication date: Available online 3 May 2017 Source:Annals of Pure and Applied Logic Author(s): Jacob Davis Starting from a supercompact cardinal we build a model in which 2 ℵ ω 1 = 2 ℵ ω 1 + 1 = ℵ ω 1 + 3 but there is a jointly universal family of size ℵ ω 1 + 2 of graphs on ℵ ω 1 + 1 . The same technique will work for any uncountable cardinal in place of ω 1 .

Authors:Vasco Brattka; Andrea Cettolo; Guido Gherardi; Alberto Marcone; Matthias Schröder Abstract: Publication date: Available online 29 April 2017 Source:Annals of Pure and Applied Logic Author(s): Vasco Brattka, Andrea Cettolo, Guido Gherardi, Alberto Marcone, Matthias Schröder The purpose of this addendum is to close a gap in the proof of [1, Theorem 11.2], which characterizes the computational content of the Bolzano–Weierstraß Theorem for arbitrary computable metric spaces.

Authors:Samaria Montenegro Abstract: Publication date: Available online 21 April 2017 Source:Annals of Pure and Applied Logic Author(s): Samaria Montenegro The main result of this paper is that if M is a bounded PRC field, then T h ( M ) eliminates imaginaries in the language of rings expanded by constant symbols. As corollary of the elimination of imaginaries and the fact that the algebraic closure (in the sense of model theory) defines a pregeometry we obtain that the complete theory of a bounded PRC field is superrosy of U th -rank 1.

Authors:Kaisa Kangas Abstract: Publication date: Available online 6 April 2017 Source:Annals of Pure and Applied Logic Author(s): Kaisa Kangas We show that if M is a Zariski-like structure (see [6]) and the canonical pregeometry obtained from the bounded closure operator (bcl) is non locally modular, then M interprets either an algebraically closed field or a non-classical group.

Authors:David Cerna; Alexander Leitsch; Giselle Reis; Simon Wolfsteiner Abstract: Publication date: Available online 5 April 2017 Source:Annals of Pure and Applied Logic Author(s): David Cerna, Alexander Leitsch, Giselle Reis, Simon Wolfsteiner In this paper we present a procedure allowing the extension of a CERES-based cut-elimination method to intuitionistic logic. Previous results concerning this problem manage to capture fragments of intuitionistic logic, but in many essential cases structural constraints were violated during normal form construction resulting in a classical proof. The heart of the CERES method is the resolution calculus, which ignores the structural constraints of the well known intuitionistic sequent calculi. We propose, as a method of avoiding the structural violations, the generalization of resolution from the resolving of clauses to the resolving of cut-free proofs, in other words, what we call proof resolution. The result of proof resolution is a cut-free proof rather than a clause. Note that resolution on ground clauses is essentially atomic cut, thus using proof resolution to construct cut-free proofs one would need to join the two proofs together and remove the atoms which where resolved. To efficiently perform this joining (and guarantee that the resulting cut-free proof is intuitionistic) we develop the concept of proof subsumption (similar to clause subsumption) and indexed resolution, a refinement indexing atoms by their corresponding positions in the cut formula. Proof subsumption serves as a tool to prove the completeness of the new method CERES-i, and indexed resolution provides an efficient strategy for the joining of two proofs which is in general a nondeterministic search. Such a refinement is essential for any attempt to implement this method. Finally we compare the complexity of CERES-i with that of Gentzen-based methods.

Authors:F. Delon; P. Simonetta Abstract: Publication date: Available online 29 March 2017 Source:Annals of Pure and Applied Logic Author(s): F. Delon, P. Simonetta We classify abelian C-minimal valued groups up to pure and elementary extensions and small modifications. We define first the notion of almost regularity for abelian valued groups. Then we introduce on the chain of valuations the structure which enables us to characterize C-minimal abelian valued groups as the almost regular ones with an o-minimal chain.

Authors:Will Boney; Rami Grossberg; Monica M. VanDieren; Sebastien Vasey Abstract: Publication date: Available online 27 March 2017 Source:Annals of Pure and Applied Logic Author(s): Will Boney, Rami Grossberg, Monica M. VanDieren, Sebastien Vasey Starting from an abstract elementary class with no maximal models, Shelah and Villaveces have shown (assuming instances of diamond) that categoricity implies a superstability-like property for nonsplitting, a particular notion of independence. We generalize their result as follows: given any abstract notion of independence for Galois (orbital) types over models, we derive that the notion satisfies a superstability property provided that the class is categorical and satisfies a weakening of amalgamation. This extends the Shelah–Villaveces result (the independence notion there was splitting) as well as a result of the first and second author where the independence notion was coheir. The argument is in ZFC and fills a gap in the Shelah–Villaveces proof.

Authors:Sebastien Vasey Abstract: Publication date: Available online 22 March 2017 Source:Annals of Pure and Applied Logic Author(s): Sebastien Vasey We prove: Theorem 0.1 Let K be a universal class. If K is categorical in cardinals of arbitrarily high cofinality, then K is categorical on a tail of cardinals. The proof stems from ideas of Adi Jarden and Will Boney, and also relies on a deep result of Shelah. As opposed to previous works, the argument is in ZFC and does not use the assumption of categoricity in a successor cardinal. The argument generalizes to abstract elementary classes (AECs) that satisfy a locality property and where certain prime models exist. Moreover assuming amalgamation we can give an explicit bound on the Hanf number and get rid of the cofinality restrictions: Theorem 0.2 Let K be an AEC with amalgamation. Assume that K is fully LS ( K ) -tame and short and has primes over sets of the form M ∪ { a } . Write H 2 : = ℶ ( 2 ℶ ( 2 LS ( K ) ) + ) + . If K is categorical in a λ > H 2 , then K is categorical in all λ ′ ≥ H 2 .

Authors:John Goodrick; Byunghan Kim; Alexei Kolesnikov Abstract: Publication date: Available online 18 March 2017 Source:Annals of Pure and Applied Logic Author(s): John Goodrick, Byunghan Kim, Alexei Kolesnikov We give an explicit description of the homology group H n ( p ) of a strong type p in any stable theory under the assumption that for every non-forking extension q of p the groups H i ( q ) are trivial for 2 ≤ i < n . The group H n ( p ) turns out to be isomorphic to the automorphism group of a certain part of the algebraic closure of n independent realizations of p; it follows from the authors' earlier work that such a group must be abelian. We call this the “Hurewicz correspondence” by analogy with the Hurewicz Theorem in algebraic topology.

Authors:Andrey Bovykin; Andreas Weiermann Abstract: Publication date: Available online 14 March 2017 Source:Annals of Pure and Applied Logic Author(s): Andrey Bovykin, Andreas Weiermann In this article, we conduct a model-theoretic investigation of three infinitary Ramseyan statements: the Infinite Ramsey Theorem for pairs and two colours ( RT 2 2 ), the Canonical Ramsey Theorem for pairs ( CRT 2 ) and the Regressive Ramsey Theorem for pairs ( RegRT 2 ). We approximate the logical strength of these principles by the strength of their first-order iterated versions, known as density principles. We then investigate their logical strength using strong initial segments of models of Peano Arithmetic, in the spirit of the classical article by Paris and Kirby, hereby re-proving old results model-theoretically. The article is concluded by a discussion of two further outreaches of densities. One is a further investigation of the strength of the Ramsey Theorem for pairs. The other deals with the asymptotics of the standard Ramsey function R 2 2 .

Authors:Rutger Kuyper; Joseph S. Miller Abstract: Publication date: Available online 10 March 2017 Source:Annals of Pure and Applied Logic Author(s): Rutger Kuyper, Joseph S. Miller For a class C of sets, let us say that a set A is C stabilising if A △ X ∈ C for every X ∈ C . We prove that the Martin-Löf stabilising sets are exactly the K-trivial sets, as are the weakly 2-random stabilising sets. We also show that the 1-generic stabilising sets are exactly the computable sets.

Authors:Grigory K. Olkhovikov Abstract: Publication date: Available online 9 March 2017 Source:Annals of Pure and Applied Logic Author(s): Grigory K. Olkhovikov The paper continues the line of [6], [7], and [8]. This results in a model-theoretic characterization of expressive powers of arbitrary finite sets of guarded connectives of degree not exceeding 1 and regular connectives of degree 2 over the language of bounded lattices.

Authors:Daniel Perrucci; Marie-Françoise Roy Abstract: Publication date: Available online 8 March 2017 Source:Annals of Pure and Applied Logic Author(s): Daniel Perrucci, Marie-Françoise Roy We describe a new quantifier elimination algorithm for real closed fields based on Thom encoding and sign determination. The complexity of this algorithm is elementary recursive and its proof of correctness is completely algebraic. In particular, the notion of connected components of semialgebraic sets is not used.

Authors:Will Boney; Rami Grossberg Abstract: Publication date: Available online 2 March 2017 Source:Annals of Pure and Applied Logic Author(s): Will Boney, Rami Grossberg We develop a notion of forking for Galois-types in the context of Elementary Classes (AECs). Under the hypotheses that an AEC K is tame, type-short, and failure of an order-property, we consider Definition 1 Let M 0 ≺ N be models from K and A be a set. We say that the Galois-type of A over N does not fork over M 0 , written A ⫝ M 0 N , iff for all small a ∈ A and all small N − ≺ N , we have that Galois-type of a over N − is realized in M 0 . Assuming property (E) (Existence and Extension, see Definition 3.3) we show that this non-forking is a well behaved notion of independence, in particular satisfies symmetry and uniqueness and has a corresponding U-rank. We find conditions for a universal local character, in particular derive superstability-like property from little more than categoricity in a “big cardinal”. Finally, we show that under large cardinal axioms the proofs are simpler and the non-forking is more powerful. In [10], it is established that, if this notion is an independence notion, then it is the only one.

Authors:Dan Hathaway Abstract: Publication date: Available online 1 March 2017 Source:Annals of Pure and Applied Logic Author(s): Dan Hathaway For each a ∈ ω ω , we define a Baire class one function f a : ω ω → ω ω which encodes a in a certain sense. We show that for each Borel g : ω ω → ω ω , f a ∩ g = ∅ implies a ∈ Δ 1 1 ( c ) where c is any code for g. We generalize this theorem for g in a larger pointclass Γ. Specifically, when Γ = Δ 2 1 , a ∈ L [ c ] . Also for all n ∈ ω , when Γ = Δ 3 + n 1 , a ∈ M 1 + n ( c ) .

Authors:Carmi Merimovich Abstract: Publication date: Available online 28 February 2017 Source:Annals of Pure and Applied Logic Author(s): Carmi Merimovich The extender based Magidor-Radin forcing is being generalized to supercompact type extenders.

Authors:Somayyeh Tari Abstract: Publication date: Available online 28 February 2017 Source:Annals of Pure and Applied Logic Author(s): Somayyeh Tari Continuous extension cells, or CE-cells, are cells whose defining functions have continuous extensions on closure of their domains. An o-minimal structure has the CE-cell decomposition property if any cell decomposition has a refinement by CE-cells. If the o-minimal structure M has the CE-cell decomposition property, then it has the open cell property. In other words, every definable open set in M is a finite union of definable open cells. Here, we show that the open cell property does not imply the CE-cell decomposition property. Also, after introducing an existence of limit property, we show that the CE-cell decomposition property is equivalent to the open cell property and the existence of limit property.