[Agda] Hanging out with the Lean crowd

[Guillaume Brunerie]

Den lör 22 aug. 2020 kl 23:21 skrev <mechvel at scico.botik.ru>:
> Do you mean that you doubt in that question of "will F terminate or
> not?"
> is already solved somewhere?
> Well, if we doubt in that the F machine can run infinitely, then very
> naturally
> we doubt of that the above proof for the goal G is correct. Then the
> usage of EM
> is not safe in this case.

Indeed, I doubt that the question of "will F terminate or not?" is
already solved somewhere, as this requires infinite objects to exist
somewhere and I have no evidence of that.

> Well, I can write in Agda
>
> f =
>    case  isPrime? (2^(2^(2^1000)) + 7)
>    of \
>    { (yes _) -> true
>    ; (no _)  -> false
>    }
>
> where solving (IsPrime n) is by searching through all m < n and the
> division attempt
> for each m.
> Agda considers this as terminating, despite that computing f takes an
> unfeasible
> number of steps.
> Myself and Agda tend to consider this as terminating.
>
> What is your opinion: is its termination justified?

That’s a very interesting question, I’m not really sure what I think
about that yet, I have to think more about it.

> * I suspect that actual infinity exists in nature almost everywhere.
>    Observable values in quantum mechanics are somewhat said to be of a
> finite set.
>    But a wave mathematical description for particles is infinite, and it
> may occur
>    that this wave exists in reality, not only as idea.

It is maybe possible that wave functions do exist "in reality", but I
strongly suspect that if quantum mechanics uses infinite objects like
that, it is more by convenience than by conviction. It is much simpler
to reason about continuous objects than about very finely discretized
ones, and physics (i.e. mathematical modeling of reality) is all about
giving simplified models. Take for instance fluid dynamics, which
starts from the assumption that fluids are continuous, even though we
know that they are actually made of molecules. Or Newtonian mechanics,
which (mathematically speaking) contradicts special relativity. Or
essentially any other branch of physics, really. I don’t think that
many physicists studying quantum mechanics believe that wave functions
are real (or care about it). My guess is that they are mostly
interested by the fact that it approximates reality well enough (for
now).
Approximating "very large" by "infinite" (as you seem to be doing
several times in your email) is very reasonable from a practical point
of view, but seems problematic to me from a philosophical point of
view.

> * And even actual infinity does not exist in nature, it still exists as
> idea.
>    An idea of infinite objects helps to solve problems about finite
> objects.
>    The more it is helpful the more sure we are that it exists.
>    I suspect that it exists even independently of human's mind
>    (something like Plato is right).
>    And in what space does it exist, and in what precisely way, I wonder.

If you believe in platonism, then it is perfectly reasonable to
believe in the excluded middle indeed :)

Best,
Guillaume