Abstract: Publication date: Available online 7 October 2019Source: Annals of Pure and Applied LogicAuthor(s): J.P. Aguilera Takeuti introduced an infinitary proof system for determinate logic and showed that for transitive models of Zermelo-Fraenkel set theory with the Axiom of Dependent Choice that contain all reals, the cut-elimination theorem is equivalent to the Axiom of Determinacy, and in particular contradicts the Axiom of Choice.We consider variants of Takeuti's theorem without assuming the failure of the Axiom of Choice. For instance, we show that if one removes atomic formulae of infinite arity from the language of Takeuti's proof system, then cut elimination is equivalent to a determinacy hypothesis provable, e.g., in ZFC + “there are infinitely many Woodin cardinals.” A slight extension of the proof system admits cut elimination for countable sequents under the same assumptions.A simple modification of the proof system yields analogs of the results above for the Axiom of Real Determinacy and uncountably many Woodin cardinals.

Abstract: Publication date: Available online 10 September 2019Source: Annals of Pure and Applied LogicAuthor(s): Moritz Müller, Ján Pich We ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length n. In 1995 Razborov showed that many can be proved in PV1, a bounded arithmetic formalizing polynomial time reasoning. He formalized circuit lower bound statements for small n of doubly logarithmic order. It is open whether PV1 proves known lower bounds in succinct formalizations for n of logarithmic order. We give such proofs in APC1, an extension of PV1 formalizing probabilistic polynomial time reasoning: for parity and AC0, for mod q and AC0[p] (only for n slightly smaller than logarithmic), and for k-clique and monotone circuits. We also formalize Razborov and Rudich's natural proof barrier.We ask for short propositional proofs of circuit lower bounds expressed succinctly by propositional formulas of size nO(1) or at least much smaller than the 2O(n) size of the common “truth table” formula. We discuss two such expressions: one via feasible functions witnessing errors of circuits, and one via the anticheckers of Lipton and Young 1994. Our APC1 formalizations yield conditional upper bounds for the succinct formulas obtained by witnessing: we get short Extended Frege proofs from general circuit lower bounds expressed by the common “truth-table” formulas. We also show how to construct in quasipolynomial time propositional proofs of quasipolynomial size tautologies expressing AC0[p] quasipolynomial size lower bounds; these proofs are in Jeřábek's system WF.

Abstract: Publication date: Available online 5 September 2019Source: Annals of Pure and Applied LogicAuthor(s): Gabriel Conant, Kyle Gannon In NIP theories, generically stable Keisler measures can be characterized in several ways. We analyze these various forms of “generic stability” in arbitrary theories. Among other things, we show that the standard definition of generic stability for types coincides with the notion of a frequency interpretation measure. We also give combinatorial examples of types in NSOP theories that are finitely approximated but not generically stable, as well as ϕ-types in simple theories that are definable and finitely satisfiable in a small model, but not finitely approximated. Our proofs demonstrate interesting connections to classical results from Ramsey theory for finite graphs and hypergraphs.

Abstract: Publication date: Available online 21 August 2019Source: Annals of Pure and Applied LogicAuthor(s): Dmitry Itsykson, Dmitry Sokolov We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over F2; we denote this system by Res(⊕). It is well known that tree-like resolution is equivalent in behaviour to DPLL algorithms for the Boolean satisfiability problem. Every DPLL algorithm splits the input problem into two by assigning two possible values to a variable; then it simplifies the two resulting formulas and makes two recursive calls. Tree-like Res(⊕)-proofs correspond to an extension of the DPLL paradigm, in which we can split by an arbitrary linear combination of variables modulo two. These algorithms quickly solve formulas that explicitly encode linear systems modulo two which were used for proving exponential lower bounds for conventional DPLL algorithms.We prove exponential lower bounds on the size of tree-like Res(⊕)-proofs. We also show that resolution and tree-like Res(⊕) do not simulate each other.We prove a space vs size tradeoff for Res(⊕)-proofs. We prove that Res(⊕) is implicationally complete and also that Res(⊕) is polynomially equivalent to its semantic version.We consider the proof system Res(⊕)[k] that is a restricted version of Res(⊕) operating with disjunctions of linear equalities such that at most k equalities depend on more than one variable. We simulate Res(⊕)[k] in the OBDD-based proof system with blowup 2k and in Polynomial Calculus Resolution with blowup 2nH(2k/n)poly(n), where n is the number of variables and H(p) is the binary entropy; the latter result implies exponential lower bounds on the size of Res(⊕)[δn]-proofs for some constant δ>0. Raz and Tzameret introduced the system R(lin) which operates with disjunctions of linear equalities with integer coefficients. We show that Res(⊕) can be p-simulated in R(lin).

