Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics
Hi Martin, Thanks for your response. My catlist posting was using rather general formulations but there are underlying detail that can be found in our papers. Let me add just a few historical remarks. One main idea of our work is that their is a "lativity" in logic that is not respected. It's not comparable to the "lativity" in set theory where you can create classes out of sets, but you cannot throw classes back into the basket of sets, whatever that would be. The same thing happens in logic. We must start with the signature, based on which we construct terms, and terms are used inside sentences. Once we have the "bag of sentences" we may proceed "latively" to construct other things. When we eventually come to proof rules, the bag of sentences was closed a long time ago. Yet, G??del uses "provability" to create new sentences, and simply opens up that bag of sentences, and throws in these new ones. It has always been accepted, but this in fact breaches the lativity principle, which indeed is not respected in logic. The lativity principle cannot be formulated in set theory alone, and set theory is also very much untyped, we have to say. It basically also boils down to separating object languages from their metalanguages. First-order logic as developed from a fons-et-origo becomes acceptable over decades while being developed hand-in-hand, so as to say, with set theory. Type constructors in type theory are good examples that basically appear in no language whatsoever. They are simply brought in from the outside, almost like a holy spirit. But then we have category theory, and in our approach we use it as an object language where that hand-in-hand appears as a metalanguage. And then I turn category theory into a new metalanguage in order to deal with lativity of logic. There is a bit of lativity in Goguen-Burstall's and Meseguer's general models, but unfortunately types do not explicitly occur since the Sign category is considered as abstract until it is made precise for particular logics. And when it's made "precise" e.g. for first-order, it simply adopts e.g. the traditional explanation of terms, so they are not formally constructed within that categorical metalanguage. This is of course then the also reason why the Cat theory enters when dealing with semantics. It's also too general. Yes, we cannot create the set of all sets, similarly as we shouldn't even try out creating the type of all types. Nevertheless, Martin-L??f took the liberty of doing that, and was opportunistic enough to publish it. Things went wrong but it was not called a paradox. Constructions were "improved" over decades, but the HoTT community still uses universality, so that paradox just appears as the emperors new clothes. Sch??nfinkel, Curry and Church saw all these problems, and Hilbert saw it, too, of course, since all of these three were discussing these quite frequently over many years in G??ttingen. Hilbert never wrote anything about it, but probably because he couldn't solve it (or wasn't interested in medals), and he was becoming too old at that time anyway. Sch??nfinkel and Church write more explicitly that something remains to be understood, but Curry less so. Curry just went on even if the foundations were shaky. Kleene never did that, and he was in any case cleaning up other things. von Neumann probably saw what was going on, but he kept himself always out of that mess. So when that mess now has rooted itself like the Mentha Piperita, opportunists travel around, and the bank voles follow them.
I am not sure why these questions are being asked in this list:
In our work now it's indeed about understanding that lativity, and these questions turn up when we use categories as a metalanguage for logic. We thereby also say that types are not fundamental, but rather given because of an object in a category. We also see how we need to debate category theory itself. Take monoidal categories. They are not really categories, are they? They do contain a category, but they are not categories. They are not algebraic structures either, are they? Freeness issues become tricky, and it becomes doubtful if universal algebra can overcoat lativity of logic. Universal algebra kind of strangles logic to become what it is generally accepted to be. Cheers, Patrik -- Prof. Patrik Eklund Ume?? University Department of Computing Science SE-90187 Ume?? Sweden ------------------------- mobile +46 70 586 4414 website www8.cs.umu.se/~peklund [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Some claims quoted below need to be rectified, given that this is a public forum: On 29/07/15 06:54, Patrik Eklund wrote:
Yes, we cannot create the set of all sets, similarly as we shouldn't even try out creating the type of all types. Nevertheless, Martin-L??f took the liberty of doing that, and was opportunistic enough to publish it. Things went wrong but it was not called a paradox.
It is called Girard's Paradox, and the construction resembles Burali-Forti's Paradox, rather than Russell's paradox. The idea was to have a type U of all types, including U itself, written U:U. This may seem naive given Russell's Paradox was known. However, there is more to U:U than Russell's paradox, because "U:U" is not a proposition (it is a so-called judgment), and hence it cannot be true or false, or taken as a hypothesis in a mathematical statement. In particular, using U:U, you cannot form the type of all types that don't belong to themselves, because there is no "belong" relation in type theory, and for instance writing something such as "not(X:X)" is not even grammatically correct. To derive a contradiction using U:U (in a type theory extended with this judgement) is much harder than to derive a contradiction from the hypothetical existence of a set of all sets (in set theory).
Constructions were "improved" over decades, but the HoTT community still uses universality, so that paradox just appears as the emperors new clothes.
The improvement adopted both in MLTT in the 1980's, and in MLTT+HoTT axioms now, was already available, and is the same as the one Russell proposed a century ago to avoid his paradox, and adopted in Principia Mathematica, namely to instead have a hierarchical stratification U_0 : U_1 : U_2 : U_3 : ... by "size", where U_0 is the type of all small types, which lives in the type U_1 of large types, which lives in the type U_2 of even larger types, etc. The idea is at least 107 years old. M. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Yet, G??del uses "provability" to create new sentences, and simply opens up that bag of sentences, and throws in these new ones. It has always been accepted, but this in fact breaches the lativity principle, which indeed is not respected in logic.
The point is that the provability predicate doesn't require new syntax but can be formulated already with a modicum of arithmetic (that's what has become known as "Goedelization"). It would be a different issue with a "truth" predicate which cannot be expressed in the language (known as Tarski's theorem). Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (3)
-
Martin Escardo -
Patrik Eklund -
Thomas Streicher