4 ms·

> In traditional mathematics equality is treated as a relation. Two things are either equal or not. That sounds like the way to go. No (identity) types needed.

kazinator 1y ago
But can you escape from that relation being identifiable as having a type or being a type, even if you don't find it interesting/helpful and don't use it? Also the concept of a proof of equality strikes as relevant, because some equalities are actually incomputable. E.g. suppose you want a an equality type for whether two functions are equivalent (two instances of the same function type).
- auggierose 1y ago
  Don't use types for logic, then you have already escaped. Of course, if you prefer living in a prison, that's up to you. If you want equivalence, use an equivalence relation.
drumnerd 1y ago
In type checking, particularly in dependent types, it is not trivial to check that two types are the same. Different notions of equality are useful in this field. A type can contain a function value inside. How to prove that two functions are the same? Is not enough to prove that for all X f X and g X implies f is g.
- auggierose 1y ago
  Don't use types for logic. It will lead to confused statements like yours.
lmm 1y ago
The problem is that you have model everything in a lossy way to make that work. If you want to say that 2 green apples plus 2 red apples equals 4 apples, you have to just say that you have 2 apples plus 2 apples, and you can't then go back and ask what colour your apples are. Whereas in homotopy type theory you can say a red apple is equivalent to a green apple, and that equivalence is a mathematical object you can manipulate in nice ways, but if you ever need to go back and work with the colour again it's still there.
- auggierose 1y ago
  > 2 green apples plus 2 red apples equals 4 apples What a load of malarkey. This statement is not a problem for traditional mathematics. I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. What is the problem? I can tell you: type theory.
  - lmm 1y ago
    > I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. Well, is your set equal to a set of 3 green apples and 1 red apple, or not? (And actually how can you have multiple green apples in the same set if they're equal?)
    - auggierose 1y ago
      Just because two apples are both green doesn't mean that they are equal. In fact, if there are two apples, that means they are definitely not equal, otherwise there would be just one green apple. No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa). Any more questions?
      - lmm 1y ago
        > Just because two apples are both green doesn't mean that they are equal. In fact, if there are two apples, that means they are definitely not equal, otherwise there would be just one green apple. Well, a green apple had better be equal to itself. So if you've got a green apple and another green apple that isn't equal to the first, you're already in trouble and going to have to resort to hacks like numbering them. > No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa). What if you want to manipulate it in a context where you only care about the number of apples, not their colour?
GolDDranks 1y ago
However, that leaves you without any tools to check whether two things are equal or not, save for trivial, syntactic equality. It's like, in a programming sense equality declared to exist, but not actually defined.
- auggierose 1y ago
  Mathematics is not programming. Not everything that is well-defined needs to be "executable" in a specific sense. That's a feature, not a bug.
drdeca 1y ago
I agree that the law of the excluded middle is true, but it is actually useful in a number of contexts to have equality types, and witnesses for two given terms being equal. Of course, in some contexts when one has those types, it may be better to forget any distinction between different ways a witness to an equality can be produced, leaving identity types with at most one element. Just because the LEM is true doesn’t mean intuitionistic reasoning that avoids the use of the LEM isn’t sometimes useful.
- auggierose 1y ago
  I have no problem with intuitionistic reasoning as a mathematical technique (you don't need types for that). Reasoning is really about inequalities in the first place anyway, not equalities.
colbyn 1y ago
That’s too simplistic because there’s different types of equality. Things can be different but semantically equal in other regards. Equality in elementary algebra is very vague.
- auggierose 1y ago
  You can have different equivalence relations. You can also form quotients with respect to these different relations. Nothing to see here, move on. No need to be vague about anything.
cjfd 1y ago
Both approaches have their advantages and disadvantages. Personally, I am interested in doing proofs on a computer. Type theory does seem the most convenient way to do this. The issue with the equality of proofs is a minor inconvenience in this. Recently I looked a bit into metamath which is (at least in the standard library) a set theory based way of formalizing mathematics. In the end I found that they need to add definitions as axioms. This is okay provided that these axioms satisfy certain conditions. But now they have a standard library where there are hundreds of axioms which is, in my opinion very ugly. I do start to wonder whether one of them is not correctly stated yielding an inconsistent system. There does not seem to be a guard against this in place. The thing is that if one wants to make set theory practical, one probably ends up implementing something close to type theory anyway. The main beauty of type theory is that one gets two for the price of one. There are definitions of functions with typed arguments (e.g., this is a function that takes a function from the natural numbers to the natural numbers), which one probably wants anyway at some point, and dependent types, which are also really nice and suddenly one can do logic as well. In set theory one can ask 'interesting' questions like 'is the trivial group equal to the number five?'. If both are sets the question actually means something, but it actually really doesn't. I would suggest, like I do in another post in this thread, that the problem just disappears if one adds proof irrelevance as an axiom.
- auggierose 1y ago
  > The main beauty of type theory is that one gets two for the price of one. You get what you pay for. > The thing is that if one wants to make set theory practical, one probably ends up implementing something close to type theory anyway. That is wrong. Unless you want to argue that types are pretty close to sets already. Let's just throw away what makes types different from sets, and I am happy with that. Your point is that axioms are scary, and I agree with that. When you use them, you should be aware where they come from, and why they are consistent with each other. In type theory, everything is definitions from the bottom up, but that also restricts your freedom in what you can do. But you can view these definitions just as one source of axioms that you trust, because you trust the type theory. But I argue that it would be just as safe to have two or three or ... sources of axioms, as long as you can argue why you trust the combination of these sources (in fact, every type theory implementation has multiple such sources inside, they just don't advertise that). Ideally that argument is machine-checked, which leads the way to trusted extensions of the prover without sacrificing flexibility.
