Abstract: Publication date: Available online 15 May 2019Source: Annals of Pure and Applied LogicAuthor(s): Arnold Beckmann, Sam Buss This paper studies the complexity of constant depth propositional proofs in the cedent and sequent calculus. We discuss the relationships between the size of tree-like proofs, the size of dag-like proofs, and the heights of proofs. The main result is to correct a proof construction in an earlier paper about transformations from proofs with polylogarithmic height and constantly many formulas per cedent.

Abstract: Publication date: Available online 7 May 2019Source: Annals of Pure and Applied LogicAuthor(s): Philipp Hieronymi Let K be a subfield of R. The theory of R viewed as an ordered K-vector space and expanded by a predicate for Z is decidable if and only if K is a real quadratic field.

Abstract: Publication date: Available online 25 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Henk Barendregt, Sebastiaan A. Terwijn In the context of his theory of numberings, Ershov showed that Kleene's recursion theorem holds for any precomplete numbering. We discuss various generalizations of this result. Among other things, we show that Arslanov's completeness criterion also holds for every precomplete numbering, and we discuss the relation with Visser's ADN theorem, as well as the uniformity or nonuniformity of the various fixed point theorems. Finally, we base numberings on partial combinatory algebras and prove a generalization of Ershov's theorem in this context.

Abstract: Publication date: Available online 24 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Miloš S. Kurilić A complete first order theory of a relational signature is called monomorphic iff all its models are monomorphic (i.e. have all the n-element substructures isomorphic, for each positive integer n). We show that a complete theory T having infinite models is monomorphic iff it has a countable monomorphic model and confirm the Vaught conjecture for monomorphic theories. More precisely, we prove that if T is a complete monomorphic theory having infinite models, then the number of its non-isomorphic countable models, I(T,ω), is either equal to 1 or to c. In addition, the equality I(T,ω)=1 holds iff some countable model of T is simply definable by (or, equivalently, freely interpretable in) an ω-categorical linear order on its domain.

Abstract: Publication date: Available online 12 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Tatsuji Kawai Brouwer (1927) claimed that every function from the Baire space to natural numbers is induced by a neighbourhood function whose domain admits bar induction. We show that Brouwer's claim is provable in Heyting arithmetic in all finite types (HAω) for definable functions of the system. The proof does not rely on elaborate proof theoretic methods such as normalisation or ordinal analysis. Instead, we internalise in HAω the dialogue tree interpretation of Gödel's system T due to Escardó (2013). The interpretation determines a syntactic translation of terms, which yields a neighbourhood function from a closed term of HAω with the required property. As applications of this result, we prove some well-known properties of HAω: uniform continuity of definable functions from NN to N on the Cantor space; closure under the rule of bar induction; and closure of bar recursion for the lowest type with a definable stopping function.

Abstract: Publication date: Available online 12 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Willem Conradie, Alessandra Palmigiano We extend the theory of unified correspondence to a broad class of logics with algebraic semantics given by varieties of normal lattice expansions (LEs), also known as ‘lattices with operators’. Specifically, we introduce a syntactic definition of the class of Sahlqvist formulas and inequalities which applies uniformly to each LE-signature and is given purely in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives. We also introduce the algorithm ALBA, parametric in each LE-setting, which effectively computes first-order correspondents of LE-inequalities, and is guaranteed to succeed on a wide class of inequalities (the so-called inductive inequalities) which significantly extend the Sahlqvist class. Further, we show that every inequality on which ALBA succeeds is canonical. Projecting these results on specific signatures yields state-of-the-art correspondence and canonicity theory for many well known modal expansions of classical and intuitionistic logic and for substructural logics, from classical poly-modal logics to (bi-)intuitionistic modal logics to the Lambek calculus and its extensions, the Lambek-Grishin calculus, orthologic, the logic of (not necessarily distributive) De Morgan lattices, and the multiplicative-additive fragment of linear logic.

Abstract: Publication date: Available online 11 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Katsuhiko Sano, Jonni Virtema We study model and frame definability of various modal logics. Let denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We show that a class of Kripke models is definable in if and only if the class is elementary and closed under disjoint unions and surjective bisimulations. We also characterise the definability of in the spirit of the well-known Goldblatt–Thomason theorem. We show that an elementary class F of Kripke frames is definable in if and only if F is closed under taking generated subframes and bounded morphic images, and reflects ultrafilter extensions and finitely generated subframes. In addition we study frame definability relative to finite transitive frames and give an analogous characterisation of -definability relative to finite transitive frames. Finally, we initiate the study of model and frame definability in team-based logics. We study (extended) modal dependence logic, (extended) modal inclusion logic, and modal team logic. We establish strict linear hierarchies with respect to model definability and frame definability, respectively. We show that, with respect to model and frame definability, the before mentioned team-based logics, except modal dependence logic, either coincide with or plain modal logic ML. Thus as a corollary we obtain model theoretic characterisation of model and frame definability for the team-based logics.This article subsumes and extends the conference articles [30] and [31].

Abstract: Publication date: Available online 11 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Fan Yang In this paper, we axiomatize the negatable consequences in dependence and independence logic by extending the systems of natural deduction of the logics given in [22] and [11]. We prove a characterization theorem for negatable formulas in independence logic and negatable sentences in dependence logic, and identify an interesting class of formulas that are negatable in independence logic. Dependence and independence atoms, first-order formulas belong to this class. We also demonstrate our extended system of independence logic by giving explicit derivations for Armstrong's Axioms and the Geiger-Paz-Pearl axioms of dependence and independence atoms.

