First-order logic formula

Question

If I want to express in first-order logic that 'the element(s) in the set with the smallest radius has the value 0', would the following be right?

∀ e₁ ∈ S.   ∀ e₂ ∈ S.   Radius e₁ ≤ Radius e₂   ⇒   Value e₁ = 0?

Are the variables correctly quantified?

Thanks

Answer 1

Just to clarify with parentheses, what you wrote is usually taken to mean:

\forall e1 \in S. (\forall e2 \in S. (Radius e1 <= Radius e2 --> Value e1 = 0))

This statement asserts that the value of every element is 0. Here's how: Pick an arbitrary e1, now pick e2 = e1, and we have: Radius e1 <= Radius e1 --> Value e1 = 0. Since the antecedent (thing before the -->) is true, we have Value e1 = 0. And since we made no assumptions about e1, we have forall e \in S. Value e = 0.

The problem is that your parentheses are off.

\forall e1 \in S. (\forall e2 \in S. Radius e1 <= Radius e2) --> Value e1 = 0

In order for the antecedent to be true now, e1's radius has to be less than or equal to every (as opposed to any) other radius, which seems like what you intended.

Answer 2

I think you want an exists

\exists e_1 . (\forall e_2 radius(e_1) <= radius(e_2)) and (radius(e_1) = 0)

I'm not sure about the precedence in the formula, but now that I think I understand the question, maybe you want (where M is the minimality condition radius(e_1) < radius(e_2))

\forall e_1 . ((\forall e_2 . M) -> value e_1 = 0)

I think your previous formula may be wrong for the following reason. Suppose you have elements with radii { 0, 1, 2 }, and values equal to radii. Then, you will have a case where 1 <= 2, but the value is not zero. If I'm interpreting your original formula correctly,

\forall e_1 . \forall e_2 . P(e_1, e_2)

Then this counterexample provides a case where P is false, therefore the entire formula fails (but the example should be true).

Answer 3

What you wrote is also true if there are no elements with the smallest radius. If this is desired, you are correct; if not, you need to add a clause to that effect:

(\forall e1 \in S. \forall e2 \in S. Radius e1 <= Radius e2 --> Value e1 = 0) \and (\exists e1 \in S. \forall e2 \in S. Radius e1 <= Radius e2)