Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Steve Vickers <s.j.vickers@cs.bham.ac.uk>]

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