arithmetic in ZF
in [Logic]
|
Prev: What is wrong with this argument?
Next: Courage?
From: H. Enderton on 5 Apr 2005 22:31 In a recent post, Bhup pointed out (correctly) that we can interpret PA into ZF. But then the post went on to say: >6. Hence, if ZF is consistent, then every Arithmetical proposition is >syntactically (i.e., independently of the semantic connotations of the >above definitions of "truth" and "satisfiability") decidable from the >axioms of ZF. As George Greene remarked, this is wrong. The arithmetic sentences provable in ZF (i.e., the arithmetic sentences whose interpretations are provable in ZF) make up "merely" an r.e. set of sentences. If we assume ZF is sound for arithmetic, then they make up an r.e. set of true sentences. This can't possibly be anywhere close to being the set of all true sentences of arithmetic (because the latter is not r.e., or even arithmetical). Let's give a name to the set: Tzf = the set of sentences of arithmetic whose interpretation is provable in ZF. Then Tzf is a theory (it is closed under provability) and, being r.e., it is a recursively axiomatizable theory extending PA. (Tzf proves Con PA.) And someone once told me a "natural" recursive axiomatization of Tzf. Unfortunately, I have forgotten what it is. Does someone out there in sci.logic land know what it is? --Herb Enderton
From: Torkel Franzen on 6 Apr 2005 08:21 hbe(a)sonia.math.ucla.edu (H. Enderton) writes: > And someone once told me a "natural" recursive axiomatization of > Tzf. Unfortunately, I have forgotten what it is. Does someone > out there in sci.logic land know what it is? It would be odd if there were such a thing.
From: george on 7 Apr 2005 11:02 H. Enderton wrote: > In a recent post, Bhup pointed out (correctly) that we can interpret > PA into ZF. But then the post went on to say: > > >6. Hence, if ZF is consistent, then every Arithmetical proposition is > >syntactically (i.e., independently of the semantic connotations of the > >above definitions of "truth" and "satisfiability") decidable from the > >axioms of ZF. > > As George Greene remarked, this is wrong. The arithmetic sentences > provable in ZF (i.e., the arithmetic sentences whose interpretations > are provable in ZF) make up "merely" an r.e. set of sentences. One thing that misled me in that presentation was multiple ways of "interpreting" the act of "interpretation". I was thinking purely in terms of the Tarskian sense of an interpretation as a mapping from the language (or its parts) to some model-theoretic structure. But there is another available and relevant sense of "interpretation" that does NOT involve interpretations-of-a-theory-into-structures/models at all, but rather is a purely LINGUISTIC sense of "interpretation" in which one takes elements of the language of Arithmetic and simply TRANSLATES them into language-of-ZF. In particular, if one maps the interpretation to the *sentence*, it becomes ambiguous which of these two "interpretations" (of "interpretation") is meant. If you take some trivial arithmetical sentence like s(0)+s(s(0))=s(s(s(0))) (which happens to be a theorem), you could use ZF to construct a model of PA and ask what the interpretation of this sentence was in that model (0 will be the empty set, s(.) will be some unary-function-represented-as-a-ZF-set, +(.,.) will be a binary function, = will be a binary predicate, and the predicate will assign T as the truth-value of the overall sentence). BUt you could instead/also just ELIMINATE everything occurring in this arithmetical language, including =, by translating it into something involving only e (there are formulations of ZF where e is the only predicate and where no function- symbols are needed at all, although the canonical dialect has them). s(x) would be x U {x}; x=y would be Az[zex<->zey]; and + and * would be, well, complicated, but basically they would be the least ordinal bijectible with some set constructed from the two argument sets (in the case of multiplication, that set could be, conventionally, the cartesian-product of the argument sets). My point is that if one wants to talk about an "axiomatization" of arithmetic under ZF, then new "axioms" one needs are instead DEFINITIONS of the linguistic entities from the language of arithmetic in the language of ZF. I know, definitions often ARE axioms, but my point is that axioms are usually NOT definitions. I mean definitions as conservative, as purely abbreviatory. > Let's give a name to the set: > Tzf = the set of sentences of arithmetic whose interpretation is > provable in ZF. I guess "interpretation" here must be the "linguistic" interpretation, but when I was responding to Bhup, I was thinking in terms of the model-theoretic one. > Then Tzf is a theory (it is closed under provability) and, being > r.e., it is a recursively axiomatizable theory extending PA. > (Tzf proves Con PA.) But there is a problem with thinking about Con PA in this context, because Neither PA NOR ANY OTHER PARTICULAR AXIOMATIZATION of first-order arithmetic IS EVEN RELEVANT to this particular theory! One important thing about Con(PA) in the context of G1 was that it was IN THE SAME language as PA. In this context, though, Con(PA) is in the language of ZF and there is no reason to think of "the axioms of PA" as axioms. They are just theorems of ZF, and the question of what a provability- predicate expressing provability FROM PA would even look like gets COMPLICATED. The axioms of ZF are available for use in proving things at every step in this framework. HOw are you supposed to express about a derivation that it needs the PA-theorems but NOT the other/additional axioms-of-ZF, when in fact ALL those axioms are NEEDED to prove the theorem-hood of the PA-axioms?? > And someone once told me a "natural" recursive axiomatization of > Tzf. Unfortunately, I have forgotten what it is. Does someone > out there in sci.logic land know what it is? I don't, but I share your hope that somebody does. The only point I wanted to make (aside from confessing my own confusion under ambiguity of "interpretation") was that beyond the ZF axioms themselves, any axioms you even MIGHT possibly need to add are just definitions.
From: Bhupinder Singh Anand on 9 Apr 2005 23:06 On Apr 5, 7:31 pm, H. Enderton wrote: HE>> ... As George Greene remarked, this is wrong. <<HE I was actually seeking the putative flaw in the six steps of the reasoning. HE>> The arithmetic sentences provable in ZF (i.e., the arithmetic sentences whose interpretations are provable in ZF) make up "merely" an r.e. set of sentences. <<HE This assumes that there is an algorithm that can 'pick' out the provable arithmetic sentences of ZF. There may not be any such algorithm. In other words there may be no uniform effective method such that, given a sentence of ZF, it can determine whether or not the sentence is ZF-provable. However, given any ZF sentence, there may yet, always, be some effective method - which is unique to the sentence - of determining whether or not it is ZF provable. HE>> If we assume ZF is sound for arithmetic, then they make up an r.e. set of true sentences. <<HE Actually, my argument sought to establish that ZF can be sound for arithmetic, but that the set of arithmetical sentences provable in ZF need not be r.e. HE>> This can't possibly be anywhere close to being the set of all true sentences of arithmetic (because the latter is not r.e., or even arithmetical). <<HE Of course, the set of true sentences under the standard interpretation of any arithmetic such as PA is not r.e., since there are sentences, such as Goedel's PA-formula [(Ax)R(x)], such that: (i) [(Ax)R(x)] is not PA-provable, and so the standard interpretation, (Ax)R(x), of [(Ax)R(x)], is not Tarskian true algorithmically - in the sense that there is no algorithm such that, given any natural number n, it can determine that R(n) is true; (ii) the standard interpretation, (Ax)R(x), of [(Ax)R(x)], is Tarskian true non-algorithmically - in the sense that [R(n)] is PA-provable for every numeral [n], and so R(n) is true for every natural number n. However, since ZF admits arbitrary infinite sub-sets of the natural numbers, we can have the interpretation of [(AxR(x)] in ZF provable in ZF, even though the corresponding arithmetical sentence is not provable algorithmically. My argument is that whereas PA proves all, and only, algorithmically true arithmetical sentences, ZF proves all algorithmically, and non-algorithmically, true arithmetical sentences. The assumption that this does not exhaust the class of true arithmetical sentences would, then, be an implicit admission of the existence of arithmetical sentences that are Platonically true. HE>> ... Tzf is a theory (it is closed under provability) and, being r.e., it is a recursively axiomatizable theory extending PA. (Tzf proves Con PA.) <<HE Again, there may be no algorithm that will establish Tzf as r.e. Regards, Bhup
From: george on 10 Apr 2005 15:18
Bhupinder Singh Anand wrote: > HE>> The arithmetic sentences provable in ZF (i.e., the arithmetic > sentences whose interpretations are provable in ZF) make up "merely" an > r.e. set of sentences. <<HE > > This assumes that there is an algorithm that can 'pick' out the > provable arithmetic sentences of ZF. That's not just an assumption. Depending on how you interpret 'pick' (the fact that you needed quotes implies that interpretation is relevant and may vary here), this issue is decided, one way or the other -- that's basically the completeness theorem. If something is provable from a recursive first- order axiom-set, then you CAN PROVE that. There is an algorithm that proves it. But this problem is only semi-decidable in that there is no algorithm for proving that something DOESN'T follow from a (sufficiently rich) first-order axiom-set. In the special case when an algorithm for detecting independence/ NON-provability ALSO exists, we say that the theory is decidable. PA is un-(or semi-)decidable. > There may not be any such algorithm. Wrong; there is; it's known; except it doesn't "pick out" the theorems, but rather, RECURSIVELY ENUMERATES the theorems. This is only half of what we want, because if a candidate sentence is NOT a theorem, this algorithm won't confirm that. All you can do, basically, is start the theorem- enumerator running. If the sentence is eventually output by the enumerator, then it's a theorem. If it never is, then it isn't, but you're not generally going to know that a sentence "will never" be output by the theorem-enumerator; usually, all you can know is that it hasn't been output *yet*; and for PA and similarly complex first-order theories, you can't recursively bound the amount of time it might take to find the proof (or the proof-length), so you never know whether you have waited long enough yet. > In other words there may be Wrong; there is no "may" involved; the answers to these questions are known and this is basically the whole content of the original proof of Godel's first incompleteness theorem. > no uniform effective method such that, > given a sentence of ZF, it can determine whether or not the sentence is > ZF-provable. Indeed, for an absolute fact, there is no such "method", if, by "uniform effective method", you are willing to mean what everybody else means, namely, Turing Machine. However, the problem IS SEMI-decidable: there IS a method of CONFIRMING the theorem-hood of things that ARE theorems (there is just not one for confirming the non-theorem-hood of things that aren't). This is directly analogous to the halting problem. There IS a TM (namely, the universal TM) that halts on all&only those TMcode/input pairs where the encoded TM halts on the input. But there is no TM that halts on all&only those pairs where the TM DOES NOT halt on the input. > However, given any ZF sentence, there may yet, always, be > some effective method - which is unique to the sentence - of > determining whether or not it is ZF provable. Of course there is. Given any sentence, either the "method" that says "This sentence is provable" OR the method that says "This sentence is not provable" is correct. Both of them are certainly effective. You just don't generally have any way of telling WHICH of them is the "correct effective method". > HE>> If we assume ZF is sound for arithmetic, then they make up an r.e. > set of true sentences. <<HE > > Actually, my argument sought to establish that ZF can be sound for > arithmetic, but that the set of arithmetical sentences provable in ZF > need not be r.e. Again, simply, wrong. The class of sentences provable in FOL from a recursive axiom- set IS NECESSARILY, PROVABLY, ALWAYS, recursively enumerable. It may even be recursive as well (although in the cause of PA and ZF, it is not; that, again, is the whole content of Godel's 1st incompleteness theorem). |