Re: Internal truth objects

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

Dear All,

The question about "logic 'in' category" sounds very "internal" and
indeed toposes (or topoi, whichever you prefer) come to mind. Subobject
classifiers and truth values dominate, and it first looks
very propositional and then quantifiers are rediscovered. So its
rediscovering first-order 'in' some category, where cartesian closedness
as a criteria already "rings a bell".

On the other hand, if we replace 'in' more with 'with' or 'over', logic
with/over categories, work using category theory as an overall
metaalanguage for logic is e.g. seen in Goguen's (and Burstall's etc.)
institutions and Meseguer's entailment systems (general logic). This
approach then creates the category of logics, and morphisms between
logics is interesting.

Concerning types, type constructors are tricky as they are usually left
out of some signature, so type constructors is a "meta business", and
modern type theory looks they way it does because of this. There are e.g.
informal notions like "soft typing", and many many other similar notions
for 'extended' types, whatever that means. Having type constructors then
outside the machinery, leaves room for ad hoc stuff, and we run the danger
of mixing meta and object languages.

The signataure is interesting and we do have the category of signatures.
Arities and sorts can be handled categorically, e.g. the way Benabou did
on schemes. In a recent paper we extended that to term monads over
monoidal biclosed categories, so the sort object must be distinguished
from the actual set of sorts. A term functors can be inductively
constructed, that is really 'constructed' and not just inductively and
verbously imagined,

We have a recent paper

http://www.sciencedirect.com/science/article/pii/S0165011413000997

where we also and maybe mainly deal with the type constructors in levels
of signatrures. We e.g. show how the informally described 'set of lambda
terms' can be more formally constructed. Some or actually many say that
the definition of lambda terms is elegant, but it is nevertheless not
strictly mathematical, certainly not categorical. We tried to do that, and
we think it looks fine. We are building some more stuff upon those
observations.

Apart from having those few remarks on lambda calculus we also briefly
look at Sch?nfinkel, Curry and Church (1920-40) in these notations. For
instance Church's iota and o are interesting. One of them we know what it
is, the other one is still unclear, and modern type theory never bothered
to look at it. "Propositions as types" looks very interesting and
appealing when you intuitively understand it, but when you develop the
math for it, it easily becomes mostly mathematics fiction. If we are
dealing with foundational issues, things must be very precies. If we only
go for constructions in functional languages, the underlying mathematics
is more fictive.

The reason why we published that paper 'fuzzy' is that we go 'over'
certain categories e.g. to decide where actually to represent
uncertainties. So we kind of "internalize" the representation of
uncertainty, but not the logic a la topoi.

Needless to say, the difference between one-sorted and many-sorted is
non-trivial, even if some say it is trivial, but they mostly look at a
signature as an end-point with respect to formal treatments of types, not
a beginning point.

Opetopes things seem go in nice directions, and we need to look more into
it. For instance, the category of signatures over a monoidal biclosed
category appears to be a monoidal biclosed category in some case at
least. We didn't check it, but we have looked at "Kleisli over Kleisli"
in a similar fashion (so has Manes), and "composing algebras" is suddenly
a possible notion on the Eilenberg-Moore side. Composing with the term
functor is one way to provide uncertainty modelling, and having term
functors over categories carrying uncertainty building blocks is another
way. We prefer to say intuitively that there is a distinction to be made
between "fuzzy computing" and "computing with fuzzy".

All this distinguishes our approach from Goguen and Meseguer in that we do
not have an abstract Sign category, nor an abstract Sen functor (yet to
be defined), but they are more specific given underlying specific
signatures. So substitution, in a more general sense remains in focus. In
the paper we so far deal only with signatures and terms, so we are now
indeed looking into sentences. Obviously, axioms, inference rules and
theories must follow also for all this to make more sense.

If we look at first-order, quantifiers are indeed very tricky, and there
are many fundamental questions related to the fons et origo birth of
first-order logic. Every logician and almost every categorist has created
their own view on this. For propositional logic, a proposition is more
clearly a term, whereas moving to predicate logic, a predicate becomes a
sentence, and in Horn clauses, atomic formulas are distinct from
non-atomic ones.

And so on and so forth. If anyone wants to know more, just let us know.

Cheers,

Patrik



On Mon, 6 May 2013, Sergey Goncharov wrote:

> Dear Philip,
>
> thank you for your answer and for the useful references. A Dogma is
> indeed the right thing, precisely what I had in mind. At least, now I
> know the name for this thing.
>
> The question is only that if a category at hand already has a candidate
> for Omega (e.g. externally complete Heyting algebra), what would be
> easy-to-check conditions that it is a dogma w.r.t. that Omega. Or,
> alternatively, what would be constructions for creation dogmas from
> other dogmas. I bet, no one has bothered to investigate this issue.
>
> Best,
> Sergey
>
> On 04/05/13 21:46, Philip Scott wrote:
>> Dear Sergey:   this was explored a bit in the early days of categorical
>> logic. The key topos isomorphism  Sub(A) \iso Hom(A,\Omega) combines two
>> possible viewpoints (of course, Bill Lawvere was a key figure in both
>> developments):   the LHS (as you point out) considers categories with
>> distinguished "logical" structure imposed on the subobject posets (and
>> quantifiers arising as adjoints): e.g. the work of Makkai-Reyes-Joyal,
>> et.al  (see, for example,  Makkai-Reyes' book "First-Order Categorical
>> Logic, SLNM 611, where one sees a discussion focussed on Regular
>> Categories, Heyting Categories, etc.). On the other hand, the right hand
>> side is based on looking at appropriate categories with an object \Omega
>> and distinguished logical structure, giving a "theory of types".  These
>> categories model (intuitionistic as well as classical versions of)
>> Russell's type theory. This viewpoint was developed for example in early
>> work of Hugo Volger (on "semantical categories" of various kinds) and in
>> Lambek's "Dogmas"  (for the latter, see Lambek's article "From Types to
>> sets" in Advances in Math [1980]. )
>>
>> For Lawvere's discussions on these matters, see his two introductions
>> (to SLNM 445 "Model Theory and Topoi", ed. by Lawvere, Maurer, and
>> Wraith [1975], where Volger's works appeared, along with other early
>> workers ) and  Lawvere's introduction to SLNM 274). See also Lawvere's
>> introduction [2006] to the reprinted version of "Adjointness in
>> Foundations"  on the TAC webpage).  More early history (from the 1970's)
>> is discussed in the historical comments at the end of Part II of my 1986
>> book with Lambek (Introduction to Higher Order Categorical Logic) as
>> well as several books in topos theory (e.g. Johnstone's books).
>>
>> Of course Lawvere's early categorical logic papers ("Adjointness in
>> Foundations", "Equality in Hyperdoctrines", etc.) inspired numerous
>> other directions in categorical logic leading to other kinds of
>> structures beyond "Dogma-like"  categories, which you asked about. [For
>> this, I'll just mention the keywords and let you look up the individuals
>> involved: indexed categories and fibrational approaches to categorical
>> logic, categorical models of polymorphism, and (most recently) dependent
>> (Martin-Lof) type theory and homotopy lambda calculus].
>>
>> 							Cheers,
>> 							Philip Scott

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]