3 ms·

> 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 pra

> 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 .

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 .