8
$\begingroup$

An anti-classical axiom $\phi$ is one which is inconsistent with LEM

Are there any sources for good examples of anti-classical theories in intuitionstic first-order logic? There are many examples of topoi with anti-classical properties (such as "all functions $\mathbb{N} \to \mathbb{N}$ are computable"), but I'm unable to find many simple first-order theories.

One which we can devise is the theory of the non-trivial tiny object: (with no extra symbols besides equality) $$ \forall xy, \neg\neg(x = y)\\ \neg \forall xy, (x=y) $$ This is inspired by the set of infinitesimals in SDG.

Are all anti-classical theories of a sort like this? I suppose equality could be replaced with any relational symbol.

$\endgroup$
21
  • 1
    $\begingroup$ Since you are careful about first-order vs. higher-order, what is $LEM$ in $\phi \land LEM \vdash \bot$? In first-order logic LEM would be a schema, not a formula, but then your characterization of anti-classical is not well formed. Wouldn't it be better to just say that a theory (as opposed to an axiom) is anti-classical if it proves $\neg (\phi \lor \neg \phi)$ for at least one formula $\phi$? $\endgroup$ Commented Oct 29 at 21:12
  • 1
    $\begingroup$ Also, you should allow multi-sorted theories here, because in intuitionsitic logic we cannot play tricks that reduce multi-sorted theories to single-sorted ones. $\endgroup$ Commented Oct 29 at 21:13
  • 2
    $\begingroup$ @AndrejBauer A theory that proves $\neg(\phi\lor\neg\phi)$ is not just anti-classical, but inconsistent. Anyway, I think the intent is clear: a formula $\phi$, or a theory $T$ if you wish, is anticlassical if it is inconsistent with classical logic, i.e., if $\mathrm{LEM}\cup T\vdash\bot$ to use a more formally correct notation. This amounts to $T\vdash\neg\bigwedge_{i<n}\forall\vec x\,(\phi_i(\vec x)\lor\neg\phi_i(\vec x))$ for some formulas $\phi_i$. $\endgroup$ Commented Oct 29 at 21:42
  • 2
    $\begingroup$ @AndrejBauer I'm sure higher-order people use it in ways I am not familiar with, but in the context of first-order arithmetic, no, ECT is just a first-order axiom schema: $\forall x\,(\psi(x)\to\exists y\,\phi(x,y))\to\exists e\,\forall x\,(\psi(x)\to\exists y\,(\{e\}(x)\simeq y\land\phi(x,y)))$, where $\psi$ is essentially negative, and $\{e\}(x)\simeq y$ denotes a $\Sigma_1$ formula expressing "the program with code $e$ computes $y$ on input $x$". $\endgroup$ Commented Oct 30 at 8:05
  • 2
    $\begingroup$ @AndrejBauer Regarding many-sorted theories, for theories with finitely many sorts, don't the standard classical model theory tricks of coding functions as relations and coding sorts as disjoint (decidable) sets still work intuitionistically? In other words, isn't it still true that every theory with finitely many sorts is biinterpretable with a single-sorted (relational) theory? What tricks don't work exactly? $\endgroup$ Commented Oct 30 at 16:13

1 Answer 1

9
$\begingroup$

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

$\endgroup$
3
  • $\begingroup$ It took me a second to see why this schema is anti-classical. Since all intuitionistically definable functions can truly be computed by a Turing machine regardless of the presence of LEM, it would seem that each instance would be fine and so the whole would be. So the interesting character is in the $\forall x, \exists y, \phi(x, y) \to ...$ portion, for specific formulae. And so rather it's a direct assertion of the non-existence of such a proof for non-computable functions $\neg \forall x, \exists y, \phi(x,y)$. The contrapositive feels more enlightening here. $\endgroup$
    – Jason Carr
    Commented Oct 30 at 15:16
  • $\begingroup$ Also: are there other original sources for the claims in the second half of this answer? Of course they're brief enough to understand here, but I was curious how much this topic has been addressed before $\endgroup$
    – Jason Carr
    Commented Oct 30 at 15:34
  • 3
    $\begingroup$ I don't know. It sounds like a basic thing that was probably observed before, but to be honest, I'm not well read in literature on intuitionistic logic. $\endgroup$ Commented Oct 30 at 16:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .