Justify intuitionistic logic through the BHK interpretation could be problematic
还没有人认领这个 Issue。
评估
- 难度
- 5/5
- 预计耗时
- 一周以上
- 新手友好度
- 25/100
- Issue 类型
- 文档
- 描述清晰度
- 需要澄清
- 活跃度
- 停滞
- 技术栈
- tex
调研方向
该 issue 没有指出文件、测试或入口点。首先定位 OLT 的 BHK 论证，并将其与所引用的 van Dalen 和 Troelstra 的讨论进行比较。完成的标准是添加一份清晰且达成共识的说明，解释构造性函数或变换的含义，以及为什么经典解释并不充分。
由索引模型根据 Issue 内容生成。
描述
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.
- 主要语言
- TeX
- 星标
- 1.4k
- 派生
- 289
- PR 合并指标
- 30 天内没有已合并 PR
环境准备
这个项目没有提供开发容器、Dockerfile 或贡献指南，环境需要你自己搭建：先看它的 README，通用步骤见我们的新手贡献指南。
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
OpenLogicProject/OpenLogic 的其他 Issue
-
难度 1/5 1 小时以内 新手友好度 65/100
OpenLogicProject/OpenLogic#339 · 1 条评论 ·
-
难度 4/5 3-5 天 新手友好度 50/100
OpenLogicProject/OpenLogic#436 ·
-
难度 3/5 1-2 天 新手友好度 68/100
OpenLogicProject/OpenLogic#435 · 1 条评论 ·
-
难度 5/5 一周以上 新手友好度 30/100
OpenLogicProject/OpenLogic#425 · 1 条评论 ·
-
Improve docs未关闭
难度 5/5 一周以上 新手友好度 25/100
OpenLogicProject/OpenLogic#390 ·
查看 OpenLogicProject/OpenLogic 的全部 Issue
相似的 Issue
-
难度 1/5 1 小时以内 新手友好度 82/100
-
documentation good first issue hacktoberfest help wanted
难度 2/5 1-3 小时 新手友好度 78/100
Finntegrate/tapio#200 ·
维护者通常 1 天内回复
-
enhancement
难度 1/5 1 小时以内 新手友好度 88/100
-
难度 1/5 1 小时以内 新手友好度 88/100
-
[bug] README_CN.md 的通道清单缺 Telegram 与 Discord，与 README.md 不一致可能已有人在做 @sxh313 今天认领。 未关闭
难度 1/5 1 小时以内 新手友好度 62/100
TencentCloud/Octop#1768 · 1 条评论 ·
维护者通常 1 天内回复