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 surprise: Bi-intuitionistic logic fails Craig interpolation (Kuznetsov and Muravitsky; Crolard). IPC has it; the dual has it; putting them together destroys it. The failure was unexpected and is the system's best-known fact.

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.

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 combining the two destroys Craig interpolation 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, which costs the combined system most of the metatheory each half had. And Rauszer's cut elimination was wrong for three decades, which suggests the sequent presentation is fighting the semantics rather than expressing it.

© 2026 Lingenic LLC