One of the corollaries that easily follow from Gödel’s first incompleteness theorem for arithmetic is the incompleteness of second-order logic: there can be no proof system that generates all and only the validities of second-order logic. It follows from the incompleteness of arithmetic because for any sentences φ of first-order arithmetic, there is a sentence of second-order logic φ′ which is valid iff φ is true in the standard model. So if second-order logic was recursively enumerable (r.e.) then true arithmetic (the sentences true in the standard model) would be r.e. Now you may ask (and students regularly do ask): but what if Gödel’s theorem had been false? What if arithmetic were complete? Would second-order logic then be complete, too? This question is usually not answered in the usual textbooks (at least I wasn’t able to find it covered in the ones I looked). Now a conditional with a necessarily false antecedent is true, so “if arithmetic were complete, second-order logic would still be incomplete” is trivially true. But there’s of course a way to give a non-trivial answer: There is no Turing machine that churns out all the valid sentences of second-order logic, even if that machine has access to an oracle which answers “yes” or “no” according to whether any given sentence of arithmetic is true in the standard model. (The function of such an oracle, of course, cannot itself be performed by a Turing machine, since the set of Gödel numbers of true arithmetic sentences is undecidable, and not even r.e.) That this is so is most easily seen by thinking of computability in terms of definability.
A set V of numbers is Σ01-definable if there is a Σ01 formula ψ(x) of arithmetic (one existential quantifier, then only bounded quantifiers) with a free variable x so that ψ(n) is true in the standard model iff n ∈ V. V is r.e. iff it is Σ01-definable. (In one direction: ψ(x) says “there is a number k which codes a computation of a Turing machine started on input l ≤ k and with output n.”) If W is a set of numbers, we say that V is Σ01(W)-definable if there is a formula ψ(x, Y) with a second-order variable Y so that n ∈ V iff ψ(n, Y) is true in the standard model when Y is interpreted as the set W. V is enumerable by a Turing machine with access to an oracle for W iff it is Σ01(W)-definable.
If we let TA be the set of Gödel numbers of the true sentences of arithmetic and Val2 the set of Gödel numbers of valid sentences of second-order logic, our question:
Is Val2 enumerable by a Turing machine with an oracle for TA?
can be restated as:
Is Val2 Σ01(TA)-definable?
It isn’t: the class {TA} is definable in arithmetic, that is, there is an arithmetical formula σ(Y) with a free second-order variable Y so that σ(Y) is true iff Y = TA (see Theorem 23.2 in Boolos, Burgess, Jeffrey, Computability and Logic, 4th ed.). So if Val2 were Σ01(TA)-definable by some formula ψ(n, Y), it would then also be definable in second-order arithmetic by the formula ∃ Y(σ(Y) ∧ ψ(n, Y)). And if Val2 were definable in second-order arithmetic, then TA2, the set of Gödel numbers of true sentences of second-order arithmetic would be definable in second-order arithmetic, since the Gödel number of a sentence α of second-order arithmetical sentence is in TA2 iff the Gödel number of PII → α is in Val2 (where PII is the conjunction of the the second-order Peano axioms, as in Example 22.6 of BBJ). But by Tarski’s Theorem, TA2 is not definable in second-order arithmetic (see Theorem 41C of Enderton’s A Mathematical Introduction to Logic).
Hi Richard!I like the argument. But I guess that — given that Tarski’s Theorem yields Gödelian incompleteness in short step, and is proved via Gödelian diagionalization — your argument might still be said to be “almost” Gödelian!But if your students are asking, in effect, “Is there a proof of the incompleteness of second-order logic that doesn’t go via any sort of fancy Gödelian argument” then what’s wrong with the standard argument via compactness? (For other readers! Take the sets of wffs {First-order successor axioms, Second-order induction axiom, w =/= 0, w =/= 1, w =/= 2…} The set is inconsistent, because the successor axioms plus induction tell us that everything in the domain is zero or one of its successors, so there can’t be a w distinct from them all. But any finite subset is consistent. So second-order consequence isn’t compact. So it can’t have a complete formal axiomatization.) Kind regards, Peter Posted by Peter Smith
This just shows that consequence doesn’t have a complete axiomatization — but not that validity doesn’t.You’re of course right with your other point, although it is not entirely obvious that incompleteness implies that Val2 is not r.e., and so I tried to avoid formulating the argument without incompleteness. Posted by Richard Zach
Ah … but of course, of course! Guilty of a very careless reading there!! So: the argument for second-order logic not being strongly complete is “direct and easy”; one very familiar argument for second-order logic not being weakly complete is (shall we say) “indirect and fancy”, going via Gödel’s incompleteness theorem. That’s certainly how things are done on e.g. page 87 of Shapiro’s book.Shapiro doesn’t actually comment there on that perhaps initially surprising contrast (and I can’t remember him commenting on that constrast elsewhere in book either, but that means nothing!!). So another good question in the same neck of the woods to your students’ “what if …” question is: “Does there have to be that asymmetry? Could there be an ‘easy’ proof of weak incompleteness that doesn’t tangle (broadly speaking) Gödelian arguments?” But that’s not your question! Posted by Peter Smith
This may not be directly relevant, but…I’ve seen is stated repeatedly (by people that should know), though never seen it proved in print, that the set of valid sentences of SO logic, not only fails to be Sigma-0-1, but is not Sigma-m-n for any finite m and n. Does anyone know how this is proved?Best, Panu Posted by Panu Raatikainen
My argument shows that Val^2 not Sigma^1_n for any n. Joukko Vaananen has a nice paper in the BSL (Second-Order Logic and Foundations of Mathematics , Jouko Vaananen, The Bulletin of Symbolic Logic, Vol. 7, No. 4. (Dec., 2001), pp. 504-520). On p. 517, he gives a reference for the more general result, and also shows that Val^2 is Pi_2 complete in set theory.Jouko’s references for the Sigma^m_n result are toHintikka, Reductions in the theory of types, Acta Philosophica Fennica 8 (1955) 57-115.Montague, Reduction of higher-order logic. Theory of models (Proceedings of the 1963 international symposium in Berkeley), North Holland, 1965, 251-264. Posted by Richard Zach
PS to Peter: a. Showing that Val^2 is not r.e. by showing TA^2 is incomplete via Goedel’s theorem also requires Craig’s Trick: whatever’s r.e. is also recursively axiomatizable. (That’s why it’s not obvious.)b. Showing that Val^2 is not Sigma^0_1 or Sigma^1_1 or whatever can be proved using diagonalization. But you can only diagonalize if you have a proof/truth predicate in the language. If you want to show that Val^2 is not Sigma^0_1(W) this way (as I did above), you need W to be definable in the langauge. For the case of W = TA, this is the case, but it isn’t in general. For instance, by Vaananen’s result (that Val^2 is Pi_2 definable in set theory), Val^2 is Sigma^0_1(W) for W the Goedel numbers of the Pi_2 sentences of set theory true in V. Posted by Richard Zach
Hello Panu!The easy way to show that second order validity is not Sigma-m-n is based on a device originally devised by Hintikka, I think, found in the article referred to by Zach (which I’ve never read… I have no idea where I originally learned this stuff from). The trick is as follows: introduce infinitely many new predicate symbols P_0, P_1, … and consider the second order PA with all axioms restricted to P_0. Then add an axiom saying that P_1 comprises the powerset of P_1, an axiom saying that P_2 the powerset of P_1 and so forth. Now, for any Sigma-m-n sentence P there is a conjunction S of a finite subset of the axioms of the new theory such that S –> P’ is a second order validity iff P is true, where P’ is obtained from P by replacing first order quantifiers with quantifiers restricted to P_0, second order quantifiers to P_1 and so forth. Thus Sigma-m-n truth reduces to second order valditiy. Posted by Aatu Koskensilta
Yes, of course, I should have seen the relevance of Hintikka’s trick (which I’ve known for a long time) here… Thanks!Best, Panu Posted by Panu Raatikainen
Of course, the easy proof of second order validity not being Sigma-m-n shows more than stated in the theorem: it shows that Sigma^1 validity already isn’t Sigma-m-n for any m,n. (You need only universal second order quantifiers in the S of S –> P’, which is equivalent to ~S \/ P; thus S –> P’ is Sigma^1). So IF-validity (validity of sentences in the language of Independence Friendly logic of Hintikka and co), for example, is also not Sigma-m-n for any m,n.Panu and Richard know all this already, but perhaps someone will find it interesting. Posted by Aatu Koskensilta
While I’m at it, here’s a problem I’ve been playing with: give a “nice” example of an axiomatizable complete second order theory that is not categorical. (Here we take “T is complete” to mean “for all A, either T |= A or T |= ~A”). I haven’t been able to come up with an answer yet, though perhaps something like the following (in the language of set theory) might do the trick: T = “the universe has a cardinality of cofinality omega” + for every formula P “the class of second order definable cardinals is not defined by P” + for every formula P “if P then P relativized to V_kappa for some kappa”…Any ideas? Posted by Aatu Koskensilta