OpenLogicProject / OpenLogic

An open-source, customizable intermediate logic textbook
http://openlogicproject.org/
Creative Commons Attribution 4.0 International
1.06k stars 240 forks source link

Justify intuitionistic logic through the BHK interpretation could be problematic #288

Open feffemannen opened 2 years ago

feffemannen commented 2 years ago

Using the BHK interpretation to justify intuitionistic logic requires a discussion on what we mean by a "function" that transforms a construction of A to a construction of B. van Dalen and Troelstra writes (in Constructivism in Mathematics):

This exercise shows that the BHK-interpretation in itself has no "explanatory power": the possibility of recognizing a classically valid logical schema as being constructively unacceptable depends entirely on our interpretation of "construction", "function", "operation".

The OLT is justifying the ND-rules for intuitionistic logic using the BHK-construction, but a similar BHK based argument justifies the RAA rules as well (interpreting "function" as a classical set theoretic object).

I think this should be commented on in the text together with a discussion on what a constructive transformation could mean. I'm afraid I won't be able to do it good enough.