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 3

The semantics of equality in FOL

MoeBlee
aka I. Kabruob

Usergroup: Members
Joined: May 19, 2005
Total Topics: 5
Total Posts: 1114

Posted 04/02/08 - 10:48 AM:	#21
moonlight wrote: But I think one could argue that the method is still satisfiability preserving. Since both the original and the derived formulas are satisfiable in the model I'm unclear what you mean. What do you mean by 'satisfiability preserving'? And the method you refer to is that thing about using second order quantification? Also, a point to keep our communication clear: We don't say a formula is satisfiable in the model. Rather we say that a formula is satisfied by the model (and assignment to the variables if the formula is not a sentence) or is not satisfied by the model (and assignment to the variables if the formula is not a sentence). Then we may also say that a formula is satisfiable iff there is a model in which the formula (and assignment for the variables if the formula is not a sentence) is satisfied.

moonlight
Lunatic

Usergroup: Members
Joined: Oct 09, 2005
Location: stuck on earth
Total Topics: 19
Total Posts: 601

Posted 04/02/08 - 12:27 PM:	#22
Hi MoeBlee, MoeBlee wrote: I'm unclear what you mean. What do you mean by 'satisfiability preserving'? By satisfiability preserving I mean if the original formula is satisfiable, then the resulting is also satisfiable. MoeBlee wrote: And the method you refer to is that thing about using second order quantification? Yes, the method I'm thinking of here basically consists of putting a formula in PNF, which preserves satisfiability, and then putting the matrix of the resulting formula in DNF, which again preserves satisfiability, and then you have a matrix which looks something like: A1 v A2 v A3 v ... with each Ai being a conjunction of atoms. Finally an atom of the form (x=y) in a given Ai is removed, and an "axiom" formula of the type I presented with 2nd order quantifiers is joined to the said Ai. The "axiom's" 2nd order quantifiers are then expanded. This is supposed to be done for every equality atom, and every Ai. I'm guessing this should preserve satisfiability: although the equalities won't be enforced anymore, and whereas x and y should have been assigned to the same constant value in the original formula (if we had x=y), in the new formula, x and y will be possibly assigned to 2 constant values, but equivalent ones, i.e. belonging to exactly the same set theoretical extensions of the predicates and relations in the models. I add that I'm only considering predicates and binary relations in the formulas now for simplicity's sake, and I'm guessing this preserves satisfiability, but I haven't proved it yet. What do you think? "MoeBlee" wrote: Also, a point to keep our communication clear: We don't say a formula is satisfiable in the model. Rather we say that a formula is satisfied by the model (and assignment to the variables if the formula is not a sentence) or is not satisfied by the model (and assignment to the variables if the formula is not a sentence). Then we may also say that a formula is satisfiable iff there is a model in which the formula (and assignment for the variables if the formula is not a sentence) is satisfied. Yes thanks for that. I admire a lot the way you are comfortable with formally stating things with the right language. I always have slips of language in my explanations which can make it hard to convey what I mean. I'll make a mental note of that: formula satisfied by the model, not in the model. Thanks again. One last point. Regarding the formulas in PNF with only universal quantifiers in the prefix and the equality symbol occurring in them. I've just read a method to decide their satisfiability on domains where the number of elements is inferior to the number of variables in the formula. There's a follow up for considering cases where the domain has more elements than the number of variables, but God it's complicated: a hell of a lot of combinatorics. The paper is from 1930, & written by F. P. Ramsey. I don't know of any simpler method that came after. It doesn't seem like there is any. I think it's an open research problem. 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: 5
Total Posts: 1114

Posted 04/02/08 - 02:17 PM:	#23
moonlight wrote: By satisfiability preserving I mean if the original formula is satisfiable, then the resulting is also satisfiable. 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? 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. 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. moonlight wrote: I admire a lot the way you are comfortable with formally stating things with the right language. 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.

MoeBlee
aka I. Kabruob

Usergroup: Members
Joined: May 19, 2005
Total Topics: 5
Total Posts: 1114

Posted 04/02/08 - 02:26 PM:	#24
moonlight wrote: formula satisfied by the model, not in the model. But that wasn't my point. It's not a matter of which preposition to use - 'in' or 'by' - but rather the distinction between, on the one hand, a formula being satisfied by the model, and on the hand, a formula being satisfiable. In the first case, we have that the formula is satisfied by the model M. In the second case, we have that there esists a model that satisfies the formula. Those are two different claims. The first implies the second but the second does not imply the first, since even though there exists a model that satisfied the formula, it is not entailed that the SPECIFIC model M satisfies the formula. So, again, we say "The formula P is satisfied by the model M" or we say "The formula P is satisfiable." Two different claims. The first is about a relation between the formula P and the model M. The second is just about the formula P itself.

moonlight
Lunatic

Usergroup: Members
Joined: Oct 09, 2005
Location: stuck on earth
Total Topics: 19
Total Posts: 601

Posted 04/02/08 - 03:11 PM:	#25
Hi MoeBlee, Yes, I can tell the difference between the 3 statements: - a formula F being satisfiable w.r.t to a model M, i.e. M \|= F, and - a formula F being satisfiable (i.e. by some unspecified model, which exists). - a formula F being satisfiable in all models, i.e. \|= F. Which entails by Godel's completness theorem that \|- F, i.e. F is valid. When I'm saying "satisfiability is preserved", I mean the formula is satisfiable. I'm not referring to a particular model, I'm just saying that there is one. Cordially, moonlight. Edited by moonlight on 04/02/08 - 03:30 PM
All are lunatics, but he who can analyze his delusion is called a philosopher. - Ambrose Bierce -

moonlight
Lunatic

Usergroup: Members
Joined: Oct 09, 2005
Location: stuck on earth
Total Topics: 19
Total Posts: 601

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: 5
Total Posts: 1114

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: 19
Total Posts: 601

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: 5
Total Posts: 1114

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 3

You don't have permission to post.

Please login or register.