G1. What is a formal system?

In mathematical logic, a formal system is something that can “derive theorems” from a set of axioms, using a set of transformation rules. That’s incredibly abstract, I know, so we will elaborate with examples.

Before that, though: Naming Is Hard™. Often, the same thing is referred to by many names, which creates unnecessary confusion, especially when you’re first learning a topic. Formal systems are no exception. Here are a few other names that, as far as I can tell, refer to the same idea: a deductive system, a logical calculus, a formalized calculus, a formalism, or an axiomatized theory.

A formal system consists of four parts:

1. An alphabet (or vocabulary) is a description of all the symbols used in the system. For example, you might define your system to include the numerals ‘0’ through ‘9’, the numerical variables ‘x’ and ‘y’, and the symbols ‘+’ and ‘=’.
2. A grammar (or formation rules) explains what strings of symbols are syntactically valid. For example, ‘5’, ‘+’, ‘=’ and ‘0’ might all be valid symbols in the alphabet, but the string of symbols ‘5+=0’ is not syntactically valid, whereas ‘5+4=0’ might be a syntactically valid. A formula, or well-formed string, is a syntactically valid string of symbols from your alphabet. A formula is not necessarily true, it’s just something that is expressible within the system.
3. A set of transformation rules (or rules of inference) describe valid ways of transforming one formula into another. Put another way, they specify the valid ways to derive new formulas from other formulas. For example, one rule could be that a numeral may be substituted for a numerical variable in all places that numerical variable appears in the formula. So, from the formula ‘x+y+x+2=0’ one could derive the formula ‘1+y+1+2=0’.
4. A set of axioms are a set of formulas given to you with the system. Intuitively, one can think of the set of axioms as the set of assumptions on which the formal system is based (the transformation rules are in some sense assumptions as well). A theorem is a formula that can be derived (via the transformation rules) from the axioms. It follows that the axioms are (trivially) theorems.

As always, examples are necessary to make these abstract ideas clear. Let’s go through a few.

Example I: The MIU system (from GEB)

1. Alphabet: ‘M’, ‘I’, and ‘U’
2. Grammar: Any combination of symbols is valid (e.g. ‘MIU’, ‘MU’, ‘UM’, etc)
3. Transformation Rules:
   • If you posses a string whose last symbol is ‘I’, you can add on a ‘U’ at the end.
   • Supposed you have ‘Mx’ where x (informally) stands for a string of symbols. From this you can derive ‘Mxx’. For example, from ‘MIU’, you can derive ‘MIUIU’.
   • You can replace any occurrence of ‘III’ in a formula with ‘U’ (e.g. ‘MIIIM’ => ‘MUM’).
   • You may delete any occurrences of ‘UU’ in a formula (e.g. ‘MUU’ => ‘M’).
4. Axioms: Just one: ‘MI’

Exercises:

1. Is ‘MIU’ a theorem of the ‘MIU’ system?
2. Is ‘MUI’ a theorem?
3. How about ‘MU’?

What does it mean?

If this is the first time you’ve come across formal systems, you might be pretty confused by the previous example. Maybe you expected “formulas” to correspond to, well, formulas, like 5 + 5 = 10, or at least some intelligible mathematical statement. Aren’t formal systems supposed to mean something? How do the random strings above correspond to math?

Great questions. To satisfactorily answer them, though, I’ll need more space: The Meaning of a Formal System.

Very quickly, though, a formal system only takes on meaning when interpreted, and what interpretation to choose is up to you. Not all interpretations are created equal, though. Some interpretations might map every theorem to a true statement, whereas others might not, and others still might map them to complete gibberish.

My last comment, for now, is that many formal systems were designed with an interpretation in mind, often called the standard interpretation. This next example is such a system.

Example II: The Add System

1. Alphabet: 0, S, +, =
2. Grammar:
   • Let’s introduce the notion of a numeric term: N
     • 0 is a numeric term
     • An S can immediately precede a numeric term to generate a new numeric term
   • Valid formulas follow the pattern: N + N = N
3. Transformation rules:
   • Assume X, Y, and Z are numeric term
   • From a formula X + Y = Z, the formula X + SY = SZ can be derived
   • From a formula X + Y = Z, the formula Y + X = Z can be derived
4. Axioms:
   • Just one: 0 + 0 = 0

Exercises:

1. Derive the formula ‘S000 + S00 = S00000’
2. Is ‘S0000 + S00 = 0’ a formula of the Add system?
3. Is ‘S0000 + S00 = 0’ a theorem of the Add system?
4. What do you think ‘S’ means?

Example III: The Boolean algebra system

1. Alphabet: \(T\), \(F\), \(\land\), \(\lor\), \(\lnot\), \((\), and \()\)
2. Grammar:
   • \(T\) is a valid formula, so is \(F\)
   • If B is a valid formula, so is \((B \land B)\)
   • If B is a valid fomula, so is \((B \lor B)\)
   • If B is a valid formula, so is \(\lnot B\)
   • any boolean term is a valid formula
3. Transformation rules: Assume \(X\) and \(Y\) are valid formulas.
   • If you have derived \(X\), you can derive \((X \lor Y)\)
   • If you have derived both \(X\) and \(Y\), you can derive \((X \land Y)\)
   • If you have derived \((X \lor Y)\), you can derive \(\lnot (\lnot X \land \lnot Y)\)
   • If you have derived \(\lnot \lnot X\), you can derive \(X\).
   • If you have derived \(X\), you can derive \(\lnot \lnot X\).
4. Axioms:
   • \(T\).
   • \(\lnot F\).

Exercises:

1. Derive \((T \land T) \lor F\)
2. Derive \(\lnot (\lnot T \land F)\)
3. Is \(F \lor T\) a theorem? A formula?
4. Is \(F \land T\) a theorem? A formula?
5. Can you guess the standard interpretation for each symbol?