Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics
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. In logic we typically have signatures, terms, sentences, structured sets of sentences, entailment, models, satisfactions, axioms, theories and proof calculi. We cannot e.g. define entailment before we have a notion of sentences, and we should not define sentences before we have a notion of terms. The latter is a bit more controversial. In first-order logic I would see P(x), where P is a "predicate symbol", as a term, and not as a sentence, whereas putting a quantifier in front of it, Ex.P(x), makes it no longer a term. This is why I have difficulties e.g. to accept that the two 'not's in expressions like "not Ex.P(x)" and "Ex.not P(x)" would be the same. I am starting to think they are only informal as symbols, a bit similar as Church said lambda is and informal symbol, so actually not part of the formal syntax. Am I wrong or am I wrong? In logic we indeed need a signature (sorts and operators) in order to construct the categorical object of terms. Construction is important. We need terms to categorically construct sentences, which appear because of a sentence functor not being extendable to a monad. Otherwise sentences are terms, aren't they, because then we could substitute sentences within sentences, and that does not comply with our traditional view of sentences. Traditional first-order pretty much doesn't care, and neither did Aristotle about these things. Aristotle's and first-order logic are therefore very "illative" and also very unsorted, I would like to add. You are not broadcasting illiteracy at all, and your shame couldn't even be small because no shame whatsoever is justified to exist, at least not on your side. There may, however, be some of it now or eventually on my side, but let us see what happens if/when/how this dialogue develops. It may indeed turn out that at least some members of this catlist will see me just as a devoted soldier "seeking the bubble reputation, even in the canon's mouth". When we were searching for a name describing what we try to explain, we wanted to be careful not to use a "reserved word" that is more easily misunderstood than not well understood. In the latter case, we thought we can always try to explain, as I am about to do now. In the former case it would be a differentiation, which is more tricky. So here goes. 'Lative' is related to motion, and more specifically, motion 'to' and 'from', so when terms appear in sentences, terms 'move into' sentence, and 'appear within' sentences. At the same time, sentences 'move away from' terms, and separates terms from sentences. In comparison, 'ablative' is motion 'away', and nominative is static. The lative locative case (casus) indeed represents "motion", whereas e.g. a vocative case is identification with address. We want to underline the need not to have "mixed bags", so that we can ensure that a term does not appear in the bag of sentences, or a structured set of sentences would appear in the bad of entailment. I shouldn't compare with waste sorting, because then somebody might say "Patrik Eklund said Kurt G??del didn't care about waste sorting". Obviously, I do respect the work of G??del, even if at the same time I do find his approach "illative". From categorical point of view, G??del also complies only with the underlying category of sets, but as we have shown (e.g. in http://www.sciencedirect.com/science/article/pii/S0165011413000997), we may have other underlying categories for the the term monad. The term constructor and the use of category theory as the metalanguage for logic is here important. Logic developed "hand-in-hand" with set theory and as being a metalanguage for category theory should then not be confused with the lativity of logic we explain using categorical notions. Let me also again underline that nomenclatures and classifications in health care is one of our motivation areas of examples and applications. Nomenclatures exist also elsewhere, but he ones appearing in health we find very motivating. At this point of our "research program" we believe we have a fair understanding of the lativity as related to signatures, terms and sentences, and we hope we have a fair intuition about how we now proceed to investigate the lativity of that with respect e.g. to to entailment and models. Thanks again, and indeed, possible shame in whatever form or magnitude is all mine. Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
In logic we typically have signatures, terms, sentences, structured sets of sentences, entailment, models, satisfactions, axioms, theories and proof calculi. We cannot e.g. define entailment before we have a notion of sentences, and we should not define sentences before we have a notion of terms. The latter is a bit more controversial. In first-order logic I would see P(x), where P is a "predicate symbol", as a term, and not as a sentence, whereas putting a quantifier in front of it, Ex.P(x), makes it no longer a term. This is why I have difficulties e.g. to accept that the two 'not's in expressions like "not Ex.P(x)" and "Ex.not P(x)" would be the same. I am starting to think they are only informal as symbols, a bit similar as Church said lambda is and informal symbol, so actually not part of the formal syntax. Am I wrong or am I wrong?
I don't understand why atomic formulas are terms but not formulas. Always thought the Lawvere's hyperdoctrines made all this very clear: terms are in the base and formulas are in the fibres. In case there is a generic family of propositions A:Prop |- True(A) we can turn predicates into terms of type Prop. That's the shift to HOL. The 2 different negations are just negations in two different fibres. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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/ ]
Patrik Eklund wrote:' ... at least some members of this catlist will see me just as a devoted soldier "seeking the bubble reputation, even in the _canon's_ mouth". I'm trying to figure out if this is a misspelling or a pun so clever that I can't quite figure it out. Robert Dawson [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (4)
-
Patrik Eklund -
Robert Dawson -
Steve Vickers -
Thomas Streicher