[Agda] Hanging out with the Lean crowd

Sat Aug 22 17:21:34 CEST 2020

Hi all,

Let me participate in this debate and share my opinion as well, which
is maybe more philosophical than practical.

I personally see constructivism as being very much based on reality
and physics, much more than classical mathematics which lives in a
completely imaginary world that requires a huge leap of faith to
believe the existence of.
Let me explain.

For all we know, our observable universe is finite, be it on a large
scale (we only see a finite volume of the universe) or on a small
scale (Planck constants and such). I’m sure this is an outrageous
oversimplification of physics, but in any case I believe that there is
no way we can, or ever will, observe or experience something truly
infinite.
Yet, classical mathematics takes for granted that infinite sets exist.
The set of natural numbers, which is considered quite small in
mathematics, is actually *infinitely* larger than the entirety of our
universe, no matter how you measure it! Understand that "infinite" is
really much much bigger than "finite", even for a very large version
of "finite" (maybe that’s where other people may have a different
opinion and decide to approximate "very large" by "infinite"). So my
point here is that I see the belief in the existence of infinite sets
as an act of faith, absolutely not based on reality, and absolutely
non-trivial.
Not that there is anything wrong with that, you are free to believe
whatever you want, but I still find it a bit strange to
unconditionally accept the existence of infinite sets given that our
entire experience of life is finite.

Now let’s look at Sergei’s example about distinguishing whether a
program terminates or not. This essentially asks about the existence
of a natural number (the number of steps the algorithm would take to
terminate) satisfying some property P, and assumes that
- if such a natural number exists, we can prove G
- if none exists, we can prove G
But how do we know that such a natural number either exists or
doesn’t? It seems to me that the only way to justify this instance of
the excluded middle is to believe in the existence of the set of all
natural numbers which, as explained above, is a highly non-trivial
assumption (at least for me).

Here is another way to see it (maybe the "other possibility" that
Sergei is looking for).
Suppose that the algorithm does terminate, but that it would take a
very very long time, much longer than the lifetime of the universe,
even on a computer that is as fast as is theoretically possible
(taking into account physical limitations).
Is it really justified to say that the algorithm terminates, then? How
is that based on reality, if it is absolutely impossible that it would
terminate in reality?

Constructive type theory solves the question of infinity in a
different way. The type of natural numbers is very different from the
set of natural numbers in that it is not an infinite object at all, it
is simply a (finite!) description of how it is possible to construct
new natural numbers, and what you can do with them. But unlike the set
of natural numbers, the type of natural numbers does *not* collect all
such natural numbers before we even get started, so it does not
require us to believe in the existence of infinite objects.
Therefore, as there is no totality of all natural numbers anymore,
there is no reason to believe that either there exists a natural
number satisfying P or not.
And if you do want to show the existence of some natural number, then
you have to construct it (or at least explain how you would go about
constructing it) because that number does not exist a priori
(otherwise that would again imply the existence of an infinite
object), which is why constructive mathematics is constructive.
Similarly, deducing that a natural number exists from the fact that it
cannot not exist (double negation elimination) requires you to believe
that all natural numbers already exist to begin with, which is again
assuming the existence of infinite objects.

Anyway, I’m not sure if my explanation convinced anyone of anything,
but it is at least very convincing to me :)

Best,
Guillaume

Den lör 22 aug. 2020 kl 15:20 skrev <mechvel at scico.botik.ru>:
>
> On 2020-08-22 03:57, Martin Escardo wrote:
> > [..]
> > On 22/08/2020 00:11, mechvel at scico.botik.ru wrote:
> >> On 2020-08-21 23:21, Martin Escardo wrote:
> >>> You don't think the model in which types are spaces and functions are
> >>> continuous convincing enough? Excluded middle is not continuous.
> >>
> >> Too abstruse, unnatural.
> >
> > It is actually quite natural: continuity says that "a finite amount of
> > information about the value of a function depends only on a finite
> > amount of information about the argument of the function".
> > [..]
>
> Martin, thank you for your attention.
> I am going to look more closely into your explanation and
> to try to understand the topological model for logic.
> May be your topological explanation can be translated into some simple
> explanation.
>
> But first we need to try to discover a simple explanation, desirably
> something
> close to experience, may be, to physics.
>
> To tell the truth, I suspect currently that there is not any fundamental
> reason to
> restrict the excluded third law. As to the possibility to restrict it
> and to develop the consequences - all right, it may be an interesting
> area, just for curiosity. I consider
> this possibility as important, usually some useful knowledge comes out
> from such
> investigations "for curiosity".
> Well, we can try to remove modus ponens, and see ...
>
>
>
> >> It has sense to consider this only if simpler explanations are not
> >> found.
>
> > Oh, with this I agree fully. There are suitations, indeed, such as the
> > above, where simple explanations are not available.
>
>
> a) For modus ponens - do we have intuition to assume it? even without
> topology?
>     Why modus ponens is more reliable than excluded third?
>
> b) I believe that important models always have simple description and
> explanation.
>
> For example, Lobachevsky's plane is a simple model showing a certain
> important
> independence in geometry.
> I recall also the model showing that  forall n (1 + n = n + 1)  is not
> true in variety for a certain simplest definition for _+_ on naturals
> (I have seen such in a certain Huet's paper). It is also simple.
>
> Meanwhile, let us address our basic intuition.
>
> A naive person thinks
> "I shall buy a yacht. Let us call this goal G.
>   I reach the goal through buying a lottery ticket.
>   (1) If it wins enough, then I buy this yacht.
>   (2) If it does not win enough, then I sell my second home, and this
> gives enough
>       to buy the yacht.
>   In any case the goal G will be reached.
> "
>
> Constructivist>
> "No, this is not for sure. This is not in any case.
> Because you cannot provably predict whether (1) will hold or (2).
> Also you do not and cannot demonstrate why (1) must hold, as you do not
> and cannot describe the whole process of the lottery game and cannot
> derive (1) from this. For the same reason neither you can demonstrate
> why (2) must hold. It follows that not all cases are considered.
> "
>
> Naive Person>
> "The ticket either wins enough or does not. The set {(1), (2)} of
>   possible outcomes does not depend on what happens during the lottery
> game,
>   neither it depends on whether anyone has proofs related to this
> process.
>   So, what case besides (1) and (2) may happen?
> "
>
> Constructivist>
> "I shall explain now.
>   I cannot describe in simple words what third case may happen.
>   Even no hint at all.
>   But consider types and type constructions, and a certain correspondence
>   between types and topological spaces. A topological space is a set V
> and
>   a set of certain subsets in V, called open sets ... A continuous map is
>   ...
> "
> ??
>
> Next day, Constructivist has to arrive to the airport before 16.00.
> He says
> "Let me go to the bus stop.
>   (1) If the bus comes to the stop before 15.00, then I take a bus.
>       This way it is cheaper.
>   (2) Otherwise, I call for taxi.
>   So that in any case I get to the airport in time.
> "
> His wife says:
> "There is a danger! You cannot provably predict whether (1) holds or
> (2).
>   Please, recall the correspondence between types and topological spaces
> ...
> "
> ?
>
> Regards,
>
> --
> SM
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda