Two-variable logic

Two-variable logic, also known as \( \text{FO}^2 \) or \( \text{FO}_2 \), is a fragment of first-order logic that restricts the use of variables to only two kinds, often denoted as \( x \) and \( y \). In this logical system, formulas can contain only two distinct variable names, regardless of the number of predicates or functions involved.