---
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 (${\ensuremath{\mathrm{ESO}^2}\xspace}$) 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 ${\ensuremath{\mathrm{ESO}^2}\xspace}$ has been known. In addition, the finite satisfiability problem for ${\ensuremath{\mathrm{ESO}^2}\xspace}$ on structures with one linear order and its induced successor relation is shown to be decidable in non-deterministic exponential time.'
author:
- |
    Thomas Zeume\
    TU Dortmund University\
    `thomas.zeume@cs.tu-dortmund.de`
- |
    Frederik Harwath\
    Goethe Universität Frankfurt am Main\
    `harwath@cs.uni-frankfurt.de`
bibliography:
- 'bibliography.bib'
title: 'Order-Invariance of Two-Variable Logic is Decidable'
---

Introduction {#section:introduction}
============

Order-invariance plays a crucial role in several areas of finite model theory. In descriptive complexity theory, for example, various well-known results establish that a logic captures a complexity class on structures that are equipped with a linear order. Usually, in such results, the particular order on a given structure is not important. That is, the formulas constructed in the 