I have started a category:reference page
such as to be able to point to it for reference, e.g. from Kontsevich 15 etc.
]]>felt like archiving a quote by Paul Taylor somewhere, it is now at folklore.
Besides being funny, it is actually a useful comment for the newbie, and so I linked to it from category theory.
]]>felt the desire to have an entry on the general idea (if any) of synthetic mathematics, cross-linking with the relevant examples-entries.
This has much room for being further expanded, of course.
]]>stub for Hilbert’s sixth problem
]]>I was contacted by somebody involved in The QED Project. I have given that an Lab page now, linked to from proof assistant, cross-linked with ForMath. (Maybe we should have a page formal mathematics or the like?)
]]>I assume nobody still around here still cares much about Rafael Borowiecki’s entry Timeline of category theory and related mathematics?
I know this entry mostly from when I create new entries: every now and then I think I am creating an entirely un-linked-to new entry, only to see then that the “timeline” is already pointing to it.
For procrastination purposes I just looked at the entry itfelf for the first time in years. While I still have the opinion that I once voiced there, that more important than making it entirely complete is to remove some (few) weird items, I have to admit it has something to it. Would be a fun thing to look at… if there were fewer broken links in grey.
But I notice one thing: for a whole bunch of those grey links we actually do have entries. Only the “timeline” does not follow our entry-naming conventions. For instance it asks for a bunch of capitalized keywords which we do have in lower case. It also asks for “Peter Johnstone (mathematician)”, which we don’t have, while of course we do have “Peter Johnstone”, and so on.
Just in case anyone feels inspired to work on fixing some of these links…
]]>added to Descartes as section On space, matter and mechanics with some quotes on Descartes’ picture of mechanism.
(I was looking for sources that would argue clearly that Descartes’ mechanism is closer to modern continuum mechanics than to modern point particle mechanics. I found something, but I imagine there might be better such sources still.)
]]>created as stub for Zeno’s paradox of motion, for the moment mainly in order to record pointers to texts that expand on its relation to the modern concept of convegence and differentiation, for which I found
Added cross-pointer to this from the References-section of differential calculus, convergence, differentiation and analysis
]]>Bas Spitters had mentioned the following article on the HoTT list. While I suppose the conclusion has to be taken with several grains of salt, I found this discussion interesting and illuminating, and have added it now to the references at foundations of mathematics:
Freek Wiedijk, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (pdf)
Abstract This paper presents Automath encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.
The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church’s higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo’s extended calculus of constructions, and Martin-Löf predicative type theory) and one foundation based on category theory. The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf’s type theory.
started a dismabiguation page for phase. Feel invited to add further meanings.
]]>The following interesting question(s) have been raised by Martin Escardó on the Agda mailing list and the constructive-news list.
Is there a constructive proof that there is no injection ?
Is there a constructive proof that given any function , there exist functions and such that but ?
Both are obviously true assuming classical logic, and the latter can apparently also be proven if one assumes “continuity principles”. As far as counterexamples go, in the effective topos, is a subquotient of , but not a subobject of it. In D4.1.9 of the Elephant there is a Grothendieck topos in which is a subquotient of , namely the classifying topos of the theory of a partial surjection from to – but afterwards he explains why that approach wouldn’t work for an injection , and how one can prove constructively that there is no surjection .
It seems like surely the answer to (1), at least, should be known… but I don’t know it.
]]>I have added a brief note about type-theoretic polymorphism to the list of impredicative axioms at predicative mathematics.
]]>Should the predicate on a formal topology be regarded as making it into an overt space?
]]>