We define a function:

$f: \mathbb{N} \to \mathbb{N}_0, \quad f(n) = n - 1$

• Well-defined: For every $n \in \mathbb{N}$, we have $n \ge 1$, so $n-1 \ge 0$. Hence $f(n) \in \mathbb{N}_0$, and the function is well-defined.
  
• Injective: Suppose $f(n_1) = f(n_2)$. Then
  $n_1 - 1 = n_2 - 1 \implies n_1 = n_2$.
  Hence $f$ is injective.
  
• Surjective: Let $m \in \mathbb{N}_0$. Define $n = m + 1 \in \mathbb{N}$. Then
  $f(n) = f(m+1) = (m+1)-1 = m$.
  Hence $f$ is surjective.

Conclusion: The function $f(n) = n-1$ is a bijection between $\mathbb{N}$ and $\mathbb{N}_0$.

It is defined as a bijection. The same way square-circles are defined as shapes that are both circles and squares. That does not mean they are logical possibilities, i.e. free from internal contradictions.

And there's a subtle difference between "You can pick any number from N and map it onto a unique number from N0" and "You can pick every number from N and map it onto a unique number from N0".

You wouldn't expect completion from a thread titled "Infinity" would you?

Not really, but ignoring the infinite level of irrelevance of the topic is a pretty important omission.

It is defined as a bijection. — Magnus Anderson

$\mathbb{N}_0$?

Well, no. It is defined as f(n)=n−1 and then shown to be a bijection. That definition does not mention bijectivity at all. At this stage, the function could turn out to be injective, surjective, neither, or both. Nothing is being smuggled in.

While a square-circle is defined using incompatible properties, there is no contradiction in $\mathbb{N}_0$.

N0? — Banno

Not N0 but f(n) = n - 1. That function is a bijection by definition.

It is defined as f(n)=n−1 and then shown to be a bijection. That definition does not mention bijectivity at all. At this stage, the function could turn out to be injective, surjective, neither, or both. Nothing is being smuggled in. — Banno

Yes. It is not explicitly stated in the definition. However, the definition implies it. And because it implies it, it is a bijection by definition.

It's like defining the symbol "S" as "a closed figure with three straight sides". It does not explicitly state that it has 3 angles but it does imply it. So it is correct to say that S has 3 angles by definition.

"By definition" does not mean "explicitly stated by the definition". It means "fixed by the definition ( either explicitly or implicitly )".

In mathematics, functions are defined as sets of input-output pairs. f( n ) = n - 1, in this view, is a set of input-output pairs where every element from N is paired with exactly one element from N0 and vice versa. That makes it a bijection by definition. But that does not mean that the bijection between N and N0 exists, i.e. that it is a logical possibility. It merely means that's what the symbol can represent. It's similar to how simply saying that the term "square-circle" means "a shape that is both a square and a circle" does not mean that square-circles exist.

The seemingly devastating consequences of accepting that no bijection exists between N and N0 is that f( n ) = n - 1 does not exist either, i.e. that it is an oxymoron. The good news is that that's merely a consequence of an incorrect definition of functions. Functions aren't sets of input-output pairs. They are sets of rules.

Not N0 but f(n) = n - 1. That function is a bijection by definition. — Magnus Anderson

Here's the definition again: $f: \mathbb{N} \to \mathbb{N}_0, \quad f(n) = n - 1$

$\quad f(n) = n - 1$ as it stands is not a definition of a bijection. It can't be, because it lacks a domain and a codomain, as provided by $f: \mathbb{N} \to \mathbb{N}_0$

$\quad f(n) = n - 1$ could be applied to any domain, with differing results. With $\mathbb{Z}$ as the domain and codomain also $\mathbb{Z}$, it would be a bijection. If the domain were $\mathbb{N}$ and the codomain $\mathbb{Z}$, bijectivity would again depend on proof, not stipulation.

Yes. It is not explicitly stated in the definition. However, the definition implies it. — Magnus Anderson

An odd thing to say, since making that implication explicit is exactly what the proof presented above does. you treat $\quad f(n) = n - 1$ as if it secretly meant "let $f$ be a bijection defined by $\quad f(n) = n - 1$"; but that is not what is being done. What was done, step by step, was:

1. Define a function by a rule.
2. Specify domain and codomain.
3. Prove that, given those, the function is injective and surjective.

$\quad f(n) = n - 1$ might be bijective, non-surjective, or non-injective depending on the domain and codomain.