[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-22 17:36, Nicolai Kraus wrote:
> [..]
> 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 think, the given naive  _proof for the goal G_  for this algorithm is 
not constructive,
it relies on the unsafe usage of excluded middle. Namely, a part of the 
process of the
lottery game is hidden from Naive Person and even from the organizers. 
For example, one
cannot observe all the details of the process of balls rolling inside 
the reel.
To decide/predict on the win is even less possible than to decide on  
(Exsts? n such that P n)
where P is the problematic predicate on Nat of which I wrote earlier.
The rule of 72 hours does not help, because the game process in the reel 
is not predictable
and runs through practically infinite set of stages.
This is similar as to run through all Nat in 72 hours and to decide P 
about each n.

This was what I meant. I assumed these details, but probably needed to 
spell them more
explicitly.

I say "unsafe usage" because there also is a safe usage of EM - when the 
predicate P is
solvable.

So, do I confuse something about logic?
a) Do people agree that the given earlier naive discourse about the 
machine F for
    (Exsts? n such that P n) bases on the unsafe usage of excluded 
middle?
b) Do people agree that the above naive discourse about lottery bases on 
the
    unsafe version of excluded middle?

The lottery example is a live version of this earlier example with 
natural numbers.
I tried to demonstrate that people who pay attention to restrict EM in 
mathematics always
rely on this "unsafe" proof tool in their life.


> Same here:
> 
> On Sat, Aug 22, 2020 at 2:20 PM <mechvel at scico.botik.ru> wrote:
> 
>> 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!
> 
> Again, a perfectly fine algorithm. No need for excluded middle at all.
> 

Again, I mean that the goal proof uses EM in unsafe version.
Because one cannot provably predict what case will happen: (1) or (2).
The result of (1) or (2) is formed as a result of practically infinite 
number
of composed events happening before 15.00.
One only naively assumes that {(1), (2)} is a full set of possible 
outcomes of this
process.

So, is it similar to my example with (Exists? n such that P n) ?

Thanks,

------
Sergei