# Provability and Truth

The relationship between provability and truth is obviously a fundamental one and the most interesting games played in mathematics are motivated by interesting structures (sets or categories, in other words mathematical objects) that are models for the game being played. The models are mathematical objects, but the relationship between provability and truth (and between formal systems and their models), fundamental as it may be, belongs to mathematical logic, not mathematics. Within a model one can verify whether the axioms hold (i.e., are true) and if they are, the game can be played. That is the whole point of formal systems, there may be many models for one game, but by playing the game, you prove things that are true in all the models. Those things are true, and you can see that they are true because the models are real constructions, not games. The symmetries of a window are a model for a specific formal system called a group. The symmetries of the star fish on the right are also a model of a group. So are the integers under the rules of addition, but not the natural numbers under addition; one of the axioms for the group game is not true for natural numbers, so the group game cannot be played for them. The symmetry groups of particle physics are other such models of group, as well as any objects in the physical world which exhibit symmetries under some operation. The group game formally captures the idea of informal "symmetry". By playing the group game, we prove theorems about all these models which have some symmetry to them. That's how powerful games can be. In the rest of the article, this distinction between provability (in a formal system) and truth (in its models) is essential. When in a mathematics class the question "But what does it mean?" pops up, it is usually because students want to see how a game is being relevant to models. Models provide the meaning, but they are separate from the game.

What are some examples of such formal systems? We will be interested in 3 of them: First Order Logic (FOL), Peano Arithmetic (PA), and Zermelo-Fraenkel (ZF). FOL is meant to capture the basic laws of reasoning with propositions and predicates. FOL is an extension of the simple calculus of propositions (PC), which most readers have seen in high school. PC introduced propositional variables, the logical operators $$\wedge, \vee, \sim, \Rightarrow, \Leftrightarrow$$ and the logical values $$\top, \bot$$. PC has simple axioms governing the use of the logical operators, and a simple rule of deduction, the famous modus ponens : $$A, A \Rightarrow B \ \ \vdash \ \ B$$

The symbol $$\ \vdash \$$ means entails, i.e., the right-hand side can be deduced from the left-hand side. The entire deduction can be read as: if we have $$A$$ and if $$A$$ implies $$B$$, then we can deduce $$B$$. To PC, FOL adds predicate symbols, the logical quantifiers $$\forall$$, "for all", and $$\exists$$, "exists", and axioms governing the use of the logical quantifiers. To modus ponens, it adds two more rules of deduction: $$A \Rightarrow F(x) \ \ \vdash \ \ A \Rightarrow \forall x F(x)$$ $$F(x) \Rightarrow A \ \ \vdash \ \ \exists x F(x) \Rightarrow A$$

The PA   formal system is built on top of FOL and formalizes the properties of the natural numbers $$0,1,2,3, ...$$ Again, the natural numbers are only a model for PA, albeit the model that motivates PA. The ZF   formal system is also built on top of FOL and allows a formalization for working with sets; it is the most used such system which prohibits the construction of the problematic Russell set $$S$$.

What are some of the desirable properties of these systems built on top of FOL? First, let's mention from the outset that the terminology is a bit confusing, especially when it comes to two overly used terms: decidability and completeness. Since we promised to be persnickety, we will separate these terms, going against historical traditions. Because Gödel's incompleteness theorems are our main focus we will use completeness to have the meaning which it has in those theorems, while the completeness in the earlier Gödel's completeness theorem we will call l-completeness.

A formula is called logically valid if it is true in all the models of the system. The system is called l-complete if every logically valid formula is provable in the system, and sound if every provable formula is logically valid. Consequently, in a system which is both sound and complete, provability and logical validity are equivalent, this being the ideal situation. Gödel's completeness theorem of 1929 shows that FOL is such an ideal system, it is both sound and l-complete. This is a very positive result. The most important property of a formal system, and one that we cannot relax at all, is consistency, i.e., that we cannot prove both a formula and its negation within the system. If the system is not consistent, then the system is worthless because anything can be proved then. A formula is decidable if either it or its negation is provable within the system. Another wishful property of a system is completeness, i.e., that any formula be decidable. Undecidable statements are sometimes called independent, or logically independent. These terms are many times preferable since decidability is very much used in computability to mean something else: we say that a yes-no problem is decidable if there is an algorithm that decides yes-no for instances of the problem; we will call such a problem Turing decidable, in honor of the great man who invented it and proved its main properties. A much deeper and more entertaining coverage of all these issues can be found in the classic "Gödel, Escher, Bach" by Douglas Hofstadter.