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. 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. 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. But categorical logic goes further than ordinary logic in its attempt to define 'theory'. 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). 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/ ]