That is, we assert the existence of a triple with three properties: (i) no two of its members are the same, (ii) each member is a bird, and (iii) each member is in the tree. The sentence Heinz produces at least 57 varieties could be handled (in principle if not in practice) by extending the same ideas to assert the existence of a series of 57 things no two of which are the same and each of which is both a variety and produced by Heinz. If you are mathematically minded, you might try calculating the number of denied equations you would need in that case.
In the other direction, if the scopes of quantifier phrases are confined to parts of the sentence in which they bind variables, we would have instead
(∃x: Bx) (Nxt
∧ (∃y: By ∧ ¬ y = x) (Nyt
∧ (∃z: Bz ∧ (¬ z = x ∧ ¬ z = y)) Nzt))
which might be expressed in English as Some bird is such that (i) it is in the tree and (ii) some bird other than it is such that (a) it, too, is in the tree and (b) some bird different from both of the them is in the tree also.
As a general pattern for At least n things are such that … they …, we might use either
∃x1 (∃x2: ¬ x2=x1)
⋱
(∃xn: ¬ xn=x1 ∧ ¬ xn=x2 ∧ … ∧ ¬ xn=xn-1)
(θx1 ∧ θx2 ∧ … ∧ θxn)
or
∃x1 ∃x2 … ∃xn ((¬ x2=x1) ∧
⋱
∧ (¬ xn=x1 ∧ ¬ xn=x2 ∧ … ∧ ¬ xn=xn-1)
∧ (θx1 ∧ θx2 ∧ … ∧ θxn))
where θτ abbreviates … τ …. These logical forms differ in whether the denied equations appear as restrictions on quantifiers or as conjuncts of the formula to which the quantifiers are applied. In either case, the list of denied equations should include ¬ xi = xj for each i > j where i, j ≤ n—i.e., one denied equation for each pair of different variables (where requiring that the variable with the higher index appears on the left is just a systematic way of choosing one of the two ways of writing the equation). At least n Cs are such that … they … can be captured by adding the formulas xi is a C, for each i ≤ n, either as restrictions on the relevant quantifiers or as further conjuncts of the quantified formula.
If we rewrite the logical forms displayed above so that quantifiers are confined to apply only to the formulas which contain variables bound to them, we would get The corresponding pattern with the quantifiers confined would be:
∃x1 (θx1 ∧
(∃x2: ¬ x2=x1) (θx2 ∧
⋱
(∃xn: ¬ xn=x1 ∧ ¬ xn=x2 ∧ … ∧ ¬ xn=xn-1) θxn …))
This says roughly, Something is such that …it… and so is something else … and so is something else. In spite of appearances, this English sentence is not a conjunction because each use of else refers implicitly to all of the previous uses of something and cannot be separated from them in an independent component.
We are also now in a position to analyze the other two sorts of numerical quantifier phrases mentioned earlier, for claims made using them can be restated as truth-functional compounds of claims made using at least n.
At most n Cs are such that … they …
may be paraphrased as
¬ at least n+1 Cs are such that … they …
and
Exactly n Cs are such that … they …
may be paraphrased as
At least n Cs are such that … they …
∧ at most n Cs are such that … they …
For example, to claim that there was at most one winner is to deny that there were at least two, and to claim that there was exactly one is to say both there was at least one and that there was at most one—i.e., it is to say that there was at least one and deny that there were at least two.