The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

Dear José,

If it appears alone, impredicativity (self-reference) shouldn't be a problem.

I have tried to give some reasoning from a philosophical perspective here:

The two characteristics of an antinomy: self-reference and negation

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html

Similarly, not all mathematicians consider impredicativity (self-reference) as problematic.

For example, Freek Wiedijk doesn't seem to share the common view, as this rather

sceptical quote might indicate:

"Apparently impredicativity is not to be trusted for philosophical reasons." [Wiedijk, 2007, p. 127]

http://www.cs.ru.nl/F.Wiedijk/pubs/qed2.pdf, p. 7

My concern with induction is that it shouldn't be formalized in a way extending

the syntax, as it can be encoded in a perfectly natural way within the formal

(syntactic) language of higher-order logic.

The Principle of Mathematical Induction can simply be expressed in a definition,

see Andrews' definition of N in Q0:

"Noσ stands for [λnσ∀poσ 􏰀 [poσ0σ ∧ ∀xσ􏰀 poσxσ ⊃ poσ􏰀Sσσxσ] ⊃ poσnσ]"

[Andrews, 2002, p. 260], also available online at

http://www.owlofminerva.net/files/fom.pdf, p. 5

Peter Andrews explains: “The Induction Principle simply limits the size of the set.”

[Andrews, 2002, p. 259]

The definition of N in the R0 software implementation is available as wff 332 at

http://doi.org/10.4444/100.3, p. 370

The wff 333 is the well-formed formula with type abstraction (type variable t bound

by lambda).

I have to admit that I'm not too familiar with the details of Coq, but I believe that in it

induction is hardwired into the formal language (the syntax), which I consider problematic.

The rationale of expressing all of mathematics from very few means, which Andrews

calls "expressiveness", is discussed at

https://sympa.inria.fr/sympa/arc/coq-club/2017-02/msg00024.html

For references, please see: http://doi.org/10.4444/100.111

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

Am 11.05.2018 um 20:21 schrieb José Manuel Rodriguez Caballero <josephcmac AT gmail.com>:

Dear Siddharth,

  The mathematics is not a religion. The question is not if you believe or not. The question is to organize a hierarchy of consistency. I quote Bishop 1967, Chapter 1, A Constructivist Manifesto, page 2:

"The primary concern of mathematics is number, and this means the positive integers. . . . In the words of Kronecker, the positive integers were created by God. Kronecker would have expressed it even better if he had said that the positive integers were created by God for the benefit of man (and other finite beings). Mathematics belongs to man, not to God. We are not interested in properties of the positive integers that have no descriptive meaning for finite man. When a man proves a positive integer to exist, he should show how to find it. If God has mathematics of his own that needs to be done, let him do it himself."

In this wonderful book there is an explanation of why even "induction" is problematic because of impredicativity : https://web.math.princeton.edu/~nelson/books/pa.pdf

Kind Regards,

José M.