John Carlos Baez on Nostr: - modern logician use : a lot in "type theory", and would write 𝑛:ℕ to mean 𝑛 ...

- modern logician use : a lot in "type theory", and would write 𝑛:ℕ to mean 𝑛 is of type "natural number". Type theory works differently from set theory, so while n:ℕ means something very similar to 𝑛∈ℕ, the former tells us we're not doing set theory.

Thanks to all this, the older usage of : to mean 'such that' is becoming less popular in logic. However, other mathematicians still use it.

There is no one "official standard". Still, there are ways to look like an expert and ways to look strange!

If you read very serious logic books, they will all develop their own "official standard" and stick with it, at least until they introduce abbreviations. A bunch will say that for any formula P and any variable 𝑛 there is a formula ∃𝑛 (P). When P is 𝑛²+1=10 this gives ∃𝑛(𝑛²+1=10). The reason for using the parenthesis is that we need to distinguish between

∃𝑛 (P) ∧ Q

and

∃𝑛 (P ∧ Q)

I wouldn't worry about the difference between ( ) and [ ].