Abstract: Publication date: Available online 19 February 2020Source: Annals of Pure and Applied LogicAuthor(s): Bahareh Afshari, Stefan Hetzl, Graham E. LeighAbstractThis article examines the computational content of the classical Gentzen sequent calculus. There are a number of well-known methods that extract computational content from first-order logic but applying these to the sequent calculus involves first translating proofs into other formalisms, Hilbert calculi or Natural Deduction for example. A direct approach which mirrors the symmetry inherent in sequent calculus has potential merits in relation to proof-theoretic considerations such as the (non-)confluence of cut elimination, the problem of cut introduction, proof compression and proof equivalence. Motivated by such applications, we provide a representation of sequent calculus proofs as higher order recursion schemes. Our approach associates to an LK proof π of ⇒∃vF, where F is quantifier free, an acyclic higher order recursion scheme H with a finite language yielding a Herbrand disjunction for ∃vF. More generally, we show that the language of H contains all Herbrand disjunctions computable from π via a broad range of cut elimination strategies.

Abstract: Publication date: Available online 19 February 2020Source: Annals of Pure and Applied LogicAuthor(s): Brent CodyAbstractHellsten [15] gave a characterization of Πn1-indescribable subsets of a Πn1-indescribable cardinal in terms of a natural filter base: when κ is a Πn1-indescribable cardinal, a set S⊆κ is Πn1-indescribable if and only if S∩C≠∅ for every n-club C⊆κ. We generalize Hellsten's characterization to Πn1-indescribable subsets of Pκλ, which were first defined by Baumgartner. First we show that under reasonable assumptions the Π01-indescribability ideal on Pκλ equals the minimal strongly normal ideal NSSκ,λ on Pκλ, which is different from NSκ,λ. We then formulate a notion of n-club subset of Pκλ and prove that a set S⊆Pκλ is Πn1-indescribable if and only if S∩C≠∅ for every n-club C⊆Pκλ. We also prove that elementary embeddings considered by Schanker [26] witnessing near supercompactness lead to the definition of a normal ideal on Pκλ, and indeed, this ideal is equal to Baumgartner's ideal of non–Π11-indescribable subsets of Pκλ. Additionally, as applications of these results we answer a question of Cox-Lücke [10] about F-layered posets, provide a characterization of Πnm-indescribable subsets of Pκλ

Abstract: Publication date: Available online 14 February 2020Source: Annals of Pure and Applied LogicAuthor(s): Zeinab Bakhtiari, Hans van Ditmarsch, Umberto Rivieccio Baltag, Moss, and Solecki proposed an expansion of classical modal logic, called logic of epistemic actions and knowledge (EAK), in which one can reason about knowledge and change of knowledge. Kurz and Palmigiano showed how duality theory provides a flexible framework for modelling such epistemic changes, allowing one to develop dynamic epistemic logics on a weaker propositional basis than classical logic (for example an intuitionistic basis). In this paper we show how the techniques of Kurz and Palmigiano can be further extended to define and axiomatize a bilattice logic of epistemic actions and knowledge (BEAK). Our propositional basis is a modal expansion of the well-known four-valued logic of Belnap and Dunn, which is a system designed for handling inconsistent as well as potentially conflicting information. These features, we believe, make our framework particularly promising from a computer science perspective.

Abstract: Publication date: Available online 11 February 2020Source: Annals of Pure and Applied LogicAuthor(s): Jun Le Goh We study the computational content of various theorems with reverse mathematical strength around Arithmetical Transfinite Recursion (ATR0) from the point of view of computability-theoretic reducibilities, in particular Weihrauch reducibility. Our main result states that it is equally hard to construct an embedding between two given well-orderings, as it is to construct a Turing jump hierarchy on a given well-ordering. This answers a question of Marcone. We obtain a similar result for Fraïssé's conjecture restricted to well-orderings.

Abstract: Publication date: Available online 11 February 2020Source: Annals of Pure and Applied LogicAuthor(s): Dag Normann, Sam Sanders We study the logical and computational properties of basic theorems of uncountable mathematics, in particular Pincherle's theorem, published in 1882. This theorem states that a locally bounded function is bounded on certain domains, i.e. one of the first ‘local-to-global’ principles. It is well-known that such principles in analysis are intimately connected to (open-cover) compactness, but we nonetheless exhibit fundamental differences between compactness and Pincherle's theorem. For instance, the main question of Reverse Mathematics, namely which set existence axioms are necessary to prove Pincherle's theorem, does not have an unique or unambiguous answer, in contrast to compactness. We establish similar differences for the computational properties of compactness and Pincherle's theorem. We establish the same differences for other local-to-global principles, even going back to Weierstrass. We also greatly sharpen the known computational power of compactness, for the most shared with Pincherle's theorem however. Finally, countable choice plays an important role in the previous, we therefore study this axiom together with the intimately related Lindelöf lemma.

