Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have started something in an entry
which has grown out of the the desires expressed in the thread The Wiki history of the universe.
This is tentative. I should have maybe created this instead on my personal web. I hope we can discuss this a bit. If it leads nowhere and/or if the feeling is that it is awkward for one reason or other, I promise to remove it again. But let’s give this a chance. I feel this is finally beginning to converge to something.
Whoosh, there is a lot that I would change about that, starting with the phrase “the foundations”. Maybe I’ll write my own table and then we can compare them.
Erk, maybe my view of foundations can’t be condensed into such a table. I think of all the words that you’ve used as more like bubbles in a Venn diagram, which intersect but most of them aren’t contained in any other. Also I have many specific objections – structural set theory is not a type theory at all, excluded middle (let alone the axiom of choice) is not generally considered predicative, a “traditional foundation” sounds to me more like ZFC than any large cardinal axioms, etc. Is discussing this really a productive use of time?
Okay, I removed some “the”-s.
Maybe I’ll write my own table
Please do.
and then we can compare them.
I am prepared to discard mine. It’s more a question than an answer. But something roughly of this sort would be nice to make explicit.
Hmm, I’m sorry to have such a negative reaction. I think this caught me at a bad time when I was feeling tired and overworked. It is nice to have a big picture to tell people, but I need to think a little more about how I think it ought to be presented.
Oh, I see #3 only now! I guess we overlapped.
Let me react a bit:
structural set theory is not a type theory at all,
Yeah, I am aware of that. What would be the right term to put there? What’s the set theory that is founded in type theory called? (Hopefully not “setoid theory”!?)
excluded middle (let alone the axiom of choice) is not generally considered predicative
I was wondering whether I should carry that adjective around. That adjective was my way of alluding to the fact that I am talking about setoids there! So it’s related to the above objection. Is there an easy way to resolve it?
a “traditional foundation” sounds to me more like ZFC than any large cardinal axioms,
I was thinking mostly of the axiom of universes, which seems to be very “traditionally” considered. But okay, I have removed that “traditional”. Was just looking for a term there.
Is discussing this really a productive use of time?
To me it’s interesting. Whether its going to be productive will have to be seen, as with many discussions here ;-) From Andrej Bauer’s post and the comments I gather that other people find it intersting, too.
I should maybe tell you my attitude: I am frustrated that I need to be guessing such tables from the little I know about foundations. I am irritated that there is no textbook that explains all this: “Foundations for the working mathematician”. There is so much known, I find it disappointing that so few specialists care to explain the modern view of the origin of the mathematical universe to their mathematical but non-foundational colleagues – or are reluctant to reply if somebody asks… Maybe the big exception is Paul Taylor, who makes a genuine effort, and reading his writing helped me a lot. But I am thinking that there could be more systematic accounts, accounts that give me more “hard facts” than general philosophy.
I’ll write more later, but I think one reason there is no ’foundations for the working mathematician’ is that usually, foundations are irrelevant to the working mathematician. Usually it’s only people who are interested in foundations for it’s own sake who want to know about it, and it’s them that the existing literature is aimed at. (Also, mathematicians generally assume a set theoretic foundation.) This may change with the advent of homotopy type theory, but there there are still so many questions about the theory itself before we can write a coherent exposition.
What do you think about this table?
What do you think about this table?
Thanks!
Let’s see. I have a few questions.
Some entries contain numbers between 1 and 9 instead of crosses. What does this mean? (Maybe my system is not displaying the table correctly? Are these footnotes, maybe? )
the rows “material set theory” and “structural set theory” appear without any entries. Okay, that’s because they are not type theories. But is the table meant to indicate some relation to them nevertheless?
Maybe I have a question about “structural set theory” after all: how about the theory of h-sets in HoTT. Would you call that a structural set theory?
Also “setoids” appears with nothing filled in. Not sure what to make of this. Of course “setoids” is not a type theory. But surely it is of interest that the theory of setoids exist in type theory. But I understand that your table is probably not meant to say this.
first-order logic has nothing in “type formers”. Shouldn’t it have crosses at $\sum$ or at least $\prod$ for quantifiers?
*
foundations are irrelevant to the working mathematician.
I am not sure if this is true.
Recent example is the hype around the abc-conjecture. All around one saw people express awe about Mochizuki’s use of universes and universe enlargement. I think it is clear that working mathematicians find universes by and large mysterious and don’t know how to work with them. The fact that universes are so unmysterious that there are even computer systems who easily do that mysterious “universe enlargement” automatically is an information that might be quite relevant to mathematicians working on such mundane things as the abc-conjecture.
Similar statements hold for axioms of choice etc. Even in just plain basic abelian sheaf cohomology it is good to have a clear idea of what it actually means to have the choice to adopt this axiom. Without that clear idea central fragments of abelian sheaf cohomology are opaque.
Judging from my own experience, the situation may be quite opposite: a clear exposition of foundations would be quite helpful for the mathematical practice, but in the absence of any such people feel that it is as irrelevant to them as they think other theories which they never heard about must be irrelevant to them.
Re 10, I did say usually. (-: I also think there’s a difference between understanding particular “foundational” axioms, like the axiom of choice, and caring about the choice of foundational system, which is often a completely orthogonal thing. E.g. the axiom of choice behaves just about the same whether you build things on set theory or on type theory (unless you choose propositions-as-types).
Re 9, there is a second “sheet” of the spreadsheet which contains the footnotes. Look for the tabs at the bottom.
The entries marked by dashes I put in to indicate that they are not themselves type theories, but are formulated inside of the type theory immediately above them. If you can think of a way to clarify that, that would be great.
Now that you mention it, I guess I would regard the theory of hSets in HoTT as a “structural set theory” in an inclusive sense. When I wrote “structural set theory” I was thinking of theories like ETCS and SEAR that are formulated with axioms in first-order logic, but I would agree that the theory of hSets in HoTT is certainly “a set theory” in the inclusive sense of “a theory about sets” (I would probably say the same about any extensional type theory admitting quotients, including setoids in MLTT), and it’s certainly structural.
Finally, I intentionally meant “type formers” to omit “proposition formers”, so as to be able to distinguish FOL which has lots of “proposition formers” but no formers of non-proposition types.
I see. Sorry for the stupidity with the footnotes.
The entries marked by dashes I put in to indicate that they are not themselves type theories, but are formulated inside of the type theory immediately above them. If you can think of a way to clarify that, that would be great.
Well, that’s going in the direction that I had amplified in my attempt: to show the hierarchy of systems that one gets by assuming one and then building on that. I’d like to see that idea combined with what you have.
Some thoughts on that:
You could streamline the “Type formers” column by collapsing the first 8 subcolumns to $\to$, $\prod$ and $Ind$ (which implies all the rest). That would help amplify the hierarchy here, which goes
no type formers
add function types
refine to dependent product
Can’t we in this vein put classical set theory in context, too, after all?
Just give me a sanity check on the following: it is possible to write out the ZF axioms in the FOL inside Coq, isn’t it?
I guess I would regard the theory of hSets in HoTT as a “structural set theory”
Great. I have tuned my table a bit more.
I guess what I’m saying is that I don’t see it as a ’hierarchy’ in the sense that your list suggests. There are two steps: you choose an ambient type theory, then you maybe formulate some axioms therein. You could choose to ’build your type theory up in stages’ by adding one type forming rule at a time, but there’s no distinguished ’order’ in which you must do that, so I think my table layout describes better the relationship between all the type theories.
Maybe, although there are type theories that have some particular inductive types but not all of them, and some of those type formers (like dependent sums and binary products) can also be formulated negatively. Also, I think it is useful pedagogically not to require the reader to be familiar with the general notion of inductive type.
I did include classical set theory. You can formulate it in any theory at least as powerful as its traditional home, but people don’t generally bother.
Maybe the time is not ripe for this yet. I have cleared the entry.
(I left a pointer to my personal web, but everybody should feel free to overwrite it.)
I'm sorry that I didn't see this the first time around; I only have a couple of comments in reply to some things written by Mike:
excluded middle (let alone the axiom of choice) is not generally considered predicative
I don't agree with this; I'd go so far as to guess that most mathematicians or logicians concerned with predicativity use excluded middle (although maybe not the axiom of choice). Certainly Harvey Friedman does.
However, if you add excluded middle to a set theory with function sets, then it does become impredicative. But such set theories are already impredicative in a sense, hence the compromise term ‘weakly predicative’ for them.
structural set theory is not a type theory at all
Urs should be able to say something like ‘add a top-level layer of first-order logic with quantification over types [which we will now call sets]’ to transition from a type theory to a structural set theory like SEAR.
ETA: I guess that this is what ‘logic-enriched’ means in your table?
Well, it’s hard to know numbers. All the predicativists that I know personally use function sets and not excluded middle. There seem to be two main schools calling themselves “predicative”: people like Friedman, and people who use things like dependent type theory, CZF, and Pi-pretoposes.
And no, that’s not what logic-enriched means; logic-enriched means you have a separate collection of “propositions” in addition to the “types”, like Coq’s Prop. But yes, when you interpret a type theory in an outer system like LF, then it becomes much more like a structural set theory.
There seem to be two main schools
On predicative mathematics, I called them the ‘classical’ and ‘constructive’ schools.
1 to 18 of 18