From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7758 Path: news.gmane.org!not-for-mail From: Patrik Eklund Newsgroups: gmane.science.mathematics.categories Subject: Re: Publicity Date: Mon, 10 Jun 2013 09:53:17 +0200 (CEST) Message-ID: References: <24659_1370525088_51B08DA0_24659_212_1_E1Uka9s-0001mR-LE@mlist.mta.ca> <51B1D325.9090803@univ-savoie.fr> Reply-To: Patrik Eklund NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; format=flowed; charset=ISO-8859-15 Content-Transfer-Encoding: 8BIT X-Trace: ger.gmane.org 1370911040 27615 80.91.229.3 (11 Jun 2013 00:37:20 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Tue, 11 Jun 2013 00:37:20 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Tue Jun 11 02:37:18 2013 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1UmCaM-0002ng-3k for gsmc-categories@m.gmane.org; Tue, 11 Jun 2013 02:37:18 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:39723) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1UmCYC-0004B9-Ck; Mon, 10 Jun 2013 21:35:04 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1UmCYD-0003Qn-ED for categories-list@mlist.mta.ca; Mon, 10 Jun 2013 21:35:05 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7758 Archived-At: These discussions on trinity and similar seem to raise only irritation where there would be opportunity to provide constructive discussions. CT has done a good job in explaining and providing rigour. Some like it, some don't. Type theory is a typical example where computer science is "on its own", unless trying to understand trinity like suggestions. Take 'lambda', for instance. Church said already back in 1940 that 'lambda' is an "improper symbol" and that his 'o' type for something in direction of propositions, but Church says: "We purposely refrain from making more definite the nature of the types o and iota" (peklund: the 'type' type!) ", the formal theory admitting of a variety of interpretations in this regard. Of course the matter of interpretation is in any case irrelevant to the abstract construction of the theory, and indeed other and quite different interpretations are possible (formal consistency assumed)." 'Trinity' also raises irritation and even fear as it refers to the Holy Trinitiy, and many feel very uncomfortable even talking about these things. The wordpress blog mentioned is also very shallow in its introduction, just mentioning "manifest in three persons". Some may be interested to look more into the relation of "the three" as it has been part of history and e.g. the split of the Latin and Greek Churches. The so called Filioque addition and why it happened, and how it appears in the Latin language is far beyond just saying "manifests". The way Augustinus opposed Arianism and his choices of 'language' is, I think, a bit interesting in this context. Or maybe not. Rigour to me is just being clear about what is what. For instance, sentences build upon terms, and satisfaction/entailment needs sentences. This shold mean we need to be precise about terms, and then closing that door. Then we are precise about sentences, and closing that door, and so on. We should somewhere along that path, e.g. after having closed the "sentences door", come up with new and nice sentences still to be used. G?del was doing that all the time. We shouldn't, I think, allow "circadian rhythms" into science and mathematics, in particular in type theory concerning how types and propositions are "manifested" in each other. Cheers, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]