runeblaze 1y ago
I mean sure we can do ZFC or ZF as the foundation, and I am sure with enough effort we can make metamath or some modern derivative great again. At some point though I like having years of type-directed program synthesis research helping me write proofs; I like type-checking research helping me check my proofs, and I like my proof assistants to work well for verified program extraction if I also happen to write code because the mathematics academic job market is quite shit for your average pure maths PhD, and if I were to do logic then it might be even shittier. Admittedly the above (except program extraction I suppose) can all be achieved with ZFC + a layer of type theory on top, and again that's a reasonable thing to do, but I hope this makes a strong enough case for the type theoretical foundation.
- auggierose 1y ago
  Type theory is definitely the dominant paradigm in current proof assistants, so yes, if you want an easy life, and your head doesn't hurt from unreflected type theory propaganda as witnessed here in this thread, do that. But if you want an easy life, instead of trying to do what is right, why did you do math in the first place?
  - runeblaze 1y ago
    ZF(w or w/o C)/type theory/other foundations of maths are "equally" right? My argument is that even if we are trying to build PAs from scratch, type theory provides tangible benefits to the working mathematician because we can just borrow CS research in many stuffs like proof checking and synthesis. Of course that is a benefit in the "meta" level, but it is not like ZFC is a better foundation than topoi/types/etc..
    - auggierose 1y ago
      There is nothing wrong with learning from CS research, but mathematicians are just better at thinking about mathematics than computer scientists are. Would you think in types if you didn't have to do it on a computer in a system designed by computer scientists? No way. Would you think in ZFC? Not really, either. We are now in a moment that might decide for the foreseeable future how we think about math, and we better get it right.

kazinator 1y ago

But can you escape from that relation being identifiable as having a type or being a type, even if you don't find it interesting/helpful and don't use it? Also the concept of a proof of equality strikes as relevant, because some equalities are actually incomputable. E.g. suppose you want a an equality type for whether two functions are equivalent (two instances of the same function type).

auggierose 1y ago
Don't use types for logic, then you have already escaped. Of course, if you prefer living in a prison, that's up to you. If you want equivalence, use an equivalence relation.

drumnerd 1y ago

In type checking, particularly in dependent types, it is not trivial to check that two types are the same. Different notions of equality are useful in this field. A type can contain a function value inside. How to prove that two functions are the same? Is not enough to prove that for all X f X and g X implies f is g.

auggierose 1y ago
Don't use types for logic. It will lead to confused statements like yours.

lmm 1y ago

The problem is that you have model everything in a lossy way to make that work. If you want to say that 2 green apples plus 2 red apples equals 4 apples, you have to just say that you have 2 apples plus 2 apples, and you can't then go back and ask what colour your apples are. Whereas in homotopy type theory you can say a red apple is equivalent to a green apple, and that equivalence is a mathematical object you can manipulate in nice ways, but if you ever need to go back and work with the colour again it's still there.

auggierose 1y ago
> 2 green apples plus 2 red apples equals 4 apples What a load of malarkey. This statement is not a problem for traditional mathematics. I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. What is the problem? I can tell you: type theory.
- lmm 1y ago
  > I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. Well, is your set equal to a set of 3 green apples and 1 red apple, or not? (And actually how can you have multiple green apples in the same set if they're equal?)
  - auggierose 1y ago
    Just because two apples are both green doesn't mean that they are equal. In fact, if there are two apples, that means they are definitely not equal, otherwise there would be just one green apple. No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa). Any more questions?
    - lmm 1y ago
      > Just because two apples are both green doesn't mean that they are equal. In fact, if there are two apples, that means they are definitely not equal, otherwise there would be just one green apple. Well, a green apple had better be equal to itself. So if you've got a green apple and another green apple that isn't equal to the first, you're already in trouble and going to have to resort to hacks like numbering them. > No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa). What if you want to manipulate it in a context where you only care about the number of apples, not their colour?

GolDDranks 1y ago

