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).
翻译:Sandqvist 提出了一种经典逻辑的证明论语义学,该语义学在不假定二值性的前提下阐释了联结词的意义。随后,他又为直觉主义命题逻辑提供了一种语义学。尽管在这两种情况下,可靠性都通过标准技术得以证明,但经典逻辑的完备性证明复杂且有些晦涩,而直觉主义命题逻辑的完备性证明则清晰而简洁。Makinson 通过将证明论语义学直接与该逻辑现有的真值函数语义学联系起来,给出了经典命题逻辑完备性的一个简化证明。在本文中,我们利用应用于直觉主义命题逻辑的技术,给出了一种关于经典逻辑证明论语义学完备性的初等、构造性且本原的证明——所谓本原,是指它不预设经典逻辑的模型论解释。同时,我们给出了一阶直觉主义逻辑的可靠性与完备性证明。