coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
Date: Sat, 05 May 2018 18:15:23 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:68ZNJxCCxA/XE5h2y87zUyQJP3N1i/DPJgcQr6AfoPdwSPv5pMbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzQisx+gqxUohGvqBJwzIHIb4+YL+Z+frrHcN8GWWZMRMRcWipcCY28dYsPCO8BMP5XoYn4plsOqRq+BQ60C+3r1DBInWXu3bYi3OogCw7G2AggEMwBsHTTtNr4KL0SUeGvw6nT0D7OaO1Z1Czy6YXLbhwtu/aMXah/ccfIz0QkCgDLjk2IpID4PD6Y1f4Bv3aF4+dhT+6jlmwqpxxrrjSyyMoglJHFi4EUx1ze9Ch0wpw5KNmiREJmfdKoDJ1dvDyAOYRsWMMtWWRotT46yrIYvZ67ezAHyZskyhLDcfCHdJKI4h37WOaQJzd3mm5ldaqiixux8kWs0PPwWte13VpQsyZIkMTAumoQ2xHd9MSLUv598V2g2TaL2QDT8OZEIUUsmKXFMJMgzb09moYJvUTEBC/2l136jLWKeUU85uio9+Pnb636qZ+bLo94kx3xMqAzmsOkGuk4KQgPX22D+eumzrHj/Ev5QK9LjvIsiKXZvoradownofubBBTUmqMq7QuyC3+c19gCnHYaIUANUxuNhoztNkvJaKT6Cuyym1SnlT5g7//DN7zlRJ7KKy6Qvq3meONQ7k9YyQ0E791EdYljJbgFJP/8XXjYrt3RFVdtPiSkk76hD89ygNBNEVmTC7OUZfuB+WSD4fgidrHVNd0l/Q3lIv1g3MbAyHowmFsTZ66sjMkHOCj+Ge5pcRzAPSjcx+wZGGJPhTIQCfTwgQzQQW4LIXGoUPBkv2xpOMedFY7GA7uVrvmB0SO8T89GNjgADUqDQy7l
Organization: X80 Heavy Industries

Hi José Manuel,

José Manuel Rodriguez Caballero
<josephcmac AT gmail.com>
writes:

> There should be a justification for the privilege of the standard model
> over the non-standard models of PA.

Again, I am not truly an expert here. I think the usual justification
for the privilege of the standard model is that it is the initial or
free one, that turns out to be quite convenient in Computer Science.

> To say that the memory of a computer is a standard natural number is a
> valid argument in some cases, but maybe this number is so huge that it
> is better to think about is as non-standard.

I am afraid I cannot understand what you mean here.

E.

Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), (continued)
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), roconnor, 05/03/2018