first-order logic with equality FOL⁼ first-order logic with equality