 |
 | Home | Contact Us | FAQ | Search & Site Map | Link to Us |
 | Sign In | Join | Other 45 Sites in Network |
Math Forum / Mathematics / Mathematical Logic / January 2008What's the weakest metatheory in which Goedel's theorem can be proved?
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. > Bounded Arithmetic Would you specify the language and axioms of bounded arithmetic and perhaps remark on how it compares with the first order theories of PRA, Robinson arithmetic, and PA? Thanks, MoeBlee > > Bounded Arithmetic > [quoted text clipped - 5 lines] > > MoeBlee All right. Let me try to be sure I get this right. Bounded arithmetic has all the axioms of Robinson arithmetic, plus every instance of the induction schema where all the quantifiers are bounded. To make it stronger, add exponentiation to the language with the obvious axioms. Now add every instance of the induction schema where all the quantifiers are bounded in the new language. This is Exponential Function Arithmetic, or EFA. Now we can add superexponentiation, and supersuperexponentiation, and so on. Each theory in this hierarchy can prove the consistency of the theory two levels down. If you take the union of all these theories, you get the deductive closure of PRA in classical logic. Sigma-1- induction arithmetic is conservative over this theory for pi-1- sentences. Then you have sigma-2-induction arithmetic, sigma-3- induction arithmetic, and so on, and the union of all these theories is PA. A useful way of thinking about the strength of these theories is in terms of the provably total recursive functions. The provably total recursive functions of PA are those with level less than epsilon-zero in the Wainer hierarchy. You can interpret PA in a theory which is "logic-free" like PRA and has symbols for all these functions. There is a good description of this in "Proof Theory" by Kurt Schutte. I think also, considering the tower of theories starting with Bounded Arithmetic, EFA, and so on, there are "logic-free" counterparts for these theories along the lines of PRA over which they are at least pi-1-conservative. With Bounded Arithmetic we would have the symbols for the polynomial-time-computable functions (polynomial-time- computable using base 1 notation), then for EFA we would have symbols for the elementary recursive functions, and so on, increasing in computational complexity as we move up the tower. I'm not sure about this part of it, however. I'd like to know more about this topic, particularly about the relationship between the intuitionistic versions of these theories, the classical versions of these theories, and the "logic-free" versions of these theories. But the impression I get is that the differences are not that important. Bounded Arithmetic can be interpreted in Robinson Arithmetic. A good discussion of theories which can be interpreted in Robinson Arithmetic is in Edward Nelson's "Predicative Arithmetic", which is available for free at his website. Edward Nelson is the most extreme mathematical skeptic that I know of. In "Predicative Arithmetic" he reports his attempts to prove in Bounded Arithmetic that exponential is not total. This would imply that EFA is inconsistent. Bounded Arithmetic is just about the weakest system in which we can do any reasonable amount of mathematics. > Bounded Arithmetic is just about the weakest system in which we can do > any reasonable amount of mathematics. There is no sense to your thread's title or to this remark. The strength of systems is not a well-ordering, and among a class of systems there may not be a "weakest" system. > > Bounded Arithmetic is just about the weakest system in which we can do > > any reasonable amount of mathematics. > > There is no sense to your thread's title or to this remark. The > strength of systems is not a well-ordering, and among a class of > systems there may not be a "weakest" system. The class of systems which logicians generally consider to be reasonable metatheories in which to reason about object theories is well-ordered, pretty much, or at any rate certainly well-founded. (You might consider something like PRA+Con(ZF), perhaps). There might be some counterexamples, perhaps, such as the weak arithmetic you've been investigating. It doesn't matter. The title of the thread and my statement were reasonable. > > > Bounded Arithmetic > [quoted text clipped - 59 lines] > Bounded Arithmetic is just about the weakest system in which we can do > any reasonable amount of mathematics. Thanks, I'll be reading that over tonight. MoeBlee |
Reply to this Message |
 Sign In
 Join
 My Latest Posts My Monitored Threads My Blog My Photo Gallery My Profile My Homepage Start New Thread Enable EMail Alerts Rate this Thread
|
©2010 Advenet LLC Privacy Policy - Terms of Use
This website includes both content owned or controlled by Advenet as well as content owned or controlled by third parties.