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

moonlight
Lunatic

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

Posted 04/01/08 - 04:51 AM: Subject: The semantics of equality in FOL	#1
Hi all, A question came to mind when reading the thread on intuitionism. In there the participants discuss the equality relation in FOL. As I understand it the semantics of this relation can be represented by adding some axioms to FOL without equality, namely the following: Ax.(x=x) Ax,y.((x=y) => (P(..,x,..) => P(..,y,..))) Now these axioms for '=' are the same as presented in the wikipedia article. The second axiom is a replacement schema, and a similar one may be added for functions. The second axiom means roughly if 'x' holds as a the n^th argument of a predicate P, then y should hold as the n^th argument of that same predicate. The problem I'm looking at is the following. Consider the following formula: Ax,y. ((x=y) v (Px ^ ~Py)) The above formula is clearly only satisfiable on domains of 1 element. But when applying the equality axioms we get: Ax,y. ((Px ^ Py) v (Px ^ ~Py) ...which is a formula satisfiable on domains of any size. Does this mean the equality axioms are not enough to represent the true semantics of equality. How could the FOL formulas with equality be then translated into a FOL formulas without equality? Cordially, moonlight.
All are lunatics, but he who can analyze his delusion is called a philosopher. - Ambrose Bierce -

7
Graduate

Usergroup: Members
Joined: Mar 23, 2008
Total Topics: 3
Total Posts: 182

Posted 04/01/08 - 07:47 AM:	#2
The axiom seems to be of the form P -> (Q -> R). If you have x = y, then: if you have P(...x...), then you have P(...y...). To make a substitution by getting to R, you first need to have Q. P does not imply it. You're making the substitution without having Q. In other words, if you have that x = y, you need to have some statement of the form P(...x...) before you can substitute P(...y...). You can't just make the statement up at your discretion. E.g., say you have x = y. You can't then say that you have Rxy, so you have Ryx. That move is only justified if you do have Rxy.

moonlight
Lunatic

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

Posted 04/01/08 - 08:47 AM:	#3
hi 7, 7 wrote: The axiom seems to be of the form P -> (Q -> R). If you have x = y, then: if you have P(...x...), then you have P(...y...). Yup, that's right. 7 wrote: To make a substitution by getting to R, you first need to have Q. P does not imply it. Agreed again. 7 wrote: You're making the substitution without having Q. In other words, if you have that x = y, you need to have some statement of the form P(...x...) before you can substitute P(...y...). This is where I disagree. We have (x=y) in the formula. And we have Px too in the formula, therefore we have Py. Cordially, moonlight.
All are lunatics, but he who can analyze his delusion is called a philosopher. - Ambrose Bierce -

7
Graduate

Usergroup: Members
Joined: Mar 23, 2008
Total Topics: 3
Total Posts: 182

Posted 04/01/08 - 11:00 AM:	#4
I am a bit confused. How does the first formula ensure that x is P?

moonlight
Lunatic

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

Posted 04/01/08 - 11:20 AM:	#5
7 wrote: I am a bit confused. How does the first formula ensure that x is P? It doesn't. It ensures that (x=y), with x, y bound by universal quantifiers is valid only on a domain of 1 element. The (P(x) ^ ~P(y)) part of the formula is satisfiable on no domain, because both variables are bound by the universal quantifier. So in fact the formula is satisfiable on every domain (I was wrong when I said it is SAT only on domains of 1 element), but it is only valid on a domain of 1 element. What I'm after, is a way to translate this formula into an equivalent formula of FOL but without equality, i.e. no atom of the form (x=y) would occur in it. 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: 8
Total Posts: 1095

