Consistency and Soundness
full of meaning, significance, purpose, or value; purposeful; significant
Let us deal with formal systems. Interesting formal systems. “Formal” means they consist of formulas. “Interesting” means the formulas are constructed from basic arithmetical relations connected by propositional relations and quantifiers. It can contain other relations too. It has rules of inference and a set of axioms that allow to define the set of provable formulas. And “define” means that the sets of rules and the axioms are decidable.
There are some important classes of formulas that are called Π1 and Σ1. Π1 are formulas of the form ∀n: P(n) where P is a decidable property. And Σ1 is the dual class: ∃n: P(n).
The system is called consistent if there is no provable formula f such that the system proves ~f. Note that consistency is a purely syntactical condition. Also note that inconsistent theories prove all formulas.
The system is called ω-consistent if there is no provable formula ∃n: f(n) such that the system proves ~f(n) for each natural number n. This condition is still syntactical because “natural number” means here “a finite string of a certain form”, e.g. 0, S(0), S(S(0)). If the system is ω-consistent just for decidable formulas f, it is called 1-consistent.
Obviously, ω-consistency implies 1-consistency which in turn implies consistency.
The system is called sound if it only proves formulas that when interpreted as statements about numbers turn out true. The system is called complete if it proves any formula that represents a true statement. Soundness and completeness are semantic conditions: they require to interpret formulas and deal with truth values.
Interesting formal systems possess the following very neat properties that bridge syntax and semantics:
- They are Σ1-complete. That is, if ∃n: P(n) is true then for some number k the system must indeed prove P(k).
- 1-consistency is equivalent to Σ1-soundness. If we prove ∃n: f(n) then there must exist an n such that S(n) holds, since otherwise we could prove ~S(n) for each n.
- consistency is equivalent to Π1-soundness. If we prove ∀n: f(n) then for each n, we prove f(n), so f(n) must be true, otherwise ~f(n) would be provable.
What’s curious, we normally consider Π formulas (universal statements) more strong and important than Σ formulas (existence statements). And apparently, if we don’t prove any existential falsehoods, we don’t prove any universal falsehoods either. But universal soundness is also implied by the simple, weak, purely syntactical condition of consistency. The latter fact was considered fundamentally important by Hilbert.
I haven’t said anything about Π1-completeness yet. Unfortunately, Π1-sound systems are Π1-incomplete. If we reformulate this as “consistent systems don’t prove all true Π1 statements” we immediately recognize that it’s a part of Gödel’s 1st incompleteness theorem. (Popular books often say that the above statement is Gödel’s theorem, but that’s not the case).