User:Marc Schroeder/sandbox6

Co-implication

Subtraction, Exclusion
Definition	$x\not \to y$
Truth table	$(0100)$
Logic gate	File:NOT IMPLY ANSI.svg
Normal forms
Disjunctive	${\overline {x}}\land y$
Conjunctive	$(x\lor y)\land ({\overline {x}}\lor y)\land ({\overline {x}}\lor {\overline {y}})$
Zhegalkin polynomial	$y\oplus xy$
Post's lattices
0-preserving	yes
1-preserving	no
Monotone	no
Affine	no
Self-dual	no

Co-implication, denoted $A\not \leftarrow B$, is a binary logical connective used in co-intuitionistic logic, which is a dual to intuitionistic logic. While implication $A\to B$ is false iff $A$ is true and $B$ is false, co-implication $A\not \leftarrow B$ is true iff $A$ is true and $B$ is false.

So it captures the failure of implication.

It has applications in theories of information removal, relevance, and resource-sensitive logics.

Syntax

The co-implicational fragment is formed from propositional variables and the binary connective $\not \leftarrow$. The well-formed formulas are:

1. Each propositional variable is a formula.
2. "$\bot$" is a formula.
3. If $A$ and $B$ are formulas, so is $(A\not \leftarrow B)$.
4. Nothing else is a formula.

In co-implicational logic, standard logical operators can be defined using only $\not \leftarrow$ and $\bot$:

$${\begin{aligned}\neg A&\ {\overset {\text{def}}{=}}\ \bot \not \leftarrow A\\A\lor B&\ {\overset {\text{def}}{=}}\ (\bot \not \leftarrow A)\not \leftarrow B\\A\land B&\ {\overset {\text{def}}{=}}\ \bot \not \leftarrow ((\bot \not \leftarrow A)\not \leftarrow B)\\A\leftrightarrow B&\ {\overset {\text{def}}{=}}\ ((A\not \leftarrow B)\not \leftarrow \bot )\land ((B\not \leftarrow A)\not \leftarrow \bot )\end{aligned}}$$

Truth table

From a classical semantic perspective, material co-implication is the binary truth functional operator which returns "true" iff its first argument is true and its second argument is fals. This semantics can be shown graphically in the following truth table:

$A$	$B$	$A\not \leftarrow B$
F	F	F
F	T	F
T	F	T
T	T	F

One can also consider the equivalence $A\not \leftarrow B\equiv \neg (A\to B)\equiv A\land \neg B$.

Kripke semantics

Co-intuitionistic semantics is dual to that of intuitionistic logic and is often defined using dual Kripke frames, where falsity rather than truth is persistent across worlds. In co-intuitionistic logic, the semantics of the co-implication connective ($\not \leftarrow$) is formulated using a variant of Kripke semantics, dual to that used for intuitionistic logic.

Let $(W,\leq ,\Vdash )$ be a Kripke frame, where

• $W$ is a set of worlds,
• $\leq$ is a partial order (accessibility relation),
• $\Vdash$ is the forcing relation.

The semantics for the co-implication (also called subtraction) connective $A\not \leftarrow B$ is:

Co-implication is not about excluding A in the past — it’s about assuming A is true now and ruling out B in all past worlds. That is:

$w\Vdash A\prec B\iff w\Vdash A\;{\text{and}}\;\forall v\leq w,\ (v\Vdash B\Rightarrow v\Vdash \bot )$

This captures the idea that:

• A holds at the current world;
• B is inconsistent with any past state (constructively “refuted”).

Restall’s —more loneral—version allows co-implication to hold if there is at least one accessible past world that refutes B.

Summary: Direction and Condition

Connective	Accessibility Direction	Semantic Condition
$A\to B$ (Implication)	future worlds $v\geq w$	$\forall v\geq w,\ (v\Vdash A\Rightarrow v\Vdash B)$
$A\prec B$ (Co-implication)	past worlds $v\leq w$	$w\Vdash A{\text{ and }}\forall v\leq w,\ (v\Vdash B\Rightarrow v\Vdash \bot )$

2. Semantics Determines Validity

Restall proposes a different Kripke clause:

• Standard:

$w\Vdash A\prec B\iff w\Vdash A\land \forall v\leq w,(v\Vdash B\Rightarrow v\Vdash \bot )$

• Restall:

$w\Vdash A\prec B\iff w\Vdash A\land \exists v\leq w,(v\Vdash B\Rightarrow v\Vdash \bot )$

So: Same rules, different model validation, ⇒ different theorems are valid.

The same natural deduction rules for co-implication (e.g., subtraction, $A\prec B$) can be interpreted in different ways, depending on the semantics you choose.

That is:

• The syntax of the ND rules stays the same
• But the logic they generate (i.e. the set of valid theorems) differs depending on the underlying Kripke semantics

This is not a mistake — it’s a feature of how proof theory and model theory relate in intuitionistic logic.

Analytic Tableau Rules

The semantic tableaux method for co-implication mirrors that of implication but dualized:

In classical logic the validity of co-implication formulas can be semantically established by the method of analytic tableaux. The logical rules are

