# Deduce a new quantifier that negates “there are at least two objects with property P.”

Source: p 195. Sweet Reason: A Field Guide to Modern Logic (2010 2 ed) by Henle, Garfield, Tymoczko.
I replaced the author's, 2 rotated by 180º with ❷, and 2 horizontally flipped by 180º ✌; because I know not how to produce them with Unicode.

We have a new quantifier for you. It’s ❷. ❷xPx means “there are at least two objects with property P.” [The rest of the question is immaterial to the following.]

29!! [The author uses two exclamation marks (out of 3) to classify difficulty of an exercise.]
The ∀ quantifier has a partner, ∃. They’re partners in the sense that ∀¬ means the same as ¬∃ and ¬∀ means the same as ∃¬. Define a quantifier (call it ✌) such that:
29.1. ❷¬ and ¬✌ have the same meaning
29.2. ✌¬ and ¬❷ have the same meaning.

[Book's answer on p 364:] ✌xPx means that all or all but one have the property P.

29.1. By definition, ❷¬ means: ∃ 2 objects not.

29.2 By definition, ¬❷ means: ¬(∃ ≥ 2 objects) ⇔ ∄ ≥ 2 objects ⇔ ∃ 0 or 1 object.

But I do not know how to continue to deduce the meaning of ✌.

• I'm a little confused. Given, ❷, you can just define ✌x(...) = ¬❷x¬(...). Is that what the answer is supposed to look like, or is there something else (or does ❷ have to be defined too)? – Eliran Aug 11 '16 at 6:45
• The proper relation here is not negation, it is generally called 'duality'. It shares with negation the property that if you do it twice you get back what you had, but it is not negation in the sense that the two propositions involved do not give you a contradiction when you conjoin them. You want a quantifier dual to the one that requires two objects to exist. – user9166 Aug 11 '16 at 19:17
• @EliranH I clarified my post above: the citation from p 264 is the answer from the book, but it does not define ❷ explicitly. – NNOX Apps Aug 14 '16 at 17:14

The negation of "there are at least two..." is "there is at most one..." i.e. either "there is no..." or "there is one and only one...". Therefore

¬❷xPx ≡ (¬∃xPx) ∨ (∃!xPx)

where ∃! is the unique existential quantifier defined by

∃!xPx ≡ ∃*x(Px* ∧ ∀y(Pyy=x))

By definition

x¬Px ≡ ¬❷xPx

Hence (replacing Px by ¬Px)

xPx ≡ ¬❷x¬Px ≡ (¬∃x¬Px) ∨ (∃!x¬Px) ≡ (∀xPx) ) ∨ (∃!x¬Px)

so ✌xPx means "either all objects have property P, or else exactly one object does not have property P" – in other words, "at most one object does not have property P".

❷¬Px means: 'there are at least two x for which Px does not hold'. This has to be equivalent to ¬✌Px. Hence, ✌Px has to be the negation of 'there are at least two x for which Px does not hold'. This is then, 'there is at most one x (i.e. zero or one) for which Px does not hold' or 'for all x except at most one, Px holds' (in the second formulation, you see the analogy with the exists-forall pair).

If we take this definition, then ✌¬Px means: 'for all x except at most one, Px does not hold'. This is equivalent to 'there is at most one x for which Px holds'. The negation of this is 'there are at least two x for which Px holds', which is formalised as ❷Px, as required.

To deduce the meaning of ✌, it can be helpful to list the situations where ✌Px should hold. This is done implicitly in the first paragraph: from 29.1 we derive that ✌Px holds when there are zero or one x with Px.

❷xPx can be expressed without creating a new quantifier, because ❷xPx means:

1. Ǝx[Px & Ǝy[Py & ~(x = y)]]

1 simply asserts that there exists x with the property P, and there exists another object with the same property which is not equivalent to it. That leaves open the possibility for there being more than two objects with the same property. From that, we can derive the partner expression by negating 1 as follows:

```2.  ~Ǝx[Px & Ǝy[Py & ~(x = y)]]
3.  ∀x[~(Px & Ǝy[Py & ~(x = y)]]
4.  ∀x[~Px ∨ ~Ǝy[Py & ~(x = y)]]
5.  ∀x[Px → ~Ǝy[Py & ~(x = y)]]
6.  ∀x[Px → ∀y[~(Py & ~(x = y))]]
7.  ∀x[Px → ∀y[~Py ∨ (x = y))]]
8.  ∀x[Px → ∀y[Py → (x = y))]]
```

That asserts that for every x with the property P, any instance of y with the same property must be identical with x. In other words, the partner expression says that there is at most one x with that property.