In this post we will discuss three of the most fundamental properties of mathematical logic: soundness, consistency, and completeness. We’ll start with some intuitive but imprecise definitions, then work through some examples, and then we will discuss the precise definitions of each property.

  • Soundness: A formal system is sound if it only derives true statements. Put another way, if a formula is a theorem, then it is a true statement (when interpreted). The fact that soundness refers to “truth”, and not just derivability, means that it’s a property with respect to a particular interpretation.
  • Consistency: A formal system is consistent if it cannot derive a contradiction. This often assumes that the formal system includes a symbol (such as \(\lnot\)) that is meant to be interpreted as the standard logical negation operator “not”. Assuming the \(\lnot\) symbol, deriving both \(X\) and \(\lnot X\) would be a contradiction.
  • Completeness: A formal system is complete if it can derive all true statements. Put another way, if a formula is a true statement (when interpreted), it is a theorem. This is the logical converse of soundness.

As always, examples will help make these ideas clear. Let’s revisit a formal system that we’re already familiar with: the Add system.

In Meaning in a formal system, we already discussed the standard interpretation for Add. I won’t recall the entire mapping here, since most of it is obvious (e.g. \(0\) means 0), but I will remind you that \(S\) means “the successor of” (e.g. \(S0\) means “the successor of 0”, i.e. 1).

So, is Add sound, consistent, and or complete?


Soundness is normally a matter of having true axioms and truth-preserving transformation rules. If you start with a true statements (axioms), and every transformation rule turns a true statement into another true statement (preserves truth), then your formal system will only derive true statements.

Is Add sound? We will evaluate Add’s soundness with respect to its standard interpretation. To start, are Add’s axioms true? This one is easy; Add only has one axiom (\(0+0=0\)) whose standard interpretation looks identical and is a statement that we would all agree is true.

Are Add’s transformation rules truth-preserving? There are only two to consider. The first states that from a formula with the pattern X + Y = Z, one can derive X + SY + SZ. This rule can be interpreted as if \(x + y = z\) then \(x + (1 + y) = (1 + z)\). This looks truth-preserving to me. The second transformation rule states that from a formula with the pattern X + Y = Z, one can derive Y + X = Z. In other words, addition is commutative. This is also true for numbers. Note that I’m not saying this is always true for all possible addition operators, just that - in the standard interpretation of the Add system, where numerical patterns are interpreted as natural numbers and the ‘+’ symbol is interpreted as the standard addition operator - this is true.

In summary, we’ve concluded (in a non-rigorous way) that Add’s axiom is a true statement when interpreted and that Add’s transformation rules are truth-preserving and therefore Add is sound with respect to its standard interpretation; it will only derive theorems that make true statements (when interpreted using its standard interpretation).

Before we move on, can you imagine how we could change Add so that it was no longer sound? There are an infinite number of ways, but here is one: Add the axiom \(0 + S0 = 0\). With this tweak, Add will still derive an infinite number of theorems, but many will make false statements (e.g. \(0 + 1=0\), \(0 + 2 = 1\), \(0 + 3 = 2\), etc.).


A formal system is consistent if it cannot derive a contradiction. This lack of contradiction can be defined in either semantic or syntactic terms.

Semantic consistency: A formal system is semantically consistent if there exists an interpretation under which every theorem is true. From this definition, it’s clear that soundness implies semantic consistency, and therefore soundness is a stronger property.

Syntactic consistency: A formal system is syntactically consistent if there does not exist a sentence \(\varphi\) such that the formal system can derive both \(\varphi\) and \(\lnot \varphi\). Often, the word syntactic is omitted and this is just referred to as consistent.

Is Add consistent? It is trivially syntactically consistent. It does not include a symbol that represents “not”, and therefore it cannot derive a syntactic contradiction. Is Add semantically consistent? The answer is again yes. We’ve already shown that Add is sound with respect to the standard interpretation and therefore there exists an interpretation - the standard one - under which every theorem is true.


A formal system is complete if it can derive all true statements. There are a few non-obvious points of clarification:

  • A complete system doesn’t need to only derive true statements (i.e. be sound). It might derive all true statements and all false statements!
  • When we say all true statements, we do not mean literally all. We’re only referring to the set of statements that can be expressed within the formal system. For example, consider the Add system. It cannot derive the (true) statement \(5 \cdot 4 = 20\). Does that mean it’s not complete? No, because Add cannot even express the idea of multiplication. So the fact that it cannot derive true statements about multiplication is outside the scope of interest. If it could not derive a statement that it could express, \(5 + 4 = 9\) for example, then it would be incomplete.

So, is Add complete? Can you come up with a statement of the form \(x + y = z\) that Add can express but not derive? I can’t.

Take, for example, \(5 + 4 = 9\), which would be expressed by the formula \(SSSSS0 + SSSS0 = SSSSSSSSS0\). The derivation is tedious, to be sure, but straightforward:

\[\begin{align} 0 + 0 &= 0 \tag{axiom} \\ 0 + S0 &= S0 \tag{transformation rule 1} \\ 0 + SS0 &= SS0 \tag{transformation rule 1} \\ 0 + SSS0 &= SSS0 \tag{transformation rule 1} \\ 0 + SSSS0 &= SSSS0 \tag{transformation rule 1} \\ 0 + SSSSS0 &= SSSSS0 \tag{transformation rule 1} \\ SSSSS0 + 0 &= SSSSS0 \tag{transformation rule 2} \\ SSSSS0 + S0 &= SSSSSS0 \tag{transformation rule 1} \\ SSSSS0 + SS0 &= SSSSSSS0 \tag{transformation rule 1} \\ SSSSS0 + SSS0 &= SSSSSSSS0 \tag{transformation rule 1} \\ SSSSS0 + SSSS0 &= SSSSSSSSS0 \tag{transformation rule 1} \\ \end{align}\]

