Expressing “$n$ is the $k$-th number to satisfy $P$” in FOL If we're in the domain of natural numbers and want a formula that expresses that $n$ is the $k$-th number to satisfy $P,$ how would we write this? For example, if we're trying to express the least number that satisfies P, we could do that through the formula $Pn ∧ ∀x(Px→n≤x).$ If we wanted to express the second least number that satisfies $P,$ again no issue. But how do I expand this to $k$-th number while still keeping the formula well formed in FOL?
The way I think this might be doable is through this formula, or something like it 
So to find the k-th number we first show all the numbers before it in the sequence, indicate that it isn't any of them, and then show that it's the next least number to satisfy P.
But it has ellipses, so is it really a formula of FOL?
 A: It is excellent that you are asking yourself about the ellipsis. If $k$ is a fixed natural number, then your formula works. It is an FOL formula for each $k$, even if it is different for each $k$. I suspect that this is actually all you were looking for.
But your formula (and DanielV's formula) both have length quadratic in $k$. Just for fun, we can actually do better:
  $∃x_{1..k}\ \Big( \ n = x_k ∧ \bigwedge_{i=1}^{k-1} ( x_i < x_{i+1} ) ∧ \bigwedge_{i=1}^k P(x_i)$
  $\quad\quad\quad{}∧ ∀y\ \big( \ P(y) ∧ y ≤ x_k ⇒ \bigvee_{i=1}^k ( y = x_i ) \ \big) \ \Big)$.
However, there is a highly nontrivial fact that if your base theory include PA− (or even just Robinson's Q), then we can actually have a single formula where $k$ is a parameter, instead of one formula for each $k$! Basically it is possible to encode any finite sequence as a single natural, such that there are definable functions $l,e$ over PA− where $l(c)$ is the length of the sequence coded by $c$ and $e(c,i)$ is the $(i{+}1)$-th term in the sequence coded by $c$ (for each $i<l(c)$). There are also definable functions over PA− for manipulation of sequences (e.g. constructing a singleton or obtaining the concatenation of two sequences). Using these, we can translate the above formula schema into a single formula where $k$ is a parameter, essentially by replacing the $k$ existential quantifiers in front by a single quantifier over finite sequences of length $k$:
  $∃x\ \Big( \ l(x) = k ∧ n = e(x,k) ∧ ∀i_{<k-1}\ ( \ e(x,i) < e(x,i+1) \ ) ∧ ∀i_{<k}\ ( \ P(e(x,i)) \ )$
  $\quad\quad\quad{}∧ ∀y\ \big( \ P(y) ∧ y ≤ e(x,k) ⇒ ∀i_{<k} ( y = e(x,i) ) \ \big) \ \Big)$.
By the way, Bram28's approach is not incorrect, and is a reasonable 'intermediate' approach, but to justify that approach we must show that the extension (with the extra predicate-symbol and the added axiom) is conservative (i.e. every theorem that it proves can be proven by the original). That fact is essentially due to what I have explained above.
For reference take a look at Rautenberg's "A Concise Introduction to Logic", specifically "definitorial expansion" for when we can extend a theory conservatively (including the use of $l,e$ above) as well as "Godel number" for the sequence coding.
A: Where $P(x,y)$ means that the $x$-th number that has property $P$ is $y$, maybe you could introduce an axiom that recursively defines this:
$\forall x \forall y P(x,y) \leftrightarrow (P(y) \land \\ ((x = 1 \land \forall z (z < y \to \neg P(z))) \\ \lor (1<x \land \exists v \exists w (s(v) = x \land P(v,w) \land \forall z (w < z \land z < y \to \neg P(z))))))$
Here, $s(x)$ is a function that returns the successor of $x$, for which you can use the Peano axioms.
With this as a background axiom, you can just use $P(k,m)$ wherever needed.
Also, while user21820 is correct in pointing out that adding this as an axiom would not be obviously conservative, and that we can actually use a formula that does not introduce any new predicates using Godel’s encoding scheme, I do believe that the above method is a lot more practical. For example, if $Prime(x)$ is a formula that expresses that $x$ is s prime number (this is quite straightforward using the language of arithmetic), then you can use the above scheme to represent $Prime(x,y)$, where the $x$-th prime number is $y$, and you can actually prove something like $Prime(3,5)$ without too much trouble.
A: 
"But it has ellipses, so is it really a formula of FOL?"

Yes it still is.  For 1 given value of k there is 1 FOL expression in which k is not a free variable.  Technically, using $=$ makes it not FOL but that is a common thing to ignore.  If you are wanting to maintain k as a free variable, then you might need something as strong as this: https://mathoverflow.net/questions/374169/how-can-i-prove-that-primitive-recursion-preserves-representability-in-peano-a

Here is an alternative derivation of a formula.  It's pretty well known how to say $\exists ! j . P(j)$ "there is one value such that P holds:"
$$\exists s . P(s) \land \forall t. P(t) \to s=t$$
That can be continued for $\exists_2 j . P(j)$ "there are two values such that P holds:"
$$\exists s_1, s_2 . s_1 \ne s_2 \land P(s_1) \land P(s_2) \land \forall t. P(t) \to (s_1=t \lor s_2 = t)$$
That can be continued for $\exists_k j . P(j)$ "there are k values such that P holds:"
$$\exists s_1 \dots s_k . \underbrace{s_1 \ne s_2 \land \dots \land s_{k-1} \ne s_{k}}_{O(k^2) \text { distinctions }} \land \underbrace{P(s_1) \land \dots \land P(s_k)}_{O(k) \text{ conjunctions}} \land \forall t. P(t) \to (\underbrace{s_1=t \lor \dots \lor s_k = t}_{O(k) \text{ disjunctions}})$$
So to say "n is the k'th value such that P holds:"
$$P(n) \land \exists_k  j . j \le n \land P(j)$$
This has the problem of being $O(k^2)$ sized expression and that $k$ is not a free variable.  But $\le$ can mean anything you want.
