Skip to main content
2 of 2
edited body
Emil Jeřábek
  • 47.9k
  • 4
  • 151
  • 210

One example of an anti-classical theory that’s not artificially constructed for that purpose is $\mathsf{HA+CT_0}$, where the Church–Turing thesis $\mathsf{CT_0}$ is the schema $$\forall x\:\exists y\:\phi(x,y)\to\exists e\:\forall x\:\exists y\:\bigl(\{e\}(x)\simeq y\land\phi(x,y)\bigr).$$ Here, $\{e\}(x)\simeq y$ denotes a $\Sigma_1$ formula formalizing the predicate “the program with code $e$ computes output $y$ on input $x$”, and $\phi$ may have other parameters besides $x$ and $y$. This contradicts classical logic, as $\mathsf{PA}$ proves the existence of noncomputable definable functions.

More generally, there is the extended Church–Turing thesis $\mathsf{ECT_0}$, $$\forall x\:\bigl(\psi(x)\to\exists y\:\phi(x,y)\bigr)\to\exists e\:\forall x\:\bigl(\psi(x)\to\exists y\:\bigl(\{e\}(x)\simeq y\land\phi(x,y)\bigr)\bigr),$$ where $\psi(x)$ is an almost negative formula (a formula constructed from $\Sigma_1$ formulas using $\to$, $\land$, and $\forall$, again with possibly other free variables). The theory $\mathsf{HA+ECT_0}$ is important due to its connections to Kleene realizability.

But concerning Are all anti-classical theories of a sort like this?—in a way, yes. Let me elaborate the characterization of anti-classical theories from the comments. Given a (first-order intuitionistic) theory $T$, and a formula $\phi$, let $T\vdash_i\phi$ denote that $T$ proves $\phi$ over intuitionistic logic, and $T\vdash_c\phi$ that $T$ proves $\phi$ over classical logic. First, we have:

Lemma. $T\vdash_c\phi$ iff there is a formula $\psi(\vec x)$ such that $T\vdash_i\forall\vec x\,(\psi(\vec x)\lor\neg\psi(\vec x))\to\phi$.

Proof: The right-to-left implication is trivial. For the left-to-right implication, let $\pi$ be a classical Hilbert-style proof of $\phi$ from $T$. Then $\pi$ is an intuitionistic proof of $\phi$ from $T$ and from some instances $\{\psi_i(\vec x)\lor\neg\psi_i(\vec x):i<n\}$ of LEM (here $\vec x$ is a list including all free variables of all the $\psi_i$). Put $$\psi(\vec x)=\bigwedge_{i<n}(\psi_i(\vec x)\lor\neg\psi_i(\vec x)).$$ Since $\vdash_i\neg\neg\psi(\vec x)$, the formula $\psi(\vec x)\lor\neg\psi(\vec x)$ is equivalent to $\psi(\vec x)$ itself, which obviously implies each $\psi_i(\vec x)\lor\neg\psi_i(\vec x)$. Thus, passing also to a universal closure, we get $$T+\forall\vec x\:(\psi(\vec x)\lor\neg\psi(\vec x))\vdash_i\phi.$$ Then the result follows by the deduction theorem. QED

Corollary. For a given theory $T$, the following are equivalent:

  1. $T\vdash_c\bot$ (i.e., $T$ is anti-classical).

  2. $T\vdash_i\neg\forall\vec x\,(\psi(\vec x)\lor\neg\psi(\vec x))$ for some formula $\psi$.

  3. $T\vdash_i\forall\vec x\,\neg\neg\psi(\vec x)$ and $T\vdash_i\neg\forall\vec x\,\psi(\vec x)$ for some formula $\psi$.

Proof: 1 → 2 follows from the Lemma, 2 → 3 from $\vdash_i\forall\vec x\,\neg\neg(\psi(\vec x)\lor\neg\psi(\vec x))$, and 3 → 1 is clear.

An interesting consequence of this is that an intuitionistic theory is consistent with classical logic iff it is consistent with the double-negation shift schema $$\tag{DNS}\forall x\:\neg\neg\phi(x)\to\neg\neg\forall x\:\phi(x),$$ even though the latter is strictly weaker than classical logic. (Even better, DNS can be characterized as the weakest extension of intuitionistic first-order logic with this property: that is, whenever $T$ is a theory such that all consistent extensions of $T$ are consistent with classical logic, then $T$ proves DNS.)

Emil Jeřábek
  • 47.9k
  • 4
  • 151
  • 210