Why is $\Bbb Z = \Bbb N$ independent of Lean?

Question

In this answer, it is noted

For a silly example, in ZFC with the usual encoding, $\mathbb{Z} \neq \mathbb{N}$, but in Lean it is well-known that this is independent. Of course in both ZFC or Lean, one could have defined $\mathbb{Z} := \mathbb{N}$ and then we have $\mathbb{Z} = \mathbb{N}$.

As someone totally new to Lean: why is $\mathbb{Z} \neq \mathbb{N}$ independent of Lean? How are $\mathbb{Z}$ and $\mathbb{N}$ formalized in Lean such that this makes sense?

Answer 1

I hesitate to give an answer since I don't know the full details, but here is my understanding.

Consistency of all types of the same cardinality being equal

There is a model of Lean, the cardinality model, where types are modeled by cardinalities (instead of sets), and in this model two types are equal if and only if they have the same cardinality.

This cardinality model might seem weird to a ZFC set theorist, but if you think instead of the category $\mathsf{Set}$ as your model of set theory (which is more like Lean's model) it isn't that weird. In category theory, you only care about objects up to isomorphism. For example, a group theorist would be more likely to say there is just one group on two elements than a proper class worth. And with the category $\mathsf{Set}$, two objects are isomorphic iff they have the same cardinality. (I haven't looked that closely at various axiomatizations for $\mathsf{Set}$, like ETCS or the more general Elementary Topos axioms, but I think they say nothing about whether there are or aren't two distinct objects that are isomorphic.) So for all practical purposes, the category $\mathsf{Set}$ can be replaced with the category of cardinal numbers.

While I think this cardinality model is folklore, it is also known that it basically follows from the set-theoretic model of Lean in Mario Carneiro's masters thesis The Type Theory of Lean.

Consistency that every inductive type and structure type is unique from any other

On the other hand, it is also consistent that any two named inductive and/or structure types, like Nat and Int are not equal to each other. The idea is that there is a model of Lean where each inductive and each structure comes with a unique label. So in this model inductive Foo | foo : Foo and inductive Bar | bar : Bar would be different just because they have different labels. (I'm a bit unclear on some of the details, including what a "label" means in this context, but I think it isn't that different from just the Lean name.)

Again, this is folk-lore. See the discussions here and here (especially any of the messages by Mario Carneiro).

What else do we know about equal and not-equal types

Here are all the things I know about type equality.:

• Types of different cardinalities are provably not equal (because they have different properties). (I'm assuming choice, which is needed to define cardinality.)
• It is consistent that types of the same cardinality are equal.
• It is consistent that any inductive or structure type is distinct from any other such type (and also from function types, I think).
• Types are provably equal if they are definitionally equal, like def Foo := Nat or Fin (1+1) = Fin 2.
• Two elements of a parameterized family of types, like List A, Fin n, and A -> B, are equal if their parameters are equal, like Fin 2 = Fin (Nat.card Prop).

I don't think there is much else constraining type equality besides those and the following final fact which I learned from Mario Carneiro: If you have a parametrized type Foo (x : Type -> Bool) : Type (which you can create with say inductive or structure in Lean), then by cardinality concerns, there has to be distinct elements x y : Type -> Bool such that Foo x = Foo y (but you can't prove anything about what x and y are).

Answer 2

It suffices to give two models of Lean's type theory, one in which $\mathbb{Z} = \mathbb{N}$ and another in which $\mathbb{Z} \ne \mathbb{N}$.

We shall use the interpretation of Lean type theory in set theory: types are sets, type families are families of sets.

Importantly, all that is required for the interpretation of an inductive type is for it to be the initial algebra for the signature given by the definition of the inductive type. Specifically, the interpretation of

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

should be a set a set $N$ with an element $\mathtt{zero} \in N$ and a map $\mathtt{succ} : N \to N$, such that $(N, \mathtt{zero}, \mathtt{succ})$ is an initial algebra for structures with one constant and one unary operation. A customary choice is to take $\mathtt{zero} = \emptyset$, $\mathtt{succ}(x) = x \cup \{x\}$, and $N$ the least set containing $\emptyset$ and closed under $x \mapsto x \cup \{x\}$, let us write $\mathbb{N}$ for this particular set.

The interpretation of

inductive Int : Type where
  | ofNat   : Nat → Int
  | negSucc : Nat → Int

amounts to exhibiting a set $\mathbb{Z}$ that is the disjoint union of two copies of $\mathbb{N}$, i.e., $\mathbb{Z}$ must be of the form $$\{\mathtt{ofNat}(k) \mid k \in \mathbb{N}\} \cup \{\mathtt{negSucc}(m) \mid m \in \mathbb{N}\} $$ where $\mathbb{N}$ is the above interpretation of Nat, and $\mathtt{ofNat}$ and $\mathtt{negSucc}$ are injective maps with disjoint images.

With these constraints it is easy to arrange either option. To arrange $\mathbb{N} = \mathbb{Z}$, take \begin{align*} &\mathtt{ofNat} : \mathbb{N} \to \mathsf{Set} & &\mathtt{negSucc} : \mathbb{N} \to \mathsf{Set} \\ &\mathtt{ofNat}(k) = 2 k & &\mathtt{negSucc}(k) = 2 k + 1 \end{align*} And to arrange $\mathbb{N} \ne \mathbb{Z}$, take \begin{align*} &\mathtt{ofNat} : \mathbb{N} \to \mathsf{Set} & &\mathtt{negSucc} : \mathbb{N} \to \mathsf{Set} \\ &\mathtt{ofNat}(k) = (\emptyset, k) & &\mathtt{negSucc}(k) = (\{\emptyset\}, k) \end{align*} where we used Kuratowski's pairing $\{x, y\} = \{\{x\}, \{x,y\}\}$. Because $\emptyset = \mathtt{zero} \in \mathbb{N}$ and $(x,y) \neq \emptyset$, we indeed have $\mathbb{N} \ne \mathbb{Z}$.

Answer 3

A less confusing and more common situation happens in algebra, where people write the group $2\mathbb Z \hookrightarrow \mathbb Z$. For example we can define the dyadic rationals as the direct limit $\mathbb Z \to \frac12\mathbb Z \to \cdots$. The group $2\mathbb Z$ is actually the exact same as the group of integers, so for group theory purposes you can define $2\mathbb Z = \mathbb Z$, and all the mathematics remain the same. You just have to replace the diagram above with $\mathbb Z \xrightarrow{\times 2} \mathbb Z \xrightarrow{\times 2}\cdots$, instead of relying on inclusion maps.

So the only difference of $2\mathbb Z$ is that it invokes different conventions. If I say "consider the obvious map $2\mathbb Z \to \mathbb Z$", you immediately think of the inclusion, which is equivalent to the map $2 : \mathbb Z \to \mathbb Z$. So mathematicians only use this as a tool to shorten their notation and expressing their intent, which is not strictly necessary for writing a proof. Hence in a purely formal proof involving groups, defining $2\mathbb Z = \mathbb Z$ makes perfect sense.

Similarly, for set theory purposes, $\mathbb N$ and $\mathbb Z$ have no difference, since they have a bijection. We only write one in place of another to invoke different conventions. For example when I say "consider the usual multiplication map on ...", it refers to different maps in the two cases. But in a formal proof involving sets, we can always replace one with another without any substantial change.

A final note: we cannot make this replacement in the theorem $\mathbb Z = \mathbb Z$, because it produces the unprovable statement $\mathbb Z = \mathbb N$. But this is not a theorem about sets. It is a theorem about the name of sets (types).