Undecidability results on two-variable logics
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 \(\varepsilon\)-operator. In fact all these extensions of \(L^2\) prove to be undecidable both for satisfiability, and for satisfiability in finite models. Moreover most of them are hard for \(\Sigma^1_1\), the first level of the analytical hierarchy, and thus have a much higher degree of undecidability than first-order logic.
- Undecidability results on two-variable logics
- Undecidability of First-Order Intuitionistic and Modal Logics with Two variables
- Undecidability of modal and intermediate first-order logics with two individual variables
- Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
- Undecidability of propositional separation logic and its neighbours
- Undecidable properties of extensions of provability logic. II
- The undecidability of second order multiplicative linear logic
- scientific article; zbMATH DE number 1114339
- Undecidable properties of extensions of the logic of provability
- Undecidability of multiplicative subexponential logic
- Two results in negation-free logic
- On logics with two variables
- One-variable logic meets Presburger arithmetic
- On transitive modal many-valued logics
- A logic of reachable patterns in linked data-structures
- Computational complexity of theories of a binary predicate with a small number of variables
- Two variable first-order logic over ordered domains
- Undecidable first-order theories of affine geometries
- Small substructures and decidability issues for first-order logic with two variables
- Syllogistic logic with ``most
- Two-Variable Separation Logic and Its Inner Circle
- On the expressive power of query languages for matrices
- Undecidability of First-Order Intuitionistic and Modal Logics with Two variables
- Logics for two fragments beyond the syllogistic boundary
- Undecidability of modal and intermediate first-order logics with two individual variables
- Syllogistic logic with comparative adjectives
- Separation logics and modalities: a survey
- Monadic Second-Order Logic and Transitive Closure Logics over Trees
- On the Restraining Power of Guards
- Undecidability results on two-variable logics
- Finite satisfiability of unary negation fragment with transitivity
- Expressive completeness of separation logic with two variables and no separating conjunction
- Guarded negation
- Guarded negation
- Бинарный предикат, транзитивное замыкание, две-три переменные: сыграем в домино?
- INTERLEAVING LOGIC AND COUNTING
- Two variable logic with ultimately periodic counting
- Two variable logic with ultimately periodic counting
- The triguarded fragment with transitivity
- On homogeneous models of fluted languages
This page was built for publication: Undecidability results on two-variable logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1306795)
