nounou said:
Hurkyl,
to extend
Ex(Dx) & AxAy((Dx & Dy) -> x = y) : Ex(Dx & Ay(Dy -> x = y).
Just to be clear those are two equivalent formulas above- I could have put an equivalence sign but I had a thing going with the colons.
to make it represent two edges
There exists at least one edges and there exists at most two edges: There exists exactly two edges: There exists two unique edges:
Ex(Dx) & AxAyAz((Dx & Dy & Dz) -> x = y & y=z) : (??I have no clue??).
Am I on the right track?
nounou
I'll run through it just to give you an idea of how the process might go, but I'm not sure my answer will be correct- we'll need someone else like Hurkyl to check. Check it yourself too. Okay, there are two parts to unique existence:
1) Existence
2) Uniqueness
You need both, and you know how to state both:
1) Existence- Ex(Dx)
2) Uniqueness- AxAy((Dx & Dy) -> x = y).
Now in the above formulas, "x" and "y" are variables, right? They range over your constants. So Ex(Dx) says that at least one of your constants has the property D (of being an edge). So you're correct that Ex(Dx) alone could mean two constants have the property D, or one or three or all, etc. So just start the formula off- you can always change it later if you need to:
Ex(Dx)
Now you need to specify exactly how many constants have the property D. You'll add this on as a conjunct:
Ex(Dx) &
Notice that this ends the scope of the first quantifier. IOW, if you then put:
Ex(Dx) & x
The last "x" is free. Okay, so how do you say that there are exactly two constants with the property D? If you say there is at least one and at most two, that means there is
either one or two. So you need to say there are at least two. IOW, there is a constant with the property D and there is another constant with the property D and those two constants aren't the same:
Ex(Dx) & ExEy(Dx & Dy & ~(x = y))
Now you need to say there are at most two constants with the property D. IOW, if there is a third constant with the property D, then it's the same as one of the first two (just add another conjunct):
Ex(Dx) & ExEy(Dx & Dy & ~(x = y)) & ExEyAz[(Dx & Dy & ~(x = y) & Dz) -> ((z = x) v (z = y))]
I don't know if I should have used the exclusive "or", but since it's not familiar and we already have that ~(x = y), I don't think it's needed. Now we can get rid the extra conjuncts:
ExEyAz[(Dx & Dy & Dz & ~(x = y)) -> ((z = x) v (z = y))]
Something doesn't seem right. I want to say that
ExEy(Dx & Dy & ~(x = y))
I don't want to say if ... then ... so I don't think I want it in the implication. Instead:
ExEyAz[(Dx & Dy & ~(x = y)) & (Dz -> ((z = x) v (z = y)))]
Now I'm saying if there is another constant- any constant- then it will be equal to one of the first two. Final answer ;) Correct?
Notice the formula for exactly one can be written as:
ExAy(Dx & (Dy -> x = y))
Which has the same general form as my best guess (seeing a pattern?), making me more confident. But...