G2. Meaning in a formal system
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:
Add:
 Alphabet: 0, S, +, =
 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
 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
 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
 Axioms:
 Just one: 0 + 0 = 0
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 proof^{1}).
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.

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… ↩