Quantifier elimination: can anyone spot what is wrong here?: Philosophy Forums

Philosophy Forums » Logic and Philosophy of Math » Logic Homework » Quantifier elimination: can anyone spot what is wrong here? » Quantifier elimination: can anyone spot what is wrong here?

Quantifier elimination: can anyone spot what is wrong here?
Quantifier elimination: can anyone spot what is wrong here?

Quantifier elimination: can anyone spot what is wrong here?

moonlight
Lunatic

Usergroup: Members
Joined: Oct 09, 2005
Location: stuck on earth
Total Topics: 17
Total Posts: 510

Posted 03/17/08 - 09:19 PM: Subject: Quantifier elimination: can anyone spot what is wrong here?	#1
Hi all, Note: I use 'A' and 'E' for the universal and existential quantifiers respectively. Can anyone see what is wrong with this?!? I simply can't :/ phi = Ax.~P(x) ... the original formula ~phi = ~Ax.~P(x) ... formula negated ~phi= Ex.P(x) ... swap quantifiers: negations eliminated ~phi= P(a) ... "a" is a new Skolem constant. phi = ~P(a) ... negate phi again So according to this derivation Ax.~P(x) is equi-satisfiable with ~P(a). Is this correct? It seems slightly odd, because if it is correct then what stops one from doing the same with a formula like this: psi = Ax.Ey.Az. M(x,y,z) ~psi= Ex.Ay.Ez. ~M(x,y,z) ~psi= Ay.Ez. ~M(a,y,z) psi = Ey.Az. M(a,y,z) psi = Az. M(a,b,z) ~psi= Ez. ~M(a,b,z) ~psi= ~M(a,b,c) psi = M(a,b,c) Cordially, moonlight.
All are lunatics, but he who can analyze his delusion is called a philosopher. - Ambrose Bierce -

The Bearded Monkey
Professor

Usergroup: Members
Joined: May 02, 2003
Total Topics: 100
Total Posts: 641

Posted 03/17/08 - 09:59 PM:	#2
Well I believe the rule of inference that: AxP(x)->P(a) for an individual constant is given to you is it not. But it's not equisatisfiable, you need to add such a rule that you can deduce from P(a) a generalisation. Anyway for the example youv'e given it's quite simple: For every a in the model there exists b (depends on the choice of a) in the model s.t for every c in the model M(a,b,c) is satisfied. That's the semantic interpratation. Back to your original question, if Ax~P(x) then obviously we get ~ExP(x) which is identically as saying there isn't a s.t P(a) is satisfied, I think you can see that this is identical to for every a ~P(a) is satisfied. Edited by hyena in petticoat on 03/23/08 - 11:54 PM. Reason: Illiteracy.
i shall take the whichpath to quantum catastrophe theory.

moonlight
Lunatic

Usergroup: Members
Joined: Oct 09, 2005
Location: stuck on earth
Total Topics: 17
Total Posts: 510

Posted 03/17/08 - 10:19 PM:	#3
Hi Bearded Monkey, I read your answer: thanks for that. But in the case of Ax.P(x) or Ax.~P(x) it does seem to be equisatisfiable with P(a) - respectively ~P(a). I think it is because, if it is satisfiable on a domain of one element {a}, then it can be satisfiable on any larger domain: you just need to interpret every other element in the larger domain in the same way you interpret 'a' on the original domain {a}. So it does hold I think that Ax.~P(x) is equisatisfiable with ~P(a). But this doesn't seem to work for the second example. Well I can't find any straight forward way to make it work anyways. Cordially, moonlight.
All are lunatics, but he who can analyze his delusion is called a philosopher. - Ambrose Bierce -

MoeBlee
aka I. Kabruob

Usergroup: Members
Joined: May 19, 2005
Total Topics: 10
Total Posts: 1041

Posted 03/19/08 - 09:42 AM:	#4
moonlight wrote: phi = Ax.~P(x) ... the original formula ~phi = ~Ax.~P(x) ... formula negated ~phi= Ex.P(x) ... swap quantifiers: negations eliminated Okay, but here instead of '=' I strongly suggest using '<->'. moonlight wrote: ~phi= P(a) ... "a" is a new Skolem constant. Putting Skolem aside for a moment, no, we don't have ExPx <-> Pa. Rather we have Pa by existential instantiation, which is a TEMPORARY step in an argument.

moonlight
Lunatic

Usergroup: Members
Joined: Oct 09, 2005
Location: stuck on earth
Total Topics: 17
Total Posts: 510

Posted 03/19/08 - 10:10 AM:	#5
Hi MoeBlee, MoeBlee wrote: Okay, but here instead of '=' I strongly suggest using '<->'. Yes, good point. Thanks for that. MoeBlee wrote: Putting Skolem aside for a moment, no, we don't have ExPx <-> Pa. Rather we have Pa by existential instantiation, which is a TEMPORARY step in an argument. This bit I didn't understand. 'Pa' is the Skolemized version of the sentence 'ExPx', which means that it should be an equi-satisfiable sentence. So why is not legal to write 'ExPx <-> Pa'? Maybe I should mention that this is not a formal proof derivation I'm doing but just a meta-theoretical argument to show that Ax.~Px is satisfiable. So I say that it is equivalent to a sentence ~Pa, and thus to a propositional variable ~X, which means it is satisfiable. Do you still something wrong with such an argument? Cordially, moonlight.
All are lunatics, but he who can analyze his delusion is called a philosopher. - Ambrose Bierce -

MoeBlee
aka I. Kabruob

Usergroup: Members
Joined: May 19, 2005
Total Topics: 10
Total Posts: 1041

Posted 03/21/08 - 08:50 AM:	#6
moonlight wrote: This bit I didn't understand. 'Pa' is the Skolemized version of the sentence 'ExPx', which means that it should be an equi-satisfiable sentence. So why is not legal to write 'ExPx <-> Pa'? Would you point me to the pages in the textbook you're referring to regarding Skolemization? It would help me to see better the technical specifics. moonlight wrote: Maybe I should mention that this is not a formal proof derivation I'm doing but just a meta-theoretical argument to show that Ax.~Px is satisfiable. So I say that it is equivalent to a sentence ~Pa, and thus to a propositional variable ~X, which means it is satisfiable. Do you still something wrong with such an argument? The part about an atomic sentence being equivalent to a propositional letter is clear to me, but not the part before it. I don't know why you would say Ax~Px is equivalent to a sentence ~Pa. The way I would approach is this: To say Ax~Px is satisfiable is to say ~ExPx is satisfiable, which is to say there is a domain of discourse (domains of discourse are non-empty) in which nothing has the property denoted by 'P'. And that is trivial to prove, just by choosing any domain of discourse and assigning 'P' to the empty set. Edited by MoeBlee on 03/21/08 - 08:55 AM

moonlight
Lunatic

Usergroup: Members
Joined: Oct 09, 2005
Location: stuck on earth
Total Topics: 17
Total Posts: 510

Posted 03/21/08 - 03:09 PM:	#7
Hi MoeBlee, MoeBlee wrote: Would you point me to the pages in the textbook you're referring to regarding Skolemization? It would help me to see better the technical specifics. I'm not working with a textbook here. I'm just using the usual definition for Skolemization: for a formula in PNF, replace every existentially bound variable by a Skolem function that has for arguments the universally bound variables preceeding it in the prefix. Obviously since there are no arguments to the Skolem function, it means we get a new Skolem constant. MoeBlee wrote: The part about an atomic sentence being equivalent to a propositional letter is clear to me, but not the part before it. I don't know why you would say Ax~Px is equivalent to a sentence ~Pa. Skolem's theorem states that the resulting formula is equisatisfiable with the original one. So we get in effect a grounded formula for a domain of 1 element. Obviously, since this is a formula without equality, therefore if the formula is satisfiable on this domain, it is satisfiable on every larger domain. MoeBlee wrote: The way I would approach is this: To say Ax~Px is satisfiable is to say ~ExPx is satisfiable, which is to say there is a domain of discourse (domains of discourse are non-empty) in which nothing has the property denoted by 'P'. And that is trivial to prove, just by choosing any domain of discourse and assigning 'P' to the empty set. I agree: this is perfectly fine to do as well. But I need to consider quite a few formulas with more complicated prefixes, all of the form EA. The aim of my work is to generated a program, i.e. an automated procedure, to deal with such formulas. The formula I posted is just a simple example to get me going. Because it needs to be automated, I thought of using the Skolemized version of the formula, and to do this, I need the formula to be in PNF, which means all the quantifiers at the front, and no negations preceeding any quantifier. So I can't use the formula in the following form: ~Ex.Px since it is not in PNF. So when I write "~ExPx <=> Pa" it is in a document explaining the "legality" of the procedure I will code. It isn't in the context of a formal proof derivation. Cordially, moonlight. Edited by moonlight on 03/21/08 - 03:16 PM
All are lunatics, but he who can analyze his delusion is called a philosopher. - Ambrose Bierce -

MoeBlee
aka I. Kabruob

Usergroup: Members
Joined: May 19, 2005
Total Topics: 10
Total Posts: 1041

Posted 03/24/08 - 04:41 PM:	#8
Now I'm not clear what specific question we're trying to answer. Your first post was to ask why a certain derivation (which gave Ax~Px <-> ~Pa) is incorrect. That question was answered. Now, we've moved on to something different, which is Skolemization, which has to do with EXTENDING theories. A certain formula can be a theorem of a theory EXTENDED by Skolemization while it is NOT the case that, e.g., 'Ax~Px <-> ~Pa' is a theorem of the predicate calculus. Also, you mentioned wanting to put formulas in prenex normal form. There is an effective procedure for doing that.

moonlight
Lunatic

Usergroup: Members
Joined: Oct 09, 2005
Location: stuck on earth
Total Topics: 17
Total Posts: 510

Posted 03/27/08 - 07:42 AM:	#9
Hi MoeBlee, Sorry for the delay in my answer. MoeBlee wrote: Now I'm not clear what specific question we're trying to answer. Your first post was to ask why a certain derivation (which gave Ax~Px <-> ~Pa) is incorrect. That question was answered. Now, we've moved on to something different, which is Skolemization, which has to do with EXTENDING theories. Yes, I'm clear on that now. My original question was pretty answered much by TheBeardedMonkey and your following message. I basically got mixed up with Skolemization: it is satisfiability preserving, but doesn't preserve validity from I now collect, so one cannot derive theorems with it. "MoeBlee" wrote: A certain formula can be a theorem of a theory EXTENDED by Skolemization while it is NOT the case that, e.g., 'Ax~Px <-> ~Pa' is a theorem of the predicate calculus. Also, you mentioned wanting to put formulas in prenex normal form. There is an effective procedure for doing that. Yes, I understand what you mean. What I meant is that (Ax.~Px) is satisfiable, iff (~Pa) is satisfiable. In this case, the reason has nothing to do with Skolemization. It is simply that (Ax.~Px) only has universal quantifiers in its prefix, so it is enough to test it on domains of 1 element, to check whether or not it is satisfiable on all domains. This doesn't constitute of course a validity check, i.e. something equivalent to a proof derivation. My apologies for confusing you with talks of Skolemization and a specific example of the A* prefix class like this. And thanks very much for all your input. Cordially, moonlight.
All are lunatics, but he who can analyze his delusion is called a philosopher. - Ambrose Bierce -

You don't have permission to post.

Please login or register.