Correct logical quantifier notation with greater than/less than relations

Question

I’m in the middle of some exercises for an intro to proofs class, and want to know if it is possible to write the following:

“For all real $n \geq N$” as $(\forall n \in \mathbb{R} \geq N)$.

If that is incorrect syntax, I’d like to know the correct way!

Answer 1

While abbreviations like that may be used informally, they are usually not valid formal syntax. Most commonly, you would write $\forall n\in\mathbb R(n\geq N \to(\dots))$ (or some minor notational variation of this). In fact, the $\forall n\in\mathbb R(\dots)$ is usually itself an informal abbreviation for $\forall n.(n\in\mathbb R \to (\dots))$.

An alternative approach would be to use set builder notation and write $\forall n\in\{x\in\mathbb R\mid x\geq N\}(\dots)$.

What exactly is valid depends on the exact formal notation you're using. I would not be surprised, though, if you haven't been given a clear, comprehensive description of the formal syntax you're supposed to be using. The above is based on common conventions, but conventions vary¹. If you have been given a description of the formal syntax you're supposed to use, you can check yourself whether your translation is a well-formed formula with respect to that syntax.

I do recommend trying to stick to a clear syntax and not use abbreviations, especially undefined abbreviations, at least early on. It is quite common, for example, for people to not have a clear understanding of the abbreviation $\exists x\in\mathbb R.P(x)$.

¹ Eindhoven notation (as illustrated here, for example), explicitly covers this pattern of usage, and would lead to something like $(\forall n:\mathbb R\mid n\geq N\bullet(\dots))$.

Answer 2

To add to Derek's answer, the restricted quantification syntax is "$∀x∈S\ ( P(x) )$" or "$∀x:S\ ( P(x) )$", where $S$ is a set/type and "$P(x)$" is a statement about $x$ that is meaningful in the context where $x∈S$. So we cannot have "$∀x∈\mathbb{R}≥N\ ( ... )$". But we can have "$∀x∈\mathbb{R}_{≥N}\ ( ... )$" after we define $\mathbb{R}_{≥N} := \{ x : x∈\mathbb{R} ∧ x≥N \}$. This would be not only rigorous but also immediately understandable. Moreover, this syntax makes certain theorems short and elegant:

Strong induction: $∀m∈\mathbb{N}\ ( ∀k∈\mathbb{N}_{<m}\ ( P(k) ) ⇒ P(m) ) ⇒ ∀m∈\mathbb{N}\ ( P(m) )$ for any property $P$ on $\mathbb{N}$.