Posted 04/01/08 - 02:10 PM:	#6
moonlight wrote: As I understand it the semantics of this relation can be represented by adding some axioms to FOL without equality, namely the following: Ax.(x=x) Ax,y.((x=y) => (P(..,x,..) => P(..,y,..))) No, those are axioms, not semantics. But those do axiomatize identity theory. I would put it this way (1) Ax x=x (2) If P is an atomic formula and P' is just like P except y occurs in P' in zero or more places where x occurs in P, then all closures of the following are axioms: Axy(x=y -> (P -> P')) Then by induction on formulas we get that this holds for all formulas (where substitutions are on free occcurrences of x and where y is free for x). moonlight wrote: Ax,y. ((x=y) v (Px ^ ~Py)) The above formula is clearly only satisfiable on domains of 1 element. But when applying the equality axioms we get: Ax,y. ((Px ^ Py) v (Px ^ ~Py) ...which is a formula satisfiable on domains of any size. But that is NOT a legitimate application of an identity axiom (even expanded for formulas in general). Your formula is Axy(x=y v (Px & ~Py)). (1) That doesn't even have any FREE variables to replace. And if you mean just the matrix of that formula, then x=y v (Px & ~Py) is different from x=y -> (Px -> [conclusion here]) (2) And anyway you are lacking the antecdents in the theorem, which are x=y and Px. moonlight wrote: Does this mean the equality axioms are not enough to represent the true semantics of equality. It is true that there is NO first order axiomatization to capture identity, but not for the reason you've asked about. Ordinarily, we capture identity by brute force: We simply stipulate that the '=' symbol maps to the identity relation on the universe of the model. We have to stipulate that; there are no first order axioms that enforce that '=' may map only to the identity relation on the universe of the model. Meanwhile, though, for the purpose of making deductions, we do use the identity axioms. Edited by MoeBlee on 04/01/08 - 03:34 PM

MoeBlee
aka I. Kabruob

Usergroup: Members
Joined: May 19, 2005
Total Topics: 8
Total Posts: 1095

Posted 04/01/08 - 02:26 PM:	#7
moonlight wrote: We have (x=y) in the formula. And we have Px too in the formula, therefore we have Py. What? Just because x=y and Px are subformulas doesn't mean that the formula itself is an instance of a form (x=y -> (Px -> Py)). You have (x-y v (Px & ~Py). What does that have to do with having the two things you need: x=y itself and Px itself. Edited by MoeBlee on 04/01/08 - 03:35 PM

MoeBlee
aka I. Kabruob

Usergroup: Members
Joined: May 19, 2005
Total Topics: 8
Total Posts: 1095

Posted 04/01/08 - 02:32 PM:	#8
moonlight wrote: It ensures that (x=y), with x, y bound by universal quantifiers is valid only on a domain of 1 element. It seems you're getting mixed up between models and axioms. Clear your mind for a moment of your thoughts about this. Now, look at the axioms just for what they are: axioms from which you can deduce other formulas. In order to deduce a certain formula Py from the schema of substituion, you have to have ALREADY established x=y and Px. Then, if your handling of variables is correct (not substituting so that variables get bound that weren't already bound), you will see that, yes, it also makes semantic sense that if x is y and the predicate P holds for x, then the predicate P holds for y.

moonlight
Lunatic

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

Posted 04/01/08 - 02:39 PM:	#9
Hi MoeBlee, Thanks, for that. You're right, I was way too loose on the replacement and lost track of the fact that they were axioms. Got me confused this issue. Thanks also for confirming that when equality occurs you can translate it into a sentence without equality. I was wondering how that sentence could be translated into one without equality. Do you know of a method to determine such a formula's satisfiability? I mean one with only universal quantifiers in its prefix, and in which the equality symbol occurs? Cordialmente, Luz de Luna.
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: 8
Total Posts: 1095

Posted 04/01/08 - 03:29 PM:	#10
moonlight wrote: Thanks also for confirming that when equality occurs you can translate it into a sentence without equality. But I didn't say that. What I mentioned is not a matter of translating a sentence S into another sentence, but rather of interpreting the language (and thereby the sentence S) via models. Interpretation, in the sense of models, is not translation from sentence into another sentence. moonlight wrote: Do you know of a method to determine such a formula's satisfiability? I mean one with only universal quantifiers in its prefix, and in which the equality symbol occurs? As I think you know, the dyadic predicate calculus (and with identity) is undecidable - there is no algorithm to decide of an arbitrary dyadic formula whether it is a validity. So there is no algorithm to determine whether an arbitrary dyadic formula is satisfiable, since if there were, then any formula determined to be unsatisfiable would have a validity as its negation thus we would have, contrary to the undecidability of dyadic logic, an algorithm for deciding validity. More succinctly: Identity theory is not a decidable theory. Edited by MoeBlee on 04/01/08 - 03:34 PM

Page: 1 2 3

You don't have permission to post.

Please login or register.