A formal system in a vacuum is not meaningful. Meaning comes when an interpretation is given to the symbols in the formal system. For example, take the Add formal system, from the last post. As a reminder:

Can you guess the intended (standard) interpretation for each symbol in the Add’s alphabet?

  • “0” means 0
  • “S” means “the successor of”. So, “S0” means the successor of 0, i.e. 1.
  • ”+” means +
  • ”=” means =

Under this interpretation, Add seems to be able to derive all true statements of the form x + y = z, where x, y, and z are natural numbers.

Is this the only possible interpretation? No, of course not. We could interpret the symbol “+” to mean - (minus). Under that interpretation, Add produces blatantly false statements, like 0 - 1 = 1.

Are there any other interpretations, other than the intended one, where Add continues to make true statements? Sure. What if we interpreted “=” to mean “greater than or equals”. Under this interpretation, the formal system also only produces true statements. Is 0 + 0 greater than equal to 0? Yes, and we can derive “0 + 0 = 0”.

However, there’s an important difference between the intended “equals” interpretation and this new “greater than equal to” interpretation. Under the intended interpretation, Add is able to derive all true statements of the form x + y = z (where x, y, and z are natural numbers), whereas under this new interpretation, Add still derives only true statements, but not all true statements. For example, 1 + 1 >= 0 (represented by the formula “S0 + S0 = 0”) is true, but cannot be derived. Put another way, it is not a theorem of Add.

Let’s make this a bit more precise. I’ve been using the word “statement” and phrase “true statement” in the preceding paragraphs, but what do they mean? Recall that a formal system deals in what we call formulas. A formula is a syntactically valid string of symbols from the alphabet of the system. More intuitively, a formula is something that can be expressed within the formal system.

Is “5 + 4 = 9” a formula of Add? No! “5”, “4”, and “9” are not even part of Add’s alphabet, so regardless of the rules of grammar, it’s not a formula of Add. How about “S0 + 0S = 0”? Also no. Although that string only uses symbols that are part of the alphabet, “0S” is not syntactically valid (“S” can only precede a numeric term). Ok, how about “0 + 0 = S0”? Yes. That string is a syntactically valid string of symbols within Add’s alphabet, so it is a formula of Add.

Is “0 + 0 = S0” true? Well, under what interpretation? Whether something is true or not is not something a formal system, by itself, can answer.

Maybe you meant, can “0 + 0 = S0” be derived within Add? In other words, is “0 + 0 = S0” a theorem of Add? That we can answer without reference to any particular interpretation, and I claim it is not a theorem (without proof1).

Ok, so “0 + 0 = S0” is not a theorem of Add, but back to our original question: is it true? For that, we need to adopt an interpretation of Add. Let’s pick the intended one. What is the interpretation of “0 + 0 = S0”? It’s 0 + 0 = 1. This is what we call a statement. A formula, when interpreted, becomes a statement, and in this case, it is a false statement.

To summarize: Under a specific interpretation, a formula can be interpreted to make a statement, and that statement can be true or false.

  1. I can prove it, but that opens up a whole new can of worms. What do I mean by “prove”? I certainly don’t mean “derive within Add”. I mean prove in the normal sense of the word, where I’m allowed to use any intuitive, logical arguments I want. But isn’t the whole point of these formal systems to prove claims in a more rigorous way? I digress… ↩