WFFs

Well-formed formulas, abbreviated WFFs, are the strings that constitute the syntactically valid formulas of a formal language in logic. They are built from a given vocabulary, which may include propositional variables or predicate symbols, along with logical connectives and, in the case of first-order logic, quantifiers. The formation rules specify how to combine symbols into larger formulas, and only strings that follow these rules count as WFFs.

In propositional logic, WFFs are formed from atomic propositions such as p, q, r. If φ and ψ are WFFs, then ¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), and (φ ↔ ψ) are also WFFs. Parentheses are commonly used to disambiguate structure. Examples of WFFs include p, ¬p, (p ∧ q), and ((p ∨ r) → q). Invalid examples include ∧p, (p ∨), or p ∨ (q ∧) because they violate the formation rules.

In first-order logic, WFFs incorporate predicates and terms. An atomic WFF is something like P(a) or R(x, f(y)). If φ and ψ are WFFs, then ¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), and (φ ↔ ψ) are WFFs. If x is a variable and φ is a WFF, then ∀x φ and ∃x φ are WFFs. A sentence is a WFF with no free variables; otherwise the formula has free variables. Example: ∀x (P(x) → ∃y Q(y)) is a WFF sentence; P(x) ∧ Q(y) is a WFF but has free variables unless x and y are bound.

WFFs are central to formal logic, underpinning syntax, semantics, proofs, and automated reasoning. They enable precise definition of truth conditions, validity, and satisfiability, and are analyzed via parse trees, substitutions, and variable binding concepts.