[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

Guillaume,

thank you for explaining things in simple words.


On 2020-08-22 18:21, Guillaume Brunerie wrote:
> [..]

> 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.


Whether Nature, and our life, is finite or not, I doubt.
But surely they are not provably finite. We cannot fully measure and 
describe
the system of atoms and their possible states in most real objects, for 
example,
a mouse or a bee. An bee, a flower, and a virus are very infinite 
objects for us.
?


> 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).

Does this mean that using EM in this case assumes that someone is able 
to run
the machine F through the infinite Nat set in a finite time?
(actual infinity?).

Probably a EM proof in this case presumes that the question of "will F 
terminate or not?"
is already solved somewhere in the Nature. We do not know is it solved 
to "yes"
or "no". But as it is solved somewhere, we decide that the machine F 
_has result_.
and hence, it is in only in the set {yes, no}.

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.

If so, then the question of "What can be the third case" occurs 
senseless.
Because even the statement of the second case, "F never stops" occurs 
senseless.
?

On the other hand, compare this to the example with the lottery reel 
with balls inside.
In one minute this system runs through practically infinite number of 
states,
with unpredictable result. Nevertheless you can discourse like this
"If it returns an even number, then I do variant (1), and reach the 
goal.
  If it returns an odd number, then I do variant (2), and reach the goal.
  So the goal will be reached in any case.
".
Can you reason this way?
Is this relying on unsafe excluded middle?



> 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?

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?

Well, this doubt about actual infinity gives indeed more weight to the 
area of constructive
mathematics.


> Constructive type theory solves the question of infinity in a
> different way.
> [..]
> it is possible to construct new natural numbers
> [..]

All right, it assumes a potential infinity.


> 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.

The only way out is to develop both theories.
Evidently the theory with actual infinity is more fruitful.
But it is interesting to investigate the possibilities and bounds of the 
theory
with only a potential infinity.


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


Yes, this looks like something essential. Thank you.

I thought earlier of something of this sort, but after years of 
programming in Agda
have somehow forgotten the discourse.

* 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.

* 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.


Regards,

--
SM