From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8673 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics Date: Tue, 11 Aug 2015 11:12:10 +0200 Message-ID: References: <536THicJV0416S02.1439086221@web02.cms.usa.net> Reply-To: Thomas Streicher NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1439408113 4414 80.91.229.3 (12 Aug 2015 19:35:13 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 12 Aug 2015 19:35:13 +0000 (UTC) Cc: Categories , fejlinton@usa.net To: Patrik Eklund Original-X-From: majordomo@mlist.mta.ca Wed Aug 12 21:35:06 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 1ZPbnl-0006XC-12 for gsmc-categories@m.gmane.org; Wed, 12 Aug 2015 21:35:05 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:45556) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1ZPbmM-0003De-Rn; Wed, 12 Aug 2015 16:33:38 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1ZPbmO-0006sG-8M for categories-list@mlist.mta.ca; Wed, 12 Aug 2015 16:33:40 -0300 Content-Disposition: inline In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8673 Archived-At: > 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/ ]