Prop, Sort, and Type

Stream: new members

[Sam]

Is there a good resource/can someone explain what the relations between Prop, Sort m, and Type n are? I have found https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html but I am still confused about why Prop = Sort 0 and why the Sort and Type hierarchies have to exist. Second, my brain can comprehend, say, how "float" in C++ consists of "floating point numbers", but what lives in Sort 42?

[Kenny Lau]

@Sam the simple explanation is, everything has a type, term : type means term has type type. For example, 37 : Nat means "37 is a natural number", and rfl : 3 = 3 means that "rfl is a proof of the proposition 3 = 3". (i.e. the "type" thing has two different translations depending on whether the RHS is mathematically a set or a proposition)

Now, what mathematicians think of sets (e.g. Nat) correspond to types. in colon notation, this says Nat : Type.

But then Type, which is the "type of all types", needs to have a type as well. That is Type 1, which mathematically corresponds to a "larger universe", so Type : Type 1

this goes on, since Type 1 also needs a type, so Type 1 : Type 2, and Type 2 : Type 3, and so on. (and 3 = 3 : Prop)

[Kenny Lau]

So now we have Prop for the type of propositions, then Type for the mathematical sets, but then on top of that we also have a hierarchy Type 1, Type 2, Type 3, ...

Sort is just a way to unify these two things, so Sort 0 = Prop, Sort 1 = Type, Sort 2 = Type 1, Sort 3 = Type 2, etc.

[Sam]

Thanks for the explanation. More silly questions coming:

• Is the main idea just that "Type" and "Prop" are two orthogonal (for lack of a better word) concepts that have both been lumped together as lowercase-t types?
• How does Prop differ from a true/false type in any other programming language? Hovering over Prop tells me "Every proposition is propositionally equal to either True or False." In my head I picture some boolean type with two "members": "true" and "false". Is that what the Prop type consists of? Or does it contain the statements "3 = 3" themselves?

[Julian Berman]

In backwards order:

How does Prop differ from a true/false type in any other programming language? Hovering over Prop tells me "Every proposition is propositionally equal to either True or False." In my head I picture some boolean type with two "members": "true" and "false".

A first approximation is "Prop is for math and bool is for programming, but otherwise they're representing the same thing". https://lean-lang.org/doc/reference/latest/Basic-Types/Booleans/#The-Lean-Language-Reference--Basic-Types--Booleans has a slightly longer explanation.

Or does it contain the statements "3 = 3" themselves?

3 = 3 : Prop (is a term of type Prop). Note that 3 = 7 : Prop -- i.e. is also a term of type Prop. The former you will be able to find proofs of, the latter you (hopefully) will not. (Finding a proof of 3 = 3 is equivalently constructing a term of type 3 = 3. ) Here perhaps is where bool and Prop start to feel different, as 3 = 7 would "Evaluate" to false, but the point in Lean is generally you want to be able to state things without necessarily evaluating them, as the point is to prove (or disprove) them and there isn't some general algorithm which "solves" any proposition, whereas when we're programming we want to know "do we go this way in the if statement or not?".

Is the main idea just that "Type" and "Prop" are two orthogonal (for lack of a better word) concepts that have both been lumped together as lowercase-t types?

A key concept in type theory/interactive theorem provers/Lean is that these are in fact not orthogonal -- specifically, or perhaps mindbendingly -- checking "does X prove Y" is in a real sense precisely the same as "is X of type Y" -- where the latter is certainly a familiar operation for programmers and the former is a familiar operation for mathematicians, and this nice correspondence is what makes theorem provers possible .

You might also find https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/ hepful to read.

[Kevin Buzzard]