Abstract: Publication date: Available online 21 August 2019Source: Annals of Pure and Applied LogicAuthor(s): Marcos Mazari-Armida We study limit models in the class of abelian groups with the subgroup relation and in the class of torsion-free abelian groups with the pure subgroup relation. We show: Theorem 0.1.(1)If G is a limit model of cardinality λ in the class of abelian groups with the subgroup relation, then G≅(⊕λQ)⊕⊕pprime(⊕λZ(p∞)).(2)If G is a limit model of cardinality λ in the class of torsion-free abelian groups with the pure subgroup relation, then:•If the length of the chain has uncountable cofinality, thenG≅(⊕λQ)⊕Πpprime(⊕λZ(p))‾.•If the length of the chain has countable cofinality, then G is not algebraically compact. We also study the class of finitely Butler groups with the pure subgroup relation, we show that it is an AEC, Galois-stable and (

Abstract: Publication date: Available online 14 August 2019Source: Annals of Pure and Applied LogicAuthor(s): Junhua Yu Instantial neighborhood logic (INL) is classical propositional logic enriched by a two-sorted operator □. In a neighborhood model, a formula like □(α1,...,αj;α0) (for an arbitrary natural number j) means that, the current point has a neighborhood in which α0 universally holds and none of α1,...,αj universally fails. This paper offers to INL: (1) a cut-free sequent calculus, and (2) a constructive proof of its Lyndon interpolation theorem.

Abstract: Publication date: Available online 19 July 2019Source: Annals of Pure and Applied LogicAuthor(s): Lorna Gregory, Sonia L'Innocente, Carlo Toffalori We provide algebraic conditions ensuring the decidability of the theory of modules over effectively given Prüfer (in particular Bézout) domains whose localizations at maximal ideals have dense value groups. For Bézout domains, these conditions are also necessary.

Abstract: Publication date: Available online 9 July 2019Source: Annals of Pure and Applied LogicAuthor(s): Vera Koponen We prove that if T is an ω-categorical supersimple theory with nontrivial dependence (given by forking), then there is a nontrivial regular 1-type over a finite set of reals which is realized by real elements; hence forking induces a nontrivial pregeometry on the solution set of this type and the pregeometry is definable (using only finitely many parameters). The assumption about ω-categoricity is necessary. This result is used to prove the following: If V is a finite relational vocabulary with maximal arity 3 and T is a supersimple V-theory with elimination of quantifiers, then T has trivial dependence and finite SU-rank. This immediately gives the following strengthening of [18, Theorem 4.1]: if M is a ternary simple homogeneous structure with only finitely many constraints, then Th(M) has trivial dependence and finite SU-rank.

Abstract: Publication date: Available online 4 July 2019Source: Annals of Pure and Applied LogicAuthor(s): Ian Herbert, Sanjay Jain, Steffen Lempp, Mustafa Manat, Frank Stephan This paper considers reductions between types of numberings; these reductions preserve the Rogers Semilattice of the numberings reduced and also preserve the number of minimal and positive degrees in their semilattice. It is shown how to use these reductions to simplify some constructions of specific semilattices. Furthermore, it is shown that for the basic types of numberings, one can reduce the left-r.e. numberings to the r.e. numberings and the k-r.e. numberings to the (k+1)-r.e. numberings; all further reductions are obtained by concatenating these reductions.

Abstract: Publication date: Available online 4 July 2019Source: Annals of Pure and Applied LogicAuthor(s): François Dorais, Zachary Evans, Marcia Groszek, Seth Harris, Theodore Slaman Good m-tuples, m-tuples of r.e. sets without Schmerl decompositions, were introduced by Schmerl, who used them to investigate the reverse mathematics of Grundy colorings of graphs. Schmerl considered only standard m, for which our definitions of weakly good, good, and strongly good coincide. The existence of good tuples for nonstandard m depends on how much induction is available in the model. We show that in models of first-order arithmetic, over a base theory of IΔ10+BΣ10+EXP, the existence of arbitrarily long weakly good tuples is equivalent to IΣ10 and the existence of arbitrarily long good or strongly good tuples is equivalent to BΣ30. Consequences for second-order arithmetic include that, over RCA0⁎, the existence of arbitrarily long good tuples is equivalent to BΣ30+¬ACA.

Abstract: Publication date: Available online 3 July 2019Source: Annals of Pure and Applied LogicAuthor(s): Erik Palmgren First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.

Abstract: Publication date: Available online 1 July 2019Source: Annals of Pure and Applied LogicAuthor(s): G. Bezhanishvili, N. Bezhanishvili, T. Santoli, Y. Venema We introduce a simple modal calculus for compact Hausdorff spaces. The language of our system extends that of propositional logic with a strict implication connective, which, as shown in earlier work, algebraically corresponds to the notion of a subordination on Boolean algebras. Our base system is a strict implication calculus SIC, to which we associate a variety SIA of strict implication algebras. We also study the symmetric strict implication calculus S2IC, which is an extension of SIC, and prove that S2IC is strongly sound and complete with respect to de Vries algebras. By de Vries duality, this yields completeness of S2IC with respect to compact Hausdorff spaces. Since some of the defining axioms of de Vries algebras are Π2-sentences, we develop the corresponding theory of non-standard rules, which we term Π2-rules. We study the resulting inductive elementary classes of algebras, and give a general criterion of admissibility for Π2-rules. We also compare our approach to approaches in the literature that are related to our work.1

Abstract: Publication date: Available online 27 June 2019Source: Annals of Pure and Applied LogicAuthor(s): Maxwell Levine Cummings, Foreman, and Magidor proved that for any λ

Abstract: Publication date: Available online 25 June 2019Source: Annals of Pure and Applied LogicAuthor(s): Nathanael Ackerman, Will Boney, Sebastien Vasey The third author has shown that Shelah's eventual categoricity conjecture holds in universal classes: class of structures closed under isomorphisms, substructures, and unions of chains. We extend this result to the framework of multiuniversal classes. Roughly speaking, these are classes with a closure operator that is essentially algebraic closure (instead of, in the universal case, being essentially definable closure). Along the way, we prove in particular that Galois (orbital) types in multiuniversal classes are determined by their finite restrictions, generalizing a result of the second author.

Abstract: Publication date: Available online 5 June 2019Source: Annals of Pure and Applied LogicAuthor(s): Dag Normann, Sam Sanders Compactness is one of the core notions of analysis: it connects local properties to global ones and makes limits well-behaved. We study the computational properties of the compactness of Cantor space 2N for uncountable covers. The most basic question is: how hard is it to compute a finite sub-cover from such a cover of 2N' Another natural question is: how hard is it to compute a sequence that covers 2N minus a measure zero set from such a cover' The special and weak fan functionals respectively compute such finite sub-covers and sequences. In this paper, we establish the connection between these new fan functionals on one hand, and various well-known comprehension axioms on the other hand, including arithmetical comprehension, transfinite recursion, and the Suslin functional. In the spirit of Reverse Mathematics, we also analyse the logical strength of compactness in Nonstandard Analysis. Perhaps surprisingly, the results in the latter mirror (often perfectly) the computational properties of the special and weak fan functionals. In particular, we show that compactness (nonstandard or otherwise) readily brings us to the outer edges of Reverse Mathematics (namely Π21-CA0), and even into Schweber's higher-order framework (namely Σ12-separation).

Abstract: Publication date: Available online 3 June 2019Source: Annals of Pure and Applied LogicAuthor(s): Rosalie Iemhoff This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus G4ip for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of K and KD (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.

Abstract: Publication date: Available online 31 May 2019Source: Annals of Pure and Applied LogicAuthor(s): Roberto Maieli This paper studies the so-called generalized multiplicative connectives of linear logic, focusing on the question of finding the “non-decomposable” ones, i.e., those that cannot be expressed as combinations of the default binary connectives of multiplicative linear logic, ⊗ (times) and ⅋ (par). In particular, we concentrate on generalized connectives of a surprisingly simple form, called “entangled connectives”, and prove a characterization theorem giving a criterion for identifying the undecomposable entangled ones.