On 2016-11-01 17:16, Joyal wrote:
It is marvelous that the two notions should be so related. But it is be better to keep them appart before uniting them. Otherwise the miracle disappear in confusion.
The "miracle disappears in confusion" is an important observation, as is the need to "keep apart before uniting". Syntax and semantics is like that, or meta and object language. Foundations of mathematics without categorical consideration is basically then over Set, naively speaking. Logic is similar. Fons et origo logic from late 19th century and decades after is confused about being before set theory or after. Topos internalizes logic but is different from the Goguen-Meseguer approach to institutions and entailment systems. The apples and pears of logic should not be seen as a fruit salad. I've sometimes thought (and written some pieces about, e.g. to be found under www.glioc.com) what if G??del's Incompleteness Theorem wasn't a Theorem but a Paradox. After all, G??del basically transforms the Liar Paradox to a Liar Theorem, and logicians at that time (except maybe Hilbert, but he was too old to quarrel) found it to be very smart. However, if we use underlying categories and functors to start from signatures, then create terms, then sentences, then entailments, then models, then proof strategies, and so on, it means we close doors behind us, so that we disable ourselves to mix truth and provability as being "of the same kind or type", which G??del did. Categorically, terms come from monads, because they enable substitution, but sentences just from functors, because otherwise everything is 'term'. The functorial description and generality of entailment and model is of course more tricky, in particular if the underlying category is something more elaborate (like monoidal closed categories) than just Set. In this (heretic?) view, G??del's Theorem/Paradox is actually an example where that miracle appears because of the unintended (?) confusion, so this is why I sometimes think what if it was ween as a Paradox. Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]