WFF

WFF stands for well-formed formula in formal logic. It refers to strings of symbols that are constructed according to the formation rules of a given formal language. Well-formed formulas are syntactically correct expressions that can be subjected to truth-functional evaluation or used in formal proofs. The term is common in mathematical logic, computer science, and related fields.

In propositional logic, the basic building blocks are atomic propositions such as P, Q, R. If A and B are WFFs, then (A ∧ B), (A ∨ B), (A → B), and ¬A are also WFFs. Parentheses are typically used to remove ambiguity, although some systems rely on defined operator precedence.

In first-order logic, the construction rules extend to predicates, terms, and quantifiers. If P is an n-ary predicate and t1, ..., tn are terms, then P(t1, ..., tn) is a WFF. If φ is a WFF, then ∀x φ and ∃x φ are WFFs. If φ and ψ are WFFs, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ) are WFFs, with parentheses clarifying structure.

WFFs are central to formal reasoning because they separate syntax from semantics. They are the objects of inference rules, truth-functional analysis, and automated theorem proving. Only WFFs can be reliably manipulated within a formal system, while their truth values are determined by interpretations or models that assign meanings to the symbols.

Examples include: P is a WFF; P ∧ Q is a WFF; ¬(P ∨ Q) is a WFF; ∀x (P(x) → Q(x)) is a WFF. P ∧ is not a WFF, and ambiguous strings without proper structure fail to be well-formed.