In → predicate logic, a → well-formed formula with one or more → free occurrences of → variables.
→ open; → wff.
