1. Syntax

From Euclid's time until the 19th century (with the publication of Frege's Begriffsschrift), "axioms were stated in a natural language (eg. Greek, English, etc.), and proofs were just given in "ordinary reasoning"; exactly what a proof is was not formally analyzed. This is still the case now in most mathematics. Logical symbols are frequently used as abbreviations of English words, but most math books assume that you can recognize a correct proof when you see it, without formal analysis." - quote from Kenneth Kunen from his book The Foundations of Mathematics.

Formal system

In 0. The Very Beginning, I've mentioned that we need to communicate without ambiguity. A way to achieve such clarity is through the use of a formal system, which will allow us to derive formal proofs. Formal proofs are simply proofs written in a specific form, adhering to a given syntax. A formal system is a formal language equipped with a deductive apparatus. You may think of a formal system as a model of reasoning.

Remarks:

• A language must contain wffs, but not necessarily terms (as for example the alphabet of propositional logic that will be defined)
• In Mathematical Logic, definitions and metatheorems often follow an inductive structure. An inductive structure consists of a base case and of an inductive case. For example, the definition of a term for the decimal number system language consists of the base case "a digit symbol is a term" and of the inductive case "a term concatenated with another term is a term"

Given a formal language, one may go on to do two things:

• Explore the semantics by defining an interpretation of the language, which is an assignment of meaning to its symbols
• Specify a deductive apparatus for the language, which takes us down the road of proof theory

A deductive apparatus consists of wffs called axioms and inference rules/rules of inference. By definition, the theorems of a formal system are the axioms and all wffs derived from the inference rules. Thus, proofs are pure mechanical manipulations of symbols, with no regard whatsoever to their meaning. When dealing with syntax, you must abstract from the semantics. Ignore this warning at your own peril.

I've recently come across an excellent example about the distinction between syntax and semantics. In the movie Guardians of the Galaxy Vol. 3, as the guardians are infiltrating the Orgosphere, Star-Lord has an embarrassing talk with Gamora. He is eventually interrupted by his teammates who point out that he's talking on an open line and they have been listening to everything. They then go on arguing about which button does what. Their interaction goes like this:

