Complete axiomatizations of fragments of monadic second-order logic on finite trees

DOI10.2168/LMCS-8(4:12)2012MaRDI QIDQ4899112zbMATH OpenOpenAlexFDO

Authors Amélie Gheerbrant, Balder ten Cate

Publication date 7 January 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.2620

zbMATH Keywords

treescompleteness theoremaxiomatizationHenkin semanticsEhrenfeucht-Fraïssé gameFeferman-Vaught theoremfragments of MSO

Mathematics Subject Classification ID

Data structures (68P05) Logic in computer science (03B70) Second- and higher-order model theory (03C85)

Abstract: We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., each formula that is valid on all finite trees is provable using our axioms. As a backdrop to our positive results, on arbitrary structures, the logics that we study are known to be non-recursively axiomatizable.

Recommendations

• Complete Axiomatizations of MSO, FO(TC 1 ) and FO(LFP 1 ) on Finite Trees
• A first-order axiomatization of the theory of finite trees
• Monadic second-order logic on tree-like structures
• Linguistics, Logic and Finite Trees
• Monadic second order logic on tree-like structures

Cited in

(15)

• A first-order axiomatization of the theory of finite trees
• Recursive axiomatisations from separation properties
• On the completeness and the decidability of strictly monadic second‐order logic
• A complete axiomatization of MSO on infinite trees
• Complete Axiomatizations of MSO, FO(TC 1 ) and FO(LFP 1 ) on Finite Trees
• Monadic Second-Order Logic and Transitive Closure Logics over Trees
• scientific article; zbMATH DE number 7269253 (Why is no real title available?)
• scientific article; zbMATH DE number 2086419 (Why is no real title available?)
• Finitistic proofs of 0-1 laws for fragments of second-order logic
• A model theoretic proof of completeness of an axiomatization of monadic second-order logic on infinite words
• Existential monadic second order logic on random rooted trees
• Approximating trees as coloured linear orders and complete axiomatisations of some classes of trees
• Logics and Automata for Totally Ordered Trees
• A model-theoretic characterization of monadic second order logic on infinite words
• Monadic second order logic on tree-like structures

Describes a project that uses

Uses Software

• XPath

This page was built for publication: Complete axiomatizations of fragments of monadic second-order logic on finite trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4899112)