[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-22 03:57, Martin Escardo wrote:
> [..]
> On 22/08/2020 00:11, mechvel at scico.botik.ru wrote:
>> On 2020-08-21 23:21, Martin Escardo wrote:
>>> You don't think the model in which types are spaces and functions are
>>> continuous convincing enough? Excluded middle is not continuous.
>> 
>> Too abstruse, unnatural.
> 
> It is actually quite natural: continuity says that "a finite amount of
> information about the value of a function depends only on a finite
> amount of information about the argument of the function".
> [..]

Martin, thank you for your attention.
I am going to look more closely into your explanation and
to try to understand the topological model for logic.
May be your topological explanation can be translated into some simple 
explanation.

But first we need to try to discover a simple explanation, desirably 
something
close to experience, may be, to physics.

To tell the truth, I suspect currently that there is not any fundamental 
reason to
restrict the excluded third law. As to the possibility to restrict it 
and to develop the consequences - all right, it may be an interesting 
area, just for curiosity. I consider
this possibility as important, usually some useful knowledge comes out 
from such
investigations "for curiosity".
Well, we can try to remove modus ponens, and see ...



>> It has sense to consider this only if simpler explanations are not 
>> found.

> Oh, with this I agree fully. There are suitations, indeed, such as the
> above, where simple explanations are not available.


a) For modus ponens - do we have intuition to assume it? even without 
topology?
    Why modus ponens is more reliable than excluded third?

b) I believe that important models always have simple description and 
explanation.

For example, Lobachevsky's plane is a simple model showing a certain 
important
independence in geometry.
I recall also the model showing that  forall n (1 + n = n + 1)  is not
true in variety for a certain simplest definition for _+_ on naturals
(I have seen such in a certain Huet's paper). It is also simple.

Meanwhile, let us address our basic intuition.

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.
Because you cannot provably predict whether (1) will hold or (2).
Also you do not and cannot demonstrate why (1) must hold, as you do not
and cannot describe the whole process of the lottery game and cannot
derive (1) from this. For the same reason neither you can demonstrate
why (2) must hold. It follows that not all cases are considered.
"

Naive Person>
"The ticket either wins enough or does not. The set {(1), (2)} of
  possible outcomes does not depend on what happens during the lottery 
game,
  neither it depends on whether anyone has proofs related to this 
process.
  So, what case besides (1) and (2) may happen?
"

Constructivist>
"I shall explain now.
  I cannot describe in simple words what third case may happen.
  Even no hint at all.
  But consider types and type constructions, and a certain correspondence
  between types and topological spaces. A topological space is a set V 
and
  a set of certain subsets in V, called open sets ... A continuous map is
  ...
"
??

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! You cannot provably predict whether (1) holds or 
(2).
  Please, recall the correspondence between types and topological spaces 
...
"
?

Regards,

--
SM