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	Name	Meaning
−	U+2212	Minus sign	Denial: −A is the rejection of A
⟺	U+27FA	Long left-right double arrow	Coordination equivalence, as in +¬A ⟺ −A
⟹	U+27F9	Long rightwards double arrow	Bilateral consequence between signed formulas
¬	U+00AC	Negation	Object-language connective, governed by the denial rules
⊥	U+22A5	Falsum	Absurdity, discharged by the Smileian reductio rules
∨	U+2228	Disjunction	Object-language connective
∧	U+2227	Conjunction	Object-language connective
+	—	Assertion sign	Force marker: +A is the assertion of A
A, B	—	Formula variables	Unsigned sentences, to which a force marker attaches

Metatheory. Rumfitt's bilateral natural deduction is sound and complete for classical propositional logic under the obvious semantics for signed formulas: +A is correct iff A is true, −A iff A is false. The interest of the result is proof-theoretic rather than model-theoretic. Dummett's argument for intuitionism held that classical negation has no introduction and elimination rules in harmony, so classical logic cannot be justified by rules of use; Rumfitt's response is that the rules must govern two forces, not one, and that once they do, negation is given by the pair of clauses +¬A from −A and −¬A from +A, which are in harmony. Classicality is then supplied by the coordination principles, which state that assertion and denial of the same content are both incompatible and jointly exhaustive, and by the Smileian reductio rules that discharge a signed assumption on deriving absurdity. Excluded middle is derivable from these, not assumed.

Applies to. Proof-theoretic semantics. Justification of deduction. Inferentialism. Assertion and denial in speech act theory. Paraconsistent and paracomplete systems. Debates over classical versus intuitionistic logic.

Limitations. Bilateralism by itself settles no logic. Weakening the coordination principles yields paraconsistent bilateral systems such as LP and ST, so classicality is carried entirely by those principles and not by the two-force architecture advertised as doing the work. The principles are also where the dispute lies: the reductio rule inferring +A from a derivation of absurdity out of −A is a form of the very inference an intuitionist rejects, which is why the defence has been charged with begging the question. Force markers cannot embed — there is no well-formed +(+A → B) — so the system inherits the Frege–Geach problem in full and gives no compositional account of asserted or denied content in embedded position. And no independent criterion distinguishes denying A from asserting ¬A, which the theory needs if denial is to be primitive. The system is propositional; the quantifiers are not part of it.