Well-Formed Formulas in Set Theory: WFFs Explained Clearly

What Is a Well-Formed Formula in Set Theory?

A well-formed formula (wff) in set theory is a string of symbols built strictly from the alphabet of set theory (quantifiers, connectives, brackets, equality, and the element-of symbol) according to a fixed set of formation rules. This formal definition, following the treatment in Hrbacek and Jech’s set theory text, matters because it draws a hard line between statements mathematics can reason about and vague English statements that lead to paradoxes such as Berry’s paradox.

Key Takeaways

• The alphabet of set theory consists of eleven logical symbols: universal quantifier, existential quantifier, and, or, not, implies, if and only if, left bracket, right bracket, equality, and element-of.
• A wff is built from four formation rules, starting from atomic formulas of the form (x_n in x_m) or (x_n = x_m).
• The logical system used has six logical axioms plus the ZFC axioms, and exactly one inference rule: modus ponens.
• Symbols such as or, and, if-and-only-if, and the existential quantifier are not primitive; they are defined as abbreviations built from not, implies, and the universal quantifier.
• Berry’s paradox arises because a phrase like “cannot be defined with less than 1000 letters” cannot be expressed as a wff, which is precisely why the formal system avoids the paradox.

Why Set Theory Needs a Formal Alphabet

Hrbacek and Jech’s set theory text does not give a full formal definition of what a “property” is, since that topic belongs to mathematical logic proper. Providing a precise definition matters because informal reasoning about properties can produce contradictions, so set theory restricts itself to a fixed alphabet and a fixed grammar for building formulas.

An alphabet, in this formal sense, is the complete list of symbols permitted when writing any theorem, definition, or proof in set theory. In principle, every theorem or proof could be written using only these symbols, though in practice mathematicians write in a mix of symbols and natural language because writing everything in raw symbols would be extremely inconvenient.

The Logical Symbols of Set Theory

The alphabet of set theory contains the following logical symbols:

Logical symbols used in the formal alphabet of set theory

Symbol	Name
$\forall$	universal quantifier
$\exists$	existential quantifier
$\wedge$	and
$\vee$	or
$\neg$	not
$\rightarrow$	implies
$\leftrightarrow$	if and only if
(	left bracket
)	right bracket
=	equality
$\in$	element of

Beyond these fixed symbols, the alphabet also includes an unlimited supply of variables, denoted here as $x_1,~x_2,~x_3,\ldots$, though other naming schemes are equally valid.

How Well-Formed Formulas (WFFs) Are Built

A well-formed formula, abbreviated wff, is defined recursively by the following four rules:

1. Every expression of the form $(x_n\in x_m)$ or $(x_n = x_m)$ is a wff. These are the atomic formulas.
2. If $\psi$ is a wff, then $(\neg \psi)$ is also a wff.
3. If $\psi$ and $\varphi$ are wffs, then $(\psi\wedge \varphi)$, $(\psi\vee \varphi)$, $\psi\rightarrow \varphi$, and $(\psi\leftrightarrow \varphi)$ are also wffs.
4. If $\psi$ is a wff and $x$ is a variable, then $(\forall x\psi)$ and $(\exists x\psi)$ are also wffs.

For example, $(\forall x_1(x_1=x_1))$ and $(\exists x_3((x_3=x_3)\wedge (\neg(x_3\in x_4))))$ both satisfy these four rules and are therefore wffs. By contrast, $\neg\wedge x_5=$ does not satisfy the rules and is not a wff.

Bound Versus Free Variables

A variable $x_n$ inside a wff $\psi$ is called bound if it falls within the scope of a quantifier applied to that same variable; otherwise it is called free. In the wff $(\forall x_1(x_1=x_1))$, the quantifier $\forall x_1$ makes $x_1$ a bound variable throughout the formula.

In the wff $(\exists x_3((x_3=x_3)\wedge (\neg(x_3\in x_4))))$, the quantifier $\exists x_3$ makes $x_3$ bound, while $x_4$ remains free because no quantifier $\forall x_4$ or $\exists x_4$ appears anywhere in the formula.

The fourth formation rule for wffs is often stated with the additional requirement that $x$ be a free variable of $\psi$, and this requirement is always followed in practice. The formal definition, however, can be stated without this requirement and still work correctly.

Axioms and the Single Inference Rule

Determining which wffs count as true requires a fixed collection of axioms together with an inference rule. The full axiom set combines the logical axioms below with the ZFC axioms, which are covered separately in later material.

The logical axioms used are:

1. For any wffs $\psi$ and $\varphi$: $(\psi\rightarrow (\varphi\rightarrow \psi))$ is true.
2. For any wffs $\psi$, $\varphi$, $\chi$: $((\psi\rightarrow (\varphi\rightarrow \chi))\rightarrow ((\psi\rightarrow \varphi)\rightarrow (\psi\rightarrow \chi)))$ is true.
3. For any wff $\psi$: $((\neg(\neg \psi))\rightarrow \psi)$ is true.
4. For any wffs $\varphi$ and $\psi$ and variable $x$: $((\forall x(\varphi\rightarrow \psi))\rightarrow ((\forall x\varphi)\rightarrow (\forall x \psi)))$ is true.
5. For any wff $\varphi$ and variable $x$: $(\varphi\rightarrow (\forall x \varphi))$ is true.
6. For any wff $\varphi$, variable $x$ free in $\varphi$, variable $y$, and $\varphi’$ formed by replacing every occurrence of $x$ with $y$: $((\forall x \varphi)\rightarrow \varphi’)$ is true.

