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.

]]>I am a university student studying mathematics and computer science and I have been building my own wiki using mediawiki as the software. Recently I stumbled across nLab, it looks beautiful and the thing that I like the best was that I could embed tikz directly into it without hassle, and I'd like to switch to it.

If someone could help direct me how to install it on my own server it would be greatly appreciated!

I also wonder if anyone knows if it's easy to work with pseudocode in nLab as I would be using it alot.

Best,

C ]]>

stub for *Hilbert’s sixth problem*

I was contacted by somebody involved in *The QED Project*. I have given that an $n$Lab page now, linked to from *proof assistant*, cross-linked with *ForMath*. (Maybe we should have a page *formal mathematics* or the like?)

Thank you so much for responding or pointing me in the right direction if this forum isn't the place to find this help! ]]>

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…

]]>I'm a programmer by trade and have recently acquired the urge to build a solid formal foundation for structuring the data I collect, which includes news articles, books, scientific papers, research datasets and much more. To get closer to this goal I am going to develop a semantic database with the purpose of representing any and all human knowledge formally. (Good starter project, no?)

I've come to the conclusion that if I am to structure the very wide range of knowledge I want to represent, I will not only have to use mature NLP techniques (for acquiring the set of all possible interpretations) in combination with either human aid or statistical/ML techniques for disambiguation, I will then have to find a mathematical foundation that is able to represent all of mathematics, because I anticipate needing a lot of mathematics to get at all close to being able to represent all human knowledge formally and also because I think having most if not all the mechanics behind the system be represented inside the system will be the only way to make it flexible enough to get close to representing all human knowledge including all knowledge from all sciences.

Once I have a working system I will then extend it to have isolation as a data management and security feature, add more ways of interfacing with the database (e.g. via streams) and then implement federation through implementing models of trust and related algorithms in the system and connecting that to a distributed data index such as the output of a BitTorrent DHT crawler. The end result I envision is a crossing between a knowledge base, a computation engine and a wiki, which can be used as any and all of those.

Some elements I think I will need to be able to represent at the very least are:

- numbers, bytes, words, mathematical formulas, theorems, tables, images, files...

- relations between any possible object in the database (e.g. between sets, functions and relations between higher level relations)

It would be ideal I could start with a relatively simple model on which to build the more complex model that is capable of encompassing much more if not all of mathematics.

Some of the possible applications of this semantic database would be:

- (initially heavily human-aided) conversion of novel mathematical objects to a formal representation that is also executable (e.g. import new pages on nLab and hand-annotate them -> directly use the new concepts in computations)

- analysis of news on a wide range of aspects (e.g. representations of different groups, logical consistency, consistency with source material, consistency and conflicts with related articles, consistency with related scientific literature)

- automatic inference (e.g. new weather data comes in, combine with existing corpus on weather and seismic data -> new model of predicted weather, combine with models on how weather affects human beings -> storm warning)

- formalize scientific papers to find out if they are internally inconsistent or otherwise faulty, and also analyze them for external consistency (in relation to other papers) and on their effects of the probabilities of propositions they have in common with other research papers, this could potentially be very useful pre-publication but also dangerous because it opens the door for manipulation

- expert systems

- accidentally creating AGI

- extracting parts of the knowledge base to get consistent formal models for many knowledge domains

I'm a bit afraid that the response will be "congratulations, you've basically invented Lisp and this is why it won't work" because I haven't learned Lisp yet and because I have some vague sense that there is similarity between this idea and the ideas behind Lisp. If so, please pick apart my post in the greatest possible detail, I would absolutely love that because I'm very isolated from the mathematics community and I could use any and all feedback.

I have some familiarity with algebra, formal logic, set theory and NLP, but it's quite limited. Reading the nLab right now is very intimidating, although I think I might've found a small foothold from directed graph -> quiver -> category.

tl;dr: I'm looking for recommendations reading material on how to build a knowledge base capable of representing all of mathematics, remarks on why this is a bad idea or who tried before me are also very appreciated, and I'd also appreciate a "required reading list" for nLab. ]]>

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

- Carl Benjamin Boyer,
*The history of the Calculus and its conceptual development*, Dover 1949

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 $\mathbb{N}^\mathbb{N} \to \mathbb{N}$?

Is there a constructive proof that given any function $H\colon \mathbb{N}^\mathbb{N} \to \mathbb{N}$, there exist functions $f,g\colon \mathbb{N}\to\mathbb{N}$ and $k\in \mathbb{N}$ such that $H(f)=H(g)$ but $f(k)\neq g(k)$?

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, $\mathbb{N}^\mathbb{N}$ is a sub*quotient* of $\mathbb{N}$, but not a subobject of it. In D4.1.9 of the Elephant there is a Grothendieck topos in which $\mathbb{N}^\mathbb{N}$ is a subquotient of $\mathbb{N}$, namely the classifying topos of the theory of a partial surjection from $\mathbb{N}$ to $\mathbb{N}^\mathbb{N}$ – but afterwards he explains why that approach wouldn’t work for an injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$, and how one *can* prove constructively that there is no surjection $\mathbb{N}\to \mathbb{N}^\mathbb{N}$.

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 $\Diamond$ on a formal topology be regarded as making it into an overt space?

]]>