The semantics of equality in FOL: Philosophy Forums

Philosophy Forums » Logic and Philosophy of Math » The semantics of equality in FOL » The semantics of equality in FOL

The semantics of equality in FOL
Are the remplacements axioms for equality enough in FOL?

Page: 1 2

The semantics of equality in FOL

moonlight
Lunatic

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

Posted 04/02/08 - 03:27 PM:	#26
Hi MoeBlee, MoeBlee wrote: So if I understand you correctly, you have a method that takes a formula and converts to another formula, and if the first formula is satisfiable then the new formula is satisfiable. Is that right? Yes, that's right. This is what I'm referring to. MoeBlee wrote: But that doesn't address what I thought we were talking about at this juncture, which was proving one formula from another. Just because I start with a formula that is satisifiable and end with another formula that is satisfiable doesn't give me that the first formula PROVES the new formula. No, that's not what I'm after. I don't need to prove that the formula is valid. Proving that it is satisfiable will do. If I get a procedure that does that, and that is always satisfiability preserving, then all I need to do in order to prove that it is valid, is to prove that F is satisfiable, while ~F is not. That proves that F is valid. MoeBlee wrote: Earlier, your point was that a certain formula is satisfiable in all models of a certain kind so any formula derivable from it should be satifiable in all models of that kind. Yes, that's true. But for it to be relevent to your example, the second formula has to be derivable from the first formula. And "preservation of satisfiability" doesn't give us that the new formula is DERIVABLE from the first formula. Again, I'm not interested in proving that a formula is valid. But obviously if it is valid, then it is also satisfiable. In any case, the satisfiability, validity and invalidity problems are all equivalent formulations of the decision problem. A method for any one will do really. MoeBlee wrote: I try my best. Sometimes it's difficult, though. And when I ask other people to be exact, perhaps some people (not you) think I'm just trying to give the person a hard time or that I'm just being pedantic for the sake of being pedantic. But that's not true. Actually, the reason I ask other people to be exact is that it makes things much EASIER for me, and I think it adds to the person's own clarity on the matter. I can work with an exact statement much more quickly and clearly than with something that is vague or imprecise enough to leave wiggle room as to just what the mathematics of the situation is. Then even if my answer ends up being "I don't know", at least I know the meaning of what it is that I am saying 'I don't know' to. I understand you perfectly. No worries. As I said, I agree, and wish that I could formulate things as precisely and simply as you do. Although I'm finding it hard as this isn't my background (never took a logic class in my life) and I've pretty much discovered logic 3 years ago and have been teaching myself since. Since I've got some pretty serious time constraints (got to finish my research), I sometimes allow myself to skip the learning of the exact wording and just learn the 'mechanisms'. My biggest regret is to not have discovered logic earlier. University curriculums these days are plain shit: they should have included some of this stuff in ours when we were undergrads. 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: 9
Total Posts: 1041

Posted 04/02/08 - 05:53 PM:	#27
moonlight wrote: No, that's not what I'm after. I don't need to prove that the formula is valid. What formula? Of course, neither (1) Axy(x=y v (Px & ~Py)) nor (2) Axy((Px & Py) v (Px & ~Py)) are valid. So what is at stake, I would think is whether (3) Axy(x=y v (Px & ~Py)) -> Axy((Px & Py) v (Px & ~Py)) is valid (given the definition of 'valid' that includes the fixed semantics for '=). And (3) is not valid, as you saw from the model I mentioned. moonlight wrote: Proving that it is satisfiable will do. Proving that (3) is satisfiable? That's no problem. (3) is satisfiable: universe = {1} P = {1}. But what does it have to do with any thoughts about identity theory? moonlight wrote: If I get a procedure that does that, and that is always satisfiability preserving, then all I need to do in order to prove that it is valid, is to prove that F is satisfiable, while ~F is not. That proves that F is valid. Yes, that's true. But what is your F here? Is it (3)? If so, you'll not be able to show that the negation of (3) is not satisfiable; I already proved in a previous post that the negation of (3) is satisfiable. Hmm, perhaps it would help if you re-stated, from the very beginning, what it is you want to prove and what proving that would have to do with any thoughts about identity theory.

moonlight
Lunatic

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

Posted 04/02/08 - 06:05 PM:	#28
Hi MoeBlee, Thanks for the answer. To answer back, no it's not 3) that I'm trying to prove as being satisfiable. What I am after, is a procedure to decide if the following is satisfiable: - Any arbitrary formula F, that is in prenex normal form, and that contains only universal quantifiers in its prefix, and that allows equality to occur in its quantifier free matrix. While searching for such a procedure, I thought that I could eliminate the equality atoms from the matrix, by transforming the matrix in DNF, and then using that formula 3). I was wondering whether the result of doing this will preserve satisfiability. If it does, then the problem is solved, since I know of a procedure to decide whether forumlas like the ones I described in italics, but without equality, are satisfiable or not. Do you see what I mean now? 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: 9
Total Posts: 1041

Posted 04/03/08 - 04:35 PM:	#29
I have a better picture now. But a couple of points of clarification are still needed. I'm out of time to mention them today, but I'll try for tomorrow.

Page: 1 2

You don't have permission to post.

Please login or register.