3 ms·

> Many people are seriously bothered by definitions such as (x,y)={{x},{x,y}} I am bothered by the fact that most mathematicians aren’t bothered by that! Am I

> Many people are seriously bothered by definitions such as (x,y)={{x},{x,y}} I am bothered by the fact that most mathematicians aren’t bothered by that! Am I missing something? Would love to understand why like, system F isn’t the foundation of math (i should care about)

AlexSW 3y ago
Why should one be bothered by it?
- hackandthink 3y ago
  It makes a simple thing (pair) complicated. This may be true for Category Theory as well (Product of two objects): https://en.wikipedia.org/wiki/Product_(category_theory) https://en.wikipedia.org/wiki/Product_(category_theory) But Category Theory captures the essence of Products/Pairs, so I am more inclined to accept it.
  - reuben364 3y ago
    Yes it captures the essence, but if you have a category of ZF sets you still need to demonstrate that a product exists. This is just a possible product (along with its projections).
  - Sharlin 3y ago
    > It makes a simple thing (pair) complicated. Well, yeah, but {x, y} is also a pair. How is (x, y) different? It's ordered, you say? All right, an ordering is a relation that's antisymmetric and so on, but in this case let's say we have a function that maps x to 0 and y to 1… But what is a function? Okay, a function is a type of relation, so let's define a relation first: a set of ordered pairs… oops. The real problem with defining (x, y) = {{x}, {x, y}} is that elements of a set must also be elements of some universal set 𝓤, {x, y} ⊂ 𝓤, but as we know, there is infamously not such a thing as a "set of all things". Sets have to be typed. But in a pair, x and y can be of entirely different kinds of entities.
- VirusNewbie 3y ago
  It seems to be ignoring β-reduction for one. But an ordered set is fundamentally different than an unordered set as well!
howling 3y ago
System F just isn't flexible enough to encode most of mathematics. You need at the minimum dependent type and preferably a more flexible identity type to avoid setoid hell. The closest attempts I know of are HOTT in Coq and Cubical Agda. These systems still have a lot of kinks to be sorted out though, e.g. https://www.youtube.com/watch?v=TpUOweB2kHU https://www.youtube.com/watch?v=TpUOweB2kHU
vouaobrasil 3y ago
I've never seen anyone bothered by such a definition. It's a good definition that shows that you can construct ordered tuples in set theory without the need for a new primitive notion, and then you can promptly forget it.
consilient 3y ago
> I am bothered by the fact that most mathematicians aren’t bothered by that! Am I missing something? Outside of logic and set theory, most mathematicians aren't really working in any particular foundation: they're working directly with the relevant structures. An ordered pair `(x,y)` can be modeled as the set `{{x},{x,y}}`, but that doesn't mean it is that set. What it is, to the extent the question is even coherent, is a thing that has the data ordered pairs are supposed to have: a first element, and a second element.

AlexSW 3y ago

Why should one be bothered by it?

hackandthink 3y ago
It makes a simple thing (pair) complicated. This may be true for Category Theory as well (Product of two objects): https://en.wikipedia.org/wiki/Product_(category_theory) https://en.wikipedia.org/wiki/Product_(category_theory) But Category Theory captures the essence of Products/Pairs, so I am more inclined to accept it.
- reuben364 3y ago
  Yes it captures the essence, but if you have a category of ZF sets you still need to demonstrate that a product exists. This is just a possible product (along with its projections).
- Sharlin 3y ago
  > It makes a simple thing (pair) complicated. Well, yeah, but {x, y} is also a pair. How is (x, y) different? It's ordered, you say? All right, an ordering is a relation that's antisymmetric and so on, but in this case let's say we have a function that maps x to 0 and y to 1… But what is a function? Okay, a function is a type of relation, so let's define a relation first: a set of ordered pairs… oops. The real problem with defining (x, y) = {{x}, {x, y}} is that elements of a set must also be elements of some universal set 𝓤, {x, y} ⊂ 𝓤, but as we know, there is infamously not such a thing as a "set of all things". Sets have to be typed. But in a pair, x and y can be of entirely different kinds of entities.
VirusNewbie 3y ago
It seems to be ignoring β-reduction for one. But an ordered set is fundamentally different than an unordered set as well!

howling 3y ago

System F just isn't flexible enough to encode most of mathematics. You need at the minimum dependent type and preferably a more flexible identity type to avoid setoid hell. The closest attempts I know of are HOTT in Coq and Cubical Agda. These systems still have a lot of kinks to be sorted out though, e.g. https://www.youtube.com/watch?v=TpUOweB2kHU https://www.youtube.com/watch?v=TpUOweB2kHU

vouaobrasil 3y ago

I've never seen anyone bothered by such a definition. It's a good definition that shows that you can construct ordered tuples in set theory without the need for a new primitive notion, and then you can promptly forget it.

consilient 3y ago

> I am bothered by the fact that most mathematicians aren’t bothered by that! Am I missing something? Outside of logic and set theory, most mathematicians aren't really working in any particular foundation: they're working directly with the relevant structures. An ordered pair `(x,y)` can be modeled as the set `{{x},{x,y}}`, but that doesn't mean it is that set. What it is, to the extent the question is even coherent, is a thing that has the data ordered pairs are supposed to have: a first element, and a second element.