Undecidability and incompleteness
Peter James Smith · Cambridge University Press eBooks · 2013
With a bit of help from Church's Thesis, our Theorem 39.2 – Q is recursively adequate – very quickly yields two new Big Results: first, any nice theory is undecidable; and second, theoremhood in first-order logic is undecidable too. The old theorem that Q is p.r. adequate is, of course, the key result which underlies our previous incompleteness theorems for theories that are p.r. axiomatized and extend Q. Our new theorem correspondingly underlies some easy (but unexciting) generalizations to recursively axiomatized theories that extend Q. More interestingly, we can now prove a formal counterpart to the informal incompleteness theorem of Chapter 7. Some more definitions We pause for some reminders, interlaced with definitions for some fairly self-explanatory bits of new jargon. (a) First, recall from Section 3.2 the informal idea of a decidable property, i.e. a property P whose characteristic function cP is computable. In Section 14.6 we introduced a first formal counterpart to this idea, the notion of a p.r. property, i.e. one with a p.r. characteristic function. However, there can be decidable properties which aren't p.r. (as not all effective computations deliver primitive recursive functions). We now add: A numerical property P is recursively decidable iff its characteristic function cP is μ -recursive. That it is to say, P is recursively decidable iff there is a μ -recursive function which, given input n , delivers a 0/1, yes/no, verdict on whether n is P . The definition obviously extends in a natural way to cover recursively decidable numerical relations. …