Order-invariance of two-variable logic is decidable

DOI10.1145/2933575.2933594zbMATH Open1394.03017arXiv1604.05843OpenAlexW2335953814WikidataQ130847046 ScholiaQ130847046MaRDI QIDQ4635945FDOQ4635945

Authors: Thomas Zeume, Frederik Harwath 

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: It is shown that order-invariance of two-variable first-logic is decidable in the finite. This is an immediate consequence of a decision procedure obtained for the finite satisfiability problem for existential second-order logic with two first-order variables ($mathrm{ESO}^2$) on structures with two linear orders and one induced successor. We also show that finite satisfiability is decidable on structures with two successors and one induced linear order. In both cases, so far only decidability for monadic $mathrm{ESO}^2$ has been known. In addition, the finite satisfiability problem for $mathrm{ESO}^2$ on structures with one linear order and its induced successor relation is shown to be decidable in non-deterministic exponential time.

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

Recommendations

• Two variables and two successors
• Decidability issues for two-variable logics with several linear orders
• Two-variable logic with two order relations
• Two variable first-order logic over ordered domains
• Small substructures and decidability issues for first-order logic with two variables

zbMATH Keywords

linear ordertwo-variable logicfinite satisfiabilityorder invariancesuccessor relation

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25)

Cited In (3)

• Title not available (Why is that?)
• Finite satisfiability for two‐variable, first‐order logic with one transitive relation is decidable
• Two-Variable Logic over Countable Linear Orderings

This page was built for publication: Order-invariance of two-variable logic is decidable

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