A binary connective $\leftarrow$—known also as difference or subtraction—introduced by logician Cecylia Rauszer (1942–1994) as a formal dual to the intuitionistic conditional. To see this duality, recall that in Kripke semantics for intuitionistic logic, the truth condition for the conditional $\to$ at a world is:

• • $\phi \to \psi$ is true at $w$ if and only if for all worlds $w^{\prime }$ accessible from $w$ at which $\phi$ is true, $\psi$ is also true.

The corresponding truth condition for coimplication introduced by Rauszer is:

• • $\phi \leftarrow \psi$ is true at $w$ if and only if there is a world $w^{\prime }$ from which $w$ is accessible at which $\phi$ is true but $\psi$ fails.

Unlike intuitionistic implication, which admits myriad interpretations (e.g., the BHK interpretation), coimplication was not provided—and resists—a reasonable analogue in natural language. The most salient involves understanding the accessibility relation as describing succeeding stages in a scientific investigation, whence $\phi \leftarrow \psi$ is read as ‘at some stage in the investigation, $\phi$ held although $\psi$ did not’. Just as the intuitionistic conditional is employed in defining intuitionistic negation by the scheme $\neg \phi {=}_{df}\phi \to \perp$ (where $\perp$ is falsum), so does coimplication support a dualized form of negation (i.e., conegation) by the scheme $\sim \phi =\top \leftarrow \phi$ (where $\top$ is verum).