7
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ See this discussion on the Coq Zulip for some information. And here on the Lean Zulip. Maybe someone can summarize it into a nice answer here. $\endgroup$
    – Jason Rute
    Commented Jun 10 at 1:28
  • $\begingroup$ How would you prove that $\mathbb{Z} \neq \mathbb{N}$ without relying on any particular encoding of $\mathbb{N}$ and $\mathbb{Z}$ as sets? $\endgroup$ Commented Jun 10 at 6:29
  • 1
    $\begingroup$ I think the confusion arises that in set theoretic foundations these types are encoded explicitly as sets (usually not equal ones). Also in some other non DTT programming languages, distinct inductive types are not equal (if you can compare types at all). And in homotopy type theory something like isomorphic types are equal. But in Lean and other vanilla DTT implementations there just is nothing in the language forcing an answer to this equality, so it is independent. $\endgroup$
    – Jason Rute
    Commented Jun 10 at 11:43

3 Answers 3

3
$\begingroup$

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).

$\endgroup$
6
  • $\begingroup$ Thank you, this is fantastic! This is exactly the kind of answer I was looking for. Aren't there any resources to learn about this kind of thing, beyond just folklore? $\endgroup$ Commented Jun 12 at 17:26
  • $\begingroup$ @MikeBattaglia The challenge is that with real world systems, the details matter. For example Mario’s thesis shows the consistency of Lean’s type theory, but doesn’t clearly extend to Coq’s. (I’ve heard some even say that Coq’s type theory may be inconsistent.) So I think a lot of this stuff is left to work out in masters theses and folk-lore conversations. However I also have hope for formalization itself as a solution. For example, the project lean4lean is formalizing Mario’s thesis in Lean (among many other things). Hopefully these little folklore details will be included in that project. $\endgroup$
    – Jason Rute
    Commented Jun 12 at 22:24
  • $\begingroup$ However, if you are interested more generally in Martin-Löf type theory, the HoTT book is a good resource. In pure MLTT the story is interesting. It is consistent that something called the univalence axiom holds, which (sort of) says that types are equal iff they are isomorphic. In that setting, types no longer behave like sets, but instead like homotopy types (where equality behaves like a path connecting two points, and you can also have paths connecting paths, etc), hence the name homotopy type theory. Lean is incompatible with Univalence though. $\endgroup$
    – Jason Rute
    Commented Jun 12 at 22:38
  • 1
    $\begingroup$ @MikeBattaglia There are some books like that already. Mathematics in Lean is targeted for mathematicians. Software Foundations is targeted for those with more of a programming languages bent interested in Coq. Theorem Proving in Lean 4 is more on the logical side. Functional Programming in Lean is for learning functional programming. Also Mathematical Logic and Computation is a good logic book covering more of this side of the fence (the syntactic side). It doesn’t go into a lot of depth about type theory, but it gets you started. Nonetheless, I recommend you do ask that question on here. $\endgroup$
    – Jason Rute
    Commented Jun 13 at 2:28
  • 2
    $\begingroup$ But also learning how to program in Lean vs learning how to write proofs in Lean, vs learning about the foundations of Lean aren’t really the same thing. So one needs different resources for each. $\endgroup$
    – Jason Rute
    Commented Jun 13 at 2:29
8
$\begingroup$

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}$.

$\endgroup$
5
  • $\begingroup$ Thanks, that is a very good start to making sense of this. I would just say that, intuitively, it is pretty strange to imagine trying to formalize much of "normal" math without being able to just write $\Bbb N \subsetneq \Bbb Z$ and not think much about it! But I guess we have the same situation with ZFC, where also we could have $\Bbb N \subsetneq \Bbb Z$ be false if we encode the two sets in two different ways. $\endgroup$ Commented Jun 11 at 6:29
  • $\begingroup$ Did you mean to write $\mathbb{N} \subset \mathbb{Z}$? Also, what does that have to do with your question, which was "why is $\mathbb{Z} = \mathbb{N}$ independent in Lean"? That's what the answer is about, the $\mathbb{N} \subset \mathbb{Z}$ is a different issue that is dealt with separately. It would make sense to ask another question. $\endgroup$ Commented Jun 11 at 7:39
  • $\begingroup$ Not sure I'm following your objection, but I wrote that it's strange to imagine formalizing math in a system where one can't say things like "$\Bbb N \subsetneq \Bbb Z$", meaning that $\Bbb N$ is a subset of $\Bbb Z$ which isn't equal to the entire thing. $\endgroup$ Commented Jun 11 at 7:45
  • 2
    $\begingroup$ I think what you really mean to say is "the canonical inclusion $\mathbb{N} \to \mathbb{Z}$ is not onto", which you can perfectly well say and prove in Lean. And it wouldn't be any different in set theory, except that there you can also prove the "garbage theorem" $\mathbb{N} \not\subseteq \mathbb{Z}$ which holds "by accident of encoding natural numbers and integers". $\endgroup$ Commented Jun 11 at 7:47
  • $\begingroup$ As I said, there is much to be said about this issue, but it really should go into a separate answer. $\endgroup$ Commented Jun 11 at 7:49
2
$\begingroup$

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).

$\endgroup$
8
  • 1
    $\begingroup$ I'm really not sure I follow. When you say these things are the same for "group theory" or "set theory" purposes, I take it as though you are saying they are isomorphic objects in the relevant category. But I don't get why that means that Lean can't prove the two sets - or any two sets with the same cardinality - aren't equal. $\endgroup$ Commented Jun 10 at 4:27
  • $\begingroup$ @MikeBattaglia I explained why you can simply define $\mathbb Z := \mathbb N$ and mathematics will not change, since that's the quote in your question. If we take such a definition then the sets are, of course, equal. Do you mean you want a technical proof of independence? $\endgroup$
    – Trebor
    Commented Jun 10 at 4:30
  • 1
    $\begingroup$ The quote in my question says that it's well known that in Lean, the statement $\Bbb Z = \Bbb N$ is formally independent (of, I presume, the Lean axioms). That would seem to be a much stronger statement than just saying that they are isomorphic in the category of sets, or that you could build a group isomorphic to $\Bbb Z$ using $\Bbb N$ or $2\Bbb Z$ as the base set, or etc. What does it even mean, formally, unless the symbols $\Bbb Z$ and $\Bbb N$ have some formal meaning? $\endgroup$ Commented Jun 10 at 4:40
  • 1
    $\begingroup$ @MikeBattaglia What is "formal meaning"? Do you mean the definitions of the two things? (It doesn't matter because any two countable sets will do.) The proof is basically that you can interpret types as cardinal numbers, and if you could prove $\mathbb Z \ne \mathbb N$ then in the model $\aleph_0 \ne \aleph_0$, contradiction. $\endgroup$
    – Trebor
    Commented Jun 10 at 5:00
  • $\begingroup$ I'm just saying that as someone familiar with set theory but not with Lean, I'm trying to understand what the limitation is. Of course I get the philosophical view that $\Bbb Z$ and $\Bbb N$ are isomorphic in various categories, or you can dress $\Bbb N$ up with a weird group structure to make it isomorphic to $\Bbb Z$, etc. But it seems like you are saying that Lean cannot prove that two sets with the same cardinality aren't literally equal. Is that it? Because if that's true, that is very very surprising to me, as someone new to Lean... $\endgroup$ Commented Jun 10 at 5:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.