- 8,943
- 2,955
sysprog said:Similarly, the statement "this statement is not provable" is by its form a second-order statement, in that it refers to a statement, and not directly to a logical or empirical fact. The statement is improper, because its referent is a second-order statement. The statement "the statement '2 + 2 = 4' is provable" is a valid and true second-order statement; not a first-order statement -- the first-order statement "2+ 2 = 4" is a legitimate first-order statement within the second-order statement as its first-order referent.
Yes, "this sentence is not provable" seems like a second-order statement, but it's not. That's the beauty of Godel's proof.
What Godel did was to come up with a way to map the "second-order" concept of proof to first-order concepts. The idea is roughly this:
- Come up with a numerical "code" for each statement of arithmetic. For example, you can write down the statement using ASCII characters. Each ASCII character can be represented as a base-8 numeral. Concatenate all the base-8 numerals in a statement to get a base-8 number. Given a code, we can talk about [itex]S_n[/itex], the nth statement of arithmetic. Every statement of arithmetic will be [itex]S_n[/itex] for some value of [itex]n[/itex]
- Similarly come up with a code for each proof in the theory of Peano arithmetic.
- Then corresponding to "the set of provable statements of arithmetic" is a set of numbers, "the set of codes of provable statements of arithmetic".
- Show that this set of numbers can be defined by a formula of arithmetic. So there is some formula [itex]P(x)[/itex] with one free variable, x, such that for every natural number [itex]n[/itex], we have that [itex]P(n)[/itex] is true (and in fact, provable in Peano arithmetic) if and only if [itex]S_n[/itex] is a provable statement of arithmetic. What's important to note is the formula [itex]P(x)[/itex] is just an ordinary arithmetic formula, involving zero, plus, times, equality, etc.
- Come up with a statement [itex]G[/itex] with corresponding code [itex]g[/itex] (that is, [itex]G = S_g[/itex]) such that it is provable in Peano Arithmetic that [itex]G \Leftrightarrow \neg P(g)[/itex]
- [itex]G[/itex] is true if and only if [itex]G[/itex] is not provable.