Abstract: Publication date: Available online 7 March 2019Source: Annals of Pure and Applied LogicAuthor(s): Junguk Lee We introduce a notion of μ-structures which are certain locally compact group actions and prove some counterparts of results on Polish structures (introduced by Krupinski in [9]). Using the Haar measure of locally compact groups, we introduce an independence, called μ-independence, in μ-structures having good properties. With this independence notion, we develop geometric stability theory for μ-structures. Then we see some structural theorems for compact groups which are μ-structure. We also give examples of profinite structures where μ-independence is different from nm-independence introduced by Krupinski for Polish structures.In an appendix, Cohen and Wesolek show that a profinite branch group gives a small action on the boundary of a rooted tree so that this actions provides a small profinite structure on the boundary of a rooted tree.

Abstract: Publication date: Available online 5 March 2019Source: Annals of Pure and Applied LogicAuthor(s): Tomasz Kowalski, George Metcalfe A variety V is said to be coherent if every finitely generated subalgebra of a finitely presented member of V is finitely presented. It is shown here that coherence corresponds to a key ingredient of uniform deductive interpolation for equational consequence in V: the property that any compact congruence on a finitely generated free algebra of V restricted to a free algebra over fewer generators is compact. A general criterion is derived for establishing failures of coherence, and hence also of uniform deductive interpolation. The criterion is then applied in conjunction with properties of canonical extensions to prove that coherence and uniform deductive interpolation fail for certain varieties of Boolean algebras with operators (including varieties for the modal logic K and KT), double-Heyting algebras, residuated lattices, and lattices.

Abstract: Publication date: Available online 28 February 2019Source: Annals of Pure and Applied LogicAuthor(s): Tommaso Moraschini We prove that the problem of determining whether a finite logical matrix determines an algebraizable logic is complete for EXPTIME. The same result holds for the classes of order algebraizable, weakly algebraizable, equivalential and protoalgebraic logics. Finally, the same problem for the class of truth-equational logic is shown to be hard for EXPTIME.

Abstract: Publication date: Available online 19 February 2019Source: Annals of Pure and Applied LogicAuthor(s): Daniel Max Hoffmann We fix a monster model D of some stable theory and investigate substructures of D which are existentially closed within the class of substructures equipped with an action of a fixed group G. We describe them as PAC substructures of D and obtain results related to Galois theory.Assuming that the class of these existentially closed substructures is elementary, we show that, under the assumption of having bounded models, its theory is simple and eliminates quantifiers up to some existential formulas. Moreover, this theory codes finite sets and allows a geometric elimination of imaginaries, but not always a weak elimination of imaginaries.

Abstract: Publication date: Available online 4 February 2019Source: Annals of Pure and Applied LogicAuthor(s): Albert Visser, Jetze Zoethout The logic iGLC is the intuitionistic version of Löb's Logic plus the completeness principle A→□A. In this paper, we prove an arithmetical completeness theorems for iGLC for theories equipped with two provability predicates □ and △ that prove the schemes A→△A and □△S→□S for S∈Σ1. We provide two salient instances of the theorem. In the first, □ is fast provability and △ is ordinary provability and, in the second, □ is ordinary provability and △ is slow provability.Using the second instance, we reprove a theorem previously obtained by Mohammad Ardeshir and Mojtaba Mojtahedi [1] determining the Σ1-provability logic of Heyting Arithmetic.

