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

DOI10.2168/LMCS-8(4:12)2012zbMATH Open1261.03111arXiv1210.2620OpenAlexW2101754569MaRDI QIDQ4899112FDOQ4899112

Authors: Amélie Gheerbrant, Balder ten Cate 

Publication date: 7 January 2013

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

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.

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

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

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)

Cited In (11)

• On the completeness and the decidability of strictly monadic second‐order logic
• Title not available (Why is that?)
• Existential monadic second order logic on random rooted trees
• Monadic Second-Order Logic and Transitive Closure Logics over Trees
• Logics and Automata for Totally Ordered Trees
• A MODEL-THEORETIC CHARACTERIZATION OF MONADIC SECOND ORDER LOGIC ON INFINITE WORDS
• A first-order axiomatization of the theory of finite trees
• Title not available (Why is that?)
• 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
• Complete Axiomatizations of MSO, FO(TC 1 ) and FO(LFP 1 ) on Finite Trees

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)