[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-21 08:38, Martin Escardo wrote:
> [..]
> Excluded middle is like parallel postulate in Euclidean geometry: if 
> you
> assert it, you get one kind of geometry, and if you negate it you get
> another kind. It is meaningless to ask whether the parallel postulate 
> is
> true. What you can ask is whether it is true in the particular geometry
> you are interested in. The same goes for EM and other classical 
> creatures.
> 

The matter is that so far nobody explained me that this is similar.

Because the possibility of removing the fifth postulate in geometry is 
accompanied
with various models for the remaining abstract theory.
For example, the Lobachevsky's plane is a hyperboloid H, in which 
"straight lines"
are put to be sections of H with Euclid's planes. And we see that all 
the postulates
are preserved except the fifth one. Because for any hyperbola G on H 
there and a point
P out of G there are visible many hyperbolas that contain P and does not 
intersect
with G - a certain cone of lines "parallel" to G.

I do not see such a convincive model for constructivism.
Suppose that excluded middle proof is removed (in a certain sense).
Consider the above search procedure F for n : Nat such that P(n)
in the example with searching a singular number.
In the classical philosophy:
"(1) either F terminates, and then A gives the proof of G,
  or
  (2) F does not terminate, and then B gives a proof for G.
"
This is equivalent to
"(1) exists (classically) n such P(n) ...  Or (2) does not exist n such 
P(n) ...".

And constructivism pretends that this is not a proof for G.
So, it says that it is not enough to consider these two possibilities
("terminates" or "never terminates").
As it is not enough, then how can it look any other possibility?

Lobachevsky's plane demonstrates at least one variant of "how can it 
look".
And I do not see such a demonstration in constructivism - for this 
particular
example.

--
СМ