[Agda] Hanging out with the Lean crowd

[Louis Garde]

Le 22/08/2020 à 20:39, mechvel at scico.botik.ru a écrit :
> I tried to demonstrate that people who pay attention to restrict EM in 
> mathematics always
> rely on this "unsafe" proof tool in their life.
A proof is defined only within a formal system, defined by a fixed set 
of rules and axioms, whereas my life (and yours) is not governed by a 
fixed set of rules and axioms: intuitions from the real life are 
sometimes usefull, sometimes misleading !

Within a consistent set of rules and axioms, a proposition A is either 
true, false, or undecidable. Excluded middle makes sense when you have 
in mind a model in which every proposition is either true or false. But 
there are other models !

By adding excluded middle in a formal system with undecidable 
proposititions, you get rid of some of these "non-standard" models.
It is Ok for specific purposes, but when the formal system is used to 
define an algebraic structure, it just restricts the objects on which 
the structure can apply. Doing this systematically leads to a (very) 
restricted development of mathematics.

Adding EM without question is may be the symptom that in your intuition, 
a proposition is either true or false; but this is just wrong in most 
formal systems. Either you have some sort of Platonism point of view, 
and you think that this is the evidence that formal systems are not able 
to describe adequately the mathematical reality (whatever it can be). Or 
you have a more formal point of view and understand undecidability as a 
normal possible property of propositions. All points of view are 
welcome, provided we agree on what a mathematical proof is, and no 
restriction is made on the mathematics that can be done.
Banning EM from mathematics is of course an unacceptable restriction; 
but a theorem prover in which the use of EM cannot be controlled 
restricts also significantly the mathematics it can support.

Louis.