Formal Syntax and WFFs in Set Theory (Hrbacek-Jech)

Hrbacek–Jech Chapter 1.2: Formal Language and WFFs

Introduction

Hrbacek and Jech do not go into full detail about what a property is formally. This is a part of mathematical logic, but it is important here to give a precise definition of what a property is.

Alphabet of Set Theory

First, we describe the alphabet of set theory. An alphabet is the collection of all allowable symbols. In principle, when writing any theorem, definition, or proof we are allowed to use only the symbols in the alphabet (nobody does this in practice because it is inconvenient, but it can be done in principle).

Logical symbols

The alphabet consists of the logical symbols:

$$\begin{array}{|c|c|} \hline \text{Symbol} & \text{Name}\\ \hline \forall & \text{universal quantifier}\\ \exists & \text{existential quantifier}\\ \wedge & \text{and}\\ \vee & \text{or}\\ \neg & \text{not}\\ \rightarrow & \text{implies}\\ \leftrightarrow & \text{if and only if}\\ ( & \text{left bracket}\\ ) & \text{right bracket}\\ = & \text{equality}\\ \in & \text{element of}\\ \hline \end{array}$$

I hope all these symbols are familiar; if they are not, a basic proof book should introduce them.

Variables

Outside these symbols, the alphabet also includes a collection of variables. We will denote this collection by $x_1,~x_2,~x_3,\ldots$ but other names are possible.

Well-Formed Formulas (WFFs)

A well-formed formula or wff can be defined as everything satisfying the following rules:

• Everything of the form $(x_n\in x_m)$ or $(x_n = x_m)$ is a wff.
• If $\psi$ is a wff, then so is $(\neg \psi)$.
• If $\psi$ and $\varphi$ are wff’s then so are $(\psi\wedge \varphi)$, $(\psi\vee \varphi)$, $\psi\rightarrow \varphi$, and $(\psi\leftrightarrow \varphi)$.
• If $\psi$ is a wff and $x$ is a variable, then $(\forall x\psi)$ and $(\exists x\psi)$ are wff’s.

Examples of WFFs

As an example, $(\forall x_1(x_1=x_1))$ and $(\exists x_3((x_3=x_3)\wedge (\neg(x_3\in x_4))))$ are wff’s, but $\neg\wedge x_5=$ is not.

Bound and Free Variables

If $\psi$ is a wff and $x_n$ is a variable then $x_n$ is a bound variable if it is within the scope of a quantifier; otherwise it is free. This is easily explained with an example. In $(\forall x_1(x_1=x_1))$, the quantifier $\forall x_1$ means that $x_1$ is a bound variable. In $(\exists x_3((x_3=x_3)\wedge (\neg(x_3\in x_4))))$, the quantifier $\exists x_3$ means that $x_3$ is a bound variable, while $x_4$ is a free variable since there is no quantifier $\forall x_4$ or $\exists x_4$.

In axiom (4) above, it is sometimes demanded that $x$ is a free variable of $\psi$ (and this is always the practice); however, we can get away with not demanding it for the formal definition.

Axioms and Inference Rules

Let us consider which wff’s are true and false. To do this, we need a collection of axioms and inference rules. The axioms we use are the logical axioms together with the ZF(C) axioms. The ZFC axioms will be covered in detail later in the book. The logical axioms are usually covered in logic texts. For completeness, here is a collection of logical axioms:

