Prev: How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent(EASY PROOF)
Next: Herc does not understand any induction schema
From: MoeBlee on 1 Jul 2010 11:40 On Jun 30, 5:01 pm, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > The two claims > > T proves that Q is consistent. > > and > > If T is consistent, so is Q. > > are not the same. Right! Thanks for saying this. MoeBlee MoeBlee
From: MoeBlee on 1 Jul 2010 17:49 On Jul 1, 3:24 pm, herbzet <herb...(a)gmail.com> wrote: > If a consistent theory can prove a consistent theory inconsistent, Which can happen, since a consistent theory might prove false (false in the sense of arithmetic) theorems. > why can't a consistent theory prove an inconsistent theory consistent? Because if a theory T is inconsistent then there is derivation in T of an inconsistency. So the metatheory witnesses that derivation, thus the metatheory proves T is inconsistent. MoeBlee
From: herbzet on 1 Jul 2010 19:19 MoeBlee wrote: > herbzet wrote: > > > If a consistent theory can prove a consistent theory inconsistent, > > Which can happen, since a consistent theory might prove false (false > in the sense of arithmetic) theorems. > > > why can't a consistent theory prove an inconsistent theory consistent? > > Because if a theory T is inconsistent then there is derivation in T of > an inconsistency. Yes ... > So the metatheory witnesses that derivation, thus > the metatheory proves T is inconsistent. Surely, if the metatheory demonstrates "T is inconsistent", and the metatheory is consistent, then the metatheory does not also demonstrate "T is consistent". But if T demonstrates an inconsistency (and is thus inconsistent), then why must a consistent metatheory of T be able to witness (demonstrate?) that? (1) Not really sure what a "metatheory" is. If a theory X is capable of expressing "theory Y is inconsistent", is that sufficient to make theory X a metatheory of theory Y? (Because my question quoted at the top of this post assumes only a little more than that -- it assumes that X can not only express "Y is inconsistent" but also provide that string with a derivation -- positing also, of course, that X is consistent.) (2) Not sure what "witness" means in this context, what it means for some theory X to "witness" a feature of some theory Y. Above, I just guessed at its meaning. -- hz
From: MoeBlee on 1 Jul 2010 19:45 On Jul 1, 6:19 pm, herbzet <herb...(a)gmail.com> wrote: > MoeBlee wrote: > > herbzet wrote: > > > > If a consistent theory can prove a consistent theory inconsistent, > > > Which can happen, since a consistent theory might prove false (false > > in the sense of arithmetic) theorems. > > > > why can't a consistent theory prove an inconsistent theory consistent? > > > Because if a theory T is inconsistent then there is derivation in T of > > an inconsistency. > > Yes ... > > > So the metatheory witnesses that derivation, thus > > the metatheory proves T is inconsistent. > > Surely, if the metatheory demonstrates "T is inconsistent", > and the metatheory is consistent, then the metatheory does > not also demonstrate "T is consistent". Exactly. > But if T demonstrates an inconsistency (and is thus inconsistent), > then why must a consistent metatheory of T be able to witness > (demonstrate?) that? If I'm not mistaken, Aatu mentioned that we're talking about theories of a certain kind. I surmised (am I not correct?) that certain things about these theories here assumed, such as that the one theory is adequate to talk about the other theory in such basic ways (for lack of a more technical way of my putting it at this moment). > (1) Not really sure what a "metatheory" is. Doesn't matter. You were talking about theories proving things about theories. I'm just using 'meta-theory' to refer to the theory that's doing the proving about another theory (the object theory). > (2) Not sure what "witness" means in this context, what it means > for some theory X to "witness" a feature of some theory Y. For example, say Z set theory is "talking about" (is a meta-theory) for PA. If PA is inconsistent, then we can prove that in Z, just by displaying, in Z, the first proof (in an enumeration of PA proofs) of a contradiction P & ~P. We display it in Z in the sense that that proof (that sequence of formulas) is an OBJECT itself that Z talks about. So if PA is inconsistent, then in Z we have a theorem that "says", "there is a sequence of formulas that is a proof in PA such that the last entry of that sequence is a formula "P & ~P" of PA". Z talks DIRECTLY (not even any "Godel coding" needed) about |-_PA. I.e., Z can talk about provability in PA. In fact, in Z, we can DEFINE PA itself (a certain set of sentences, as sentences themselves are certain objects that Z may directly talks about) and define provability in PA and define truth in a given model for the language of PA, and define the standard model for the language of PA, and all kinds of things about PA. And one of these things is to talk about a specific PA proof that happens to have as it's last entry a PA formula "P&~P" (of course IF there is such a PA proof). MoeBlee
From: herbzet on 1 Jul 2010 20:50
MoeBlee wrote: > herbzet wrote: > > MoeBlee wrote: > > > herbzet wrote: > > > > > > If a consistent theory can prove a consistent theory inconsistent, > > > > > Which can happen, since a consistent theory might prove false (false > > > in the sense of arithmetic) theorems. > > > > > > why can't a consistent theory prove an inconsistent theory consistent? > > > > > Because if a theory T is inconsistent then there is derivation in T of > > > an inconsistency. > > > > Yes ... > > > > > So the metatheory witnesses that derivation, thus > > > the metatheory proves T is inconsistent. > > > > Surely, if the metatheory demonstrates "T is inconsistent", > > and the metatheory is consistent, then the metatheory does > > not also demonstrate "T is consistent". > > Exactly. > > > But if T demonstrates an inconsistency (and is thus inconsistent), > > then why must a consistent metatheory of T be able to witness > > (demonstrate?) that? > > If I'm not mistaken, Aatu mentioned that we're talking about theories > of a certain kind. I surmised (am I not correct?) that certain things > about these theories here assumed, such as that the one theory is > adequate to talk about the other theory in such basic ways (for lack > of a more technical way of my putting it at this moment). Yeh -- what *exactly* is being assumed has not been grindingly specified at a low level. We're not there yet. Hopefully, we won't have to go there. > > (1) Not really sure what a "metatheory" is. > > Doesn't matter. You were talking about theories proving things about > theories. Right. > I'm just using 'meta-theory' to refer to the theory that's > doing the proving about another theory (the object theory). Then we're about on the same page. We're going to have to continue to be careful about saying that X "proves" phi about Y, distinguishing formal proof from, y'know, that other thing, *proof*. I'm migrating to the terms "demonstration" or "derivation" for "formal proof". > > (2) Not sure what "witness" means in this context, what it means > > for some theory X to "witness" a feature of some theory Y. > > For example, say Z set theory is "talking about" (is a meta-theory) > for PA. If PA is inconsistent, then we can prove that in Z, just by > displaying, in Z, the first proof (in an enumeration of PA proofs) of > a contradiction P & ~P. We display it in Z in the sense that that > proof (that sequence of formulas) is an OBJECT itself that Z talks > about. So if PA is inconsistent, then in Z we have a theorem that > "says", "there is a sequence of formulas that is a proof in PA such > that the last entry of that sequence is a formula "P & ~P" of PA". Yes, we have a witness, in the sense that we can display the demonstration in PA of a contradiction, and then reason by FOL to "There exists a demonstration in PA of a contradiction" (I forget the name of the rule of inference P(term) |- Ex (Px). ) What we worry about is for an arbitrary metatheory and theory X and Y respectively we may have a pure existence proof in X of a contradiction in Y, without an actual contradiction to display. Or more generally, a derivation of some sort in X of the string "Y is inconsistent" that happens not to be sound. > Z talks DIRECTLY (not even any "Godel coding" needed) about |-_PA. > I.e., Z can talk about provability in PA. In fact, in Z, we can DEFINE > PA itself (a certain set of sentences, as sentences themselves are > certain objects that Z may directly talks about) We'd have to use abbreviative definitions so that the Z strings in question are typographically identical to PA strings. Or else rely on our ability to recognize that certain defined Z strings correspond to PA strings. > and define > provability in PA and define truth in a given model for the language > of PA, and define the standard model for the language of PA, and all > kinds of things about PA. And one of these things is to talk about a > specific PA proof that happens to have as it's last entry a PA formula > "P&~P" (of course IF there is such a PA proof). Yeh -- whew. -- hz |