Mdthbs

On notation, at first I just write $exists^{!infty}$, later I changed to $exists^infty$, which one should I use $?$

And I'm thinking what does this really mean in first-order-logic$dots$

My attempts (first formalize at least, at most, exact)

$text{Let n $inmathbb{N}$, then }exists^{ge n}x,p(x) text{ if and only if :}$
$$exists x_1dots x_n text{ s.t.}underbrace{(p(x_1)wedgedotswedge p(x_n))}_{text{$x_1dots x_n$ satisfy $p$}}
wedgeunderbrace{(x_1neq x_2dots x_1neq x_n)wedgedotswedge(x_{n-1}neq x_n)}_{text{$x_1dots x_n$ are distinct}}$$

$$Leftrightarrowunderset{i=1}{overset{n}{exists}} x_i,(bigwedge_{i=1}^np(x_i))wedge(bigwedge_{i=1}^{n-1}(bigwedge_{j=i+1}^nx_ineq x_j))$$

$exists^{le n}x,p(x) text{ if and only if :}$
$$exists^{<n+1}x,p(x)$$
$$Leftrightarrowneg(exists^{ge n+1}x,p(x))$$
$$Leftrightarrow underset{i=1}{overset{n+1}{forall}}x_i,(bigvee_{i=1}^{n+1}neg p(x_i))vee(bigvee_{i=1}^n(bigvee_{j=i+1}^{n+1}x_i=x_j))$$
$exists^{!n}x,p(x) text{ if and only if :}$
$$exists^{ge n}x,p(x)wedgeexists^{le n}x,p(x)$$
$$Leftrightarrowexists^{ge n}x,p(x)wedgeneg(exists^{ge n+1}x,p(x))$$
$$Leftrightarrow underset{i=1}{overset{n}{exists}}x_iforall x_{n+1}(p(x_{n+1})leftrightarrow(bigvee_{i=1}^nx_i=x_{n+1}))wedgebigwedge_{i=1}^{n-1}(bigwedge_{j=i+1}^nx_ineq x_j)$$

The idea is first we define at least $n$, then we notice that at most $n$ is just not (at least $n+1$), also notice exactly $n$ is just at least $n$ and at most $n$.

Then, to express exists infinitely many we can write

$exists^{infty}x,p(x)$ if and only if: $$forall ninmathbb{N},exists^{ge n}x,p(x)$$ $$Leftrightarrow forall ninmathbb{N},underset{i=1}{overset{n}{exists}} x_i,(bigwedge_{i=1}^np(x_i))wedge(bigwedge_{i=1}^{n-1}(bigwedge_{j=i+1}^nx_ineq x_j))$$

Is it correct, can anyone verify this.

Thanks for you help

The more words rather than symbols the better for your reader. I suggest

The proposition $p(x)$ is (or is not) true for infinitely many $x$.

I think it will be more clear if you use just standard notation. Instead of say "exists infinitely many $x$ such that $p(x)$" you can say that "there exists $Asubset Bbb R $ with $|A|geqslant aleph _0$ such that for all $xin A$ then $p(x)$".

You can change $Bbb R$ by any appropriate set in your context.

In formulas something like

$$
exists Aforall xbig(|A|geqslant aleph _0land (xin Aimplies p(x))big)
$$

EDIT: my answer above try to fit to the case that you want to use standard logic notation to represent what you want, however as said in the answer of @EthanBolker words are better than symbols.

The standard notation in logic would be $exists^infty$.

The exclamation mark ! is used to indicate uniqueness, $exists^{!n} x,phi(x)$ being "there are exactly $n$ distinct elements $x$ such that $phi(x)$". So, the standard reading of $exists^{!infty}x,phi(x)$ would be "there are exactly infinitely many $x$ such that..." which is awkward, as it is not very exact to simply say "infinitely many", since there are many options here. And if you are in a setting where the universe of discourse is countably infinite, for instance, then the "exactly" part is superfluous anyway.

You are correct that $exists^{infty}x,phi(x)$ is the same as $forall n,exists^{ge n}x,phi(x)$. This is the case regardless of whether you are in a situation where the axiom of choice holds. I mention this because using choice, $exists^{infty}x,phi(x)$ is equivalent to $Q_{aleph_0}x,phi(x)$, where $aleph_0=|mathbb N|$ and, for a cardinal $kappa$, $Q_kappa x,phi(x)$ means that there are at least $kappa$ distinct values of $x$ such that ... (The $Q_kappa$ are called cardinality quantifiers in the literature.) However, if choice fails, a set may be infinite without containing a countably infinite subset.

(And just to avoid confusion, let me add the remark mentioned in comments: Although each $exists^{ge n}$ is first-order definable as shown in the question, $exists^infty$ is a genuinely new quantifier, meaning that it is not first-order definable by a formula. Otherwise, its negation ("there are only finitely many") would also be first-order definable, and an easy compactness argument gives us a contradiction: the theory $${lnotexists^infty x,(x=x)landexists^{ge n}x,(x=x)mid ninmathbb N}$$ is inconsistent but any finite subset is consistent.)