[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-22 17:36, Nicolai Kraus wrote:
> Hi Sergei,
> 
> interesting examples. But I'm not sure they demonstrate what you want
> to show, at least I'm not so convinced. Our real world behaviour is
> actually pretty constructive, not classical.
> For example:
> 
> On Sat, Aug 22, 2020 at 2:20 PM <mechvel at scico.botik.ru> wrote:
> 
>> 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.
> 
> The "naive person" has given an algorithm, how can this not be
> constructive? There is no usage of the axiom of excluded middle. As a
> constructivist, I'm perfectly happy with this.
> Nitpicking: You also need to know that the result of the lottery will
> be announced, say, in no more than 72 hours (or no later than 2022).
> But again, reality and constructive intuition match. The naive person
> also would have to assume this for their plan, without knowledge of
> logic or anything.
> [..]


I tried to construct a simple example of using excluded middle in every 
day practice.

I thought that we can assume (let us assume) that one minute of the 
lottery process
in the reel with balls is in reality running infinite steps of a certain 
complex algorithm.
And so a) we cannot predict the result,
b) the result is ready in 1 minute,
c) the result is surely (let us assume) either No 7 or another number 0 
<= n <= 100,
    actually it is Boolean (result == 7  or  result /= 7).

Compare this to the example where the lottery is replaced with running 
the machine
F searching for a singular number in Nat.
The algorithm with F is surely based on excluded middle.
Right?
The difference is that there is not upper bound for the number of steps 
(time)
in running F, while the lottery ends in 1 minute.

But imagine that some interpreter runs F through all Nat in one minute.
Probably assuming that such an interpreter exists is equivalent to 
assuming that
the excluded middle holds. Because this will be something like a machine 
that
resolves in a finite time the truth for any statement.

Now, assuming that the lottery machine runs through infinite number of 
steps in one minute,
does this make the above algorithm with the lottery bases on excluded 
middle?
?

If yes, then there remains the question of whether the lottery machine 
can run through
infinite number of states in 1 minute. This reduces to the question of 
whether 1 minute
can be divided into any number of equal parts.
(?)

Regards,

--
SM