From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8665 Path: news.gmane.org!not-for-mail From: Martin Escardo Newsgroups: gmane.science.mathematics.categories Subject: Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics Date: Thu, 30 Jul 2015 15:46:26 +0100 Organization: University of Birmingham Message-ID: References: <55B82F7F.60302@cs.bham.ac.uk> Reply-To: Martin Escardo NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1438522388 21285 80.91.229.3 (2 Aug 2015 13:33:08 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 2 Aug 2015 13:33:08 +0000 (UTC) To: Patrik Eklund , Categories Original-X-From: majordomo@mlist.mta.ca Sun Aug 02 15:33:00 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 1ZLtNr-00030c-SS for gsmc-categories@m.gmane.org; Sun, 02 Aug 2015 15:33:00 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:60411) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1ZLtMu-0005ll-Np; Sun, 02 Aug 2015 10:32:00 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1ZLtMv-0007rT-7G for categories-list@mlist.mta.ca; Sun, 02 Aug 2015 10:32:01 -0300 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.8.0 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8665 Archived-At: Some claims quoted below need to be rectified, given that this is a public forum: On 29/07/15 06:54, Patrik Eklund wrote: >> Yes, we cannot create the set of all sets, similarly as we shouldn't > even try out creating the type of all types. Nevertheless, Martin-L??f > took the liberty of doing that, and was opportunistic enough to publish > it. Things went wrong but it was not called a paradox. It is called Girard's Paradox, and the construction resembles Burali-Forti's Paradox, rather than Russell's paradox. The idea was to have a type U of all types, including U itself, written U:U. This may seem naive given Russell's Paradox was known. However, there is more to U:U than Russell's paradox, because "U:U" is not a proposition (it is a so-called judgment), and hence it cannot be true or false, or taken as a hypothesis in a mathematical statement. In particular, using U:U, you cannot form the type of all types that don't belong to themselves, because there is no "belong" relation in type theory, and for instance writing something such as "not(X:X)" is not even grammatically correct. To derive a contradiction using U:U (in a type theory extended with this judgement) is much harder than to derive a contradiction from the hypothetical existence of a set of all sets (in set theory). > Constructions were "improved" over decades, but the HoTT community > still uses universality, so that paradox just appears as the > emperors new clothes. The improvement adopted both in MLTT in the 1980's, and in MLTT+HoTT axioms now, was already available, and is the same as the one Russell proposed a century ago to avoid his paradox, and adopted in Principia Mathematica, namely to instead have a hierarchical stratification U_0 : U_1 : U_2 : U_3 : ... by "size", where U_0 is the type of all small types, which lives in the type U_1 of large types, which lives in the type U_2 of even larger types, etc. The idea is at least 107 years old. M. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]