[Agda] Hanging out with the Lean crowd

[Thorsten Altenkirch]

On 20/08/2020, 23:23, "Agda on behalf of Nicolai Kraus" <agda-bounces at lists.chalmers.se on behalf of nicolai.kraus at gmail.com> wrote:

    On 20/08/2020 22:28, Jesper Cockx wrote:
    > What can be annoying are the people who are convinced non-constructive 
    > mathematics is the right tool for *every* job.

    Agreed. Those, and the people who are convinced that constructive 
    mathematics is the right tool for every job.

This sounds a bit like "All lives matter" as a response to "Black lives matter".

In the moment constructivism is a minority position and nobody (including myself) have ever suggested that Mathematicians should immediately abandon classical Mathematics and work only constructively. All what we have suggested is an awareness of the issue of constructivity.

I do believe that philosophically constructivism is preferable, because the idea that mathematical concepts are like real objects (Platonism) seems rather far fetched to me. Hence it seems sensible not to talk about truth but evidence. 

People have said that this is a religious debate. First f all it is interesting that only minority positions are being accused of being religious, as long as you are on the mainstream you are fine. Second I do think it is possible to have a rational discourse about foundations, and this has nothing to do with religion.

Thorsten





    -- Nicolai
    _______________________________________________
    Agda mailing list
    Agda at lists.chalmers.se
    https://lists.chalmers.se/mailman/listinfo/agda




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.