# Item

ITEM ACTIONSEXPORT

Released

Paper

#### Separateness of Variables - A Novel Perspective on Decidable First-Order Fragments

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

1911.11500.pdf

(Preprint), 573KB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Voigt, M. (2019). Separateness of Variables - A Novel Perspective on Decidable First-Order Fragments. Retrieved from http://arxiv.org/abs/1911.11500.

Cite as: https://hdl.handle.net/21.11116/0000-0005-8D56-C

##### Abstract

The classical decision problem, as it is understood today, is the quest for a

delineation between the decidable and the undecidable parts of first-order

logic based on elegant syntactic criteria. In this paper, we treat the concept

of separateness of variables and explore its applicability to the classical

decision problem. Two disjoint sets of first-order variables are separated in a

given formula if variables from the two sets never co-occur in any atom of that

formula. This simple notion facilitates extending many well-known decidable

first-order fragments significantly and in a way that preserves decidability.

We will demonstrate that for several prefix fragments, several guarded

fragments, the two-variable fragment, and for the fluted fragment. Altogether,

we will investigate nine such extensions more closely. Interestingly, each of

them contains the relational monadic first-order fragment without equality.

Although the extensions exhibit the same expressive power as the respective

originals, certain logical properties can be expressed much more succinctly. In

three cases the succinctness gap cannot be bounded using any elementary

function.

delineation between the decidable and the undecidable parts of first-order

logic based on elegant syntactic criteria. In this paper, we treat the concept

of separateness of variables and explore its applicability to the classical

decision problem. Two disjoint sets of first-order variables are separated in a

given formula if variables from the two sets never co-occur in any atom of that

formula. This simple notion facilitates extending many well-known decidable

first-order fragments significantly and in a way that preserves decidability.

We will demonstrate that for several prefix fragments, several guarded

fragments, the two-variable fragment, and for the fluted fragment. Altogether,

we will investigate nine such extensions more closely. Interestingly, each of

them contains the relational monadic first-order fragment without equality.

Although the extensions exhibit the same expressive power as the respective

originals, certain logical properties can be expressed much more succinctly. In

three cases the succinctness gap cannot be bounded using any elementary

function.