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: "R. Pollack" <rpollack0 AT gmail.com>
To: 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, 2 May 2018 11:03:46 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rpollack0 AT gmail.com; spf=Pass smtp.mailfrom=rpollack0 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f180.google.com
Ironport-phdr: 9a23:bJ6s0BT9P8J6z89kpqNTa5rR39psv+yvbD5Q0YIujvd0So/mwa69YB2N2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRDDYOyb4UBAekPM/tGoYbhvFYBtweyCBO2Ce/z1jNFhHn71rA63eQ7FgHG2RQtE9wSvnjOsd77LqASUeSxzKbS0TrDbP1a0ir65YjSahAhpvWMXbZqfsXNykkjCxjIjlqVqYP/PjOV0v4BvHSc7+plTO+ijXMspQJpojW32Msglo3EipgWx13E7yl13pg5KcGiREJmYtOoDJ1dvDyAOYRsWMMtWWRotT46yrIYvZ67ezAHyJE9yB7eb/yLapGI4hH/WOqILzd0mXFodK6lixa99kigzeL8Vs2q31pQsiVFldzMumgM1xzV9MeHVuNw8lm91TuLzQze6eFJLVoqmabFN5It2KM8m5kPvUjbGy/5gkT2jKuYdkU+/eio7vzqYq/+pp+bM490jhvxPbgtmsCjGuk4PQ0OUHKa+eS4zrHs4Ur5QLBSgv0sjqbZqIzaJdgcpqOhHwBV1Z8j5w+jADeizdQXhmIKLElFeRKCl4jmIUvCIPH+DfelglSjii1nx/7cPu6pPpKYBX/a1ZzlYLw1wEpBwkJnxtdGoplQF7spIfTpW0a3usaOXTEjNAnhidyhQO160ocXUmHFSvuDKKTWtVaD5boHLOyFZYtTszH4fat2r8XyhGM0zAdONZKi2oEaPTXhRqw/chepJEH0i9JEKl8k+w83TejkklqHCGcBaHO7XqZ67TY+Wtv/UdXzA7u1ibnE5x+VW4VMbzkfWF+JGHbsMY6DXqVUMX/AEopaijUBEIOZZcoh2BWp7lGozrNmKq/N+XVdu8uzjJ564OrckRx0/jtxXZyQ

Emilio says:

It is my understanding that his views were influenced by Edward Nelson
which were quite radical AFAICT. IIRC, at some point Nelson wrote a
"theorem prover" and claimed to have found a proof of "PA ⊢ ⊥", but it
seems it was not correct.

Nelson was not as nutty as this might suggest. He took the view that natural number induction is not predicative, because one quantifies over all natural numbers. In his classic monograph "Predicative Arithmetic" he discusses formal systems that are predicative in his sense. IIRC such systems do not prove totality of exponentiation, so Godel's Theorem may be unprovable.

--Randy

[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), ikdc, 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), 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), Arthur Azevedo de Amorim, 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), 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), Siddharth Bhat, 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), Andrej Bauer, 05/02/2018
    - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Adam Chlipala, 05/02/2018
      - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Jose 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), Adam Chlipala, 05/02/2018