From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3058 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: intuitionism and disjunction Date: Wed, 1 Mar 2006 16:17:34 +0100 (CET) Message-ID: <200603011517.k21FHYEH009161@fb04209.mathematik.tu-darmstadt.de> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019071 7077 80.91.229.2 (29 Apr 2009 15:31:11 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:31:11 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Wed Mar 1 19:33:48 2006 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 01 Mar 2006 19:33:48 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.52) id 1FEamT-00025B-U1 for categories-list@mta.ca; Wed, 01 Mar 2006 19:30:53 -0400 X-Mailer: ELM [version 2.4ME+ PL100 (25)] Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 4 Original-Lines: 27 Xref: news.gmane.org gmane.science.mathematics.categories:3058 Archived-At: W.r.t. to the discussion on intuitionism and disjunction I would like to remark that this relation depends heavily on whether the ambient setting is predicative or not. In an impredicative setting like toposes (or the Calculus of Constructions) one may define disjunction and existential quantification `a la Russell-Prawitz by quantification over \Omega (that's what (some) logicians call impredicative, i.e. the possibility to quantify over propositions and thus also predicates). However in a first order setting this is not possible. E.g. if one considers Heyting arithmetic with ist usual axioms and as logic the \neg,\wedge,->,\forall fragment of first order logic then all formulas are provably double negation closed. This shows that disjunction and existence are not definable from the rest via first order logic. So far the logical side. What Paul Levy had in mind was slightly different as I understand it. Categories of domains (cpos with \bot) are cartesian closed and have weak finite sums but certainly no proper finite sums (since every map has a fixpoint). For modelling his CBPV paradigm he needs in addition a category of predomains which is bicartesian closed. The former is an example of a ccc which is not bicartesian but can be embedded into the latter which is. So one doesn't get for free the finite sums from a ccc which is problematic both in logic and semantics of computation. Thomas