From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a9d:118a:: with SMTP id v10-v6mr10846530otf.102.1525255917974; Wed, 02 May 2018 03:11:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:f057:: with SMTP id o84-v6ls1536821oih.8.gmail; Wed, 02 May 2018 03:11:57 -0700 (PDT) X-Received: by 2002:aca:b441:: with SMTP id d62-v6mr9511142oif.55.1525255917120; Wed, 02 May 2018 03:11:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525255917; cv=none; d=google.com; s=arc-20160816; b=vXsuR7uOYaOrj5/nt/ltuhX+K8d4qR5ISmMuqnSyxi7+BIeNAGuqVdMe5ljk+t9io6 m26ykAQqfeucivXKJSyfPDlRKStTAay7CfB6yXuWYs4+/+6yb4ShfyQtZpGiRX2n+HbX 7d9zz/vJJNqSl5iTiaw1FfN7z3a9x883F7O5AIfkzV5amZaAhZl/vupg6x+5B47BnVpt EplwpCXXypNiA7j8aWkQemNPn5TkbC1EC3URr9K2It3qFFWptUaByV5Wdu1YH23cwEqw mgE2G8gafaS3yyYvnnOGzADp236Pm7jyTavUPdQMtSu2ojiVhbcO4vzTtwu5fU4HD+pR /xew== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=ocL1mBSxkOtBZqWmtLagwnrjcdb8pAqlzMcg3UASb/4=; b=O1MT5PlfQb4WpcPUgMr6F0jSEOoi22eXfIb0ix5gXnv7MfDXB6UqNLezEX+mZwH+8u fSV3I0EYLCymVYncVFPl++Qx89yHssFkE0SiFHVbVdhdCqYskRoMcGd6Y4jHhKxTTwxL M0RR6QEtDJjLhxRAbqdKo6ALilK7tUPiFLqSzlWL/iJSoGWOciEpmhzfdTCbQO9tsw/g 25zPSbpcQGx8fgr9SLPAyrh/4IVCsgKDymdqvB2/VRrqsbpmSgVOeSif5XlO2tyFC3Fi qy0kkIzkEvCrMbkOyvhdfMXdBM2tWPuXjQ+O7oFlGEKNDn6jYv2AnLnIMlYKVudSpKGW zNUQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=wd4zKLaf; spf=neutral (google.com: 2607:f8b0:4001:c06::22a is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Return-Path: Received: from mail-io0-x22a.google.com (mail-io0-x22a.google.com. [2607:f8b0:4001:c06::22a]) by gmr-mx.google.com with ESMTPS id e10-v6si759914otj.3.2018.05.02.03.11.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 02 May 2018 03:11:56 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4001:c06::22a is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4001:c06::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=wd4zKLaf; spf=neutral (google.com: 2607:f8b0:4001:c06::22a is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-io0-x22a.google.com with SMTP id a10-v6so16806434ioc.9 for ; Wed, 02 May 2018 03:11:56 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=ocL1mBSxkOtBZqWmtLagwnrjcdb8pAqlzMcg3UASb/4=; b=wd4zKLafyEnNFxXE62rHVScgh64jNf9IUtnxHqP7pl9kdXtqodoOyEBvcm+b582e7r 0Uh066yyjZrlDHnXxNVsfurMv+c89FP1rA+7oTOmbphxUA560WoABCJByZ0/BNeEPHWJ 8PsfBoJqgO7B2N6CslAo0GHte9Ih5FgKx1MpvsCkBPqyoXWGgk6Zg+cz6SIGhkdSm7jy i2z0tJCHR6pxxPiy0duXsrtmVxTEaop3HdBhRydP2YvR1bHw3LuIxb6QyJMn2ibhBySr YhsmYUjP6MamT7JrZV0ed8TX254akT1jd2CkeTOCZOjN6igncEMtczPJr/tDjRl1QNmS CSeQ== X-Gm-Message-State: ALQs6tA62mfXM+EMNT45g7KTKRa5liYGqsyT3TPZ1RfqeXbgW8vrB1rF L/7krfZiSdoA79Loj4p2nDAf2gDDrpTphEnFCHmgaK3Y X-Received: by 2002:a6b:3a1:: with SMTP id e33-v6mr20711578ioi.51.1525255916459; Wed, 02 May 2018 03:11:56 -0700 (PDT) MIME-Version: 1.0 Received: by 10.192.174.7 with HTTP; Wed, 2 May 2018 03:11:55 -0700 (PDT) X-Originating-IP: [193.77.148.136] In-Reply-To: <523130ad-04a8-42ae-bde3-f09ce42d905b@googlegroups.com> References: <161ab0f5-32a6-4868-b9fc-901f0df147b8@googlegroups.com> <523130ad-04a8-42ae-bde3-f09ce42d905b@googlegroups.com> From: Andrej Bauer Date: Wed, 2 May 2018 12:11:55 +0200 Message-ID: Subject: Re: [HoTT] Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument) To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" I doubt much can be added to a discussion of "using natural numbers before defining natural numbers" on this list, but just because this list if about type theory, let me point out two things. 1. Various worries about non-standard natural numbers and lack of absolute definitions are an artifact of first-order logic and the insistence that natural numbers be defined on their own, without reference to anything at all. As soon as one realizes that the natural numbers can be characterized by a universal property within a larger universe (either as an initial algebra in a category, or a type with a suitable elimnator in type theory), the mystery goes away. Within any universe of mathematics, the natural numbers are unique up to unique isomprphism. And since there are many universes of mathematics, it is not suprising that we see many incarnations of natural numbers. But each one first perfectly and uniquely in the ambient in which it lives. (In case this isn't clear, the non-standard models of PA constructed with ultrapowers are just normal natural numbers objects in an ultrapower model of set theory). 2. The idea that there can be no natural numbers before we define natural numbers, as well as statements such as "it is impossible to avoid circularity in foundations" arises from mistaken and unrealistic expectations that it is the task of the foundations of mathematics to provide something out of nothing. I explain to myself the yearning for such foundations from the fact that the human psyche is comforted by an illusion of absolute security. I have written about this on Mathoverflow (https://mathoverflow.net/a/23077/1176). With kind regards, Andrej