[Agda] Hanging out with the Lean crowd

[Martin Escardo]

On 22/08/2020 14:20, 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. 

I agree with you. As I tried to say, it depends on what you want to do
and what you are talking about.

Suppose it is your birthday today and I trying to figure out a present
for you.

You either like the Beatles or you don't particularly like them.

If you do, I can give you this vintage album I have that is considered
to be so valuable. If you don't, I'll explain constructive mathematics
to you instead.

But I don't know whether youuu like the Beatles, and so I can't use the
principle of excluded middle to decide which present I will give you.

Approximately:

  - Classical mathematics is the logic or truth.

  - Constructive mathematics is the logic of knowledge.

It may be true that "P or not P" holds.

But this is very different from knowing which of "P" or "not P" hold.

Consider e.g. P = Goldbach conjecture.

But also consider e.g. P = "all types satisfy the uniqueness of identity
principle (axiom K)".

There is a perfectly valid world of mathematics in which P is true. (The
default in Agda.)

But there is also a perfectly valid world of mathematics in which P is
undecided. (Just choose --without-K for your Agda programs.)

And here is also a perfectly valid world of mathematics in which P is
false. (Just choose --without-K and --cubical.)

In this example, you decide "P" or "not P" by an Agda flag, rather than
philosophy.

Just as you decide whether the parallel postulate holds or not by
choosing the geometry you want to study.

And just as you may study one geometry today and another one tomorrow,
you can program with "--with-K" today and with "--without-K and
--cubical tomorrow".

You can choose to live with "P" or to live with "not P". And this is not
a life choice. You can do mathematics (in some Agda files) with "P", and
also with "not P" (in other Agda files).

This particular example is rather perverse, actually, because "not P" is
more general than "P" !!! The world in which "not P" holds has a copy
inside it in which "P" holds: the subworld of hsets. (I am just trying
to confuse you.)

Best,
Martin