Abstract: Publication date: Available online 1 February 2019Source: Annals of Pure and Applied LogicAuthor(s): Ekaterina Fokina, Valentina Harizanov, Daniel Turetsky Computability-theoretic investigation of algorithmic complexity of isomorphisms between countable structures is a key topic in computable structure theory since Fröhlich and Shepherdson, Mal'cev, and Metakides and Nerode. A computable structure A is called computably categorical if for every computable isomorphic B, there is a computable isomorphism from A onto B. By relativizing the notion of computable categoricity to a Turing degree d, we obtain the notion of d-computable categoricity. For the case when d is 0(n−1), we also speak about Δn0-categoricity, for n≥1. More generally, A is relatively Δn0-categorical if for every isomorphic B, there is an isomorphism that is Δn0 relative to the atomic diagram of B. Equivalently, A is relatively Δn0-categorical if and only if A has a computably enumerable Scott family of computable (infinitary) Σn formulas. Relative Δn0-categoricity implies Δn0-categoricity, but not vice versa.In this paper, we present an example of a computable Fraïssé limit that is computably categorical (that is, Δ10-categorical) but not relatively computably categorical. We also present examples of Δ20-categorical but not relatively Δ20-cate- gorical structures in natural classes such as trees of finite and infinite heights, and homogenous, completely decomposable, abelian groups. It is known that for structures from these classes computable categoricity and relative computable categoricity coincide.The categoricity spectrum of a computable structure M is the set of all Turing degrees d such that

Abstract: Publication date: Available online 24 January 2019Source: Annals of Pure and Applied LogicAuthor(s): Philip Scowcroft This paper axiomatizes classes of Abelian lattice-ordered groups with a finite upper bound on the number of pairwise disjoint positive elements; finds model-completions for these theories; derives corresponding Nullstellensätze; determines which model-completions eliminate quantifiers; and examines quantifier elimination in a different language and for positive formulas.

Abstract: Publication date: Available online 9 January 2019Source: Annals of Pure and Applied LogicAuthor(s): M. Malliaris, S. Shelah We investigate the interpretability ordering ⊴⁎ using generalized Ehrenfeucht–Mostowski models. This gives a new approach to proving inequalities and investigating the structure of types.

Abstract: Publication date: Available online 28 December 2018Source: Annals of Pure and Applied LogicAuthor(s): Sebastian Enqvist, Fatemeh Seifan, Yde Venema We set up a generic framework for proving completeness results for variants of the modal mu-calculus, using tools from coalgebraic modal logic. We illustrate the method by proving two new completeness results: for the graded mu-calculus (which is equivalent to monadic second-order logic on the class of unranked tree models), and for the monotone modal mu-calculus.Besides these main applications, our result covers the Kozen-Walukiewicz completeness theorem for the standard modal mu-calculus, as well as the linear-time mu-calculus and modal fixpoint logics on ranked trees. Completeness of the linear-time mu-calculus is known, but the proof we obtain here is different and places the result under a common roof with Walukiewicz' result.Our approach combines insights from the theory of automata operating on potentially infinite objects, with methods from the categorical framework of coalgebra as a general theory of state-based evolving systems. At the interface of these theories lies the notion of a coalgebraic modal one-step language. One of our main contributions here is the introduction of the novel concept of a disjunctive basis for a modal one-step language. Generalizing earlier work, our main general result states that in case a coalgebraic modal logic admits such a disjunctive basis, then soundness and completeness at the one-step level transfers to the level of the full coalgebraic modal mu-calculus.

Abstract: Publication date: Available online 28 December 2018Source: Annals of Pure and Applied LogicAuthor(s): Guram Bezhanishvili, Nick Bezhanishvili, Joel Lucero-Bryan, Jan van Mill For a topological space X, let L(X) be the modal logic of X where □ is interpreted as interior (and hence ◇ as closure) in X. It was shown in [1] that the modal logics S4, S4.1, S4.2, S4.1.2, S4.Grz, S4.Grzn (n≥1), and their intersections arise as L(X) for some Stone space X. We give an example of a scattered Stone space whose logic is not such an intersection. This gives an affirmative answer to [1, Question 6.2]. On the other hand, we show that a scattered Stone space that is in addition hereditarily paracompact does not give rise to a new logic; namely we show that the logic of such a space is either S4.Grz or S4.Grzn for some n≥1. In fact, we prove this result for any scattered locally compact open hereditarily collectionwise normal and open hereditarily strongly zero-dimensional space.

Abstract: Publication date: Available online 21 December 2018Source: Annals of Pure and Applied LogicAuthor(s): Yo Matsubara, Hiroshi Sakai, Toshimichi Usuba Matsubara–Usuba [13] introduced the notion of skinniness and its variants for subsets of Pκλ and showed that the existence of skinny stationary subsets of Pκλ is related to large cardinal properties of ideals over Pκλ and to Jensen's diamond principle on λ. In this paper, we study the existence of skinny stationary sets in more detail.

Abstract: Publication date: Available online 17 December 2018Source: Annals of Pure and Applied LogicAuthor(s): Liu Yong There are very few results about maximal d.r.e. degrees as the construction is very hard to work with other requirements. In this paper we show that there exists an isolated maximal d.r.e. degree. In fact, we introduce a closely related notion called (m,n)-cupping degree and show that there exists an isolated (2,ω)-cupping degree, and there exists a proper (2,1)-cupping degree. It helps understanding various degree structures in the Ershov Hierarchy.

Abstract: Publication date: Available online 13 December 2018Source: Annals of Pure and Applied LogicAuthor(s): S.N. Popova, M.E. Zhukovskii In 2001, J.-M. Le Bars disproved the zero-one law (that says that every sentence from a certain logic is either true asymptotically almost surely (a.a.s.), or false a.a.s.) for existential monadic second order sentences (EMSO) on undirected graphs. He proved that there exists an EMSO sentence ϕ such that P(Gn⊨ϕ) does not converge as n→∞ (here, the probability distribution is uniform over the set of all graphs on the labeled set of vertices {1,…,n}). In the same paper, he conjectured that, for EMSO sentences with 2 first order variables, the zero-one law holds. In this paper, we disprove this conjecture.

Abstract: Publication date: Available online 22 November 2018Source: Annals of Pure and Applied LogicAuthor(s): Michael Shulman We study elementary theories of well-pointed toposes and pretoposes, regarded as category-theoretic or “structural” set theories in the spirit of Lawvere's “Elementary Theory of the Category of Sets”. We consider weak intuitionistic and predicative theories of pretoposes, and we also propose category-theoretic versions of stronger axioms such as unbounded separation, replacement, and collection. Finally, we compare all of these theories formally to traditional membership-based or “material” set theories, using a version of the classical construction based on internal well-founded relations.

Abstract: Publication date: Available online 13 November 2018Source: Annals of Pure and Applied LogicAuthor(s): Fabio Pasquali We characterize categories whose internal logic is Hilbert's ε-calculus as those categories which have a proper factorization system satisfying the axiom of choice and in which every non-initial object is injective. We provide an example of such a category where the law of excluded middle is not valid.

Abstract: Publication date: Available online 6 November 2018Source: Annals of Pure and Applied LogicAuthor(s): Sam Sanders Recently, a number of formal systems for Nonstandard Analysis restricted to the language of finite types, i.e. nonstandard arithmetic, have been proposed. We single out one particular system by Dinis-Gaspar, which is categorised by the authors as being part of intuitionistic nonstandard arithmetic. Their system is indeed inconsistent with the Transfer axiom of Nonstandard Analysis, and the latter axiom is classical in nature as it implies (higher-order) comprehension. Inspired by this observation, the main aim of this paper is to provide answers to the following questions:(Q1)In the spirit of Reverse Mathematics, what is the minimal fragment of Transfer that is inconsistent with the Dinis-Gaspar system'(Q2)What other axioms are inconsistent with the Dinis-Gaspar system' Our answer to the first question suggests that the aforementioned inconsistency actually derives from the axiom of extensionality relative to the standard world, and that other (much stronger) consequences of Transfer are actually harmless. Perhaps surprisingly, our answer to the second question shows that the Dinis-Gaspar system is inconsistent with a number of (non-classical) continuity theorems which one would -in our opinion- categorise as intuitionistic in the sense of Brouwer. Finally, we show that the Dinis-Gaspar system involves a standard part map, suggesting this system also pushes the boundary of what still counts as ‘Nonstandard Analysis’ or ‘internal set theory’.