Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Patrik Eklund <peklund@cs.umu.se>]

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/ ]