The symbols $\wedge$, $\vee$, $\exists$ and $\leftrightarrow$ have no dedicated axioms of their own, though a system could have been built that way. Instead each is defined as an abbreviation: $(\varphi \vee \psi)$ abbreviates $((\neg\varphi)\rightarrow \psi)$; $(\varphi \wedge \psi)$ abbreviates $(\neg ((\neg \varphi)\vee (\neg \psi)))$; $(\varphi \leftrightarrow \psi)$ abbreviates $((\psi \rightarrow \varphi)\wedge (\varphi\rightarrow \psi))$; and $(\exists x\varphi)$ abbreviates $(\neg(\forall x (\neg \varphi)))$.

The system uses exactly one inference rule, called modus ponens. Modus ponens states that if $\varphi$ is a true wff and $(\varphi\rightarrow \psi)$ is a true wff, then $\psi$ is also a true wff.

What Counts as a Theorem and a Proof

A theorem $\varphi$ is any wff for which a proof exists. A proof of $\varphi$ is a finite sequence of wffs $\varphi_1, \varphi_2, \varphi_3, \ldots, \varphi_n$ such that $\varphi_n = \varphi$, and each $\varphi_k$ in the sequence is either a logical axiom, a ZFC axiom, or follows from earlier wffs in the sequence by modus ponens.

Why Textbook Proofs Look Different From Formal Proofs

No mathematician actually writes theorems in the fully formal symbolic language or provides proofs strictly matching the definition above. Proofs in textbooks are written in English words and sentences because human readers find English arguments easier to follow than a rigorous sequence of raw symbols.

The formal definitions of theorem and proof should be treated as an ideal rather than a practical template. Textbook proofs are not ideal in this technical sense, but they are convincing evidence that an ideal, fully formal proof could be constructed if needed. Every result in Hrbacek and Jech, and in other set theory texts, can in principle be given such an ideal proof. The Metamath project, available at metamath.org, carries out exactly this kind of fully formal proof-writing, though the result is tedious and difficult to read.

Readers are not expected to worry about the exact formal nature of formulas or about constructing ideal proofs when working through introductory set theory material. These formal foundations are background; a dedicated mathematical logic textbook covers them in depth.

Why the WFF Definition Matters: Berry’s Paradox

Defining precisely which expressions count as wffs and which do not is an important safeguard in mathematics because it rules out several classic paradoxes of natural language.

“Let n be the smallest natural number that cannot be defined with less than 1000 letters in the English language.”

The word “one” takes three letters, so it is not n. The word “hundred” takes seven letters, so it is not n either. Fewer than approximately $30^{1000}$ numbers can be expressed using fewer than 1000 letters, so some number must exist that cannot be expressed that way, and n is defined as the smallest such number. But the description of n just given uses fewer than 1000 letters, meaning n has now been described in fewer than 1000 letters. This is Berry’s paradox.

The formal system of wffs resolves this paradox directly. The sentence “n cannot be defined with less than 1000 letters in the English language” cannot be written as a wff at all, because the phrase “can be defined” has no counterpart in the formal language of wffs. Requiring every mathematical statement to be expressible as a wff, rather than as an arbitrary English sentence, is precisely what prevents this kind of vague or self-referential statement from entering the system.

Glossary

• Well-formed formula (wff): a string of symbols from the alphabet of set theory built according to the four formation rules described above.
• Bound variable: a variable that falls within the scope of a quantifier applying to it.
• Free variable: a variable not within the scope of any quantifier applying to it.
• Modus ponens: the inference rule stating that from a true wff $\varphi$ and a true wff $(\varphi\rightarrow \psi)$, one may conclude $\psi$ is true.
• Logical axioms: the six foundational true wffs listed above, used alongside the ZFC axioms to build proofs.

Frequently Asked Questions

What is the difference between the alphabet of set theory and a well-formed formula?

The alphabet is the fixed list of allowable symbols, quantifiers, connectives, brackets, equality, element-of, and variables. A well-formed formula is a specific string built from these symbols according to the four formation rules, starting from atomic formulas like (x_n = x_m).

Why are or, and, if-and-only-if, and the existential quantifier not primitive symbols?

The formal system only assigns axioms to not, implies, and the universal quantifier. The other connectives, or, and, if-and-only-if, and the existential quantifier, are defined as abbreviations built from these primitives, which keeps the axiom system smaller without losing any expressive power.

What is modus ponens?

Modus ponens is the single inference rule used in this system. It states that if a wff $\varphi$ is true and the wff $(\varphi\rightarrow \psi)$ is true, then $\psi$ must also be true. It is the only rule needed alongside the axioms to build proofs.

Do mathematicians actually write proofs using only wffs?

No. Proofs in textbooks, including Hrbacek and Jech, are written in English because that is easier for human readers to follow. The formal definition of a proof as a sequence of wffs derived by modus ponens is an ideal that textbook proofs are meant to convincingly approximate, not a practical writing format.

How does the wff system resolve Berry’s paradox?

Berry’s paradox relies on the phrase “cannot be defined with less than 1000 letters,” which cannot be translated into a wff because “can be defined” has no formal counterpart in the alphabet of set theory. Since the paradoxical statement is not a wff, it simply falls outside the system and causes no contradiction.

Where can a fully formal, ideal proof be found?

The Metamath project, at metamath.org, contains fully formal proofs of results including those found in standard set theory texts. These proofs use only the raw symbolic language rather than English exposition, which makes them rigorous but tedious to read.