[Agda] Hanging out with the Lean crowd

[Martin Escardo]

You don't think the model in which types are spaces and functions are
continuous convincing enough? Excluded middle is not continuous. Martin

On 21/08/2020 14:30, mechvel at scico.botik.ru wrote:
> 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.
> 
> -- 
> СМ
> 
> 
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe