From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8674 Path: news.gmane.org!not-for-mail From: Steve Vickers Newsgroups: gmane.science.mathematics.categories Subject: Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics Date: Tue, 11 Aug 2015 10:39:05 +0100 Message-ID: References: <536THicJV0416S02.1439086221@web02.cms.usa.net> Reply-To: Steve Vickers NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1439408130 4840 80.91.229.3 (12 Aug 2015 19:35:30 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 12 Aug 2015 19:35:30 +0000 (UTC) Cc: Categories To: Patrik Eklund Original-X-From: majordomo@mlist.mta.ca Wed Aug 12 21:35:24 2015 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.19]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1ZPbo2-0006kB-J2 for gsmc-categories@m.gmane.org; Wed, 12 Aug 2015 21:35:22 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:45562) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1ZPbnS-0003IK-Cf; Wed, 12 Aug 2015 16:34:46 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1ZPbnT-0006tE-PK for categories-list@mlist.mta.ca; Wed, 12 Aug 2015 16:34:47 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8674 Archived-At: 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/ ]