coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] 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: Siddharth Bhat <siddu.druid AT gmail.com>
Cc: "R. Pollack" <rpollack0 AT gmail.com>, Coq-Club Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
Date: Wed, 02 May 2018 18:53:00 +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:puHctR9PDDM4cv9uRHKM819IXTAuvvDOBiVQ1KB41uocTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RfQ8hRUCJBDI2+YIUMAeUOMvpXopLhp1cStxayGRWgCfntxzJOm3T43bc60+MkEQze0wIgGtMOsHDVrNXyLKgcVf66zLLS1TXYd/xY2C3y6IzMch8/rvGMWqp/fNbLyUkuDQzFlUibpIv7MD6O2eUAsHSX4/BnVeK1hG4qsgd8qSWsyMc0koTFm4EYx1Pe+Sln3oo4JMe0RFN5bNK5Cpdcqi+XO5VuTs4gQWxkojs2x7MHtJKhYSQHyI4rywDBZ/GFdYWD/wjtW/yLIThigXJoYLK/iAi28Uin0uD9Wcq53EpQoipCiNnMuWgB1x3V6seZVvtw5lqt1DWM2gzJ9O1IP0E5mbDGJ5Mj37I8jIcfvErdEiPunUX5lq6WdkEq+uiy7OTnZ63rqYGHOo57iQzyLr4imsulAeQ3KgQORXSU+fyg1L3/+k30WKlFjvovkqXArJ/aIdkbqbWiDg9O0ocj7g6/AC283NQZm3kHNlNFdwidg4jnIVGdaMz/WMy+j1ismS13x7jsPrT9SsHWL3TPjfHtZ6t852ZTzQMyyZZU4JcCWZ8bJ/emd0rwsN3fOT00KJ6v9MnuDNFw2YQpcHiOC7TRZK76oQ/QoOU1LL/fN8cupD/hJq19tLbVhngjlApYJPHxhMpFWDWDBv1jZn6hTz/pi9YFH30Nu1tsXLyyzlqYXmwKPirgb+cH/jg+TbmeI8LbXIn80qzRhGG8BJIEPjkbWGDJKm/hcsC/Y9lJaC+WJZ4zgmxcE7+7RN142A==
Organization: X80 Heavy Industries

Siddharth Bhat
<siddu.druid AT gmail.com>
writes:

> What is a "finite" but memory unbounded turing machine? Asking since I have
> never heard that term before :)

As far as I can tell this is just a standard Turing machine.

E.

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