Gödel! #6 An Introduction to Gödel’s Theorems Chapter 3 Part 2

3.4 More Definitions

Some definitions we’ll be using:

i. Given a derivation of from the axioms of a theory in our particular logical apparatus, we say that is a theorem of . Symbolically, .

ii. A theory is sound iff all of its theorems are true (ie: iff ‘s interpretaion makes them true).

iii. A theory is decidable iff the property of being a theorem of is effectively decidable, ie: given a sentence there is a mechanical procedure for determining whether . This expands our notion of decidability from sentences/properties to theories.

iv. A theory  decides a sentence iff either or .

v. A theory is negation complete  iff decides every sentence in its language.

vi. is  inconsistent iff for some sentence we have both and .

The book draws attention to the idea that a theory can be decidable, without being negation complete (ie: able to decide any sentence). For example, a theory whose language contains three terms and the lone axiom . This language is decidable by using a truth table to see if a sentence is a theorem (ie: follows from the axioms) but, for example, the sentence cannot be decided by the theory.

3.5 The effective enumerability of theorems

A neat little theorem:

Theorem 3.1 If is an axiomatized formal theorey then (i) the set of wffs of , (i’) the set of sentences of , (ii) the set of proofs constructible in , and (iii) the set of theorems of can each be effectively enumerated.

Proof sketch of (i) and (i’): This one is pretty trivial, since is constructed from a finite alphabet (by our definition of axiomatized formal theory), its wffs and sentences can be enumerated by listing the length-1 strings in alphabetical order, followed by the length-2 strings and so on.

Proof sketch of (ii): Since a proof is just a linear sequence of sentences, we can take our enumeration of sentences from (i’) and enumerate them. This is a bit more complicated, since there we’re basically forming finite strings (our proofs) over an infinite, but countable alphabet (our sentences). One way of doing this will result in an enumeration where all the even numbered proofs (starting at 0) are length-1, then every other odd number will be length-2 sentence, then every other remaining number will be a length-3 sentence, and so on, and you eventually squeeze every sentence into your enumeration. The details of this are tricky, but its the same general idea as enumerating a set of programs in a given programming language, or the set of all tuples. As we go along, we must use the mechanical procedure for determining whether something counts as a valid proof (built into our definition of an axiomatized formal theory) to check whether our proof is valid. If it isn’t then we don’t count it.

Proof sketch of (iii): As with (ii), only this time we only record the conclusions from our valid proofs.

The text draws attention to the idea that just because we can enumerate all of the theorems of a theory, doesn’t make that theory decidable. The gist of this idea is that given a sentence that isn’t a theorem, we can’t simply compare it to our list of theorems to see if it isn’t on there, due to the fact that our list is infinite and we won’t know when to stop checking.

3.6 Negation-complete theories are decidable

Despite the above, there is an important special case: negation-complete theories.

Theorem 3.2 Any consistent, axiomatized, negation-complete formal theory is decidable.

Proof: Since either or for any given , we can simply enumerate all of ‘s theorems until or shows up. If we get then it is a theorem, and if we get then since is consistent, we know is not a theorem.

This concludes chapter 3. Coming up next is a little bit about the language of arithmetic and using it to express numerical properties and relations. After that, in chapters 5 and 6 we return to Gödel’s theorems and see two new ways of making the incompleteness theorems apparent. I’ll likely skip chapter 7 as it simply spells out what’s coming up in later chapters, and then in chapters 8 and 9 we’ll talk about two specific theories of arithmetic: Baby Arithmetic () and Robinson Arithmetic ()