What is a Property Formally in Mathematical Logic

** Hrbacek-Jech Chapter 1.2

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

First we describe the alphabet of set theory. An alphabet is merely the collection of all allowable systems. So that means that when writing any theorem/definition/proof, we are actually only allowed to use the symbols in the alphabet (nobody actually does that because it is inconvenient, but it can be done in principle). 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 to everybody, if they are not, a basic proof book should tell you about them.

Outside these symbols, the alphabet also allows a collection of variables. We will denote this collection by ##x_1,~x_2,~x_3,…## but other names are possible.

A well-formed formula or wff can be defined as everything satisfying the following:
# 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##, ##(\psi\leftrightarrow \varphi)##.
# If ##\psi## is a wff and ##x## is a variable, then ##(\forall x\psi)## and ##(\exists x\psi)## are wff’s.

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.

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. While 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 case in practice), but we can get away with not demanding it.

Let us go a bit into seeing which wff’s are true and false. To do this, we need a collection of axioms and we need inference rules. The axioms we use are the logical axioms and the ZF(C) axioms. The ZFC axioms will be covered in detail in the rest of the book. The logical axioms are usually only covered in logic books. 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 ##((\neq(\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 such that every occurence of ##x## is replaced with ##y##, then ##((\forall x \varphi)\rightarrow \varphi’)## is true.

There are no axioms for ##\wedge##, ##\vee##, ##\exists## and ##\leftrightarrow## (although this was certainly 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 abbrevation of ##((\psi \rightarrow \varphi)\wedge (\varphi\rightarrow \psi))##. Finally, we regard ##(\exists x\varphi)## as an abbreviation of ##(\neg(\forall x (\neg \varphi)))##.

There is only one inference rule in our system and that is the 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.

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

Of course, nobody actually writes all theorems in the exact logical language. And nobody actually provides a proof as I defined above. A proof is usually written with English words and with sentences. This is because the reader is human and finds it much easier to grasp English arguments than perfectly rigorous sequences of symbols. We should see the definition of theorem and proof as above to be the ideal. The proofs in the textbooks is not ideal, but are merely 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 this is very tedious and hard to read.

I advise the reader when reading this book to not bother much with the exact logical nature of the formulas, and with providing ideal proofs of theorems. This is merely presented as background. More information can be found in a mathematical logic text, where these kinds of things are central.

== The power of wff’s ==

Our formal definition of what is a wff and what not is a very important thing in mathematics, because it eliminates a number of paradoxes.

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, less 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 simply the smallest of those. But wait for a second, my description of ##n## was less than ##1000## letters long! So I have in fact described $n$ with less than $1000$ letters. This is a paradox.

Our system of wff’s solves this and similar problems. The resolution is simple, the sentence “##n## cannot be defined with less than ##1000## letters in the English language” can not be written as a wff. In particular, the problematic part is to find a way to write “can be defined” in the form of a wff.

This should explain why it is important to state exactly which formula’s we consider in mathematics and which not. If we rely on any sentence in the English language, then we get things that are too vague or even paradoxes.