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.
New to topics? Read the docs here!