From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 2 May 2018 01:52:38 -0700 (PDT) From: james...@berkeley.edu To: Homotopy Type Theory Message-Id: <523130ad-04a8-42ae-bde3-f09ce42d905b@googlegroups.com> In-Reply-To: <161ab0f5-32a6-4868-b9fc-901f0df147b8@googlegroups.com> References: <161ab0f5-32a6-4868-b9fc-901f0df147b8@googlegroups.com> Subject: Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_16777_169223753.1525251158617" ------=_Part_16777_169223753.1525251158617 Content-Type: multipart/alternative; boundary="----=_Part_16778_1164483579.1525251158617" ------=_Part_16778_1164483579.1525251158617 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Just a comment on this: This is one of the reasons why I have some problems to trust proofs of=20 > properties of natural numbers formalized in CIC : Are some people =E2=80= =9Cproving=E2=80=9D=20 > properties of natural numbers that are already assumed in order to define= =20 > CIC ? > This is a general foundational problem, which exists even for first-order= =20 logic. It is impossible to avoid circularity entirely in foundations. There are models of ZFC which have a non-standard version of the natural=20 numbers (easy to construct by compactness theorem, if we really believe ZFC= =20 is consistent). Let's pick such a model V*, and this non-standard version= =20 of the natural numbers N*. Then inside V*, it evaluates to true that ``N*= =20 embeds into every other model of PA, and every model of PA which embeds=20 into N* is isomorphic to N*". From outside V*, however, we see that the=20 standard natural numbers, N, embeds into N*, but is not-isomorphic to N*.= =20 What this means is that the statement "I am (isomorphic to) the standard=20 natural numbers" is not absolute over all models of set theory. But the natural numbers are used to define such primitive notions as=20 "string", "formula", and "language". This means that, depending on what=20 ambient model of set theory we are working in, the "set of first order=20 fomulas in the langauge of (0,1,+,x)" is not absolute. Different ambient=20 universes will disagree over whether something counts as a formula. From an= =20 outside perspective, V* has formulas which look to us to be=20 infinite-length. But V* sees them as having finite length, generated by=20 only finitely many applications of logical operations. For example, there are well-formed terms in V* which look like 1+1+1+... = =20 ...+1+1+1+... ... +1+1+1+... ...+1+1+1+1+... ...+1+1+1+1, where there=20 are infinitely many 1's appearing here. This means that if you were to look= =20 at the "models of PA" in V*, *all *of them would be non-standard from our= =20 outside perspective, because they would all have to interpret the term=20 1+1+1+... ...+1+1+1+... ... +1+1+1+... ...+1+1+1+1+... ...+1+1+1+1. So= =20 definitions like "the initial model of PA" won't work like we expect in V*. This means if we hoped to somehow use first-order logic to pin down the=20 natural numbers, we find ourselves not even being able to pin down the=20 language of arithmetic. We cannot define the language of arithmetic without= =20 first defining something like the natural numbers, and we cannot define the= =20 natural numbers without defining something like the langauge of arithmetic.= =20 How do set theorists fix this in practice? Well, they restrict to focus=20 only on what are known as "transtive" models of set theory. To do this,=20 they essentially need to fix a "standard" model of set theory, V, and then= =20 only look at models of set theory which, roughly, agree with V about the=20 element-of relation. But if we were skeptical about fixing a standard model= =20 of the natural numbers, we surely should be skeptical about fixing a=20 standard model of set theory, as this is much stronger. Another fix is to move to second-order logic. But this is basically the=20 same as fixing a standard model V of set theory, which again is much=20 stronger (thus philosophically less justified) than just fixing a standard= =20 model of PA. Whenever you have inductive types, you are of course in the background=20 assuming that you have a standard model N of arithmetic. Because if you=20 don't assume this, then it is ambiguous what the initial model should be,= =20 or even what counts as a model at all.=20 One of the lessons from Godel should be that there is no way of removing=20 this ambiguity which does not itself introduce more ambiguity. James Moody ------=_Part_16778_1164483579.1525251158617 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Just a comment on this:

This is one of the reasons why I have some problems to trust proof= s of properties of natural numbers formalized in CIC : Are some people =E2= =80=9Cproving=E2=80=9D properties of natural numbers that are already assum= ed in order to define CIC ?

This is= a general foundational problem, which exists even for first-order logic. I= t is impossible to avoid circularity entirely in foundations.

There = are models of ZFC which have a non-standard version of the natural numbers = (easy to construct by compactness theorem, if we really believe ZFC is cons= istent). Let's pick such a model V*, and this non-standard version of t= he natural numbers N*. Then inside V*, it evaluates to true that ``N* embed= s into every other model of PA, and every model of PA which embeds into N* = is isomorphic to N*". From outside V*, however, we see that the standa= rd natural numbers, N, embeds into N*, but is not-isomorphic to N*.
What this means is that the statement "I am (isomorphic to) the stand= ard natural numbers" is not absolute over all models of set theory.
But the natural numbers are used to define such primitive notions as &= quot;string", "formula", and "language". This mean= s that, depending on what ambient model of set theory we are working in, th= e "set of first order fomulas in the langauge of (0,1,+,x)" is no= t absolute. Different ambient universes will disagree over whether somethin= g counts as a formula. From an outside perspective, V* has formulas which l= ook to us to be infinite-length. But V* sees them as having finite length, = generated by only finitely many applications of logical operations.

= For example, there are well-formed terms in V* which look like 1+1+1+...=C2= =A0 ...+1+1+1+...=C2=A0 ... +1+1+1+...=C2=A0=C2=A0 ...+1+1+1+1+... ...+1+1+= 1+1, where there are infinitely many 1's appearing here. This means tha= t if you were to look at the "models of PA" in V*, all of = them would be non-standard from our outside perspective, because they would= all have to interpret the term 1+1+1+...=C2=A0 ...+1+1+1+...=C2=A0 ... +1+= 1+1+...=C2=A0=C2=A0 ...+1+1+1+1+... ...+1+1+1+1. So definitions like "= the initial model of PA" won't work like we expect in V*.

T= his means if we hoped to somehow use first-order logic to pin down the natu= ral numbers, we find ourselves not even being able to pin down the language= of arithmetic. We cannot define the language of arithmetic without first d= efining something like the natural numbers, and we cannot define the natura= l numbers without defining something like the langauge of arithmetic.
<= br>How do set theorists fix this in practice? Well, they restrict to focus = only on what are known as "transtive" models of set theory. To do= this, they essentially need to fix a "standard" model of set the= ory, V, and then only look at models of set theory which, roughly, agree wi= th V about the element-of relation. But if we were skeptical about fixing a= standard model of the natural numbers, we surely should be skeptical about= fixing a standard model of set theory, as this is much stronger.

An= other fix is to move to second-order logic. But this is basically the same = as fixing a standard model V of set theory, which again is much stronger (t= hus philosophically less justified) than just fixing a standard model of PA= .

Whenever you have inductive types, you are of course in the backgr= ound assuming that you have a standard model N of arithmetic. Because if yo= u don't assume this, then it is ambiguous what the initial model should= be, or even what counts as a model at all.

One of the lessons from= Godel should be that there is no way of removing this ambiguity which does= not itself introduce more ambiguity.

James Moody


<= /div> ------=_Part_16778_1164483579.1525251158617-- ------=_Part_16777_169223753.1525251158617--