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. Even though the models are mathematical objects, the relationship between provability and truth (and between formal systems and their models), fundamental as it may be, properly 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.
For example, 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.
( We can tie this with our anxiety about AI systems not proven mathematically to respect their specifications, their formal systems. You may think that it makes sense to ensure that research into formal software development of AI should outpace the development of individual AI systems, especially if these AI systems are powerful enough to have self-learning abilities; the worry that the AI can get out of control is a more digestible form of this more precise statement. If you want to read more about formal methods of software development, here is a coverage of these methods within a proposed program of study from 2011, it contains most of the important ideas. It was written for software professionals though and it has some difficult technical parts, but the main ideas are accessible. The document is in a slide presentation format, in which the contents of a page appear gradually as you move through it, not all at once. Download the document, and view it with Adobe Acrobat Reader DC (free download from Adobe), not with the Adobe Acrobat Touch. And not directly in your browser, because it will be hard to follow. It can be found in two places, here: Formal Software Development, or here: Formal Software Development)