To check your understanding, can you come up with a statement of the form \(x + y = z\) that Add cannot express? I can. How about \(-1 + 1 = 0\)? Add cannot express negative numbers, it can only make statements that refer to the natural numbers. Similarly, you could construct statements that refer to fractions, real numbers, complex numbers, etc., none of which Add can express. As we’ve already pointed out, this does not mean Add is not complete. It can derive all true statements that it can express, and is therefore complete.

How might we tweak add to be incomplete? Would the same tweak that we made before - adding the axiom \(0 + S0 = 0\) - do the trick? No! Add would still be able to derive all true statements it can express. It would also be able to derive many false statements, but that’s not a problem for completeness.

So what can we change to make Add incomplete? As before, there are many options. Here are a few: replace the axiom \(0 + 0 = 0\) with \(0 + S0 = 0\), remove the second transformation rule, remove the first transformation rule, remove both transformation rules (quite a boring system would result!).

Precise definitions

In the following definitions, we assume the existence of the \(\lnot\) symbol which represents the logical not. With this, we can reduce our dependence on semantic properties (the ones that refer to “truth”) and focus on syntactic properties. In addition, most “interesting” formal systems include propositional logic within them and therefore include the \(\lnot\) symbol.

As I’ve said before, Naming Is Hard™. One concept often has many names. Below, we use different names for concepts that we’ve already seen before. Why can’t we just stick to one set? We can, but that doesn’t mean the rest of the logic community will, and so you will leave this series of blog posts ill-prepared to read the work of others. Therefore, I think the benefits of exposing you to more common terminology outweighs the costs. With that out of the way, theory is another word for formal system and sentence is another word for formula (specifically, one that has no free variables).

These definitions come straight from An Introduction to Gödel’s Theorems:

  1. Given a derivation of the sentence \(\varphi\) from the axioms of the theory \(T\) using the background logical proof system, we will say that \(\varphi\) is a theorem of \(T\). Using the standard abbreviator symbol, we write: \(T \vdash \varphi\).
  2. A theory \(T\) is sound iff every theorem of \(T\) is true (i.e. true on the interpretation built into \(T\)’s language). Soundness is, of course, normally a matter of having true axioms and a truth-preserving proof system.
  3. A theory \(T\) is effectively decidable iff the property of being a theorem of \(T\) is an effectively decidable property - i.e. iff there is an algorithmic procedure for determining, for any given sentence \(\varphi\), whether or not \(T \vdash \varphi\).
  4. Assume now that \(T\) has a standard negation connective ‘\(\lnot\)’. A theory \(T\) decides the sentence \(\varphi\) iff either \(T \vdash \varphi\) or \(T \vdash \lnot \varphi\). A theory \(T\) correctly decides \(\varphi\) just when, if \(\varphi\) is true (on the interpretation build into \(T\)’s language), \(T \vdash \varphi\), and if \(\varphi\) is false, \(T \vdash \lnot \varphi\).
  5. A theory \(T\) is negation-complete iff \(T\) decides every sentence \(\varphi\) of its language (i.e. for every sentence \(\varphi\), either \(T \vdash \varphi\) or \(T \vdash \lnot \varphi\)).
  6. \(T\) is inconsistent iff for some sentence \(\varphi\), we have both \(T \vdash \varphi\) and \(T \vdash \lnot \varphi\).

One last note about completeness. If a theory is incomplete, that means there are true statements that it cannot derive. That was the imprecise/intuitive definition that we started with, but why does that follow from this new, more precise version (#5 above)? Simply because one of \(\varphi\) and \(\lnot \varphi\) must be true, for any \(\varphi\). And if an incomplete system cannot derive either one, and one of them must be true, then it cannot derive a true statement.

Same idea, different perspective

I won’t introduce anything new here, just give slightly different perspectives on the same ideas.

Imagine the set of all sentences of a formal system (theory) as an infinite set. A theory then partitions that set into two subsets, theorems and non-theorems.

  • A theory is consistent if, for any pair of sentences \(\varphi\) and \(\lnot \varphi\), at most one is in the theorem subset.
  • A theory is complete if, for every pair, at least one is in the theorem subset.
  • A theory is sound if, for every pair, the “false” one is not in the theorem subset.
  • A theory is sound and complete if, for every pair, only the “true” one is in the theorem subset.

Here’s a slightly different take on the same idea. Imagine a theory as a function which takes in a pair of sentences \(\varphi\) and \(\lnot \varphi\) and outputs 0 if \(\varphi\) is a theorem, 1 if \(\varphi\) is a theorem, nothing if neither is a theorem, and both 0 and 1 if both are.

  • If a theory is not consistent, the “function” will sometimes output two values (both 0 and 1) and is therefore not even a proper function.
  • If a theory is consistent, then for any pair of sentences \(\varphi\) and \(\lnot \varphi\) it will output at most one value.
  • If a theory is complete, then for any pair of sentences \(\varphi\) and \(\lnot \varphi\) it will output at least one value.
  • If a theory is consistent and complete, then one can think of the theory as a total function over the pairs of sentences \(\varphi\) and \(\lnot \varphi\). It will output exactly one value for any input pair.
  • If a theory is consistent but not complete, then one can think of it as a partial function.
  • If a theory is sound and complete, then the function is not only total, but it chooses the “true” sentence of any input pair.