Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this community
I recently read that Gödel's incompleteness theorem entails that second order logic cannot simultaneously hold the traits of: (i) completeness, (ii) soundness, and (iii) effectiveness.
However, I saw no explanation of why this is the case. In virtue of what is it the case that second order logic cannot simultaneously hold (i-iii)?
Sketch of the proof
1) We define the syntax for SOL and the corresponding deductive apparatus, adding axioms and rules for managing second-order quantification (see e.g. van Dalen, Logic and Structure (2013), Ch.5).
2) We define the "standard" semantics for the language.
3) We define the concept of standardly valid extending in a natural way the FOL concept.
Then we prove the :
Soundness Theorem : Every theorem of second-order predicate calculus is standardly valid.
4) We consider the FOL version of Peano axioms plus the Axiom of induction; it is important to note that, in the SOL version, Induction is a formula and not an axiom schema.
5) Let AR2 be the conjunction of the first-order axioms of formal arithmetic plus the second-order axiom of mathematical induction.
We prove that :
Any two standard interpretations M and M' that are models of AR2 are isomorphic.
6) Let L2A the second-order language for arithmetic (with the nonlogical constants of formal arithmetic : zero, successor, addition, multiplication).
Let N be the standard interpretation of L2A with the set of natural numbers as its domain and the usual interpretations of the nonlogical constants.
We prove (using 5) that :
Let B be any formula of the language of arithmetic. Then B is true in N if and only if AR2 ⇒ B is standardly valid.
7) We prove that :
The set SV of standardly valid formulas of L2A is not effectively enumerable.
Assume that SV is effectively enumerable. Then, by 6, we could effectively enumerate the set TR of all true formulas of first-order arithmetic by running through SV, finding all formulas of the form AR2 ⇒ B, where B is a formula of first-order arithmetic, and listing those formulas B. Then the theory TR would be decidable (which is not), since, for any closed formula C, we could effectively enumerate TR until either C or its negation appears.
8) From 7 we have that the set of all standardly valid formulas is not effectively enumerable.
An enumeration of all standardly valid formulas would yield an enumeration of all standardly valid formulas of L2A, since the set of formulas of L2A is decidable.
9) There is no effective formal system whose theorems are the standardly valid formulas of L2A.
If there were such an axiom system, we could enumerate the standardly valid formulas of L2A, contradicting 7.
10) Incompleteness of Standard Semantics : There is no effective formal system whose theorems are all standardly valid formulas.
If there were such an axiom system, we could enumerate the set of all standardly valid formulas, contradicting 8.
The last fact clearly distinguishes second-order logic from first-order logic, since Gödel’s completeness theorem tells us that there is an effective formal system whose theorems are all logically valid first-order formulas.
It's a complicated proof.
Assume we have first-order predicate calculus and basic arithmetic. We can encode logical statements numerically. (This entire posting is represented by a string of bits by the time anyone reads it, for example.) Now, supposing that we have a rigid logical system, with axioms and derivation rules, we can prove some propositions and we can prove that some can't be proven. For example, given reasonable axioms and derivation rules, "3 is prime" can be proved, but "3 is composite" can't be proved. We have three classes of propositions: ones we can prove true, ones we can prove false, and ones that we can't prove either way yet.
Now, if you will imagine a montage of blackboards and talks by someone who's better at formal logic than I am....
Provability is a numerical relation. It is possible to express numerically if a proposition can be proved. Provability is therefore a numerical relation, and we can express that relation in a proposition, which we can turn into an unimaginably large number, which we may as well call N. We can also create a number U that represents the complement of provabiity.
Given U, we can construct a number P. (Pretend we come up with it while you're on a bathroom break, since I don't remember the details.) When we decode P, we read that proposition P is not provable.
Now, there are two possibilities. P could be true, in which case we have a true statement that can't be proven, so the logical system is incomplete. It could be false, in which case it is provable, and we can prove a false proposition, so the logical system is inconsistent.
Now, we can add rules to patch this up, so that P is either provably true or provably false. At that point, we've changed what provability is, so we come up with a far bigger unimaginably large number N1, and so get U1 and come up with a new P1, which says "Proposition P1 is unprovable even with our new rules", and we're back where we started.
