stupid question: `Nat = String`?

Stream: general

[Jz Pan]

Can Nat = String be proved or disproved in Lean? The only possible case I can think of is that, if two Types have different cardinality, then they cannot be equal. But these two are all countable.

Or in general types cannot be compared, as this does not make sense?

[Riccardo Brasca]

You are right, in general the only way to disprove that two types are equal is using a cardinality argument.

[Riccardo Brasca]

In particular, the equality Nat = String is almost surely undecidable.

[Shreyas Srinivas]

What does it mean for the equality of two specific types to be undecidable? Undecidability as a concept applies to decision functions (or their corresponding sets)

[Ruben Van de Velde]

It's independent of the axioms lean is based on

[Kyle Miller]

Yeah, computability theory doesn't have a monopoly on the term. "Undecidable" also means "independent of the axioms". See https://en.wikipedia.org/wiki/Independence_(mathematical_logic)

[Riccardo Brasca]

See https://en.wikipedia.org/wiki/Independence_(mathematical_logic)

[Shreyas Srinivas]

Ah right. Now I remember that I have seen this term in model theory.

[Shreyas Srinivas]

Thanks