Adding nonconstructive disjunction to intuitionistic logic

Question

In constructive mathematics, under realizability interpretations, we can define nonconstructive disjunction $A⅋B$ as follows:
A witness for $A⅋B$ gives a candidate witness for $A$ and a candidate witness for $B$, at least one of which is correct (we need not know which one).

$A⅋B$ is the strongest connective that always satisfies $(¬C⇒A) ∧ (¬¬C⇒B) ⇒ A⅋B$. It also the strongest monotonic connective such that $¬C⅋¬¬C$ is constructively valid.

How do you formalize intuitionistic sequent calculus augmented with nonconstructive disjunction? What kind of semantics is this calculus complete for? The formalization should be conservative over intuitionistic logic. Below is what I know and more precise versions of these questions.

Note: I used symbol '⅋' because because it follows the rules of multiplicative disjunction $⅋$ (pronounced 'par') in linear logic (however, $∨_w$ ('weak or') would be another reasonable choice). For example, $A⅋A ⇒ A$ is not constructively valid: We might not know which of the two candidate witnesses is correct. The limitation on contraction is the price for using nonconstructive disjunction in a constructive framework.

To axiomatize '⅋' as an addition to intuitionistic logic, let us list its basic properties.

Axioms:
$A⅋B⇔B⅋A$
$A⅋(B⅋C)⇔(A⅋B)⅋C$
$(B⇒C) ⇒ (A⅋B⇒A⅋C)$
$¬C⅋¬¬C$
$A⅋⊥ ⇔ A$

Is this axiomatization complete for the realizability semantics above? Here, I would like to thank Andrej Bauer for his treatment and general formalization of realizability (his answer below), which includes a semantics for '⅋', though completeness of the axioms remains open.

If the axioms are insufficient, we can extend the language with infinitely many predicate variables (without second order quantification), and add inference rule:
From $A⅋B⇒D$ infer $(¬C⇒A) ∧ (¬¬C⇒B) ⇒ D$ ($C$ is a predicate variable not used in $A$, $B$, $D$).
Conversely, if the axioms above are sufficient, this extension should be conservative over them.

Number and Function Realizability

Frank Waaldjik's answer and comments note the similarity between $A⅋B$ and $(¬A⇒B)∧(¬B⇒A)$, with the later even satisfying the axioms for $A⅋B$ (unless the axiomatization is incomplete). However, for most realizability interpretations, $A⅋B$ is strictly stronger than $(¬A⇒B)∧(¬B⇒A)$. Two examples are number realizability (with natural numbers coding partial recursive functions) and function realizability (with witnesses being codes for partial continuous functions; constructive validity requires a recursive witness for the universal closure of the formula). In both cases, if $r⊩A$ and $r⊩B$ ('⊩' means 'realizes') are both $Π^0_2$, then $A⅋B$ is equivalent to $∃a,b∈ℝ[ab∉ℚ∧(a∉ℚ→A)∧(b∉ℚ→B)]$, which can be proved using $Π^0_2$-completeness of $a∉ℚ$.

For both number and function realizability, we also have the following (without complexity restrictions) $(∃n∈ℕ \, A_0(n)) ⅋ (∃n∈ℕ \, A_1(n)) ⇒ ∃i,n \, (A_i(n)⅋∃n∈ℕ \, A_{1-i}(n))$ (intuitively, run/examine both candidate witnesses until one gives an $n$). Over the domain $R$ of partial functions $ℕ→ℕ$ (treated extensionally, but witnesses enumerate values with an arbitrary order and delay), we even have $(∃a∈R \, A(a)) ⅋ (∃b∈R \, B(b)) ⇔ ∃a,b∈R \, (A(a)⅋B(b))$, which (with the axioms above) suffices to define '⅋' for both number and function realizability (since $¬A(a)⅋¬B(b)$ is $¬(A(a)∧B(b))$). However, these formulas need not hold for other interpretations of '⅋'. While investigating completeness of the axioms, I was stumbled over $(¬E→A∨B)∧(¬¬E→C∨D) → ((¬A→¬¬E)∨(¬B→¬¬E)∨(¬C→¬E)∨(¬D→¬E))$ before realizing that it holds under both number and function realizability but not intuitionistically provable.

Sequent Calculus

We would also like a reasonable sequent calculus for intuitionistic logic + '⅋', which, if possible, allows cut elimination and subformula property for cut-free proofs. Here we use an idea from linear logic, treating the succedent Δ as a multiset that is interpreted as a ⅋-disjunction of its members. Δ will have exchange and weakening but not contraction.

As Damiano Mazza noted below, Girard's LU system ("On the unity of logic") already includes intuitionistic and linear connectives. However, I do not know if its combination of intuitionistic logic and '⅋' works for us, and in any case, LU's generality likely makes it artificially complicated here.

Here is my attempt at the sequent calculus. We start with LK sequent calculus (link accessed Aug 23, 2017) and apply these changes:
* Remove right contraction.
* Strengthen $∨L$ to reflect lack of right contraction: from Γ,$A$⊢Δ and Γ,$B$⊢Δ infer Γ,$A∨B$⊢Δ.
* Add $⅋L$: from Γ,$A$⊢Δ$_1$ and Γ,B⊢Δ$_2$ infer Γ,$A⅋B$⊢Δ$_1$,Δ$_2$.
* Add $⅋R$: from Γ⊢$A$,$B$,Δ infer Γ⊢$A⅋B$,Δ.
* In $→R$, $¬R$, and $∀R$, require formulas in Δ to be Harrop. Harrop formulas are closed under '⅋'. Δ is arbitrary for other rules.

Is this the right system for intuitionistic logic with '⅋'? Can we get cut elimination to hold?

The changes are straightforward except for the $→R$, $¬R$, and $∀R$ rules. Because intuitionistic logic deals not just with truthfulness but constructiveness, we have to limit side formulas in the succedent, but Harrop formulas are fine since they are determined by their truth values. I do not know whether these restricted rules are sufficient, especially if not using the cut rule.

Nonconstructive Existential Quantifier

A disjunction can be thought of as an existential quantifier over $\{0,1\}$, and we can generalize nonconstructive disjunction into a weak or nonconstructive existential quantifier (but note that there are also other constructs of varying degrees of constructiveness). A witness for $∃_w x \, A(x)$ is like a witness for $∀x \, A(x)$ except that it need only be valid for one (potentialy unknown) $x$. '$∃_w$' appears to be the strongest connective always satisfying $(¬¬∃x \,C(x)) ∧ ∀x (¬¬C(x)⇒A(x)) ⇒ ∃_w x \, A(x)$. It is also apparently the strongest monotonic connective with $¬¬∃x \,C(x) ⇒ ∃_w x \, ¬¬C(x)$ constructively valid.

We can try to axiomatize it with the following basic properties, though the completeness is unclear.
$∃_w x ∃_w y \, A(x,y) ⇔ ∃_w y ∃_w x \, A(x,y)$
$∃_w x (A(x) ⅋ B(x)) ⇔ ((∃_w x \, A(x)) ⅋ (∃_w x \,B(x)))$
$∀x (A(x)⇒B(x)) ∧ ∃_w x \, A(x) ⇒ ∃_w x \, B(x)$
$¬¬∃x \, C(x) ⇒ ∃_w x \, ¬¬C(x)$
$(∃_w x \,A(x)) ∧ ∀x (A(x)⇒x=y) ⇒ A(y)$ (assumes equality is identity; presumably ¬¬x=y⇒x=y).

If the axioms are insufficient, we can extend the language with infinitely many predicate variables (without second order quantification), and add inference rule:
From $∃_w x \, A(x) ⇒ D$ infer $(¬¬∃x \, C(x)) ∧ ∀x (¬¬C(x)⇒A(x)) ⇒ D$ ($C$ is a predicate variable not used in $A$, $D$).

Updated (Sep 2): Added relations with both number and function realizability.

Answer 1