Type n exists for the foundational reason that everything has to have a type in type theory, so Type needs to have a type and whatever that type is needs to have a type etc, and you can't have loops because this gives contradictions. When I'm teaching lean I don't teach the existence of these universes, they're basically only there because the type theory foundations demand it. I agree that Type 42 contains nothing interesting to 99.9% of people. I just teach that types are sets and their terms are elements, and that props are theorem statements and their terms are proofs. The fact that Prop has type Type is something that I've always found misleading and I don't think it has any mathematical meaning (it does allow our definition of subset to work but I regard this as an implementation detail). My understanding is that this is not true in Isabelle, which is a perfectly good system for doing a lot of mathematics.

[Luigi Massacci]

Also, as for the difference between Prop and Bool, Lean is by default based on intuitionistic type theory, so Propisn't necessarily like Bool (note that this doesn't mean that there are propositions that are neither true nor false, but rather that you might not be able to tell which one it is, which is not the same). The moment you add classical axioms, Prop indeed collapses to being perfectly equivalent to Bool, but as @Julian Berman said it makes sense to keep them separate conceptually (so that for example when compiling programs you know you can forget about anything in Prop, as it's only going to contain specifications and proofs about your functions, but not actual data).

And as Kevin said there's a lot of arbitrariness built into the details. You want to avoid the usual paradoxes (Russel, etc), and there's various approaches one can take. Lean doesn't always take the most conceptually elegant, though it often does take the simplest and most practical (after all doing type theory itself is not the main goal)

[Kenny Lau]

@Sam for one outcome of "lumping together" Prop and Type, consider the two operations below:

1. If p and q are propositions, then f : p -> q is a mysterious blackbox that says, "if you feed to me a proof of p (i.e. a term of type p, i.e. h : p), then I will output to you a proof of q (i.e. f h : q)
2. If A and B are sets (i.e. A, B : Type), then f : A -> B is a mysterious blackbox that says, "if you give me an element of A (x : A), then I will give you an element of B (f x : B).

In type theory, these two operations are the same thing, i.e. when you lump Prop with Type, you also get that implications are the same as functions.

[Kenny Lau]

as for the difference between Prop and Bool, it's actually two additional axioms (this is only a technical detail, most mathematicians don't really care about this) that you need in order to prove that every proposition is either equal to true or equal to false.

