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.

6more comments