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.
created effects of foundations on "real" mathematics and linked to it from foundations.
This is to archive an exchange between Toby and James on the blog here. The hope would be that eventually the list of examples is expanded here.
I come to bury foundations, not to raze them …
I passed through my first foundational crisis many years ago, and have gradually since come to distrust the very word "foundations" — all despite our best intentions, it has a funny way of turning mathematicians into Bourbaki-thumping fundamentalists, though even their word "magma" would have paved a better road.
I cannot say if there's a better word ahead — for the Time Being, in the Mean Time, I have settled happily enough on the word "medium".
Discarded the derogatory “real” mathematics. Renamed to core mathematics, following an article by Frank Quinn.
We are experiencing some pretty serious bugs here. I renamed “real” to core in the article title, but instead of renaming it, a new article was created.
This now looks like the same problem that I encountered yesterday, here.
I am bringing this to the attention of the technical team…
Got a 500 Internal Server Error when I tried renaming prefield of fractions to ring of fractions, because the latter term is the one used by Frank Quinn in the section on commutative rings in his article Proof Projects for Teachers. Seems like the article was duplicated rather than renamed.
Sorry for the trouble. Christian Sattler is kindly looking into it now.
Christian says the problem is fixed now!
And Christian has now merged all the nForum threads, too.
Today’s Revision 6 seems to make a rather incredulous claim
The existence of large categories such as Grothendieck topoi requires the existence of a strongly inaccessible cardinal/universe
I am not sure what exactly is being meant here, but this appears to be false as stated.
that one needs strongly inaccessible cardinals for large categories is only true for ZF/ZFC, and not so in general (strongly predicative mathematics only needs regular cardinals).
The actual thing here needed are universes rather than cardinals, so I’ve added a separate section for universes and stuck that up there. And added statement that this is only the case for set and type theories without classes, as class theories don’t suffer from the issue since large categories are classes.
The real thing to stick in large cardinal axioms is Vopěnka’s principle
Anonymous
Re #21: This is still problematic: a class is simply a predicate with a designated free variable, so classes always exist. What does “requires classes to exist” mean here?
I have fixed (here) the link to large cardinal axiom.
By the way, the reference to Vopenka’s principle in this section may not be too convincing to the sceptical reader caring about real/core mathematics. It would help to connect this to something closer to an “application”.
The example of hypercovers of extremally disconnected profinite sets is better in this regard, but it could still do with more explanation of where the real/core mathematician would find themselves in need of such hypercovers.
I have turned the pointer to Quinn’s article into an actual reference item
(looking at this text, it’s incredibly shy with coming out about which revolution the title is referring to)
Kevin Buzzard uses the term “generic” mathematics (suggested by yours truly), if anyone wishes to include such a reference
McLarty’s article needs updating. This is a reminder to myself.
Beware that
points to version 1 of a preprint which changed title with later versions and is published under that other title. If the reader is meant to find information in version 1 which is not in the later version this should be said explicitly. If not, remove the pointer to version 1 and add the publication data.
Instead of “McLarty comments … in the following article” it is good practice to make a reference anchor and write “McLarty 2010 comments…”
let’s hyperlink doi-s, otherwise it is somewhat besides the point (NB: “doi” is for “digital object identifier”)
Let’s list references under References.
For the record, I find that most of the examples that are now in the entry are less than convincing: A good example here would discuss implication of foundations on a field of mathematics that is not itself about foundations or pure category theory or pure type theory.
For instance, the first example “universes” is essentially circular: essentially it just says that universes are a means of laying foundations.
The example with Vopěnka’s principle does not point beyond the field of foundations: It essentially just says that if you have foundations in which a certain class looks small, then it behaves like it is small.
The example on propositional resizing smells like it could lead to a followup sentence which starts with “Therefore…” and provides a practical implication. But that sentence is currently missing.
And so forth.
In short, most of the examples just show that foundations have consequences. But that’s neither surprising nor contentious. What the entry should point out is that they have practically relevant consequences, relevant to real/core/generic mathematics.
Re #29:
updated McLarty’s article to v4
But v4 has a different title, a different date, and has been published:
I have edited that in now. But please check if you are sure which version you want to pointing to. And if it matters, alert the reader of where they should go hunt for the intended information.
Dear Anonymous editor from #3 to #9 above:
please let us know if you have seen the comments #22 and #30 and are planning to react.
I agree with (what I take is) Dmitri’s point, that the example “universes” is still not a decent example. If it is meant to remain as is, then I find it should be deleted.
If the examples in this entry are not convincing (and currently few of them are, I find), then it will backfire and make sceptical readers conclude that foundations really are a waste of time.
Re #24:
The article describes the revolution relatively clearly on page 2:
Precise definitions: Old definitions usually described what things are supposed to be and what they mean, and extraction of properties relied to some degree on intuition and physical experience. Modern definitions are completely self-contained, and the only properties that can be ascribed to an object are those that can be rigorously deduced from the definition.
Logically complete proofs: Old proofs could include appeals to physical intuition (e.g., about continuity and real numbers), authority (e.g., “Euler did this so it must be OK”), and casual establishment of alternatives (“these must be all the possibilities because I can’t imagine any others”). Modern proofs require each step to be carefully justified.
the entire section on “propositional resizing” is about type theory, and it functionally doesn’t make any difference in actual mathematical practice. The only difference is whether one would call the set of all subsets or filters or Dedekind cuts small, as in traditional impredicative mathematics, or large but locally small, as in predicative mathematics paralleling category theory and higher category theory.
Also removed section on universes because it isn’t very convincing an example, and same with Vopenka’s principle.
Anonymous
just here to comment on my last edit: not the anonymous editor at #3-9 but I largely follow Mike Shulman’s views on predicative mathematics (especially in the context of type theory and homotopy type theory), that predicativity doesn’t really fundamentally change the high level picture of the mathematics, it only adds additional administrative work for the mathematician to track universe levels, largeness, and smallness for sets, propositions, and contractible types in the same way that category theorists are forced to do so for Set and other higher groupoids/categories. I remember that Mike had a comment or answer on a mathoverflow thread which he laid out his view in detail on predicative mathematics, but I could not find it.
As for the other two, agree with Dmitri Pavlov and Urs Schreiber, so I went ahead and removed all four “examples”.
re #33, still concerning
The article describes the revolution relatively clearly on page 2:
Yes, eventually it transpires, but isn’t it being overly shy, given that the title is announcing a revolution? Imagine handing this to your lay friends or family members and asking them if they can figure out what revolution the title is about.
I would have started out in the very first lines with something more up-front, like:
The modern style of “rigorous” research mathematics is possibly one of the greatest cultural achievements of humanity: A practical method which ensures that truth is established in an unambiguous way which all practitioners can verify and will, if indeed correct, eventually agree on, no matter whether they are befriended or arch-enemies.
While the often laborious and even tedious method of rigorous mathematics has contributed so much to the popular stereotype reputation of mathematics as a dry and uninspired subject that it might seem to be the only way that mathematics can be practiced, it is historically still a relatively new development: In the 19th century mathematics was already blossoming, but its practice was often quite different. It was no less than a revolution at the beginning of the 20th century when…
1 to 36 of 36