What's the weakest metatheory in which Goedel's theorem can be proved?
- From: Rupert <rupertmccallum@xxxxxxxxx>
- Date: Sun, 27 Jan 2008 19:24:35 -0800 (PST)
In the silly elsiemelsi threads, the issue has come up of in what
metatheory Goedel's theorem can be proved. I've been known to say such
things as "Goedel's theorem can be proved in Bounded Arithmetic". I've
been having a think about this lately. It seems to me that the
following two statements can be proved in Bounded Arithmetic.
Let n be the number of a Turing machine whose range consists of
sentences in the first-order language of arithmetic. Given n, we can
find a number m which is the Goedel number of a sentence GR (Goedel-
Rosser) with the following property. Given a proof of GR or ~GR in the
theory T which is the deductive closure of the axioms of Robinson
Arithmetic together with the range of our original Turing machine, we
can construct an inconsistency in T.
Let n be the number of a Turing machine whose range consists of
sentences in the first-order language of arithmetic. Given n, we can
construct a number m which is the Goedel number of the consistency
sentence for the theory T which is the deductive closure of the axioms
of Sigma-1-induction arithmetic together with the range of our
original Turing machine. Then, given a proof of this consistency
sentence in T, we can construct an inconsistency in T.
As I say, it seems to me that these two statements can be proved in
Bounded Arithmetic. In that sense, Goedel's two theorems go through in
Bounded Arithmetic. Someone let me know if I'm wrong here and I need
something a bit stronger.
However, elsiemelsi seems to be keen to focus on Goedel's original
paper. The main result of that is Proposition VI which can be
paraphrased as "Every omega-consistent primitive recursive extension
of P is pi-1-incomplete." As far as I can tell, this goes through fine
in Bounded Arithmetic so long as we remain agnostic about whether the
Turing machines that compute primitive recursive functions actually
halt. The key point is that given a proof of a sentence in a theory T,
we can construct a proof in P that the sentence can be proved in T.
This will be all right so long as we count as part of the code for the
proof the computation that witnesses that such-and-such an axiom
belongs to the primitive recursive set of axioms by which we are
extending P. However, there is some difficulty in formulating a
version which goes through in Bounded Arithmetic and perhaps it would
be more natural to say that it goes through in Primitive Recursive
Arithmetic plus Ackermann's function.
.
- Follow-Ups:
- Prev by Date: Re: Gödel's system P, Principia Mathematica, and the reducibility axiom
- Next by Date: Re: Some answers to Aatu Koskensilta
- Previous by thread: Gödel's system P, Principia Mathematica, and the reducibility axiom
- Next by thread: Re: What's the weakest metatheory in which Goedel's theorem can be proved?
- Index(es):
Relevant Pages
|
