I would suggest just adding proof irrelevance as an axiom to the theory. This also makes subtypes more convenient. I.e., if one has a set S and a property P: S -> Prop, the subset of S where the property is satisfied, in coq notation,
{ s: S, P s },
has with proof irrelevance automatically as many elements as there are elements in S that satisfy P. Without proof irrelevance one often finds oneself proving proof irrelevance for specific propositions that are needed for subtypes or even changing the definition of P such that proof irrelevance becomes provable.
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.
> Does two equal two? What if the first one is written in a larger font?
Exactly. Obviously they're different, but they're equivalent for most purposes. In traditional mathematics you have to handle this in a very awkward way: you have to say there's some kind of platonic ideal of two, and then writing two in one font or another forms a model of this platonic ideal of two. Then you can work with the platonic ideal of two, and add two and two and get four - but you've already forgotten which font you're in. Whereas if you say that twos in one font are equivalent to twos in another font or to some canonical platonic ideal of two, you can lift the fact that two plus two is equal to four back along those equivalences and get a four in the right font. (Or, more commonly, you just ignore that detail and say that you've got something equivalent to four - but you haven't erased the details, they're always there if you need them).
> That is not even wrong. You are mixing up syntax and semantics, and that is because type theorists don't have a concept of semantics.
Right back at you. I don't have to treat notation as something different from semantics, because I'm working in a theory that can handle both elegantly and consistently. Conventional mathematics struggles to describe mathematics as it is actually performed - working mathematicians rely extensively on "abuse of notation", but set-theoretic metamathematics pretends this is out of scope or safe to ignore.
If you say that semantics and syntax are the same, then you don't have semantics. That is not elegant, just confused, and your statements in this thread here are a great example of that.
Does two equal Two? Sometimes it does, sometimes it doesn't. That would depend on your definitions and axioms. I can definitely work with something without knowing all about it. It is called axiomatic reasoning. Some people seem to have a hard time with it.
> 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.
> 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?)
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?
> 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?
> 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.
Nope, no trouble at all. Those troubles only exist in your type-infested mind.
> What if you want to manipulate it in a context where you only care about the number of apples, not their colour?
Then I'll do just that. Lol, you can't make this shit up.
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.
> 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.
Well, I kind of agree with this. Also in type theory there are axioms/assumptions hidden in the implementation. I myself made an implementation of the Calculus of Constructions (https://github.com/chrisd1977/system) with the goal of having a foundation that is as small as possible while it still being practical to prove large parts of mathematics. I do have to say that it turns out the the foundation is a little bit larger than I would have preferred. I am in particular a bit disappointed that I needed to create a type hierarchy. I.e., the most basic sets have type Type(0) which has Type(1) which has type Type(2) and so on. I am also not completely liking some of the axioms that I had to add, in particular regarding to equality.
I kind of like your idea of having trusted extensions to provers. I was myself thinking along the lines of taking the foundation that I got in my Calculus of Constructions project and see if it can be put on a smaller set theory foundation. I.e., prove it in ZFC, presumably with inaccessible cardinals added.
Cool project. I was already shocked that you use C++, and then I thought, 40% assembly language, no way. Turns out Github thinks that your theory files are assembly :-)
Yes, the type universe hierarchy is the canary in the coal mine that something is wrong with type theory as a foundation, but very few take it seriously. Some do though, see for example the first chapter of http://abstractionlogic.com .
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.
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.
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).
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.
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.
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.
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.
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.
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.
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?
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..
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.
idgi tho. The average working mathematician seldomly thinks about proof theory or how proofs "work". Proof theory if must be put in a single box it is an logician's art, and at that point it is niche enough in both CS and maths that it becomes meaningless to say mathematicians know more about it. Logicians are better at thinking about proofs than either maths people or CS people.
I mean I don't know what you mean by right, but given how type theory/ZFC/categorical foundations there is no clear winner (unless you can make a good argument for set theory as our foundation, because again, the average mathematician seldomly thinks in ZFC), I'd say type theory is quite nice in its computational interpretations so let's go with that.
I also don't want to go there, but obviously research drains manpower and money. If we can get CS people to write PAs we really should do that. They're filthy rich in the grand scheme of research.
How proofs work is really simple. The question is, how do you work inside a proof assistant, which kind of math is easy to express, and what is difficult? If you leave that to the CS people, math will become computer science. The ultimate logician was Gödel, and he clearly was a mathematician.
idgi. If you do your 101 logic class often you learn natural deduction, and how do you formalize natural deduction in a computer system? (Hint: type theory is "natural" for this).
How proofs work is pretty simple, and you don't need types to do natural deduction. As usual, types only complicate the picture. Here is a more straightforward and natural way to treat natural deduction: http://abstractionlogic.com .
sure of course one does not need types to do natural deduction… if you throw what you showed me to your average maths undergrad in the US they will get confused — I truly don’t see how proofs are simple
I would suggest just adding proof irrelevance as an axiom to the theory. This also makes subtypes more convenient. I.e., if one has a set S and a property P: S -> Prop, the subset of S where the property is satisfied, in coq notation,
has with proof irrelevance automatically as many elements as there are elements in S that satisfy P. Without proof irrelevance one often finds oneself proving proof irrelevance for specific propositions that are needed for subtypes or even changing the definition of P such that proof irrelevance becomes provable.> 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.
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.
This “apple” thing…is it colored or not?
You can’t start with one definition and then throw in another.
Does two equal two? What if the first one is written in a larger font?
> Does two equal two? What if the first one is written in a larger font?
Exactly. Obviously they're different, but they're equivalent for most purposes. In traditional mathematics you have to handle this in a very awkward way: you have to say there's some kind of platonic ideal of two, and then writing two in one font or another forms a model of this platonic ideal of two. Then you can work with the platonic ideal of two, and add two and two and get four - but you've already forgotten which font you're in. Whereas if you say that twos in one font are equivalent to twos in another font or to some canonical platonic ideal of two, you can lift the fact that two plus two is equal to four back along those equivalences and get a four in the right font. (Or, more commonly, you just ignore that detail and say that you've got something equivalent to four - but you haven't erased the details, they're always there if you need them).
> Obviously they're different, but they're equivalent for most purposes
That is not even wrong. You are mixing up syntax and semantics, and that is because type theorists don't have a concept of semantics.
> That is not even wrong. You are mixing up syntax and semantics, and that is because type theorists don't have a concept of semantics.
Right back at you. I don't have to treat notation as something different from semantics, because I'm working in a theory that can handle both elegantly and consistently. Conventional mathematics struggles to describe mathematics as it is actually performed - working mathematicians rely extensively on "abuse of notation", but set-theoretic metamathematics pretends this is out of scope or safe to ignore.
If you say that semantics and syntax are the same, then you don't have semantics. That is not elegant, just confused, and your statements in this thread here are a great example of that.
Does two equal Two? Sometimes it does, sometimes it doesn't. That would depend on your definitions and axioms. I can definitely work with something without knowing all about it. It is called axiomatic reasoning. Some people seem to have a hard time with it.
> 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.
> 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?)
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?
> 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?
> 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.
Nope, no trouble at all. Those troubles only exist in your type-infested mind.
> What if you want to manipulate it in a context where you only care about the number of apples, not their colour?
Then I'll do just that. Lol, you can't make this shit up.
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.
> 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.
Well, I kind of agree with this. Also in type theory there are axioms/assumptions hidden in the implementation. I myself made an implementation of the Calculus of Constructions (https://github.com/chrisd1977/system) with the goal of having a foundation that is as small as possible while it still being practical to prove large parts of mathematics. I do have to say that it turns out the the foundation is a little bit larger than I would have preferred. I am in particular a bit disappointed that I needed to create a type hierarchy. I.e., the most basic sets have type Type(0) which has Type(1) which has type Type(2) and so on. I am also not completely liking some of the axioms that I had to add, in particular regarding to equality.
I kind of like your idea of having trusted extensions to provers. I was myself thinking along the lines of taking the foundation that I got in my Calculus of Constructions project and see if it can be put on a smaller set theory foundation. I.e., prove it in ZFC, presumably with inaccessible cardinals added.
Cool project. I was already shocked that you use C++, and then I thought, 40% assembly language, no way. Turns out Github thinks that your theory files are assembly :-)
Yes, the type universe hierarchy is the canary in the coal mine that something is wrong with type theory as a foundation, but very few take it seriously. Some do though, see for example the first chapter of http://abstractionlogic.com .
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.
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.
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).
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.
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.
Don't use types for logic. It will lead to confused statements like yours.
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.
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.
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.
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.
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.
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?
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..
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.
idgi tho. The average working mathematician seldomly thinks about proof theory or how proofs "work". Proof theory if must be put in a single box it is an logician's art, and at that point it is niche enough in both CS and maths that it becomes meaningless to say mathematicians know more about it. Logicians are better at thinking about proofs than either maths people or CS people.
I mean I don't know what you mean by right, but given how type theory/ZFC/categorical foundations there is no clear winner (unless you can make a good argument for set theory as our foundation, because again, the average mathematician seldomly thinks in ZFC), I'd say type theory is quite nice in its computational interpretations so let's go with that.
I also don't want to go there, but obviously research drains manpower and money. If we can get CS people to write PAs we really should do that. They're filthy rich in the grand scheme of research.
How proofs work is really simple. The question is, how do you work inside a proof assistant, which kind of math is easy to express, and what is difficult? If you leave that to the CS people, math will become computer science. The ultimate logician was Gödel, and he clearly was a mathematician.
> How proofs work is really simple
idgi. If you do your 101 logic class often you learn natural deduction, and how do you formalize natural deduction in a computer system? (Hint: type theory is "natural" for this).
Also how proofs work is far from simple.
How proofs work is pretty simple, and you don't need types to do natural deduction. As usual, types only complicate the picture. Here is a more straightforward and natural way to treat natural deduction: http://abstractionlogic.com .
sure of course one does not need types to do natural deduction… if you throw what you showed me to your average maths undergrad in the US they will get confused — I truly don’t see how proofs are simple
What do you have to say about Curry-Howard?
Most overrated isomorphism in the history of machine-assisted proof.
Post from yesterday (with very little discussion): https://news.ycombinator.com/item?id=45333548