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
<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
<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
<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 <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
<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 <http://doi.org/10.4444/100>
> Am 11.05.2018 um 20:21 schrieb José Manuel Rodriguez Caballero
> <josephc...@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
> <https://web.math.princeton.edu/~nelson/books/pa.pdf>
>
>
> Kind Regards,
> José M.
>
>
>
> 2018-05-11 19:37 GMT+02:00 Jason -Zhong Sheng- Hu <fdhzs2...@hotmail.com
> <mailto:fdhzs2...@hotmail.com>>:
> Hi Siddharth,
>
> Long story short, there is a very suitable paper for this question:
> https://www.cs.cornell.edu/~kozen/Papers/Structural.pdf
> <https://www.cs.cornell.edu/~kozen/Papers/Structural.pdf>
> Practical coinduction - cs.cornell.edu
> <https://www.cs.cornell.edu/~kozen/Papers/Structural.pdf>
> www.cs.cornell.edu <http://www.cs.cornell.edu/>
> http://journals.cambridge.org <http://journals.cambridge.org/> Downloaded: 10
> Feb 2016 IP address: 104.229.211.75 Practical coinduction 3 Although there is
> a coinductive step but no basis, any difficulty that would arise that
>
> I personally find the two proofs on page 5 and 6 clearly illustrates the dual
> positions between induction and co-induction.
>
> It's not rarely to see in lots of papers that "accuse" co-inductive proof of
> being "uncommon' or "not standard", while co-induction is actually as strong
> as induction, but proves things that cannot be reasoned by induction, and
> they come hand in hand. It's a common phenomenon that people are much more
> familiar with one thing, but not its dual.
>
> I would prefer to think induction as a proof of "property P must hold", while
> co-induction as a proof of "property P cannot fail". In induction, we pretty
> much discuss two things: we show that P holds for all base cases, and then
> all other cases will eventually be reduced to those base cases, which
> requires the structure we look at must be finite.
>
> In co-induction, however, for every case we look at, either the information
> is sufficient to conclude P, or we must look at the tail. Here is the kick:
> in proper co-induction, we must have some constructor appear in the head
> position, which allows the cases to be covered by the previous proof that we
> begin with.
>
> Another way to look at them is, induction is a "sum" type of proof, which is
> divided by cases; while co-induction is a "product" type of proof, which is
> divided by fields from the same constructor.
>
> Sincerely Yours,
>
> Jason Hu <>
> From: coq-club-requ...@inria.fr <mailto:coq-club-requ...@inria.fr>
> <coq-club-requ...@inria.fr <mailto:coq-club-requ...@inria.fr>> on behalf of
> Siddharth Bhat <siddu.dr...@gmail.com <mailto:siddu.dr...@gmail.com>>
> Sent: May 11, 2018 1:13:54 PM
> To: Coq-Club Club
> Subject: [Coq-Club] I don't believe Coinduction; Please help me grok it :)
>
> This title is click-baity, but I believe it captures my feelings adequately.
>
> I am able to "believe" induction on, say, the naturals, since they have a
> well-founded order. Hence, one can intuit what it means to "perform
> induction" on these kinds of objects.
>
> On the other hand, how does a Coinduction proof "start"? Or, well, how does
> one intuit cofix ? I'm now able to perform the proofs in Coq, but I really
> don't feel like I understand them.
>
> The rough argument that I have in my head to justify Coinduction is as
> follows:
>
> 1. A Coinductive proof technique is used to prove a proposition P on
> functions that lazily produce infinite amounts of data.
> 2. We can only observe a finite amount of this infinite data
> 3. Hence, to prove a Coinductive proposition, we can assume our proposition P
> holds on the "infinite tail that is unobserved", and we show that adding some
> new finite data does not break the invariant P.
> 4. So, when someone "observes" this infinite data to some length, we can
> assume that the proposition P holds for the "part that remains unobserved",
> and "work our way backwards" to add all the finite pieces that were observed,
> while making sure P holds.
>
> How do the experts think about Coinduction? Is my intuition at all correct?
> I'd love help and feedback on this!
>
> Thanks,
> ~Siddharth
>
>
> --
> Sending this from my phone, please excuse any typos!
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
