nLab antithesis interpretation

Idea

Mike Shulman (Shulman 2022) has proposed an interpretation of affine logic for use in constructive mathematics, called the antithesis interpretation.

The motivation here is that in much of constructive mathematics, especially (but not only) in constructive analysis, statements of interest seem to come in pairs, a statement $P^+$ that amounts to a constructive version of a well-known statement $P^{\mathrm{C}}$ from classical mathematics, and a statement $P^-$ that amounts to a constructive version of $\neg{P^{\mathrm{C}}}$, and which is equivalent to $\neg{P^+}$ in classical logic, but which is not the same as $\neg{P^+}$ in intuitionistic logic (being sometimes stronger, sometimes weaker, sometimes neither, and similarly for $P^+$ vis-a-vis $\neg{P^-}$). For example, if $P^{\mathrm{C}}$ is the claim that some real number $x$ is rational, then $P^+$ is

$$\exists\, q \in \mathbb{Q},\; x = q$$

(the conventional meaning of ‘$x$ is rational’ in constructive analysis), while $P^-$ is

$$\forall\, q \in \mathbb{Q},\; x \# q$$

(the conventional meaning of ‘$x$ is irrational’ in constructive analysis); here, $\#$ is the standard apartness relation between real numbers, whose negation is the equality relation $=$. As you can see, the two statements are de Morgan dual to one another, and so are negations of each other in classical logic, but neither is the negation of the other in intuitionistic logic.

That such pairs of statements commonly arise is a truism in constructive mathematics. The point of the antithesis interpretation is that the pair $(P^+, P^-)$ may be derived systematically from a single statement $P^{\mathrm{L}}$ in affine logic. And this is a sound interpretation?, in that any reasoning valid in affine logic (or even linear logic) will be constructively valid for both statements; that is, if $P^{\mathrm{L}} \vdash Q^{\mathrm{L}}$ in affine (or even linear) logic, then $P^+ \vdash Q^+$ and $Q^- \vdash P^-$ in intuitionistic logic. Therefore, as long as the reasoning is affine (or even linear), one can prove intuitionistic theorems about both at once.

The antithesis interpretation also explains why there are often both weak and strong versions of $P^-$ (or even $P^+$ sometimes), having especially to do with the interpretation of disjunction. This comes up already in defining what a set is, because of the nature of the equality relation on a set $S$. As in the example about about rational and irrational real numbers, every set should also be equipped with an antithesis inequality relation $\#$, and the axioms for this may be derived from the axioms for an equality relation. The transitivity axiom for equality has two obvious interpretations in affine logic, which lead to two different interpretations in intuitionistic logic as axioms for $\#$: a weak version (intepreting $\parr$) stating (for elements $x, y, z$ of $S$) that if $x \# z$, then $y \# z$ if $x = y$, and $x \# y$ if $y = z$; and a strong version (interpreting $\oplus$) stating that if $x \# z$, then $x \# y$ or $y \# z$. (The weak version really does follow from the strong version because we also automatically have that $x = y$ and $x \# y$ can never both be true.) Ultimately, the weak version says only that $\#$ is an inequality relation on the set $S$, while the strong version says that $\#$ is an apartness relation.

Since every proposition comes with an antithesis proposition in the antithesis interpretation, the natural notion of a subset is actually a pair of disjoint subsets, leading to a potentially far-reaching reinterpretation of the role of higher-order logic in constructive mathematics, with concepts like a family of collections of subsets becoming a disjoint pair of families of disjoint pairs of collections of disjoint pairs of subsets.

Related concepts

• constructive mathematics

• affine logic, linear logic

References

• 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)