[Agda] Hanging out with the Lean crowd

[Nicolai Kraus]

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.

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.

I'm tempted to also come up with such an example.

Naive person 1 (who believes in excluded middle): I need to make some
money. Tesla shares seem to be quite profitable lately, but I need to make
money by tomorrow. If Tesla goes up tomorrow, I buy today and sell the day
after tomorrow. If Tesla goes down tomorrow, I short sell today and bu back
the day after tomorrow. It either goes down or goes up tomorrow, and in
each case, I will have made a profit by the day after tomorrow.
Naive person 2 (who doesn't know anything about constructivism or classical
mathematics): What? Do mathematicians really believe that this will work?

-- Nicolai


On Sat, Aug 22, 2020 at 2:20 PM <mechvel at scico.botik.ru> wrote:

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200822/b093168d/attachment.html>