Order-invariance of two-variable logic is decidable

DOI10.1145/2933575.2933594MaRDI QIDQ4635945zbMATH OpenOpenAlexWikidataFDO

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)

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

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)

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.

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

Cited in

(3)

• Finite satisfiability for two‐variable, first‐order logic with one transitive relation is decidable
• scientific article; zbMATH DE number 7566055 (Why is no real title available?)
• 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)