nLab ?-modality

 Idea

In linear logic and affine logic, the $?$-modality or the exponential disjunction is the de Morgan dual of the !-modality.

Examples

Antithesis interpretation

In the antithesis interpretation of affine logic into impredicative constructive mathematics, given the set of truth values $\Omega$, one can define a set of affine propositions by the set

$$\Omega_\pm \coloneqq \{(P^+, P^-) \in \Omega \times \Omega \vdash \neg (P^+ \wedge P^-)\}$$

The ?-modality is a function $?:\Omega_\pm \to \Omega_\pm$ is defined for each affine proposition $(P^+, P^-) \in \Omega_\pm$ by

$$?(P^+, P^-) \coloneqq (\neg P^-, P^-)$$

Theorem

The ?-modality is equal to the multiplicative disjunction of $(P^+, P^-)$ with itself

$$!(P^+, P^-) = (P^+, P^-) \invamp (P^+, P^-)$$

Proof

The multiplicative disjunction is given by

$$(P^+, P^-) \invamp (P^+, P^-) = ((P^- \Rightarrow P^+) \wedge (P^- \Rightarrow P^+), P^- \wedge P^-)$$

Given two propositions $P^+$ and $P^-$ such that $\neg (P^+ \wedge P^-)$, we have $\neg P^+ = P^- \Rightarrow P^+$. Since intuitionistic conjunction is idempotent, we have

$$(P^+, P^-) \invamp (P^+, P^-) = ((P^- \Rightarrow P^+) \wedge (P^- \Rightarrow P^+), P^- \wedge P^-) = (\neg P^- \wedge \neg P^-, P^- \wedge P^-) = (\neg P^-, P^-) = ?(P^+, P^-)$$

 Related concepts

• !-modality

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in logic$\phantom{-}$
$\phantom{A}$$\in$	$\phantom{A}$element relation
$\phantom{A}$$\,:$	$\phantom{A}$typing relation
$\phantom{A}$$=$	$\phantom{A}$equality
$\phantom{A}$$\vdash$$\phantom{A}$	$\phantom{A}$entailment / sequent$\phantom{A}$
$\phantom{A}$$\top$$\phantom{A}$	$\phantom{A}$true / top$\phantom{A}$
$\phantom{A}$$\bot$$\phantom{A}$	$\phantom{A}$false / bottom$\phantom{A}$
$\phantom{A}$$\Rightarrow$	$\phantom{A}$implication
$\phantom{A}$$\Leftrightarrow$	$\phantom{A}$logical equivalence
$\phantom{A}$$\not$	$\phantom{A}$negation
$\phantom{A}$$\neq$	$\phantom{A}$negation of equality / apartness$\phantom{A}$
$\phantom{A}$$\notin$	$\phantom{A}$negation of element relation $\phantom{A}$
$\phantom{A}$$\not \not$	$\phantom{A}$negation of negation$\phantom{A}$
$\phantom{A}$$\exists$	$\phantom{A}$existential quantification$\phantom{A}$
$\phantom{A}$$\forall$	$\phantom{A}$universal quantification$\phantom{A}$
$\phantom{A}$$\wedge$	$\phantom{A}$logical conjunction
$\phantom{A}$$\vee$	$\phantom{A}$logical disjunction
symbol	in type theory (propositions as types)
$\phantom{A}$$\to$	$\phantom{A}$function type (implication)
$\phantom{A}$$\times$	$\phantom{A}$product type (conjunction)
$\phantom{A}$$+$	$\phantom{A}$sum type (disjunction)
$\phantom{A}$$0$	$\phantom{A}$empty type (false)
$\phantom{A}$$1$	$\phantom{A}$unit type (true)
$\phantom{A}$$=$	$\phantom{A}$identity type (equality)
$\phantom{A}$$\simeq$	$\phantom{A}$equivalence of types (logical equivalence)
$\phantom{A}$$\sum$	$\phantom{A}$dependent sum type (existential quantifier)
$\phantom{A}$$\prod$	$\phantom{A}$dependent product type (universal quantifier)
symbol	in linear logic
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$
$\phantom{A}$$\;?$$\phantom{A}$	$\phantom{A}$exponential disjunction$\phantom{A}$

References

The ?-modality in affine logic applied to constructive mathematics:

• Michael Shulman, Affine logic for constructive mathematics. Bulletin of Symbolic Logic, Volume 28, Issue 3, September 2022. pp. 327 - 386 (doi:10.1017/bsl.2022.28, arXiv:1805.07518)

category: logic