Dear Patrik, I think I understand what you mean by lativity - in the logical account you proceed from one kind of structure to another, defining the latter in terms of the former. By the way, your discussion of terms and sentences seems to be missing the notion of formula as distinct from terms. (I think at one point you mentioned the Goguen-Burstall institutions, which have a similar omission.) Usually one thinks of terms as referring to the things you are talking about, and formulae as what you are saying about them: so the predicate P(x) is a formula with x a term. Quantification still yields formulae, but a formula with no free variables is also a sentence. (What would you call Ex.P(x,y) in your language?) As I understand it, this is lative in that you proceed from terms to formulae to sentences. To check my understanding, here's another system that I believe you would call lative: sequent calculus where a sequent is entailment of formulae in a context (of free variables available). You proceed from formulae to sequents, and the sequent is the analogue of the sentence in this logic. Then there is a sharp, lative distinction between the quantified formula Ax.P(x), with no free variables, and the sequent T |-_{x} P(x) with context {x}. Here's an example I guess you would call illative: dependent type theory. The types are in many ways analogous to formulae, but types depend on terms and terms depend on types. (Also you have judgements similar to sequents.) Most of us are happy with that; it just means that terms and types are defined together, inductively in a well-founded way. Is dependent type theory illative? If so, what difference does that make to you? Here's another contrast. Algebraic theories are lative, in that you proceed from terms to equations (the formulae). Essentially algebraic theories are illative in that the existence of terms may depend on equations holding. For example the composite of two morphisms in a category exists only if the codomain of one equals the domain of the other. When you are constructing free algebras, the lativity of the algebraic case means you can do it in three steps: first construct the terms, then generate a congruence, then factor out the congruence. The illativity for the essentially algebraic case seems to spoil this, in that factoring out the congruence may create more equalities and hence bring more terms into existence. (Though actually you can do it in the same three steps if you first create all "potential" terms, then generate a partial congruence, where self-congruence is existence, then factor that out.) Regards, Steve. On 09/08/2015 10:52, Patrik Eklund wrote:
On 2015-08-09 05:10, Fred E.J. Linton wrote:
Not wishing to broadcast my illiteracy in the matter ... So I ask you now, in public, where my shame can be greatest: what do you mean by "lativity"?
Thank you, Fred, for your questions. We were actually nervously waiting for somebody to ask that question, so we will remember you always for having done that.
... [For admin and other information see: http://www.mta.ca/~cat-dist/ ]