proofs are *order-invariant*, i.e. they do not distinguish different linear orders on a given structure (see Section \[section:invariance\] for a precise definition).

First-order logic (${\ensuremath{\mathrm{FO}}\xspace}$) is a logic of great importance in model theory and, consequently, order-invariant ${{\ensuremath{\mbox{\sc FO}}\xspace}}$-sentences have been studied in the literature before, see e.g. [@GroheSchwentick2000; @BenediktSegoufin2009; @EickmeyerElberfeldHarwath2014], and the survey [@Schweikardt13].

It is well-known that the question whether an ${{\ensuremath{\mbox{\sc FO}}\xspace}}$-sentence is order-invariant is undecidable. Two possible remedies are to restrict either the class of structures or the logic. For the former case, it is known that order-invariance remains undecidable for colored directed paths [@BenediktSegoufin2009] and colored star graphs [@EickmeyerElberfeldHarwath2014].

In this article we study the decidability of invariance for the *two-variable fragment of first-order logic* (*two-variable logic* or ${\ensuremath{\mathrm{FO}^2}\xspace}$ for short). This fragment is reasonably expressive and yet its satisfiability and finite satisfiability problems are decidable [@Scott1962; @MortimerOn75]. As a query language, it has a strong connection to the XML query language XPATH on trees [@Marx2005]. Furthermore, many modal logics can be translated to ${\ensuremath{\mathrm{FO}^2}\xspace}$ and inherit its good algorithmic properties. Those applications as well as the inability of ${\ensuremath{\mathrm{FO}^2}\xspace}$ to express transitivity of a relation has led to an exhaustive study of the complexity 