"Iff" is not expressible in independence-friendly logic

TL;DR

This paper demonstrates that independence-friendly logic lacks the property of expressing logical equivalence between formulas through a biconditional, unlike ordinary first-order logic.

Contribution

It proves that independence-friendly logic cannot express the equivalence of formulas with a single formula, highlighting a fundamental difference from first-order logic.

Findings

Independence-friendly logic does not have the property that  iff  is true in a structure.

This shows a key limitation of independence-friendly logic compared to first-order logic.

The result clarifies the expressive boundaries of independence-friendly logic.

Abstract

Ordinary first-order logic has the property that two formulas \phi and \psi have the same meaning in a structure if and only if the formula ``\phi iff \psi'' is true in the structure. We prove that independence-friendly logic does not have this property.