Philosophical questions about equality

Stream: maths

[Mujtaba Alam]

If n is a real number, is n + 0i a real number? Is it equal to n?
According to wikipedia, "equality is a relationship between two quantities or, more generally two mathematical expressions, asserting that the quantities have the same value, or that the expressions represent the same mathematical object."

I agree they have the same value, but do they represent the same mathematical object? n is a point on the number line, while n + 0i is a point on the complex plane

[Kyle Miller]

The Lean answer is that terms of real and terms of complex are completely different things, and so (via eq) they are neither equal nor not equal. There is an injective function coe : real -> complex that lets you coerce real numbers to let you think about real numbers as being complex numbers, and it carries properties of reals over to properties of the corresponding complex numbers.

With this in mind, when you write n + 0*complex.I, what happens is that Lean will automatically insert the coercion so that it is coe n + 0*complex.I, giving you the illusion that the reals sit inside the complexes. Furthermore, if you write n + 0*complex.I = n then using the same mechanism it is actually coe n + 0*complex.I = coe n. This proposition is true in Lean.

[Kyle Miller]

In Lean, a real number is the Cauchy completion of the rationals and a complex number is a pair of real numbers. It's hard to say whether this sort of symbolic data is a number line and a plane.

If we're talking philosophy, then we have to be careful about what we mean by "equals." Lean already has definitional equality and eq, but there's the more nebulous one you seem to be talking about, which is whether two things somehow represent the same thing.

[Andrew Yang]

Kevin Buzzard had a twitter thread talking about whether ℕ = ℤ or even whether ℕ ⊆ ℤ. This is kind of the situation here as you are debating whether the reals is a subset of C, or merely isomorphic to a subset of C.

1) ℕ={1,2,3,...} or {0,1,2,3,...} (who cares) where 0={} and 1={0} and 2={0,1} etc. 2) ℤ is a localisation of ℕ, or a quotient of ℕ^2 (same thing) and you can make quotients using equivalence classes. 3) ℕ ⊆ ℤ in the obvious way. These can't all be true at once. 3/n

- Kevin Buzzard (@XenaProject)

[Kevin Buzzard]

The tl;dr answer is that in lean it doesn't even make sense to ask if a real number and a complex number are equal.

[Kevin Buzzard]

But in other foundations of mathematics you might get different answers.

[Eric Rodriguez]

(and if you really want to write the equality, n == ↑n + 0 * complex.I is undecidable [​ docs#heq​ ])

[Kevin Buzzard]

It's also not the right question (in some cardinality model you might have \R=\C in a guaranteed-to-be-mathematically-meaningless way)

[Patrick Johnson]

The way I was told to fix this was to either redefine ℕ to be the subset of ℤ, or redefine ℤ to be "ℤ with the thing isomorphic to ℕ removed, and then union with actual ℕ". Both of these approaches are actually quite problematic in practice.

In my opinion, the most intuitive way to define ℕ in ZFC is to use the axiom of (global) choice to pick a set that satisfies Peano axioms. Then we can construct ℤ by using choice again to pick a set that satisfies appropriate conditions for ℤ (including ℕ ⊆ ℤ). Using any explicit model for any of those sets seems like cheating - we're adding more information to the system that we actually need, leading to proofs that diverge from reality.

Next, addition on natural numbers can be defined using choice to be some function that satisfies n + 0 = n and n + succ m = succ (n + m). We can define subtraction using choice to be some function that satisfies n - 0 = n and succ n - succ m = n - m. We cannot prove anything about 5 - 7 for example. However, when we define ℤ, we can extend the definitions for + and - by adding new conditions to the choice predicate, so that it covers the set of integers as well. We need to prove that the new models of + and - on ℤ (used only in the proof of existence) also satisfy the conditions for + and - on ℕ.

I don't think this approach would be "quite problematic in practice", especially given that we don't use any explicit model outside of the proof that at least one model exists. Note that this only applies to set theory.

Regarding the n = n + 0i question, the most common definition of equality in math is that any two objects x and y are said to be equal iff for any statement P, if P x holds then P y also holds. In Lean, this cannot be accurately expressed because of how dependent type theory works. That is, in some cases we cannot even construct a statement (types do not match), even though in set theory the same statement would make perfect sense. So, not only that ℝ = ℂ is undecidable, but n = n + 0 * complex.I does not even type check for n : ℝ. We can use heterogeneous equality, but as pointed out already, it's undecidable in that case. Moreover, whether heterogeneous equality in Lean represents the actual math notion of equality is disputable, because if x == y and P x holds for some statement P, we may not be able to prove P y because types do not match, even though x and y are provably the same object.

[Eric Rodriguez]

That last statement is not true, Patrick: docs#type_eq_of_heq

[Patrick Johnson]

No, I mean:

example {α β : Type} {P : α → Prop} {x : α} {y : β}
  (h₁ : x == y) (h₂ : P x) : true :=
begin
  have : P y := sorry -- type mismatch
end

We can't even express P y without rewriting predicate P itself, while in set theory we can express P y directly.

[Eric Rodriguez]

sure, but you can subst type_eq_of_heq and this sorts itself out

[Eric Rodriguez]

I see what you're saying, though