arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2410.11751math.LOcs.LO
收藏

一阶逻辑的证明论语义

Proof-theoretic Semantics for First-order Logic

Alexander V. Gheorghiu

AI总结:

本文为一阶经典逻辑的证明论语义提供了一种初等、构造性且原生的完备性证明,并同时给出一阶直觉主义逻辑的可靠性与完备性证明。

摘要:

Sandqvist 为经典逻辑(CL)给出了一种证明论语义(P-tS),该语义在不假设二值性的情况下阐明了连接词的含义。后来,他又为直觉主义命题逻辑(IPL)提供了一种语义。在这两种情况下,可靠性均通过标准技术加以证明,而 CL 的完备性证明复杂且略显晦涩,IPL 的完备性证明则清晰简单。Makinson 通过直接将 P-tS 与该逻辑既有的真值函数语义相关联,给出了经典命题逻辑(CPL)完备性的简化证明。在本文中,我们利用应用于 IPL 的技术,为 CL 的 P-tS 完备性给出了一种初等、构造性且原生的证明——即不预设经典逻辑的模型论解释。同时,我们给出一阶直觉主义逻辑(IL)的可靠性与完备性证明。

英文摘要:

Sandqvist gave a proof-theoretic semantics (P-tS) for classical logic (CL) that explicates the meaning of the connectives without assuming bivalance. Later, he gave a semantics for intuitionistic propositional logic (IPL). While soundness in both cases is proved through standard techniques, the proof completeness for CL is complex and somewhat obscure, but clear and simple for IPL. Makinson gave a simplified proof of completeness for classical propositional logic (CPL) by directly relating the the P-tS to the logic's extant truth-functional semantics. In this paper, we give an elementary, constructive, and native -- in the sense that it does not presuppose the model-theoretic interpretation of classical logic -- proof of completeness the P-tS of CL using the techniques applies for IPL. Simultaneously, we give a proof of soundness and completeness for first-order intuitionistic logic (IL).

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