Abstract: Publication date: Available online 11 April 2019Source: Annals of Pure and Applied LogicAuthor(s): J.A. Makowsky, E.V. Ravve, T. Kotek Graph polynomials are graph parameters invariant under graph isomorphisms which take values in a polynomial ring with a fixed finite number of indeterminates. We study graph polynomials from a model theoretic point of view. In this paper we distinguish between the graph theoretic (semantic) and the algebraic (syntactic) meaning of graph polynomials. Graph polynomials appear in the literature either as generating functions, as generalized chromatic polynomials, or as polynomials derived via determinants of adjacency or Laplacian matrices. We show that these forms are mutually incomparable, and propose a unified framework based on definability in Second Order Logic. We show that this comprises virtually all examples of graph polynomials with a fixed finite set of indeterminates. Finally we show that the location of zeros and stability of graph polynomials is not a semantic property. The paper emphasizes a model theoretic view. It gives a unified exposition of classical results in algebraic combinatorics together with new and some of our previously obtained results scattered in the graph theoretic literature.

Abstract: Publication date: Available online 11 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Raine Rönnholm In this paper we study the expressive power of k-ary exclusion logic, EXC[k], that is obtained by extending first order logic with k-ary exclusion atoms. It is known that without arity bounds exclusion logic is equivalent with dependence logic. By observing the translations, we see that the expressive power of EXC[k] lies in between k-ary and (k+1)-ary dependence logics. We will show that, at least in the case when k=1, both of these inclusions are proper.In a recent work by the author it was shown that k-ary inclusion-exclusion logic is equivalent with k-ary existential second order logic, ESO[k]. We will show that, on the level of sentences, it is possible to simulate inclusion atoms with exclusion atoms, and in this way express ESO[k]-sentences by using only k-ary exclusion atoms. For this translation we also need to introduce a novel method for “unifying” the values of certain variables in a team. As a consequence, EXC[k] captures ESO[k] on the level of sentences, and we obtain a strict arity hierarchy for exclusion logic. It also follows that k-ary inclusion logic is strictly weaker than EXC[k].Finally we use similar techniques to formulate a translation from ESO[k] to k-ary inclusion logic with an alternative strict semantics. Consequently, for any arity fragment of inclusion logic, strict semantics is strictly more expressive than lax semantics.

Abstract: Publication date: Available online 11 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Anselm Haak, Heribert Vollmer We study the class #AC0 of functions computed by constant-depth polynomial-size arithmetic circuits of unbounded fan-in addition and multiplication gates. No model-theoretic characterization for arithmetic circuit classes is known so far. Inspired by Immerman's characterization of the Boolean circuit class AC0, we remedy this situation and develop such a characterization of #AC0. Our characterization can be interpreted as follows: Functions in #AC0 are exactly those functions counting winning strategies in first-order model checking games. A consequence of our results is a new model-theoretic characterization of TC0, the class of languages accepted by constant-depth polynomial-size majority circuits.

Abstract: Publication date: Available online 10 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Anuj Dawar, Simone Severini, Octavio Zapata Two graphs are cospectral if their respective adjacency matrices have the same multi-set of eigenvalues. A graph is said to be determined by its spectrum if all graphs that are cospectral with it are isomorphic to it. We consider these properties in relation to logical definability. We show that any pair of graphs that are elementarily equivalent with respect to the three-variable counting first-order logic C3 are cospectral, and this is not the case with C2, nor with any number of variables if we exclude counting quantifiers. We also show that the class of graphs that are determined by their spectra is definable in partial fixed-point logic with counting. We relate these properties to other algebraic and combinatorial problems.

Abstract: Publication date: Available online 10 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Jukka Corander, Antti Hyttinen, Juha Kontinen, Johan Pensar, Jouko Väänänen Directed acyclic graphs (DAGs) constitute a qualitative representation for conditional independence (CI) properties of a probability distribution. It is known that every CI statement implied by the topology of a DAG is witnessed over it under a graph-theoretic criterion of d-separation. Alternatively, all such implied CI statements are derivable from the local independencies encoded by a DAG using the so-called semi-graphoid axioms. We consider Labeled Directed Acyclic Graphs (LDAGs) modeling graphically scenarios exhibiting context-specific independence (CSI). Such CSI statements are modeled by labeled edges, where labels encode contexts in which the edge vanishes. We study the problem of identifying all independence statements implied by the structure and the labels of an LDAG. We show that this problem is coNP-hard for LDAGs and formulate a sound extension of the semi-graphoid axioms for the derivation of such implied independencies. Finally we connect our study to certain qualitative versions of independence ubiquitous in database theory and teams semantics.

Abstract: Publication date: Available online 9 April 2019Source: Annals of Pure and Applied LogicAuthor(s): Makoto Fujiwara, Tatsuji Kawai We compare Brouwer's bar theorem and Spector's bar recursion for the lowest type in the context of constructive reverse mathematics. To this end, we reformulate bar recursion as a logical principle stating the existence of a bar recursor for every function which serves as the stopping condition of bar recursion. We then show that the decidable bar induction is equivalent to the existence of a bar recursor for every continuous function from NN to N with a continuous modulus. We also introduce fan recursion, the bar recursion for binary trees, and show that the decidable fan theorem is equivalent to the existence of a fan recursor for every continuous function from {0,1}N to N with a continuous modulus. The equivalence for bar induction holds over the extensional version of intuitionistic arithmetic in all finite types augmented with the characteristic principles of Gödel's Dialectica interpretation. On the other hand, we show the equivalence for fan theorem without using such extra principles.

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.