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.

Here's the definition again — Banno

I can't quote the entire part, the LaTeX code gets messed up for some reason.

You are right that f( n ) = n − 1 by itself is not a complete definition of a function. A function definition requires a domain and a codomain. I conveniently left those out, assuming that they could be inferred from the context.

I was referring to the N -> N0 variant.

bijectivity would again depend on proof, not stipulation — Banno

When I say the function is bijective by definition, I do not mean that bijectivity is explicitly stated, but that it is an unavoidable consequence of the definition. The "proof" consists solely in unpacking what is already implied by the definition, not in adding any further stipulation.

f(n)=n−1 might be bijective, non-surjective, or non-injective depending on the domain and codomain. — Banno

That's correct. However, I was talking about f: N -> N0, f( n ) = n - 1. That specific variant does imply bijection.

The real problem is being ignored and that is that the fact that a definition implies bijection between N and N0 does not mean that such a bijection exists in the sense of being a logical possibility.

When I say the function is bijective by definition, I do not mean that bijectivity is explicitly stated, but that it is an unavoidable consequence of the definition. The "proof" consists solely in unpacking what is already implied by the definition, not in adding any further stipulation. — Magnus Anderson

Yep. that's what a proof does.