Proof-Theoretic Soundness and Completeness

2011/04/03 by Rothenberg, Robert
#03 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1104.0379

Abstract

We give a calculus for reasoning about the first-order fragment of classical logic that is adequate for giving the truth conditions of intuitionistic Kripke frames, and outline a proof-theoretic soundness and completeness proof, which we believe is conducive to automation.

Related

• Proof-theoretic Semantics for First-order Logic
• Yet another proof of Goedel's completeness theorem for first-order classical logic
• A completeness theorem in proof-theoretic semantics via set-theoretic semantics
• An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem
• Filling in the semantics for intuitionistic conditional logic