1. The first axiom is propext {a b : Prop} : (a ↔ b) → a = b, in words, if two propositions are logically equivalent, then they are equal. Without this, you cannot actually prove that the proposition 0 = 0 is equal to the proposition 1 = 1.
2. The second axiom is Classical.em (p : Prop) : p ∨ ¬p (technically, this is not the axiom itself, but for our purposes here let's pretend that it is); in words, this means that a proposition is either true or false. With this extra axiom, then you can prove that a proposition p is either = True or = False.

[Kevin Buzzard]

In my mind the biggest difference between Prop and Bool is that Bool is a type (so contains terms) and Prop is a universe (so contains types). They're at different levels of the hierarchy.

[Philippe Duchon]

This discussion just led me to understand that I had so far misunderstood the meaning of propositional extentiality, confusing it with proof irrelevance.

Propositional extentiality seems to say that any two equivalent propositions are actually equal, while proof irrelevance (and I don't know it Lean sees this as an axiom, or if it's somehow built into the definition of what Prop is) says that any two proofs of the same proposition are the same - so one is at the level of expressions of type Prop, while the other is at the level below of terms of some type which has type Prop.

Now, shouldn't this in turn imply that any two proofs of any two propositions are actually the same? if p is a term of type P and Q is another proposition provably equivalent to P (but from proofs of both P and Q is is easy to prove P ↔ Q), then shouldn't one be able to prove p : Q ? (I tried it and Lean doesn't let me state the equality p=q from hypotheses (P Q : Prop), p : P and q : Q, complaining that q doesn't have the right type - something I was comfortable with until I just re-read what "propositional extentionality" is about.

So, I'm even more confused than I already was.

[Aaron Liu]

Philippe Duchon said:

(I tried it and Lean doesn't let me state the equality p=q from hypotheses (P Q : Prop), p : P and q : Q, complaining that q doesn't have the right type - something I was comfortable with until I just re-read what "propositional extentionality" is about.

You do get docs#proof_irrel_heq, which does need a different kind of equality to make it type correct.

[Kevin Buzzard]

Yeah if you believe that there are only two propositions, the true one and the false one, then you believe that there is only one proof, namely the trivial proof. So where did all the work go? The work went into deciding whether your favourite proposition was the true one or the false one. That's where all the mathematical content moves to in this logical interpretation of mathematics.

[Kevin Buzzard]

Lean's model of mathematics forgets a proof once it's checked it, so it's no different to a tick in a box once it's been processed, ie no different to the trivial proof of the true statement. This is only a model of mathematics and it's very different to the one I was brought up with but it's basically still all the same stuff, just with different labels.

[Edward van de Meent]

indeed, the effort is in convincing lean that trivial : FLT typechecks :upside_down:

[Kevin Buzzard]

Right, that only type checks after you've found the hard maths proof, which then enables you to deduce FLT = True, which enables you to do the rewrite to make the trivial proof typecheck.

[Riccardo Brasca]

Philippe Duchon said:

Now, shouldn't this in turn imply that any two proofs of any two propositions are actually the same? if p is a term of type P and Q is another proposition provably equivalent to P (but from proofs of both P and Q is is easy to prove P ↔ Q), then shouldn't one be able to prove p : Q ? (I tried it and Lean doesn't let me state the equality p=q from hypotheses (P Q : Prop), p : P and q : Q, complaining that q doesn't have the right type - something I was comfortable with until I just re-read what "propositional extentionality" is about.

So, I'm even more confused than I already was.

One way of thinking about this is to stop thinking that A = B means "A and B are absolutely the same thing, everywhere A works we can put B". Equality is just a "normal" relation, defined in Lean, without no fundamental properties (of course it happens to have strong property, but for the system it is nothing special). Instead of saying A=B say A and B are similar, and everything becomes more clear. In particular, if at: A and B is another type that is similar to A it is not enough to conclude that t : B. The relation that allows this (being "absolutely the same thing") is what is called definitional equality, and it's not really a mathematical notion: think about it as "A and B are defined pressing the same keys on the keyboard" (the situation is more complicated, but it is similar).

[Philippe Duchon]

I'm not sure I understand much better, but at least I think I have a better mental picture. Thanks!

(Still, coming from bijective combinatorics, I have a hard time accepting the idea that, once you have a proof of a theorem, it litterally becomes trivial and there is no point in looking for a second proof.)

[Kenny Lau]

@Philippe Duchon it’s probably irrelevant, but for stating equality of terms of different types, you use heq instead of eq.

and no, in that context you cannot even state p : Q, it will just not typecheck

[Riccardo Brasca]

Philippe Duchon said:

I'm not sure I understand much better, but at least I think I have a better mental picture. Thanks!

(Still, coming from bijective combinatorics, I have a hard time accepting the idea that, once you have a proof of a theorem, it litterally becomes trivial and there is no point in looking for a second proof.)

It's not pointless, it is of course interesting and a human may find the new proof much better. Lean on the other hand only cares about whether a theorem is provable, and this clearly does not depend on the proof. Note that I love formalization, but mathematics is more than using a proof assistant.

[Edward van de Meent]

Indeed my mention of trivial : FLT type checking was mostly tongue in cheek. you can do something like it, it gives a bit of intuition of how types behave, but it would look not quite the same

[Kenny Lau]

Philippe Duchon said:

(Still, coming from bijective combinatorics, I have a hard time accepting the idea that, once you have a proof of a theorem, it litterally becomes trivial and there is no point in looking for a second proof.)

You shouldn't equate pragmatical/practical formalization decisions with "how" mathematics "should" be done

[Sam]

Thanks everyone for such detailed answers; this is all very helpful and enlightening! I've been playing around with some of the things mentioned above such as

example : (0 = 0) = (1 = 1) := by decide -- this type checks!

and I think I have a clearer grasp of what Prop is now.

Edward van de Meent said:

indeed, the effort is in convincing lean that trivial : FLT typechecks :upside_down:

How would one pull the "as long as some proof exists it typechecks" off in Lean? Something like

def FLT := 1 + 1 = 3 -- a 'simpler' version of FLT :)
def flt_proof : FLT := sorry -- my proof is too long for zulip chat :(
example : FLT := trivial
/--
type mismatch
  trivial
has type
  True : Prop
but is expected to have type
  FLT : Prop
-/

[Aaron Liu]

def FLT := 1 + 1 = 3 -- a 'simpler' version of FLT :)
def flt_proof : FLT := sorry -- my proof is too long for zulip chat :(
theorem flt_eq_true : FLT = True := eq_true flt_proof
example : FLT := flt_eq_true ▸ trivial
example : FLT := flt_eq_true.mpr trivial
example : FLT := cast flt_eq_true.symm trivial

[Kenny Lau]

def FLT := 1 + 1 = 3 -- a 'simpler' version of FLT :)
def flt_proof : FLT := sorry -- my proof is too long for zulip chat :(
theorem flt_eq_true : FLT = True := propext ⟨fun _ => trivial, fun _ => flt_proof⟩
example : FLT := flt_eq_true ▸ trivial

I've made the connection to propext more explicit

[Kenny Lau]

@Sam for another analogy, it is known that Lean is consistent with the addition of the following axiom:

import Mathlib

axiom iForgotTheName : α ≃ β → α = β

i.e. two types are equal if they have the same cardinality. Under this axiom, it would make Nat = Int provable. So as of now, without this axiom, the proposition Nat = Int is actually undecidable.

[Aaron Liu]

I think that's some version of univalence without the computation since all equalities are equal

[Sam]

Kenny Lau said:

Under this axiom, it would make Nat = Int provable. So as of now, without this axiom, the proposition Nat = Int is actually undecidable.

But mathematically the two sets $\N$ and $\Z$ aren't equal - so why would this be desirable (or even "correct")?; Am I missing some fine distinction between what = means in lean and what = means in math?

[Kenny Lau]

Sam said:

Am I missing some fine distinction between what = means in lean and what = means in math?

Yes, this is the point @Riccardo Brasca and I are trying to make. It's better to think of = in Lean to mean "similar".

The mathematical analogy breaks down here because in maths, "sets" are always subset of a larger "universe", but in Lean, each type is its own universe. There's nothing outside Nat, because Nat is everything that there is, from the perspective of terms of Nat.

[Kenny Lau]

What = means in Lean is more a syntactical thing. = is there for you to rewrite things with.

[Kenny Lau]

the identity x + y = y + x mean that in any expression containing x + y, you can rewrite it using y + x.

[Kenny Lau]

After you proved that x + y = y + x, they're still only "weakly equal", in that the proof is still not rfl!

[Kenny Lau]

example : 0 = 0 := rfl
example : 0 = 1 := rfl -- fails of course
example (m n : Nat) : m + n = n + m := Nat.add_comm m n
example (m n : Nat) : m + n = n + m := rfl -- fails!!

[Kenny Lau]

Try to fit this example into your mental model of equality.

[Riccardo Brasca]

This is maybe a little too much. When doing maths equality has the usual meaning, and you can substitute everywhere. But "having type A" is not a mathematical property (is not a Prop), so you cannot substitute equal things

[Kenny Lau]

propositions are also not mathematical objects (in the usual formulation)

[Kenny Lau]

so you can't even say that two propositions are equal

[Riccardo Brasca]

There are quirks (called dependent type hell), but you ignore those at the beginning.

[Riccardo Brasca]

Kenny Lau said:

so you can't even say that two propositions are equal

Yes, exactly. When you start doing stuff like that you stopped doing maths and type theory becomes much more relevant (same for equality of proofs)

[Kenny Lau]

Another good example for building your mental model is provable subsingletons vs. actual subsingletons (sorry I'll elaborate on this later)

[Riccardo Brasca]

My suggestion of thinking equality as being similar was only in the case you want to understand the details. If your goal is doing math in the usual sense just ignore all this stuff.

[suhr]

When I'm teaching lean I don't teach the existence of these universes, they're basically only there because the type theory foundations demand it.

It's not special to type theory though. You have a distinction between sets and proper classes in set theory too, and you can have more levels as well.

[Philippe Duchon]

This is pretty interesting (and yes, I was also joking when I wrote that looking for a new proof of something was pointless).

If I may ask - what's the reason for having propext as an axiom? I get the point for proof irrelevance (since proofs of the same proposition are equal, they cannot carry information and you cannot "hide" something in the proof), but I don't see how this one can be useful. I suppose it's a type-theoretic reason that I won't be able to understand though.

[Aaron Liu]

You get docs#Quotient.exact as a consequence

[Philippe Duchon]

OK, that's convincing enough.

[James E Hanson]

Kevin Buzzard said:

The fact that Prop has type Type is something that I've always found misleading and I don't think it has any mathematical meaning (it does allow our definition of subset to work but I regard this as an implementation detail).

What exactly would constitute 'mathematical meaning' in this context in your mind? Classically, the fact that Prop has type Type is essentially the easy but I would argue still important fact that $2$ is smaller than the first inaccessible cardinal.

[Kevin Buzzard]

Sam said:

But mathematically the two sets $\N$ and $\Z$ aren't equal - so why would this be desirable (or even "correct")?; Am I missing some fine distinction between what = means in lean and what = means in math?

Are you absolutely sure about this? What is the definition of the set of naturals? And what is the definition of the set of integers? Obviously it is not mathematically meaningful to ask if those two sets happen to be equal. But from a foundational set-theoretic viewpoint it is meaningful. Did you really ever check that it's not true that they're equal? Can you see that this is not a mathematical question, it is an irrelevant question about the underlying wiring? Why then are you not happy to accept the idea that whether FLT is equal to 2+2=4 is also a mathematically irrelevant question and that its answer just depends on the wiring of the foundations?

To a mathematician, equality of terms is meaningful but equality of types and props and proofs is not mathematics, this is all about how mathematics is encoded in your foundational system. I would encourage you to examine your confident claim that the naturals and the integers were definitely not equal in set theory.

[Kevin Buzzard]

I would say that equality of terms has the same meaning in lean as it does in regular mathematics but equality of Props is not a mathematically meaningful question and that Lean's opinion on the matter should not be taken too seriously. If you asked a mathematician whether two props were equal they would probably complain that the question is meaningless. The only reason that lean attaches a meaning to it is that this is the very nature of a foundational system -- it enables you to ask weird questions and then the answers will not shed any light into mathematics.

[Kenny Lau]

@Sam (in the same vein), here's a fun "mathematical" fact: the ordered pair (0, 1) is actually equal to the set {1, 2} in ZFC set theory!

[Philippe Duchon]

Do the sets of naturals and integers even each have a single, agreed-upon definition in set theory? I mean, any number of different "definitions" could be used (including some where the two sets are defined the same way, provided one doesn't expect "the 12 of naturals" to be the same element as "the 12 of integers - for arbitrary values of 12, of course). So the question is meaningful from a set-theoretic point of view, but the answer depends on the definitions used.

(I mean, I vaguely recall from my courses some years ago, some "definition" of the naturals from the ZFC axioms, and then the integers could be defined as equivalence classes of pairs of naturals; but surely there are other possibilities)

[Aaron Liu]

That's the whole point - whether $(0, 1) = \{1, 2\}$ depends on your specific encoding of natural numbers and ordered pairs, and so isn't a meaningful question because you can just as well choose a different encoding and everything works out the same.

[Kyle Miller]

Philippe Duchon said:

Do the sets of naturals and integers even each have a single, agreed-upon definition in set theory?

I think this is more-or-less Kevin's point, that the encoding can vary and the exact encoding doesn't have mathematical meaning.

For example, one could construct the integers by starting from the naturals and using the even naturals for the non-negative integers and the odd naturals for the negative integers. (This is inconvenient though if you want the natural function Nat -> Int to correspond to subset-of, but that's convenience rather than necessity.)

[James E Hanson]

Kevin Buzzard said:

Did you really ever check that it's not true that they're equal?

For the record this is actually pretty easy to see using any of the standard quotient constructions of $\mathbb{Z}$ in two different ways: (1) A quotient is always a set of disjoint sets. (2) Every element of $\omega$ is finite but a typical quotient construction of $\mathbb{Z}$ will involve infinite equivalence classes.

[suhr]

For things like whether Nat = Int there's a weak counterpoint though, one could interpret equality in structural way, like HoTT does. Aka "meaning as use".

But it's not a very useful interpretation, since sets/types by themself have very little structure. They are only meaningful together with operations on them, which make them different.

[Kenny Lau]

for more "wiring", consider the following purely set theoretical question: given an injection f : A -> B, construct a set X containing A, and a bijection g : X -> B that restricts to f on A.

it's "trivial" that such a set X exists, but actually constructing it in terms of set theory will take some thought.

[Kevin Buzzard]

James E Hanson said:

Kevin Buzzard said:

Did you really ever check that it's not true that they're equal?

For the record this is actually pretty easy to see using any of the standard quotient constructions of $\mathbb{Z}$ in two different ways: (1) A quotient is always a set of disjoint sets. (2) Every element of $\omega$ is finite but a typical quotient construction of $\mathbb{Z}$ will involve infinite equivalence classes.

I totally agree modulo I would argue that according to Wikipedia there are no fewer than three "standard" constructions of ordered pairs in set theory. However my point is that once you actually do this calculation you also realise that what you are doing is not mathematics, but wiring.

[James E Hanson]

Kevin Buzzard said:

James E Hanson said:

Kevin Buzzard said:

Did you really ever check that it's not true that they're equal?

For the record this is actually pretty easy to see using any of the standard quotient constructions of $\mathbb{Z}$ in two different ways: (1) A quotient is always a set of disjoint sets. (2) Every element of $\omega$ is finite but a typical quotient construction of $\mathbb{Z}$ will involve infinite equivalence classes.

I totally agree modulo I would argue that according to Wikipedia there are no fewer than three "standard" constructions of ordered pairs in set theory. However my point is that once you actually do this calculation you also realise that what you are doing is not mathematics, but wiring.

Firstly, neither of the arguments I gave depend on the choice of coding of ordered pairs, so I don't really see why you're bringing up the fact that Wikipedia contains an encyclopedic account of various set-theoretic definitions of ordered pairs that have been proposed. (Personally, if I were trying to judge what the modern 'standard' version of a construction was, I'd look in a textbook, not on Wikipedia.) My hedging had more to do with the rare cases where you do actually literally code the integers as natural numbers (such as when working in $\mathsf{PA}$).

Secondly, Professor Buzzard, with all due respect, I find the way you talk about this stuff toxic. You're sliding between a reasonable point (i.e., foundational implementation details don't matter for end-user mathematicians as long as they work) and a really ugly attitude (i.e., foundational implementation details are not mathematics). The only conclusion I can really draw from comments like this is that on some level you actually do think that people like me are not mathematicians.

[Kevin Buzzard]

James I'm sorry I'm upsetting you again; I am simply saying that the question "does the naturals equal the integers" in set theory depends on specific wiring and is not self-evident as the original poster seemed to be claiming. You have given a rigorous proof that they are not equal in the standard encoding and someone else has pointed out a nonstandard encoding where they are equal. I think that we're all clear that the point is now made.

[James E Hanson]

@Kevin Buzzard Why did you bring up the definitions of ordered pairs listed on Wikipedia? What rhetorical purpose did it serve in this conversation? You said

I totally agree modulo I would argue that according to Wikipedia there are no fewer than three "standard" constructions of ordered pairs in set theory.

but how does that addendum actually modify my point? I said 'any of the standard quotient constructions' not 'the standard quotient construction.'

[James E Hanson]

You're apologetic now, but my objection isn't to how you talk when you're being apologetic; it's to how you talk when you're being dismissive.

[Kevin Buzzard]

The observation demonstrates the point that there is not even a "canonical" set representing $\Z$ because there is not a "canonical" way to implement ordered pairs within set theory. I think that this conversation demonstrates really well that the question "does $\mathbb{N}=\mathbb{Z}$?" is really a much stranger question than one might naively imagine in set theory, which I think is at least some evidence as to why it might also be a strange question in type theory.

[Kevin Buzzard]

And in fact in Lean's type theory, ℕ = ℤ is independent of the axioms.

[Kevin Buzzard]

But when a mathematician comes here and says "how can this be a weird question in type theory, it's clearly false in set theory" we're seeing above that the actual answer is "well actually it can be proved to be false under some of the usual assumptions in set theory but actually the proof is pretty weird and not at all what we would expect", we expect a proof of the form "-1 is an integer but not a natural" but your proof is nothing of the sort.

[James E Hanson]

It's actually quite funny that you would bring up definitions of ordered pairs given the fact that just a few days ago I wrote a MathOverflow answer in which I argued that things like set-theoretic codings of ordered pairs have more mathematical content than people seem to think.

[Riccardo Brasca]

I think that the main point here is that ℕ = ℤ is more subtle than what most people think, and probably 90% of mathematician don't care about the real meaning. But let me stress that this is not because it is bad mathematics, just because it is very specific: I am sure that 90% of mathematicians don't care about $p$-adic modular forms either, but Lean makes it very simple to play with ℕ = ℤ and (unfortunately...) very difficult to play with modular forms. So the point is: if you never cared before you probably should not care now that you use Lean.

Having said that, I think that there has been a confusion because someone else mentioned pairs and @James E Hanson explained why ℕ ≠ ℤ in usual constructions in set theory more or less at the same moment (online communication is always a mess...).

[Kenny Lau]

James E Hanson said:

It's actually quite funny that you would bring up definitions of ordered pairs given the fact that just a few days ago I wrote a MathOverflow answer in which I argued that things like set-theoretic codings of ordered pairs have more mathematical content than people seem to think.

that's an interesting read. actually just yesterday I was privately talking about the other way in the context of algebraic geometry: if K is an algebraically closed field, then the unordered pair {x, y} can be encoded as the ordred pair (x+y, xy)!

[James E Hanson]

Kenny Lau said:

James E Hanson said:

It's actually quite funny that you would bring up definitions of ordered pairs given the fact that just a few days ago I wrote a MathOverflow answer in which I argued that things like set-theoretic codings of ordered pairs have more mathematical content than people seem to think.

that's an interesting read. actually just yesterday I was privately talking about the other way in the context of algebraic geometry: if K is an algebraically closed field, then the unordered pair {x, y} can be encoded as the ordred pair (x+y, xy)!

Thank you. Issues like this show up in model theory a fair amount, actually. They have to do with 'elimination of imaginaries,' which is basically about when you have definable injections from quotient sorts into non-quotient sorts.

[Sam]

Kevin Buzzard said:

we expect a proof of the form "-1 is an integer but not a natural" but your proof is nothing of the sort.

Right, when I wrote my statement above I was mainly thinking $-1 \notin \Z$ or $\N \subsetneq \Z$. Thanks for the above proofs and additional context!

[Luigi Massacci]

$-1 \notin \N$ is really a proof that they are not isomorphic as semi-rings, which you can formalize in lean virtually identically as on paper