[Agda] Hanging out with the Lean crowd

[Peter Hancock]

I'm sorry Sergey, I meant to send this to the Agda list rather than just you.
(Partly to see what Martin Escardo might respond). 

Peter Hancock

On 20/08/2020 23:06, Peter Hancock wrote:
>> As to me, my doubt about the constructive philosophy is as follows.
>>
>> We have a simple semidecision procedure F for finding an even natural number n > 2
>> which is not a sum of any two primes.
>> It is search-through, with checking each current n for this property,
>> where the check for n is by search-through among primes p < n.
>> It is a difficult problem to solve whether F terminates (whether the searched n exists).
>>
>> And suppose that we are proving a certain goal G by using the procedure F, as follows.
>> "(1) If such  n  exists (the search F terminates), then prove G in one way.
>>  (2) It such does not exist (the search is infinite), then prove B in another way.
>>  If so, then G is proved.
>> "
>> I cannot imagine: what can be wrong in this discourse.
>> In what way can it be possible the result R different from (1) and (2).
>> How may it look this R ?
>> The result of (1) or (2) exists in nature independently on whether we have shown
>> some witness or not.
> You may be arguing for Markov's axiom (MP). One way of putting it is I think
> that if a property P of natural numbers is decidable, then 
> ~(all n Pn) -> (exists n ~Pn).
> 
> It is a seductively mild form of excluded middle. 
> Friedman (see Wikipedia) proved most formal systems of constructive
> mathematics are closed under the corresponding rule. (Not sure how it is in type-theory,
> but vaguely recall Erik Palmgren proved something?? about that.) 
> 
> It is a source of non-terminating arguments about the "computational meaning" of 
> constructive mathematics (at conferences over beer).
> 
> Martin Escardo was once a virtuoso, and may still be, at playing the MP instrument.
> 
> --
> H