19 found
Order:
  1.  14
    Modal Characterisation Theorems Over Special Classes of Frames.Anuj Dawar & Martin Otto - 2010 - Annals of Pure and Applied Logic 161 (1):1-42.
    We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem’s theorem, which says that a first-order formula is invariant under bisimulation if, and only if, it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  2.  14
    Modal and Guarded Characterisation Theorems Over Finite Transition Systems.Martin Otto - 2004 - Annals of Pure and Applied Logic 130 (1-3):173-205.
    We explore the finite model theory of the characterisation theorems for modal and guarded fragments of first-order logic over transition systems and relational structures of width two. A new construction of locally acyclic bisimilar covers provides a useful analogue of the well known tree-like unravellings that can be used for the purposes of finite model theory. Together with various other finitary bisimulation respecting model transformations, and Ehrenfeucht–Fraïssé game arguments, these covers allow us to upgrade finite approximations for full bisimulation equivalence (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  3.  10
    Inquisitive Bisimulation.Ivano Ciardelli & Martin Otto - 2021 - Journal of Symbolic Logic 86 (1):77-109.
    Inquisitive modal logic, InqML, is a generalisation of standard Kripke-style modal logic. In its epistemic incarnation, it extends standard epistemic logic to capture not just the information that agents have, but also the questions that they are interested in. Technically, InqML fits within the family of logics based on team semantics. From a model-theoretic perspective, it takes us a step in the direction of monadic second-order logic, as inquisitive modal operators involve quantification over sets of worlds. We introduce and investigate (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  4.  53
    Finite Conformal Hypergraph Covers and Gaifman Cliques in Finite Structures.Ian Hodkinson & Martin Otto - 2003 - Bulletin of Symbolic Logic 9 (3):387-405.
    We provide a canonical construction of conformal covers for finite hypergraphs and present two immediate applications to the finite model theory of relational structures. In the setting of relational structures, conformal covers serve to construct guarded bisimilar companion structures that avoid all incidental Gaifman cliques-thus serving as a partial analogue in finite model theory for the usually infinite guarded unravellings. In hypergraph theoretic terms, we show that every finite hypergraph admits a bisimilar cover by a finite conformal hypergraph. In terms (...)
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  5.  23
    Undecidability Results on Two-Variable Logics.Erich Grädel, Martin Otto & Eric Rosen - 1999 - Archive for Mathematical Logic 38 (4-5):313-354.
    It is a classical result of Mortimer that $L^2$ , first-order logic with two variables, is decidable for satisfiability. We show that going beyond $L^2$ by adding any one of the following leads to an undecidable logic:– very weak forms of recursion, viz.¶(i) transitive closure operations¶(ii) (restricted) monadic fixed-point operations¶– weak access to cardinalities, through the Härtig (or equicardinality) quantifier¶– a choice construct known as Hilbert's $\epsilon$ -operator.In fact all these extensions of $L^2$ prove to be undecidable both for satisfiability, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  6.  18
    Expressive Completeness Through Logically Tractable Models.Martin Otto - 2013 - Annals of Pure and Applied Logic 164 (12):1418-1453.
    How can we prove that some fragment of a given logic has the power to define precisely all structural properties that satisfy some characteristic semantic preservation condition? This issue is a fundamental one for classical model theory and applications in non-classical settings alike. While methods differ greatly, and while the classical methods can usually not be matched for instance in the setting of finite model theory, this note surveys some interesting commonality revolving around the use and availability of tractable representatives (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  7. An Interpolation Theorem.Martin Otto - 2000 - Bulletin of Symbolic Logic 6 (4):447-462.
    Lyndon's Interpolation Theorem asserts that for any valid implication between two purely relational sentences of first-order logic, there is an interpolant in which each relation symbol appears positively (negatively) only if it appears positively (negatively) in both the antecedent and the succedent of the given implication. We prove a similar, more general interpolation result with the additional requirement that, for some fixed tuple U of unary predicates U, all formulae under consideration have all quantifiers explicitly relativised to one of the (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  8. The Expressive Power of Fixed-Point Logic with Counting.Martin Otto - 1996 - Journal of Symbolic Logic 61 (1):147-176.
    We study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count. To this end an isomorphism preserving (`generic') model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation of the relational vs. the arithmetical (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  9.  55
    Two Variable First-Order Logic Over Ordered Domains.Martin Otto - 2001 - Journal of Symbolic Logic 66 (2):685-702.
    The satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO 2 over ordered, respectively wellordered, domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  10.  28
    Small Substructures and Decidability Issues for First-Order Logic with Two Variables.Emanuel Kieroński & Martin Otto - 2012 - Journal of Symbolic Logic 77 (3):729-765.
    We study first-order logic with two variables FO² and establish a small substructure property. Similar to the small model property for FO² we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO² under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO² has the finite model property and is complete for non-deterministic (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  3
    A Lindström Characterisation of the Guarded Fragment and of Modal Logic with a Global Modality.Martin Otto & Robert Piro - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 273-287.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  12.  71
    Bounded Variable Logics: Two, Three, and More. [REVIEW]Martin Otto - 1999 - Archive for Mathematical Logic 38 (4-5):235-256.
    Consider the bounded variable logics $L^k_{\infty\omega}$ (with k variable symbols), and $C^k_{\infty\omega}$ (with k variables in the presence of counting quantifiers $\exists^{\geq m}$ ). These fragments of infinitary logic $L_{\infty\omega}$ are well known to provide an adequate logical framework for some important issues in finite model theory. This paper deals with a translation that associates equivalence of structures in the k-variable fragments with bisimulation equivalence between derived structures. Apart from a uniform and intuitively appealing treatment of these equivalences, this approach (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  13. A First-Order Framework for Inquisitive Modal Logic.Silke Meissner & Martin Otto - forthcoming - Review of Symbolic Logic:1-23.
    We present a natural standard translation of inquisitive modal logic $\mathrm{InqML}$ into first-order logic over the natural two-sorted relational representations of the intended models, which captures the built-in higher-order features of $\mathrm{InqML}$. This translation is based on a graded notion of flatness that ties the inherent second-order, team-semantic features of $\mathrm{InqML}$ over information states to subsets or tuples of bounded size. A natural notion of pseudo-models, which relaxes the non-elementary constraints on the intended models, gives rise to an elementary, purely (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  14.  7
    Canonization for Two Variables and Puzzles on the Square.Martin Otto - 1997 - Annals of Pure and Applied Logic 85 (3):243-282.
    We consider infinitary logic with only two variable symbols, both with and without counting quantifiers, i.e. L2 L∞ω2 and C2 L∞ω2mεω. The main result is that finite relational structures admit canonization with respect to L2 and C2: there are polynomial time com putable functors mapping finite relational structures to unique representatives of their equivalence class with respect to indistinguishability in either of these logics. In fact we exhibit in verses to the natural invariants that characterize structures up to L2- or (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  15.  17
    Bisimulation and Coverings for Graphs and Hypergraphs.Martin Otto - 2013 - In Kamal Lodaya (ed.), Logic and its Applications. Springer. pp. 5--16.
  16.  8
    EM Constructions for a Class of Generalized Quantifiers.Martin Otto - 1992 - Archive for Mathematical Logic 31 (5):355-371.
    We consider a class of Lindström extensions of first-order logic which are susceptible to a natural Skolemization procedure. In these logics Ehrenfeucht Mostowski (EM) functors for theories with arbitrarily large models can be obtained under suitable restrictions. Characteristic dependencies between algebraic properties of the quantifiers and the maximal domains of EM functors are investigated.Results are applied to Magidor Malitz logic,L(Q <ω), showing e.g. its Hanf number to be equal to ℶω(ℵ1) in the countably compact case. Using results of Baumgartner, the (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  17.  35
    Epsilon-Logic is More Expressive Than First-Order Logic Over Finite Structures.Martin Otto - 2000 - Journal of Symbolic Logic 65 (4):1749-1757.
    There are properties of finite structures that are expressible with the use of Hilbert's ε-operator in a manner that does not depend on the actual interpretation for ε-terms, but not expressible in plain first-order. This observation strengthens a corresponding result of Gurevich, concerning the invariant use of an auxiliary ordering in first-order logic over finite structures. The present result also implies that certain non-deterministic choice constructs, which have been considered in database theory, properly enhance the expressive power of first-order logic (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  18.  24
    Automorphism Properties of Stationary Logic.Martin Otto - 1992 - Journal of Symbolic Logic 57 (1):231-237.
    By means of an Ehrenfeucht-Mostowski construction we obtain an automorphism theorem for a syntactically characterized class of Laa-theories comprising in particular the finitely determinate ones. Examples of Laa-theories with only rigid models show this result to be optimal with respect to a classification in terms of prenex quantifier type: Rigidity is seen to hinge on quantification of type $\ldots\forall\ldots\mathbf{\operatorname{stat}}\ldots$ permitting of the parametrization of families of disjoint stationary systems by the elements of the universe.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  19.  1
    Pebble Games and Linear Equations.Martin Grohe & Martin Otto - 2015 - Journal of Symbolic Logic 80 (3):797-844.