Wouldn’t It be Cool if These Were Equivalent?
in [Logic]
|
From: Charlie-Boo on 26 Jun 2010 22:19 It would be cool if the following 3 things were equivalent: 1. |- (allX)P(X) 2. (allX) |- P(X) 3. ~ |- (existsX)~P(X) It would make a lot of things easier, you know? Like if I wanted to know if (allX) |- P(X) then all Id have to do is to look for a proof of (allX)P(X) and if I find one then I know that (allX) |- P(X). Or if I wanted to know if (existsX) ~ |- P(X) then I could look for a proof of (existsX)~P(X). Things like that. But, alas, the above cannot be. Obviously these 3 things are not equivalent, because . . . what? C-B
From: Charlie-Boo on 28 Jun 2010 07:52 On Jun 26, 10:19 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > It would be cool if the following 3 things were equivalent: > > 1. |- (allX)P(X) > 2. (allX) |- P(X) > 3. ~ |- (existsX)~P(X) The point is that if these were all equivalent, then we could do some things that we actually cannot. Form (1) shows the assertion is r.e. in that there is a procedure that will prove it if it is true. However, using form (2) we can express some propositions that are not immediately r.e. in this same sense. If the assertion being expressed by all 3 is "The system is consistent." then we would have a decision procedure for consistency: Look for a proof of ~TRUE and simultaneously look for a proof of (allX)P(X) where P is the wff such that e.g. (3) expresses the assertion that the system is consistent. If that is not clear, then consider this simpler problem: How do we prove that the following do not coincide? 1. P 2. |-P "These cannot be equivalent." is equivalent to what? These are topics of fundamental interest to Logic. If nobody will discuss them, then something is seriously wrong with this group. Actually, when people routinely give false references and attack each other ad hominem, it's already pretty bad. C-B > It would make a lot of things easier, you know? > > Like if I wanted to know if (allX) |- P(X) then all Id have to do is > to look for a proof of (allX)P(X) and if I find one then I know that > (allX) |- P(X). > > Or if I wanted to know if (existsX) ~ |- P(X) then I could look for a > proof of (existsX)~P(X). > > Things like that. > > But, alas, the above cannot be. Obviously these 3 things are not > equivalent, because . . . what? > > C-B
From: MoeBlee on 28 Jun 2010 12:44 On Jun 26, 9:19 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > It would be cool if the following 3 things were equivalent: > > 1. |- (allX)P(X) > 2. (allX) |- P(X) > 3. ~ |- (existsX)~P(X) I can help you here, if you're interested in understanding this. (1) is well formed. (2) is not well formed as you've given it. The reason is that you've mixed meta-language and object language in an incorrect way. (3) is not well formed as you've given it. The reason is that you've mixed meta-language and object language in an incorrect way. I'll explain: Let's say we have fixed some particular logical system pertaining to '|-' ('|-' is a symbol in the meta-language). 'G |- S' stands for 'the set of formulas G proves the formula S' and '|- S' stands for 'the formula S is provable from the axioms/rules of the logical system' So (1) is well formed. It asserts that AxPx is provable from the axioms/rules of the logical system. But (2) has a quantifier 'x' that is trying to cross over the '|-' symbol, which is not well formed. So, instead, I would write (2) as (2*): For all variables 'x', we have |- Px And (3) has the problem that you're intending to use the same negation sign in both meta-language and object language. So, instead, I would write (3) as (3*): It is not the case that |- Ex~Px Now, as restated, what we can correctly say (where the logical system is first order logic): (1) iff (2*) > Or if I wanted to know if (existsX) ~ |- P(X) Again, not well formed. What is well formed is: (4*) There is a variable 'x' such that it is not the case that |- Px MoeBlee
From: Charlie-Boo on 28 Jun 2010 20:04 On Jun 28, 12:44 pm, MoeBlee <jazzm...(a)hotmail.com> wrote: > On Jun 26, 9:19 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > It would be cool if the following 3 things were equivalent: > > > 1. |- (allX)P(X) > > 2. (allX) |- P(X) > > 3. ~ |- (existsX)~P(X) > > I can help you here, if you're interested in understanding this. > > (1) is well formed. > > (2) is not well formed as you've given it. The reason is that you've > mixed meta-language and object language in an incorrect way. Did you read the definition of the syntax and semantics in the previous post? The wff means what you would think by merely reading each part that is familiar to any mathematician. As I explained, "(allX)" means "For all X the following is true." Then "|-" means "The following is provable." and "P(x)" is a wff that is said to be provable. So it expresses the proposition that for all values of X, the wff P(X) is provable. The fact that conventional logic doesn't express this should not be a barrier to your learning something new. And we can see how useful it is. Now, as far as the original question goes, can you prove that these expressions cannot be all equivalent? C-B > (3) is not well formed as you've given it. The reason is that you've > mixed meta-language and object language in an incorrect way. > > I'll explain: > > Let's say we have fixed some particular logical system pertaining to > '|-' ('|-' is a symbol in the meta-language). > > 'G |- S' stands for 'the set of formulas G proves the formula S' > > and > > '|- S' stands for 'the formula S is provable from the axioms/rules of > the logical system' > > So (1) is well formed. It asserts that AxPx is provable from the > axioms/rules of the logical system. > > But (2) has a quantifier 'x' that is trying to cross over the '|-' > symbol, which is not well formed. > > So, instead, I would write (2) as (2*): > > For all variables 'x', we have |- Px > > And (3) has the problem that you're intending to use the same negation > sign in both meta-language and object language. > > So, instead, I would write (3) as (3*): > > It is not the case that |- Ex~Px > > Now, as restated, what we can correctly say (where the logical system > is first order logic): > > (1) iff (2*) > > > Or if I wanted to know if (existsX) ~ |- P(X) > > Again, not well formed. What is well formed is: > > (4*) There is a variable 'x' such that it is not the case that |- Px > > MoeBlee
From: MoeBlee on 29 Jun 2010 17:25
On Jun 28, 7:04 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > On Jun 28, 12:44 pm, MoeBlee <jazzm...(a)hotmail.com> wrote: > > > On Jun 26, 9:19 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > It would be cool if the following 3 things were equivalent: > > > > 1. |- (allX)P(X) > > > 2. (allX) |- P(X) > > > 3. ~ |- (existsX)~P(X) > > > I can help you here, if you're interested in understanding this. > > > (1) is well formed. > > > (2) is not well formed as you've given it. The reason is that you've > > mixed meta-language and object language in an incorrect way. > > Did you read the definition of the syntax and semantics in the > previous post? Sorry, I made the mistake that your first post was intelligible standalone. > "P(x)" is a wff that is said to be > provable. So it expresses the proposition that for all values of X, > the wff P(X) is provable. Then your formulations as given make even LESS sense. I'm out of time for you. I can't do what no one else in these threads has ever done: get you to understand ANYTHING. MoeBlee |