4 ms·

Both approaches have their advantages and disadvantages. Personally, I am interested in doing proofs on a computer. Type theory does seem the most convenient wa

by 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.
- cjfd 1y ago
  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 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.
  - auggierose 1y ago
    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 http://abstractionlogic.com .

by cjfd 1y ago

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.

cjfd 1y ago
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 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.
- auggierose 1y ago
  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 http://abstractionlogic.com .