A Proof-Theoretic Completeness Proof for Propositional Classical Core Logic

Abstract Alongside the sequent calculus for Classical Core Logic $${\mathbb {C}}^+$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>C</mml:mi> </mml:mrow> <mml:mo>+</mml:mo> </mml:msup> </mml:math> we set forth some new sequent calculi that we call $${\mathbb {T}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>T</mml:mi> </mml:math> , $${\mathbb {C}}^{++}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>C</mml:mi> </mml:mrow> <mml:mrow> <mml:mo>+</mml:mo> <mml:mo>+</mml:mo> </mml:mrow> </mml:msup> </mml:math> , and $${\mathbb {K}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>K</mml:mi> </mml:math> . $${\mathbb {T}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>T</mml:mi> </mml:math> encodes truth-tabular reasoning; $${\mathbb {C}}^{++}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>C</mml:mi> </mml:mrow> <mml:mrow> <mml:mo>+</mml:mo> <mml:mo>+</mml:mo> </mml:mrow> </mml:msup> </mml:math> classicizes Core Logic $${\mathbb {C}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>C</mml:mi> </mml:math> by having multiple succedents; and $${\mathbb {K}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>K</mml:mi> </mml:math> is a cut-free sequent calculus inspired by insights of Ketonen. Our aim is to establish that $${\mathbb {C}}^{++}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>C</mml:mi> </mml:mrow> <mml:mrow> <mml:mo>+</mml:mo> <mml:mo>+</mml:mo> </mml:mrow> </mml:msup> </mml:math> is weakly complete, and to do so in a way that makes no use of standard semantic notions or the rule of Cut. All the concepts defined and applied in the course of this study will be proof-theoretic, turning on rules of inference as meaning-constitutive. It is intended to be a contribution to the program of proof-theoretic semantics, from the distinctive vantage point of the Core logician.