Abstract: Publication date: Available online 3 February 2020Source: Annals of Pure and Applied LogicAuthor(s): Moti Gitik We introduce certain morass type structures and apply them to blowing up powers of singular cardinals. As a bonus, a forcing for adding clubs with finite conditions to higher cardinals is obtained.

Abstract: Publication date: Available online 31 January 2020Source: Annals of Pure and Applied LogicAuthor(s): Christopher Hampson, Stanislav Kikot, Agi Kurucz, Sérgio Marcelino Our concern is the axiomatisation problem for modal and algebraic logics that correspond to various fragments of two-variable first-order logic with counting quantifiers. In particular, we consider modal products with Diff, the propositional unimodal logic of the difference operator. We show that the two-dimensional product logic Diff×Diff is non-finitely axiomatisable, but can be axiomatised by infinitely many Sahlqvist axioms. We also show that its ‘square’ version (the modal counterpart of the substitution and equality free fragment of two-variable first-order logic with counting to two) is non-finitely axiomatisable over Diff×Diff, but can be axiomatised by adding infinitely many Sahlqvist axioms. These are the first examples of products of finitely axiomatisable modal logics that are not finitely axiomatisable, but axiomatisable by explicit infinite sets of canonical axioms.

Abstract: Publication date: Available online 20 January 2020Source: Annals of Pure and Applied LogicAuthor(s): Alejandro Poveda Let cof(μ)=μ and κ be a supercompact cardinal with μ

Abstract: Publication date: Available online 7 January 2020Source: Annals of Pure and Applied LogicAuthor(s): Ivan Georgiev We consider the complexity of the integration operator on real functions with respect to the subrecursive class M2. We prove that the definite integral of a uniformly M2-computable analytic real function with M2-computable limits is itself M2-computable real number. We generalise this result to integrals with parameters and with varying limits. As an application, we show that the Euler-Mascheroni constant is M2-computable.

Abstract: Publication date: Available online 7 January 2020Source: Annals of Pure and Applied LogicAuthor(s): Darío García We introduce the concept of o-asymptotic classes of finite structures, melding ideas coming from 1-dimensional asymptotic classes and o-minimality. Along with several examples and non-examples of these classes, we present some classification theory results of their infinite ultraproducts: Every infinite ultraproduct of structures in an o-asymptotic class is superrosy of Uþ-rank 1, and NTP2 (in fact, inp-minimal).

Abstract: Publication date: Available online 13 December 2019Source: Annals of Pure and Applied LogicAuthor(s): Alexander G. Melnikov, Victor L. Selivanov, Mars M. Yamaleev In the late 1980s, Selivanov used typed Boolean combinations of arithmetical sets to extend the Ershov hierarchy beyond Δ20 sets. Similar to the Ershov hierarchy, Selivanov's fine hierarchy {Σγ}γ

Abstract: Publication date: Available online 28 November 2019Source: Annals of Pure and Applied LogicAuthor(s): Slavko Moconja, Predrag Tanović We introduce the notions of stationarily ordered types and theories; the latter generalizes weak o-minimality and the former is a relaxed version of weak o-minimality localized at the locus of a single type. We show that forking, as a binary relation on elements realizing stationarily ordered types, is an equivalence relation and that each stationarily ordered type in a model determines some order-type as an invariant of the model. We study weak and forking non-orthogonality of stationarily ordered types, show that they are equivalence relations and prove that invariants of non-orthogonal types are closely related. The techniques developed are applied to prove that in the case of a binary, stationarily ordered theory with fewer than 2ℵ0 countable models, the isomorphism type of a countable model is determined by a certain sequence of invariants of the model. In particular, we confirm Vaught's conjecture for binary, stationarily ordered theories.

Abstract: Publication date: Available online 6 November 2019Source: Annals of Pure and Applied LogicAuthor(s): Nebojša Ikodinović, Zoran Ognjanović, Aleksandar Perović, Miodrag Rašković We study propositional probabilistic logics (LPP–logics) with probability operators of the form P≥r (“the probability is at least r”) with σ–additive semantics. For regular infinite cardinals κ and λ, the probabilistic logic LPPκ,λ has λ propositional variables, allows conjunctions of

Abstract: Publication date: Available online 4 November 2019Source: Annals of Pure and Applied LogicAuthor(s): Sato Kentaro We introduce a new axiom called inductive dichotomy, a weak variant of the axiom of inductive definition, and analyze the relationships with other variants of inductive definition and with related axioms, in the general second order framework, including second order arithmetic, second order set theory and higher order arithmetic. By applying these results to the investigations on the determinacy axioms, we show the following. (i) Clopen determinacy is consistency-wise strictly weaker than open determinacy in these frameworks, except second order arithmetic; this is an enhancement of Schweber–Hachtman separation of open and clopen determinacy into the consistency-wise separation. (ii) Hausdorff–Kuratowski hierarchy of differences of opens is faithfully reflected by the hierarchy of consistency strengths of corresponding parameter-free determinacies in the aforementioned frameworks; this result is valid also in second order arithmetic only except clopen determinacy.