Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: Charlie-Boo on 9 Jan 2006 09:37 Barb Knox & "Charlie-Boo" wrote: > >Yes, but I use the standard symbol |- for provable instead of box []. > Maybe "standard" for you, but as others have pointed out, you appear to > be importing meta-level notations (|-) into the object level, which just > doesn't make sense. No, I didn't change the semantics, only the syntax. As I have pointed out, [] is used for many things in the literature but |- only means the intended semantics, so I use |- which is better from a system design point of view. > >> Letting P be []Q, this implies: > >> (1) ([]Q <-> []Q) -> []([]Q <-> Q), i.e. > >> []([]Q <-> Q). > > > >> This is false in any system where provability is different from truth. Yes, it has been pointed out in effect that for any wff R that expresses a non-empty r.e. relation [another system design improvement: call it an r.e. wff] and Godel sentence G, the wff G^R expresses an r.e. relation but its truth does not coincide with its provability. I thanked the nice man for pointing that out and now am working on making sure when this condition holds. My need is to apply this Metatheorem to wffs that express (both r.e. and non-r.e. relations) "x is provable", "x is not provable", "x proves y", and "x does not prove y" to derive various Incompleteness Theorems. Now it seems I have to worry about how they are expressed! The great irony is that a theorem intended to replace (also generate) Godel sentences is foiled by one! But I think the Metatheorem can be worded to include the above relations with special consideration for (or elimination of) how the relation is expressed. That is what I am researching now. Which wffs express and represent the same relation? Tell me, o' wise one. C-B > >No. It isn't []Q <-> Q. It's []([]Q < - >Q) > > What are you disagreeing with? I wrote []([]Q <-> Q). Of course, in S4 > model logic, []P->P, so you also get []Q<->Q. > > > >> And indeed, []([]Q -> Q) says the system can prove its own consistency, > >> which means (via Goedel) that it either is in fact inconsistent or is > >> weaker than arithmetic. > > > >This seems valid. I really need only the "hint": that P = |-P. > > But it doesn't. In S4, []P->P and []P->[][]P, but it is NOT the case > that P->[]P. Truth does not in general imply provability. > > >Since that means (|-P)=(|-Q) I thought that would imply |-(P=Q) but > >maybe not. Do you agree that P = |-P ? > > No, as above. > > >This is what I use to derive > >Incompleteness results from any Theory of Computation theorem of the > >form "(relation) is / isn't recursively enumerable." > > > >> If you want provability and truth to be the same, > > > >Only for P! > > What is that supposed to mean? "P" is a propositional variable, so > you're saying "only for everything". > > >C-B > > > >> you can dispense with > >> all the modal machinery and just use some existing well-thought-out > >> constructive logic (e.g. Intuitionistic). > > I still think this is good advice if you're in fact interested in > systems where truth and proveability are the same. > > > >> >C-B > >> > > >> >> > (P and Q have the same sets of free variables.) This simple theorem (I > >> >> > created 12/1/05) provides the link between Theory of Computation and > >> >> > Proof Theory (Incompleteness in Logic) that theoreticians such as > >> >> > myself have been looking for since the 1930's. (Each Theory of > >> >> > Computation theorem becomes an Incompleteness theorem in Logic, > >> >> > providing almost trivial formal derivation of the exact results of > >> >> > Godel, Rosser and Smullyan.) > >> >> > > >> >> > C-B > >> >> > > >> >> > Hint: Consider the equivalent ( P = |-Q ) => ( P = |- P ) > > -- > --------------------------- > | BBB b \ Barbara at LivingHistory stop co stop uk > | B B aa rrr b | > | BBB a a r bbb | Quidquid latine dictum sit, > | B B a a r b b | altum viditur. > | BBB aa a r bbb | > -----------------------------
From: Charlie-Boo on 9 Jan 2006 09:39 Daryl McCullough wrote: > Propositional intuitionistic logic is a *refinement* of case > analysis. It's not supposed to prove more wffs, it is supposed > to prove *fewer* wffs, and it succeeds. Any subset of the axioms and rules of any axiomatic system does that. Big wup! C-B > -- > Daryl McCullough > Ithaca, NY
From: H. J. Sander Bruggink on 9 Jan 2006 09:45 Charlie-Boo wrote: > H. J. Sander Bruggink & Charlie-Boo wrote: > >>>Case analysis does not prove anything that would deem the system >>>inconsistent. >> >>You didn't really get the point of my remark, did you? > > Are you attacking the messenger again? You are no messenger, because you have no news. >>As usual. >> >>Let me restate: the fact that "case analysis" (i.e. >>classical logic) proves more theorems than intuitionistic >>logic, does *not* make it a better logic. > > But given my above comment about consistency it is. You get more valid > conclusions. No you don't. You get conclusions that are not valid. E.g. P v ~P is not valid in intuitionistic logic. I repeat: *NOT VALID*. > Playing around with subsets is like Frege endlessly > proving propositional calculus wffs IL is of both philosophical and practical interest. The fact that you don't know that, says more about you than about IL. > (instead of doing something new and > nontrivial like formalizing Smullyan's hundreds of theorems as I do.) > > (Note that I deal in general principles that quickly reveal the folly > of these various regurgitations.) > > >>Sometimes we don't >>want P v ~P to be valid. >> >>The fact that this has to be explained to someone who is >>"formalizing computer science" is quite funny, btw. > > Then you need to show that I am not one of them or that you have > somehow contradicted my formalization. To whom exactly does "them" in your sentence refer? And why would I need to show I've contradicted someone's formalization, just to be amused by his incompetence in a particular topic? groente -- Sander
From: Daryl McCullough on 9 Jan 2006 09:53 Charlie-Boo says... > >Daryl McCullough wrote: > >> Propositional intuitionistic logic is a *refinement* of case >> analysis. It's not supposed to prove more wffs, it is supposed >> to prove *fewer* wffs, and it succeeds. > >Any subset of the axioms and rules of any axiomatic system does that. Yes, intuitionistic propositional logic is a *particular* subset of classical propositional logic, namely those that are provable using intuitionistically valid rules of inference. -- Daryl McCullough Ithaca, NY
From: Daryl McCullough on 9 Jan 2006 10:03
In article <1136816019.517876.14750(a)g43g2000cwa.googlegroups.com>, Charlie-Boo says... > >H. J. Sander Bruggink & Charlie-Boo wrote: > >> > Case analysis does not prove anything that would deem the system >> > inconsistent. >> >> You didn't really get the point of my remark, did you? > >Are you attacking the messenger again? Only in the sense of pointing out that the messenger doesn't know what he is talking about. >> Let me restate: the fact that "case analysis" (i.e. >> classical logic) proves more theorems than intuitionistic >> logic, does *not* make it a better logic. > >But given my above comment about consistency it is. You get more >valid conclusions. But the additional conclusions *aren't* valid, intuitionistically. Whether a conclusion is valid or not depends on the *semantics* of the language, and intuitionism has a *different* semantics for propositional logic that classical logic. Think about the difference between the theory of real numbers and the theory of natural numbers. You can prove things using Peano arithmetic that are not provable in the theory of real numbers. For example: forall x, x*x >= x (The square of x is greater than or equal to x). That statement is provable using PA, but it is not provable using the theory of the reals. Does that mean that PA is a better theory? No, because that statement isn't *valid* for the reals. (In particular, if 0 < x < 1, then x*x < x.) The same thing is true of intuitionistic versus classical logic. They use the same syntax, but they have *different* semantics. Statements that are valid for classical logic are *not* valid for intuitionistic logic. If you want to prove things about intuitionistic semantics, then you *can't* use case analysis, because case analysis proves things that are not *valid* for that semantics. -- Daryl McCullough Ithaca, NY |