${\frac {{\boldsymbol {\mathsf {F}}}(A\not \leftarrow B)}{{\boldsymbol {\mathsf {F}}}(A)\quad \mid \quad {\boldsymbol {\mathsf {T}}}(B)}}$	${\frac {{\boldsymbol {\mathsf {T}}}(A\not \leftarrow B)}{\begin{array}{c}{\boldsymbol {\mathsf {T}}}(A)\\{\boldsymbol {\mathsf {F}}}(B)\end{array}}}$
${\boldsymbol {\mathsf {T}}}(\bot )$ : Close the branch (contradiction) ${\boldsymbol {\mathsf {F}}}(\bot )$ : Do nothing (since it just asserts no contradiction)

These rules are dual to the tableaux rules for implication in intuitionistic logic.

Natural Deduction Rules

A natural deduction system for co-implication includes the following introduction and elimination rules:

Co-implication Introduction ($\not \leftarrow I$)	Co-implication Elimination ($\not \leftarrow E$)
${\frac {A\qquad {\begin{array}{l}[B]\\\vdots \\\bot \end{array}}}{A\prec B}}\quad (\prec I)$ $[B]$ is an assumption that is discharged when applying the rule. Note: $A$ must be derivable independently or already known — this is not an implication in the direction $B\to \neg A$, but a negation of the joint possibility of $A$ and $B$.	${\frac {A\not \leftarrow B\quad A}{\bot }}$ ${\frac {A\quad A\not \leftarrow B}{\bot }}$ This expresses that from $A\not \leftarrow B$ and $A$, $B$ must not be derivable — hence contradiction.

Duality with Implication

In bi-intuitionistic logic, both implication $\to$ and co-implication $\not \leftarrow$ coexist. Their dual roles relate to constructive reasoning (building from evidence) and subtractive reasoning (removing or denying assumptions). Together they give rise to a more symmetric proof theory and semantic structure.

See also

• Co-intuitionistic logic
• Bi-intuitionistic logic
• Implication (logic)
• Substructural logic
• Sequent calculus

References

• Crolard, Thomas (2001). "Subtractive Logic". Theoretical Computer Science. 254 (1–2). Elsevier: 151–185. doi:10.1016/S0304-3975(99)00422-1.
• Dzik, Wojciech (2013). "Notes on Bi-intuitionistic Logic and Kripke Semantics". arXiv:1305.3584. This paper examines bi-intuitionistic logic, which extends intuitionistic logic by adding dual connectives. It explores Kripke semantics with both forward-looking and backward-looking modalities, including universal quantification over predecessor worlds.
• Fernández-Duque, David; McLean, Brett; Zenger, Lukas (2023). "A Family of Decidable Bi-Intuitionistic Modal Logics" (PDF). In Marquis, Pierre; Cao Son, Tran; Kern-Isberner, Gabriele (eds.). Proceedings of the Twentieth International Conference on Principles of Knowledge Representation and Reasoning (KR 2023). International Joint Conferences on Artificial Intelligence Organization. pp. 262–271. doi:10.24963/kr.2023/26.
• Pinto, Luís; Uustalu, Tarmo (2009). "Proof Search and Counter-Model Construction for Bi-Intuitionistic Logic". In Baaz, Matthias; Fermüller, Christian G. (eds.). Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science. Vol. 5607. Springer. pp. 238–252. doi:10.1007/978-3-642-02716-1_22. ISBN 978-3-642-02715-4.
• Pym, David (2002). The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Vol. 26. Springer. doi:10.1007/978-94-017-0474-7. ISBN 978-1-4020-0482-7.
• Rauszer, Cecylia (1974). "Semi-Boolean algebras and their applications to intuitionistic logic with dual operations". Fundamenta Mathematicae. 83 (3): 219–249. ISSN 0016-2736. Retrieved 31 May 2025.
• Rauszer, Cecylia (1977). "Applications of Kripke Models to Heyting–Brouwer Logic". Studia Logica. 36 (1–2). Springer: 61–71. doi:10.1007/BF02121115.
• Rauszer, Cecylia (1979). "Dual intuitionistic logic". Studia Logica. 38 (4): 321–340.
• Rauszer, Cecylia (1980). An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic. Dissertationes Mathematicae. Vol. 167. Polish Academy of Sciences, Institute of Mathematics.
• Restall, Greg (14 August 1997), Extending Intuitionistic Logic with Subtraction (Technical report / preprint), Macquarie University, School of History, Philosophy and Politics
• Restall, Greg (2005). "Multiple Conclusions". In Hájek, Petr; Valdés-Villanueva, Luis; Westerståhl, Dag (eds.). Logic, Methodology and Philosophy of Science: Proceedings of the Twelfth International Congress. King's College Publications. pp. 189–205.
• Tranchini, Luca (2018). "Natural deduction for bi-intuitionistic logic". Journal of Applied Logic. doi:10.1016/j.jal.2017.12.001.
• Uustalu, Tarmo; Buisman, Linda; Goré, Rajeev (2007). "A Cut-Free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version". arXiv:0704.1707.
• Wansing, Heinrich, ed. (2005). Negation: A Philosophical and Logical Analysis. Logic, Epistemology, and the Unity of Science. Vol. 5. Springer. doi:10.1007/1-4020-3425-5. ISBN 978-1-4020-3425-1.