Abstract: Publication date: Available online 13 November 2019Source: Annals of Pure and Applied LogicAuthor(s): Masato Fujita We define and investigate a uniformly locally o-minimal structure of the second kind in this paper. All uniformly locally o-minimal structures of the second kind have local monotonicity, which is a local version of monotonicity theorem of o-minimal structures. We also demonstrate a local definable cell decomposition theorem for definably complete uniformly locally o-minimal structures of the second kind. We define dimension of a definable set and investigate its basic properties when the given structure is a locally o-minimal structure which admits local definable cell decomposition.

Abstract: Publication date: Available online 11 November 2019Source: Annals of Pure and Applied LogicAuthor(s): Manuela Busaniche, José Luis Castiglioni, Noemí Lubomirsky Consider any subvariety of BL-algebras generated by a single BL-chain which is the ordinal sum of the standard MV-algebra on [0,1] and a basic hoop H. We present a geometrical characterization of elements in the finitely generated free algebra of each of these subvarieties. In this characterization there is a clear insight of the role of the regular and dense elements of the generating chain. As an application, we analyze maximal and prime filters in the free algebra.

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.

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.