• Mantis: What color button did you push?
• Star-Lord: Blue, for the blue suit! (they were wearing suits of different colors and Gamora's was blue)
• Drax: Oh, no!
• Nebula: Blue is the open line for everyone.
• Mantis: Orange is for blue.
• Star-Lord: What?
• Mantis: Black is for orange, yellow is for green, green is for red and red is for yellow.
• Drax: No, yellow is for yellow, green is for red, red is for green.
• Mantis: I don't think so.
• Drax: Try it then.
• [Mantis clicks on yellow]
• Mantis: HELLO! (deafening everyone)
• Mantis: You were right.
• Star-Lord: How the hell am I supposed to know all of that?
• Drax: Seems intuitive.

The game of Chess

To give an example, here's what a formal system for the game of Chess would look like.

Its alphabet would consist of the pieces (Pawn, Bishop, Knight, Rook, Queen and King, black and white), of the game board and of the information of whose turn it is, of whether each player may castle if the opportunity arises, of how many times each position has been visited (for the repetition rules) and of how many moves have been made since a Pawn has been moved or a capture has been made (for the 50 and 75-move rules). Its terms would be the pieces, and its wffs would be allocations of pieces to the game board with flags containing the above informations.

The only axiom would be the starting position, with White to move, both players being allowed to castle if the opportunity arises, no visited position except the starting one, and no made moves since last capture or Pawn move. The rules of inference would simply be the rules of the game, which from a given position indicate which positions can be reached in the next move. Thus, the theorems would simply be the starting position, as well as all positions that arise from the inference rules.

You may have noticed that it's debatable whether this is really a formal system, because a formal system is supposed to work with symbols, whereas here I've instead used pieces, informations, board positions, etc. However, it should be clear that one may make this a proper formal system by associating symbols to each piece, relation symbols to indicate where each piece stands on the board, logical connectives to allow one to say "the Pawn is in C3 and the Rook is in H1", etc. In other words, you may create a formal system for the game of chess if you reverse-engineer the semantics.

Notation and format

Let's use a concrete example to show the format in which formal proofs will be written. The following toy formal system was proposed by Paul Lorenzen.

Its alphabet consists of the symbols \(+\) and \(o\). The language has no terms and wffs are the alphabet's symbols and any concatenation of them.

The only axiom of the deductive apparatus is the symbol \(+\) and its two rules of inference are

• \(o\) concatenation: \(x \vdash xo\)
• \(+\) concatenation: \(x \vdash +x+\)

where \(x\) stands for any wff and \(\vdash\), called the turnstile, is a symbol which means "proves". For example, \(x \vdash xo\) means that \(x\) proves \(xo\), or in other words, that from \(x\) you can deduce/derive \(xo\). It's important to understand that the turnstile is a symbol of the metalanguage and is not a part of the formal language.

Let \(x\) and \(y\) be wffs. Whenever you write \(\vdash y\), even though nothing stands to the left of \(\vdash\), it's implicitly assumed that \(y\) follows from the axiom/s or from the proved theorems. Whenever you write \(x \vdash y\), \(x\) is either an hypothesis or another axiom that we wish to consider, not necessarily an axiom or a theorem from our system. To make notation clearer, in the case one wishes to add multiple axioms/hypothesis, say \(x_0\), \(x_1\), ..., we'll write \(\{x_0, x_1, ...\}\) to the left of the turnstile, to mean that some statement is provable by the set \(\{x_0, x_1, ...\}\). If we have a set of wffs \(\Phi\) and we wish to add a wff \(z\) to it, we may write \(\Phi \cup z\) or \(\Phi + z\) (the "\(+\)" symbol that is meant here is not to be confused with the "\(+\)" symbol of the language that we are considering in this example; it's just a coincidence that they're the same). If instead of adding a wff, we want to add another set of wffs \(\Phi'\) to it, then we shall write \(\Phi \cup \Phi'\). You may consider \(\Phi \vdash \varphi\), where \(\varphi\) is in \(\Phi\), as an implicit inference rule inherent to all proof systems, a property of provability.

Now, to show what a formal proof looks like, let's prove the theorem "\(++oo+o\)":

Each line is either an axiom or the output of a rule of inference applied to a previously proved wff. To refer to a previous wff, each wff is given a name, in this case ranging from \(\varphi_0\) to \(\varphi_4\). To the right of that given name stands a comment justifying the step.

This proof makes no reference to the eventual meaning of the wffs. It's a purely mechanical procedure. This is the case for all formal proofs of all formal systems.

Rigorous proof

If you formally prove something, meaning by using a formal system, then it will rigorously be proven. It doesn't mean however, that any proof conducted outside of a formal system isn't rigorous. Indeed, when we'll be studying mathematical logic in the next few chapters, we'll be analyzing formal systems by proving theorems about them. Such theorems are called metatheorems, as they are proven outside of the formal systems and provide insights about them. Metatheorems will be informally but rigorously proven in our metalanguage (English).

But what does rigorous mean? That's a tricky question. Any formal proof is objectively rigorous. An informal proof on the other hand is rigorous only as long as it justifies the conclusion. Unfortunately, what might be considered as a satisfying justification to some may be unsatisfying to others, thus making the concept of rigor subjective. To surpass that issue, metaproofs will reference definitions, which will act as axioms if you will, and be mainly constructive by providing algorithms (=step-by-step instructions) for arriving at the desired conclusions.

One could also make metaproofs formal (and thus objectively rigorous) by creating a formal system for them, but then the same problem would appear for the metametalanguage of the formalized metalanguage. Thus, it isn't a worthy endeavour.

Sources:

• Formal LogicPaul Lorenzen
• Friendly Introduction to Mathematical LogicChristopher Leary & Lars Kristiansen
• Introduction to Mathematical LogicVilnis Detlovs & Karlis Podnieks
• Metalogic, An Introduction to the Metatheory of Standard First Order LogicGeoffrey Hunter
• The Foundations of MathematicsKenneth Kunen