命题逻辑中的等式同构拓展证明
摘要：在System I中，等价命题（如$Awedge B$和$Bwedge A$，或$ARightarrow(Bwedge C)$和$(ARightarrow B)wedge(ARightarrow C)$）被认为是相等的，System I具有强规范化属性。这足以证明空类型的存在，但无法证明引入性质（每个正规形式的闭合项都是引入项）。此外，为了得到空类型的存在，必须对变量的类型做出严格限制。我们在这里展示，向System I中添加$eta$-扩展规则可以去除这个限制，并产生一个强规范的演算，该演算具有完整的引入性质。
作者：Alejandro D''iaz-Caro and Gilles Dowek
论文ID：2002.03762
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-09-01