Proof-Theoretic Soundness and Completeness

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. 1 A Semantic Calculus for Intuitionistic Kripke Models In Rothenberg (2010), we use correspondence theory (Blackburn et al., 2001) to give a cut-free calculus for reasoning about intuitionistic Kripke models (Kripke, 1965) using a fragment of first-order classical logic. Definition 1 (Partially-Shielded Formulae). We define the partially-shielded fragment (PSF) of first-order formulae: (1) ⊥; (2) P{x} iff P is an atomic propositional variable, or an atomic first-order formula with a free variable x; (3) A{x}∧B{x} and A{x}∨B{x}, iff A{x}, B{x} are in PSF; (4) Rxy, where R is a fixed atomic binary relation (5) ∀y.(Rxy∧A{y}) → B{y}, iff A{x} and B{x} are in PSF.

• Type: Journal
• Year: 2011
• Where: CORR
• Authors: Robert Rothenberg
• Keywords: CORR 2011, Education, Intuitionistic Kripke, Intuitionistic Kripke Frames, Intuitionistic Kripke Models