Well-Formed Formulas

Well-formed Formulas (WFFs) of Propositional Logic

Propositional logic expresses the logical form of compound propositions by means of a symbolic language. This language has a precise syntax-rules that determine which symbol strings count as meaningful formulas. Any expression that obeys these syntactic rules is called a well-formed formula (abbreviated WFF).

Basic symbols

• Propositional variables: capital letters such as A, B, C, ... represent atomic propositions.
• Logical connectives: common symbols are ~ (negation), • (conjunction, AND), ∨ (disjunction, OR), ⊃ (conditional, IF ... THEN), and ≡ (biconditional, EQUIVALENT).
• Parentheses: used to indicate the grouping (scope) of connectives and operands.

Formation rules (strict parenthesis convention)

The syntax can be given informally by three formation rules. Under the strict convention we always keep explicit parentheses.

1. Any capital letter by itself is a WFF (an atomic WFF).
2. If φ is a WFF then ~φ is a WFF (negation of a WFF is a WFF).
3. If φ and ψ are WFFs then (φ • ψ), (φ ∨ ψ), (φ ⊃ ψ), and (φ ≡ ψ) are WFFs. The resulting expression must be enclosed in parentheses.

Note: Some textbooks add a fourth rule allowing omission of parentheses when no ambiguity arises. This simplifies writing but complicates the syntax. Here we follow the stricter rule of always using parentheses to avoid ambiguity.

Formal (recursive) definition

The formation rules above are naturally expressed as a recursive definition:

• Basis: Every propositional variable (A, B, C, ...) is a WFF.
• Induction: If φ is a WFF then ~φ is a WFF. If φ and ψ are WFFs then (φ ◦ ψ) is a WFF for each binary connective ◦ in {•, ∨, ⊃, ≡}.
• Closure: Only formulas obtained by finitely many applications of these rules are WFFs.

Main connective, components and scope

• Main connective: The last connective introduced when building a WFF is called its main connective. It determines the overall logical form: if the main connective is ~ the formula is a negation; if it is • it is a conjunction, and so on.
• Components (or component propositions): The immediate subformulas joined by the main connective. For a binary main connective, the two components are its left and right operands.
• In a conjunction the components are called conjuncts. In a disjunction they are disjuncts. In a conditional the left component is the antecedent and the right component is the consequent.
• Scope of a connective refers to the part of the formula over which that connective has authority (the subformula whose main connective is that connective).

Examples

Here are several correct WFFs and brief explanations of how they are formed.

• (A • ~B) is a conjunction because its main connective is the dot. The components (conjuncts) are A and ~B.
• (~A ∨ (B ≡ C)) is a disjunction because its main connective is the wedge. The disjuncts are ~A and (B ≡ C). The right disjunct itself is a biconditional whose components are B and C.
• ((A ∨ B) ⊃ (C • D)) is a conditional because its main connective is the horseshoe. The antecedent is (A ∨ B) and the consequent is (C • D).

Non-well-formed expressions

Strings of symbols that do not follow the formation rules are not WFFs. Typical problems include missing connectives, missing parentheses, misplaced connectives, or incorrect application of the unary connective.

• Examples of ill-formed strings: A B (no connective between atomic symbols), A ∨ ∨ B (two binary connectives in succession), (A • B (missing closing parenthesis), ~•A (binary connective used where a unary is required).
• To determine whether a string is well formed, try to parse it according to the formation rules: locate a valid main connective and verify its components are themselves WFFs; if you cannot, the string is not a WFF.

Determining the main connective (practical method)

• Scan the formula from left to right counting parentheses (increment on '(', decrement on ')').
• The main binary connective is the binary connective encountered at the outermost parenthesis level (when the parenthesis counter returns to the level that encloses the whole formula) that connects two properly parenthesised subformulas.
• For a formula beginning with ~, that ~ is the main connective only if it applies to the entire remainder and that remainder is itself a WFF.

Parse trees and structure

Any WFF can be represented by a parse tree (syntax tree) in which internal nodes are connectives and leaves are atomic propositions. The parse tree makes clear the main connective (the root) and the hierarchical structure of components (subtrees). Building parse trees helps to:

• Identify the scope of each connective.
• Construct truth-tables by evaluating from leaves upward.
• Formally prove properties by structural induction on formula complexity.

Why WFFs matter

• Only WFFs have well-defined truth-values under an assignment of truth to atomic variables; truth-value evaluation and semantic concepts (satisfiability, tautology, contradiction) presuppose well-formedness.
• Formal proofs, syntactic transformations (such as converting to normal forms), and algorithmic manipulations (parsers, automated theorem provers) operate on WFFs.
• Maintaining strict parentheses and formation rules avoids ambiguity in interpretation-essential in rigorous reasoning and computation.

Concluding remarks

Strictly following the formation rules yields a clear and unambiguous class of expressions-WFFs-on which logical semantics and proof theory are built. When writing or reading propositional formulas, always check atomic status, proper use of unary and binary connectives, and correct parenthesisation. Use parse trees or the practical parenthesis-counting method to identify main connectives and verify well-formedness.