Is there a notation for the smallest number $n$ that satisfies property $P$?

Question

Is there some logical notation that means "the smallest $n$ that satisfies $P$", e.g. $$f(x) = \text{the smallest $n \in \Bbb{Z}$ such that $xn \ge x+n$}. $$

Answer 1

In computability theory we call this the $\mu$ operator (Wikipedia article). So $$ \mu x. P(x)$$ returns the smallest natural number for which $P(x)$ is true.

There is no ordinary notation for this outside of computability theory and logic, apart from the normal "min" operator.

One issue is that, if there is no natural number so that $P$ holds, then $\mu x. P(x)$ will be undefined.

Answer 2

There are a few different notations you could use, most of which are translations for each other. If we want to take it back to something close to Peano arithmetic, we could define it like this:

$$L(x; S) := S(x) \wedge \left(\forall y \left((S(y) \implies \left( \exists z \left( y = x + z \right)\right)\right)\right)$$

Or in other words, we define our "Least" property on the statement $S$ and the natural number $x$ as:

1. For our given statement $S$, $S(x)$ is true.
2. For any other $y$ such that $S(y)$ is true, $y$ is greater than or equal to $x$ (which we express as "there exists a $z$ such that $y = x + z$).