Dual-Intuitionistic and Bi-Intuitionistic Logic

Origin. C. Rauszer, "A formalization of the propositional calculus of H-B logic" (1974) and the series through 1980, which gave Heyting–Brouwer logic with both implication and co-implication; the dual fragment alone is Goodman's (1981) and Urbas's (1996). McKinsey and Tarski's closure algebras (1946) are the algebraic ancestor. Crolard (2001) gave the type-theoretic reading; Pinto and Uustalu (2009) the sequent calculus.

Models. Intuitionistic logic is paracomplete: p ∨ ¬p fails because a proof of the disjunction requires a proof of a disjunct. Turn the semantics upside down — read the Kripke order backwards, take refutation as primitive — and you get a logic that is paraconsistent: p ∧ ¬p is satisfiable, because a refutation of the conjunction requires a refutation of a conjunct. The dual of a gap is a glut, and the duality is exact.

Formalism.

Co-implication (subtraction, exclusion): A ⤙ B — "A excludes B", the dual of A → B. Adjunction: A ≤ B ∨ C iff A ⤙ B ≤ C where implication has: A ∧ B ≤ C iff A ≤ B → C One residuates ∧ from above; the other residuates ∨ from below.

Co-Heyting (Brouwerian) algebras: A bounded distributive lattice with ⤙ satisfying the co-residuation law. The order-dual of a Heyting algebra. Co-negation: ∼A = 1 ⤙ A. Then A ∨ ∼A = 1 fails to be the issue — instead A ∧ ∼A ≠ 0. The boundary ∂A = A ∧ ∼A is nonzero in general: in the co-Heyting algebra of closed sets of a topological space, ∂A is literally the topological boundary.

Kripke semantics: w ⊩ A ⤙ B iff ∃v ≤ w : v ⊩ A and v ⊮ B Backwards along the order, where → looks forwards.

Bi-intuitionistic logic (Rauszer's HB): Both → and ⤙ in one language. Complete for bi-Heyting algebras. Sound and complete for Kripke frames with the order read both ways.

The interpolation split: Propositional bi-intuitionistic logic has Craig interpolation (Kowalski and Ono 2017). The predicate logic fails it (Olkhovikov and Badia 2022), though predicate IPC has it. Putting → and ⤙ together destroys interpolation at first order.

Cut elimination: Rauszer's original sequent calculus had a defective cut-elimination proof. Pinto–Uustalu (2009) gave a correct one using labelled sequents; the naive calculus does not have cut elimination.

Symbols.

Symbol	Unicode	Name	Meaning
⤙	U+2919	Leftwards arrow-tail / Co-implication	A ⤙ B: A excludes B; dual of →
∼	U+223C	Tilde operator / Co-negation	∼A = 1 ⤙ A
∂	U+2202	Partial differential / Boundary	∂A = A ∧ ∼A; the topological boundary in the algebra of closed sets
≤	U+2264	Less-than or equal to	The order of the (co-)Heyting algebra
→	U+2192	Rightwards arrow / Implication	Residuates ∧ from above; looks forwards along the Kripke order
¬	U+00AC	Not sign / Negation	Intuitionistic negation, as in the failure of p ∨ ¬p
∧	U+2227	Logical and / Conjunction	Meet; residuated by →
∨	U+2228	Logical or / Disjunction	Join; co-residuated by ⤙
⊩	U+22A9	Forces	w ⊩ A: support at a point of the frame
⊮	U+22AE	Does not force	Used in the co-implication clause
∃	U+2203	There exists	The co-implication clause looks backwards for a witness
0	—	Bottom element	The least element of the lattice
1	—	Top element	The greatest element; ∼A = 1 ⤙ A
A, B, C	—	Formula metavariables	Also range over algebra elements
w, v	—	Points	Of the Kripke frame, with v ≤ w
HB	—	Heyting–Brouwer	Rauszer's bi-intuitionistic system
IPC	—	Intuitionistic propositional calculus	The forward half of Rauszer's HB

Metatheory. The exact duality is the point: intuitionistic logic's paracompleteness and dual-intuitionistic logic's paraconsistency are the same fact read in opposite directions, which is the cleanest available answer to whether paraconsistency and constructivity are opposed — they are dual, not opposed. The co-Heyting boundary operator ∂A = A ∧ ∼A being the topological boundary in the algebra of closed sets is the duality made concrete: intuitionistic logic lives in the open sets and its dual in the closed ones, and the closed sets have nonempty boundaries. That Craig interpolation survives the combination propositionally (Kowalski and Ono 2017) yet fails at first order (Olkhovikov and Badia 2022) is the field's standing surprise, and the failed cut-elimination proof that stood for thirty-five years is the second.

Applies to. Paraconsistency's relation to constructivity. Co-Heyting algebras and the topology of closed sets. Bi-intuitionistic type theory, where ⤙ types coroutines and delimited continuations (Crolard). Refutation-based reasoning. The Heyting division, whose variety this is the dual of.

Limitations. Co-implication has no natural reading: "A excludes B" is a gloss on a residuation law, not a meaning anyone had first, and dual-intuitionistic logic is a formal object with no Brouwer behind it despite the name. Craig interpolation fails at first order, so the combined predicate system loses metatheory that predicate IPC has. And Rauszer's cut elimination was wrong for three decades, which suggests the sequent presentation is fighting the semantics rather than expressing it.