Proof-Theoretic Soundness and Completeness

8 years 8 days ago
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.
Robert Rothenberg
Added 13 May 2011
Updated 13 May 2011
Type Journal
Year 2011
Where CORR
Authors Robert Rothenberg
Comments (0)