Re: How can we have a categorical definition of "theory"

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

Thanks, Steve.

On 2017-11-10 15:33, Steve Vickers wrote:
> Dear Patrik,
>
> Categorical logic can interpret, but doesn't rigidly follow, the
> standard logical path of signature, formula and sentence to reach
> theory
> = signature + sentences.

You could also more broadly write that equality as something like

Logic = Sign (giving terms) + Sen + |- + |= + Ax + Th + Inf

or in some alternative order, but clearly say that + is not commutative,
meaning "logic is latively constructed".

> I guess that's the path you had in mind that underlies your question,
> and it is also the path that influenced Goguen and Meseguer.

I did, but we should recall Sign in their model enters concretely only
in examples, not in the general model. We require to have in the general
model, so that we truly have a general substitution model.

> Even where categorical logic interprets that standard path, it can move
> away from the "Hilbert-style" idea that a sentence is a formula with no
> free variables. Look in Elephant part C (?) and you'll see that the
> sentences there are sequents in context.

We have to get rid of "free", because it's outside the categorical
machinery.

> But categorical logic goes further than ordinary logic in its attempt
> to
> define 'theory'.

I think it goes further away rather than further.

> Think of a category as loosely motivated by sets. The
> set constructions that logic most directly accesses - as formulae - are
> subsets of finite products (of carriers). It struggles to get to other
> constructions that category theory accesses quite naturally. Hence
> category theory can - and does - define 'theory' in ways that seem
> quite
> unnatural to a logician, either presented (for instance by sketches) or
> completed (as classifying categories, such as Lawvere theories).

I have difficulties with sets only. We can act over monoidal closed
categories.

Let me again underline that we are driven by concrete and real
applications of these logic constructions.

Categorical "logic" in a topos to me makes no practical sense at all.

Patrik


>
> Regards,
>
> Steve.
>
> On 09/11/2017 07:13, peklund@cs.umu.se wrote:
>> How can we have a categorical definition of 'theory', when we do not
>> have a categorical definition of 'sentence'?
>>
>> Institutions (Goguen) and Entailment Systems (Meseguer) do have a
>> Sentence functor but their underlying category of signatures is
>> abstract, so without sort (over a category?) and operators
>> (potentially
>> over another category?).
>>
>> Many-valuedness and its (algebraic) foundations is looking into these
>> things.
>>
>> Just wondering if anybody is thinking along these lines. Uwe at least,
>> I
>> guess.
>>
>> Cheers,
>>
>> Patrik
>>
>> PS Why many-valuedness? Well, for one thing, everything in and around
>> Google and Facebook is many-valued.
>>


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