However, that leaves you without any tools to check whether two things are equal or not, save for trivial, syntactic equality. It's like, in a programming sense equality declared to exist, but not actually defined.

auggierose 1y ago
Mathematics is not programming. Not everything that is well-defined needs to be "executable" in a specific sense. That's a feature, not a bug.

drdeca 1y ago

I agree that the law of the excluded middle is true, but it is actually useful in a number of contexts to have equality types, and witnesses for two given terms being equal. Of course, in some contexts when one has those types, it may be better to forget any distinction between different ways a witness to an equality can be produced, leaving identity types with at most one element. Just because the LEM is true doesn’t mean intuitionistic reasoning that avoids the use of the LEM isn’t sometimes useful.

auggierose 1y ago
I have no problem with intuitionistic reasoning as a mathematical technique (you don't need types for that). Reasoning is really about inequalities in the first place anyway, not equalities.

colbyn 1y ago

That’s too simplistic because there’s different types of equality. Things can be different but semantically equal in other regards. Equality in elementary algebra is very vague.

auggierose 1y ago
You can have different equivalence relations. You can also form quotients with respect to these different relations. Nothing to see here, move on. No need to be vague about anything.

cjfd 1y ago

Both approaches have their advantages and disadvantages. Personally, I am interested in doing proofs on a computer. Type theory does seem the most convenient way to do this. The issue with the equality of proofs is a minor inconvenience in this. Recently I looked a bit into metamath which is (at least in the standard library) a set theory based way of formalizing mathematics. In the end I found that they need to add definitions as axioms. This is okay provided that these axioms satisfy certain conditions. But now they have a standard library where there are hundreds of axioms which is, in my opinion very ugly. I do start to wonder whether one of them is not correctly stated yielding an inconsistent system. There does not seem to be a guard against this in place. The thing is that if one wants to make set theory practical, one probably ends up implementing something close to type theory anyway. The main beauty of type theory is that one gets two for the price of one. There are definitions of functions with typed arguments (e.g., this is a function that takes a function from the natural numbers to the natural numbers), which one probably wants anyway at some point, and dependent types, which are also really nice and suddenly one can do logic as well. In set theory one can ask 'interesting' questions like 'is the trivial group equal to the number five?'. If both are sets the question actually means something, but it actually really doesn't. I would suggest, like I do in another post in this thread, that the problem just disappears if one adds proof irrelevance as an axiom.

auggierose 1y ago
> The main beauty of type theory is that one gets two for the price of one. You get what you pay for. > The thing is that if one wants to make set theory practical, one probably ends up implementing something close to type theory anyway. That is wrong. Unless you want to argue that types are pretty close to sets already. Let's just throw away what makes types different from sets, and I am happy with that. Your point is that axioms are scary, and I agree with that. When you use them, you should be aware where they come from, and why they are consistent with each other. In type theory, everything is definitions from the bottom up, but that also restricts your freedom in what you can do. But you can view these definitions just as one source of axioms that you trust, because you trust the type theory. But I argue that it would be just as safe to have two or three or ... sources of axioms, as long as you can argue why you trust the combination of these sources (in fact, every type theory implementation has multiple such sources inside, they just don't advertise that). Ideally that argument is machine-checked, which leads the way to trusted extensions of the prover without sacrificing flexibility.

runeblaze 1y ago

I mean sure we can do ZFC or ZF as the foundation, and I am sure with enough effort we can make metamath or some modern derivative great again. At some point though I like having years of type-directed program synthesis research helping me write proofs; I like type-checking research helping me check my proofs, and I like my proof assistants to work well for verified program extraction if I also happen to write code because the mathematics academic job market is quite shit for your average pure maths PhD, and if I were to do logic then it might be even shittier. Admittedly the above (except program extraction I suppose) can all be achieved with ZFC + a layer of type theory on top, and again that's a reasonable thing to do, but I hope this makes a strong enough case for the type theoretical foundation.

auggierose 1y ago
Type theory is definitely the dominant paradigm in current proof assistants, so yes, if you want an easy life, and your head doesn't hurt from unreflected type theory propaganda as witnessed here in this thread, do that. But if you want an easy life, instead of trying to do what is right, why did you do math in the first place?
- runeblaze 1y ago
  ZF(w or w/o C)/type theory/other foundations of maths are "equally" right? My argument is that even if we are trying to build PAs from scratch, type theory provides tangible benefits to the working mathematician because we can just borrow CS research in many stuffs like proof checking and synthesis. Of course that is a benefit in the "meta" level, but it is not like ZFC is a better foundation than topoi/types/etc..
  - auggierose 1y ago
    There is nothing wrong with learning from CS research, but mathematicians are just better at thinking about mathematics than computer scientists are. Would you think in types if you didn't have to do it on a computer in a system designed by computer scientists? No way. Would you think in ZFC? Not really, either. We are now in a moment that might decide for the foreseeable future how we think about math, and we better get it right.