• If $\psi$ and $\varphi$ are wff’s, then $(\psi\rightarrow (\varphi\rightarrow \psi))$ is true.
• If $\psi$, $\varphi$, $\chi$ are wff’s then $((\psi\rightarrow (\varphi\rightarrow \chi))\rightarrow ((\psi\rightarrow \varphi)\rightarrow (\psi\rightarrow \chi)))$ is true.
• If $\psi$ is a wff, then $((\neg(\neg \psi))\rightarrow \psi)$ is true.
• If $\varphi$ and $\psi$ are wff’s and $x$ is a variable, then $((\forall x(\varphi\rightarrow \psi))\rightarrow ((\forall x\varphi)\rightarrow (\forall x \psi)))$ is true.
• If $\varphi$ is a wff and $x$ is a variable, then $(\varphi\rightarrow (\forall x \varphi))$ is true.
• If $\varphi$ is a wff, if $x$ is a variable that is free in $\varphi$, if $y$ is another variable and if $\varphi’$ is the formula obtained by replacing every occurrence of $x$ with $y$, then $((\forall x \varphi)\rightarrow \varphi’)$ is true.

There are no separate axioms for $\wedge$, $\vee$, $\exists$ and $\leftrightarrow$ (although that would have been possible). We regard $(\varphi \vee \psi)$ as an abbreviation for $((\neg\varphi)\rightarrow \psi)$. We regard $(\varphi \wedge \psi)$ as an abbreviation of $(\neg ((\neg \varphi)\vee (\neg \psi)))$. We regard $(\varphi \leftrightarrow \psi)$ as an abbreviation of $((\psi \rightarrow \varphi)\wedge (\varphi\rightarrow \psi))$. Finally, we regard $(\exists x\varphi)$ as an abbreviation of $(\neg(\forall x (\neg \varphi)))$.

Inference Rule: Modus Ponens

There is only one inference rule in our system, and that is modus ponens. This says that if $\varphi$ is a true wff and if $(\varphi\rightarrow \psi)$ is a true wff, then $\psi$ is also a true wff.

Theorem and Proof

So what is a theorem and a proof? A theorem $\varphi$ is any wff for which there is a proof. A proof of $\varphi$ is a sequence of wff’s $\varphi_1$, $\varphi_2$, $\varphi_3$, \ldots, $\varphi_n$ such that $\varphi_n = \varphi$ and each $\varphi_k$ is either a logical axiom, a ZFC axiom, or follows from one of the earlier wff’s $\varphi_1$,\ldots, $\varphi_{k-1}$ by application of modus ponens.

Practical Proof Writing

Of course, nobody actually writes all theorems in the exact formal language, and nobody actually provides proofs as defined above. A proof is usually written with English words and sentences because the reader is human and finds English arguments easier to grasp than a perfectly rigorous sequence of symbols. The formal definition of theorem and proof above should be regarded as an ideal. The proofs in textbooks are not ideal but are convincing that an ideal proof exists. Indeed, everything written in Hrbacek and Jech and other books can be given ideal proofs; this is done, for example, in Metamath: http://www.metamath.org — but that is tedious and hard to read.

I advise the reader not to worry excessively about the exact formal nature of formulas or about providing ideal proofs while reading this book. This material is presented as background. More information can be found in a mathematical logic text, where these issues are central.

The Power of WFFs

Our formal definition of which expressions are wff’s and which are not is an important concept in mathematics because it eliminates several paradoxes. See, for example, this note on the general importance of precise definition: important thing.

Berry’s Paradox (example)

For example, consider Berry’s paradox: “Let $n$ be the smallest natural number that cannot be defined with less than $1000$ letters in the English language”. Certainly “one” takes three letters, so it is not $n$. Likewise, “hundred” takes seven letters, so it is not $n$. On the other hand, fewer than $\approx 30^{1000}$ numbers can be expressed with less than $1000$ letters. So certainly there must be some number that cannot be expressed with $1000$ letters; $n$ is the smallest of those. But my description of $n$ was less than $1000$ letters long, so I have described $n$ with fewer than $1000$ letters. This is a paradox.

Our system of wff’s resolves this and similar problems. The resolution is simple: the sentence “$n$ cannot be defined with less than $1000$ letters in the English language” cannot be written as a wff. In particular, the problematic part is expressing “can be defined” in the formal language of wff’s.

This explains why it is important to state exactly which formulas we consider in mathematics and which we do not. If we rely on arbitrary English sentences, we get statements that are too vague or even paradoxical.