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