$\newcommand{\par}{\mathbin{⅋}}$ $\newcommand{\rz}{\Vdash}$ $\newcommand{\fst}[1]{\mathsf{fst}(#1)}$ $\newcommand{\snd}[1]{\mathsf{snd}(#1)}$

Let me write $r \rz \phi$ when $r$ realizes $\phi$.

If you allow higher-order logic, then $A \par B$ may be expressed as $$\exists X . (\lnot X \Rightarrow A) \land (\lnot\lnot X \Rightarrow B)$$ where $X$ ranges over all propositions.

To justify my claim, let us first recall how higher-order logic is interpreted in realizability. Given a partial combinatory algebra $\mathbb{A}$, the propositions are the subsets of $\mathbb{A}$. In the realizability topos $\mathrm{RT}(\mathbb{A})$ the object of all proposition is $\Omega = (\mathcal{P}(\mathbb{A}), =_\Omega)$, where $=_\Omega : \mathcal{P}(\mathbb{A}) \times \mathcal{P}(\mathbb{A}) \to \mathcal{P}(\mathbb{A})$ is the non-standard equality predicate defined by $$(A =_\Omega B) = (A \Rightarrow B) \land (B \Rightarrow A)$$ (Here read $\Rightarrow$ and $\land$ as in the realizability interpretation, i.e., they give sets of realizers.) By unraveling the realizability interpretation of existentials and applying the definition of $\Omega$, we can work out the fact that $$p \rz \exists X . \phi(X)$$ if, and only if, there is $C \subseteq \mathbb{A}$ such that $\fst{p} \in (C =_\Omega C)$ and $\snd{p} \rz \phi(C)$, where $\mathsf{fst}$ and $\mathsf{snd}$ are first and second projection, respectively. Note that $((\lambda x . x), (\lambda x . x)) \in (C =_\Omega C)$ for all $C$. Let us abbreviate $v = ((\lambda x . x), (\lambda x . x))$.

Now we may show that $$ A \par B \iff \exists X . (\lnot X \Rightarrow A) \land (\lnot\lnot X \Rightarrow B)$$ is realized. From left to right, the realizer is $$f = \lambda x . (v, ((\lambda y . \fst{x}), (\lambda z . \snd{x})),$$ Indeed, if $(p, q)$ realizes $A \par B$, then $f (p, q) = (v, ((\lambda y . p), (\lambda y . q)))$. We know that $p \rz A$ or $q \rz B$. If $p \rz A$, take $C = \bot = \emptyset$ and observe that $((\lambda y . p), (\lambda y . q))$ realizes $$(\lnot \bot \Rightarrow A) \land (\lnot\lnot \bot \Rightarrow B)$$ because this is equivalent to $$(\top \Rightarrow A) \land (\bot \Rightarrow B).$$ If $q \rz B$, take $C = \top = \mathbb{A}$ and observe that now $((\lambda y . p), (\lambda y . q))$ realizes $$(\lnot \top \Rightarrow A) \land (\lnot\lnot \top \Rightarrow B)$$ because this is equivalent to $$(\bot \Rightarrow A) \land (\top \Rightarrow B).$$

The implication in the other direction is realized by $$g = \lambda x . (\fst{\snd{x}} \star, \snd{\snd{x}} \star)$$ where $\star \in \mathbb{A}$ is some default realizer. Indeed, suppose there is $C \subseteq \mathbb{A}$ and $p \in \mathbb{A}$ such that $\fst{p} \in (C =_\Omega C))$ and $\snd{p} \rz (\lnot C \Rightarrow A) \land (\lnot\lnot C \Rightarrow B)$:

• If $C = \emptyset$ then $\fst{\snd{p}} \rz \top \Rightarrow A$ and so $\fst{\snd{p}} \star \rz A$.
• If $C \neq \emptyset$ then $\snd{\snd{p}} \rz \top \Rightarrow B$ and so $\snd{\snd{p}} \star \rz B$.

This completes the proof.

We could ask whether there is a first-order schema $\Phi(A,B)$, expressed in the propositional calculus, such that $A \par B \iff \Phi(A, B)$ is realized. I do not know, yet.

Addendum: without explaining the details, let me just say that we may realize $$A \par B \iff \exists X \in \Omega_{\lnot\lnot} . (X \Rightarrow A) \land (\lnot X \Rightarrow B)$$ where $\Omega_{\lnot\lnot p} = \{p \in \Omega \mid \lnot\lnot p \Rightarrow p\}$. This should be compared to the fact that $$A \lor B \iff \exists X \in 2 . (X \Rightarrow A) \land (\lnot X \Rightarrow B)$$ where $2 = \{p \in \Omega \mid p \lor \lnot p\}$. This gives us the following idea. Consider any object $T = (\{0,1\}, (=_T))$ whose underlying set is $\{0,1\}$, and let us call such objects "binary". (I think up to isomorphism they are the $\lnot\lnot$-dense subobjects of $\Omega_{\lnot\lnot}$.) We can then define $T$-disjunction $\lor_T$ by $$A \lor_T B \iff \exists t \in T . (t =_T 0 \Rightarrow A) \land (t =_T 1 \Rightarrow B).$$ We have a whole spectrum of disjunctions of various constructive strength, two of which were discussed above ($\par$ is $\lor_{\Omega_{\lnot\lnot}}$, and the intuitionistic $\lor$ is $\lor_2$).

To give you one in the middle, consider ordinary number realizability and the binary object $\Sigma$ in which $1$ is realized by the elements of the Halting set, and $0$ by the elements of the non-Halting set (this object is known as the Rosolini dominance). This gives a non-symmetric $\Sigma$-disjunction. One might prefer to impose a further restriction on the binary object $T$, namely that the twist map $0 \mapsto 1$, $1 \mapsto 0$ be realized, which would give symmetry of $\lor_T$. And I will leave it as an exercise to figure out what needs to be done for associativity of $\lor_T$.

In general $T$-disjunction implies $S$-disjunction iff the identity map $\mathrm{id} : \{0,1\} \to \{0,1\}$ is realized as a morphism $T \to S$. This probably leads into some sort of study of reducibilities that would make a little boring logic paper.

Supplemental 2017-08-22: The characterization of $\par$ tells us what its introduction rule should be, namely: $$ \frac{\displaystyle \Gamma, \lnot C \vdash A \qquad \Gamma, \lnot \lnot C \vdash B }{\Gamma \vdash A \par B} $$ This is weird.

Answer 2

${\rm\small\color{#808080}{(1st\ answer, also\ see\ updates\ below):}}$
I think the connective $A⅋B$ is not more constructive than existing connectives. You say that a witness for$A⅋B$ consists of two candidate witnesses for $A,B$ respectively, "at least one of which is correct (we need not know which one)".

Now take $A=\neg C$ and $B=\neg\neg C$. My candidate witnesses are $\neg C$ and $\neg\neg C$ (we need not know which one is correct, as you stated). So I conclude $\neg C⅋\neg\neg C$. But my witnesses are constructively worthless.

Therefore it seems to me that what you want $A⅋B$ to do is actually equivalent to the existing:

($\ast$) $(\neg A\rightarrow B)\wedge (\neg B\rightarrow A$).

If we know $A⅋B$ then clearly we know ($\ast$). And if we know ($\ast$), then we can take $A, B$ as our candidate witnesses for $A⅋B$.

Update Aug 28: ${\rm\small\color{#808080}{(also\ see\ update\ Sep\ 1\ below)}}$

Under the axiomatization now given, and the reference to truth values, I see that the alternative ($\ast$) above is actually too weak.

But if we let $A\dot{\small\vee} B$ be shorthand for the stronger formula

($\ast\ast$) $((B\rightarrow A)\rightarrow A)\wedge ((A\rightarrow B)\rightarrow B))$

then $A\dot{\small\vee} B$ seems more difficult to distinguish from the proposed $A⅋B$.

For a realizability-related analysis of this, perhaps Andrej could comment? My knowledge of realizability is very limited, but let me say the following nonetheless (take from it what seems useful, and turn a friendly eye to obvious errors...):

If we have a witness for $A\dot{\small\vee} B$, then I assume that by realizability we can find a witness for $(B\rightarrow A)\rightarrow A$. Can we use this witness as candidate witness for $A$? I cannot tell from the context. Likewise we find a witness for $(A\rightarrow B)\rightarrow B$ to possibly use as a candidate witness for $B$. So if indeed these witnesses are acceptable as candidate witnesses for $A, B$, we see that 'at least one of these witnesses is correct (we need not know which one)'. This leads me to believe that in a concrete realizability context $A\dot{\small\vee} B$ implies $A⅋B$ as described.

$\newcommand{\rz}{\Vdash}$To show this more clearly, I at least need more information on the realizability context. Clearly the realizability relation $\rz$ is not decidable, but we know little else.

What does 'at least one of the witnesses is correct' really mean? I think the vagueness of this expression might be what necessitates the use of the connective $A⅋B$. This vagueness is certainly interesting and might be quite useful, don't think I don't think so :-)

But clarity can be useful too, and for clarity I think it would help to specify what $A⅋B$ 'means' in terms of $\rz$, and what $\not\rz$ implies, etc. If $R$ is the set of realizers (witnesses) then possibly we could define:

$A⅋B := \exists a,b\in R\ [\, (a\not\rz A\rightarrow b\rz B)\,\wedge (b\not\rz B\rightarrow a\rz A)\,]$

(or is this not what you have in mind?) which is to be compared with the realizability of $ A\dot{\small\vee} B$:

$\rz A\dot{\small\vee} B := \exists s,t\in R\ [\, (s\rz (B\rightarrow A)\rightarrow A)\,\wedge$

$\hspace{8cm} (t\rz (A\rightarrow B)\rightarrow B))\,]$

OK, those were my 2cts worth on realizability...

Finally, let me add that in your axiomatization the axiom $A\Rightarrow A⅋B$ seems to be missing. I'm also not sure your sequent calculus works seamlessly with your axiomatization, but it is too much work for me to check this...especially since all the implications keep confusing me :-).

PS. In contrast to $A⅋B$, the existing $A\dot{\small\vee} B$ does however have the property that $A\dot{\small\vee} A$ implies $A$...

Update Sep 1

$\newcommand{\ifv}{\,\dot{\small\sqcup}\,}$More reflection, and the properties of $\rz$ stated below in the comments, lead me to update once more.

(I) The connective $A\dot{\small\vee} B$ that I proposed above, on second thought has the unsuitable property that we always have $A\dot{\small\vee} \neg A$.

(II) I think that the proposed axiomatization for $A⅋B$ is not complete, as follows:

For readability put $A\ifv B := (\neg A\rightarrow B)\wedge (\neg B\rightarrow A$).

${{\rm\small\color{#065050}{claim}}}$: $A\ifv B$ satisfies the axiomatization proposed for $A⅋B$.

${{\rm\small\color{#065050}{proof}}}$:

(i) $A\ifv B⇔ B\ifv A $ is trivial
(ii) $A\ifv (B\ifv C)⇔(A\ifv B)\ifv C$ holds because: $$X\ifv (Y\ifv Z)\Leftrightarrow ((\neg X\wedge\neg Y)\rightarrow Z)\wedge((\neg X\wedge\neg Z)\rightarrow Y) \wedge ((\neg Y\wedge\neg Z)\rightarrow X)$$
(iii)$(B⇒C) ⇒ (A\ifv B⇒A\ifv C)$ since from $(B⇒C)$ and $A\ifv B$ we infer $\neg A\rightarrow B\rightarrow C$ and $\neg C\rightarrow\neg B\rightarrow A$, in other words $A\ifv C$

(iv) $\neg C\ifv \neg\neg C$ is trivial
(v) $A\ifv (0=1)⇔ A$ is trivial

So this axiomatization does not appear to be complete.

(III) In the comments below the characterization

$A⅋B := \exists a,b\in R\ [\, (a\not\rz A\rightarrow b\rz B)\,\wedge (b\not\rz B\rightarrow a\rz A)\,]$

is affirmed, together with the property:

$\neg(a\not\rz A)\rightarrow a\rz A$

This, combined with Andrej's answer, leads me to the thought that in many situations the following characterizations could be considered:

$A⅋B$ iff ${\rm\small\color{#808080}{(first\ characterization)}}$

(i) $\exists a,b\in\mathbb{R}\,[\,(a\not=0\rightarrow A)\wedge (b\not=0\rightarrow B)\wedge (a^{2}+b^{2}\not=0)\,]$

$A⅋B$ iff ${\rm\small\color{#808080}{(second\ characterization)}}$

(ii) $\exists c\in\mathbb{R}\,[\,(c=0\rightarrow A)\wedge (c\not=0\rightarrow B)\,]$

Axiomatic and sequent calculus properties of $A⅋B$ should, I think, follow those of (i) and/or (ii) very closely, if $A⅋B$ is to be distinguished from $A\vee B$ as well as from $A\ifv B$.