Elegant predicate logic sentence representation of "at least $n$"

Question

I would like to represent in predicate logic notation (I'm not sure this is the correct name) the sentence "There are at least 3 elements in X such that A(x) is true and B(x) is false".

Without that "at least 3", I would translate the sentence as $\exists x \in X. A(x) \land \lnot B(x)$ but I have no idea how to say the same for 3 distinct elements of X.

One solution I've found is this but I feel like this would be too long, repetitive and definitely not elegant.

An elegant solution (that could also easily be modified to represent "at least n" instead of just "at least 3") may be something like:

"Let Y be the set of all elements of X such that A(element) is true and B(element) is false;

there are at least 3 (or n) distinct elements in Y".

How would this translate into "predicate logic notation"?

Is this actually more elegant?

Am I on the right track?

Answer 1

"At least three x such that P" will be:

$\exists x \exists y \exists z \ [x\ne y \land x \ne z \land y \ne z \land P(x)].$

Answer 2

You can collapse the long conjunctions into a generalized conjunction:

$$\exists x_1\ldots \exists x_n \bigwedge_{i=1}^{n} (\bigwedge_{j=1}^{i-1} x_i \neq x_j \land A(x_i) \land \neg B(x_i))$$

This is just

$$\exists x_1 \ldots \exists x_n ( \underbrace{(A(x_1) \land \neg B(x_1))}_{i=1} \underbrace{\land}_{\bigwedge_i} \ldots \underbrace{\land}_{\bigwedge_i} \underbrace{(\underbrace{x_{n} \neq x_1}_{j=1} \underbrace{\land}_{\bigwedge_j} \ldots \underbrace{\land}_{\bigwedge_j} \underbrace{x_{n} \neq x_{n-1}}_{j=n-1} \land A(x_n) \land \neg B(x_n))}_{i=n} )$$

in disugise. $\bigwedge$ is to $\land$ like what $\Sigma$ is to $+$. Note that $\bigwedge$ is not an operator of the formal language of FOL, just syntactic sugar on the meta level working as a simple abbreviation for what is actually an ordinary chain of conjunctions. Under the hood, both are the same formula with the same complexity, which can not be avoided in plain FOL, but at least you can get it into a visually and notationally more convenient format.

Answer 3

Note that addressing this heavily depends on what kind of base logic or formal system you want to work over. If you want to say "at least 3 satisfy $Q$" in pure FOL, then you have no choice but to use the long-winded formula that you are already aware of, and if you replace "3" by a larger natural number then you need a longer formula. Some other people have already suggested that you can look at other quantifiers beyond those in standard FOL. That is one option, of course, but some of those generalized quantifiers come at heavy price.

It is actually possible to stay within FOL if you work over some basic foundational system. For instance consider the following:

  $∃f{∈}FN\ ( \ \text{Dom}(f)=ℕ_{<k} ∧ ∀i{∈}ℕ_{<k} \ ( \ Q(f(i)) \ ) ∧ ∀i,j{∈}ℕ_{<k} \ ( \ i≠j ⇒ f(i)≠f(j) \ ) \ )$.

Here $FN$ is the collection of all functions. In English this says: "There is an injective function $f$ with domain $ℕ_{<k}$ (i.e. naturals less than $k$) whose every output satisfies $Q$.". Notice that this sentence does not grow ridiculously longer for larger $k$. Of course, the price you must pay is the reliance on the foundational system to provide you the ability to reason about functions and their domains and so on... And this sentence cannot be used to say something over an arbitrary FOL structure in the language of the structure itself.