Bilateral Logic

Origin. Rumfitt (2000), Smiley. Assertion and denial primitive. Two speech acts. Rejection not just negation. Classical logic defended bilaterally.

Models. Both assertion (+) and denial (−) primitive. Negation from denial. Classical logic emerges. Intuitionistic objections answered. Meaning through use.

Formalism.

Two primitives: +A: assertion of A. −A: denial of A. Both independent speech acts. Not interdefinable.

Coordination principles: Cannot both assert and deny same. +A and −A incompatible. But exhaustive: must do one. Classical excluded middle recoverable.

Negation from denial: +¬A ⟺ −A. Assertion of negation = denial. Denial of negation = assertion. −¬A ⟺ +A.

Introduction rules: From +A to +A ∨ B (∨-intro). From +A and +B to +A ∧ B (∧-intro). From derivability of −A to +¬A (¬-intro).

Elimination rules: Standard classical. Reductio available. Excluded middle derivable. Full classical logic.

Against intuitionism: BHK interprets ¬A as A → ⊥. But denial is primitive act. Not derived from absurdity. Different speech act entirely.

Assertion/denial asymmetry: Both primitive but different roles. Assertion: commitment to truth. Denial: commitment to falsity. Symmetrical yet distinct.

Symbols.

Symbol	Unicode	Meaning
+	—	assertion sign
−	U+2212	denial sign
⟺	U+27FA	coordination
⟹	U+27F9	bilateral consequence

Metatheory. Speech act foundations. Classical justification. Anti-intuitionism. Meaning as use.

Applies to. Philosophy of logic. Classical logic defense. Speech act theory. Proof theory.

Limitations. Contentious foundations. Coordination justification. Against proof-theoretic semantics. Philosophical.