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)
Chronological Thread
- From: Andrej Bauer <andrej.bauer AT andrej.com>
- To: Coq 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: Tue, 1 May 2018 22:45:45 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andrej.bauer AT andrej.com; spf=None smtp.mailfrom=andrej.bauer AT andrej.com; spf=None smtp.helo=postmaster AT mail-io0-f173.google.com
- Ironport-phdr: 9a23:7BbpNhIhn0lkEStrldmcpTZWNBhigK39O0sv0rFitYgRI/TxwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJAXslTWSxPAo2yYYgSAeQfIelWoJLwp0cXrRakGQWgGP/jxz1Oi3Tr3aM6yeMhEQTe0QE8GdIBrW7Uo8v3NKwPTO261rTIwivZb/hL3jry8o7IfQ07of6SX7J8a9HexlMyFwzblFWdspbqPzWI2eQXrWeb7fBsWv6oi24isgx8pCWkyMQ0ioTRmI4Z1lTJ+T96zYs1P9G0VlB3bNC+HJdNtSyXOZN6Tt4mTmxmoio3yL8LtYSmcCUFy5kr3QPTZvKGfoWO/xntTvyeIS1ii3JgYL+/hwi98UynyuDkU8m7yldKri5cntnNsXABywXf6saaRvZ/8EqtwzmP1wfU6uFLJUA7i7DXJIImwr41jpYTsELDETHqmEjukqOaakEp9vKr5unneLnquIGQOoFuhg3jMKkjlNSzAeEiPQgPW2ib9/681Lrm/UDhWrpKiOA5krPHv5DYP8gUvbS2AxJL3YY58BuwFTGm38kCnXYZLlJJYg6Ij4/sO13WOvD3Ee+/g0iwkDds3/3JIrrhAozUInfflLfhYK1y5lVHyAszyNBf/4hbBqsAIPL1QE/xtcbXAgU3MwyukK7bD4BW0ZpWcmaSCOfNO6TL9FSM++gHIu+WZYZTtiyreNY/4Pu7pHk1g1IfNYOgwJYNICSxGPh8Lkffa3Pxj80pGGEGpAc8CuftjQvRAnZoe3+uUvdktXkAA4W8ANKGH9j12e3T7GKABpRTI1t+JBWJGHbseZ+DXq5WOiuULtVskHoPUr3zE9Z9hyHrjxfzzv9cFsSR4jcR7Mix3d55/eDR0xo18G4sVpnP4yS2V2hx21gwaXo20aR4+xIvz16C1e15hKQdG4UMvLVGVQA1MZOaxOt/WYj/
Dear José,
your post contains a number of inaccurate statements. Let me just
focus on this one:
> Coq cannot prove the consistency of PA: no one can do it (Coq is not
> supernatural, to say it in a funny way).
You seem to think that one can never prove the consistency of PA.
Already Gentzen showed the consistency of PA by using induction up to
ordinal ∊₀. Set theory ZFC can prove consistency of PA. CiC can prove
consistency of PA. The question is not whether consistency of PA can
be proved in some theory T, but how do we know that T itself is
consistent? So, there is a proof of consistency of PA in CiC. But to
prove consistency of CiC itself requires a still stronger theory. This
is all very well known and is not mysterious at all.
I recommend a textbook on proof theory that will counteract the
popular misrepresentations of Gödel's work that are all too easy to
find. Wolfram Pohlers published a textbook in 2008 which is also quite
detailed about inductive definitions. I do not know whether it covers
CiC, though, but it surely covers lots of related systems.
With kind regards,
Andrej
- [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Jose Manuel Rodriguez Caballero, 05/01/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Andrej Bauer, 05/01/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Matej Košík, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre-Yves Strub, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Matej Košík, 05/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), R. Pollack, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), R. Pollack, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre-Yves Strub, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
Archive powered by MHonArc 2.6.18.