On Adding a Validity Predicate to PA

This note was occasioned by reading JC Beall & Julien Murzi's manuscript, "Two Flavors of Curry's Paradox" concerning the possibility of reconstructing a Curry-style paradox within a theory of validity.

Under certain circumstances, the theory is consistent, as it can be interpreted inside Peano arithmetic, $PA$. Suppose we begin with $PA$ in its usual first order language $\mathcal{L}$ with $=, 0, S, +$ and $\times$. Suppose that $\vdash$ stands for ordinary first-order deducibility. "$P$ is a derivation of $B$ from $A$" means "$P$ is a finite sequence $(P_0, ..., P_n)$ where $P_n$ is $B$, and each $P_i$ is either a logical axiom, or is $A$, or is obtained from previous formulas by Modus Ponens". The relation "$P$ is a derivation of $B$ from $A$" is decidable. So, it can be strongly represented in $PA$ by a recursive formula, $\mathbf{Proof}(x, y, z)$, in such a way that:

• (i) If $P$ is a derivation of $B$ from $A$ then $PA \vdash \mathbf{Proof}(\ulcorner P \urcorner, \ulcorner A \urcorner, \ulcorner B \urcorner)$.

and

• (ii) If $P$ is not a derivation of $B$ from $A$ then $PA \vdash \neg \mathbf{Proof}(\ulcorner P \urcorner, \ulcorner A \urcorner, \ulcorner B \urcorner)$.

Write $\mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$ to mean: "there is a derivation of $B$ from $A$".
Then (i) guarantees that we have a version of (V-Intro):

• (V-Intro) $\text{If } A \vdash B, \text{ then } PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$.

[This doesn't say that $PA$ itself is closed under this introduction rule. If that were so, we would have a version of Montague's Paradox.]

Next, as $PA$ is sound, if $PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$, then $\mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$ is true --- that is, $A \vdash B$. So, we have a version of (V-Elim):

• (V-Elim) $\text{If } PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner), \text{ then } A \vdash B$.

Finally, the difficult part. A property of $PA$ is that, for every $\mathcal{L}$-sentence $A$:

(iii) $PA \vdash A \rightarrow \mathbf{Con}(A)$.

where $\mathbf{Con}(A)$ means: "there is no derivation of $0 = 1$ from $A$".

[Update, 6 April: This is a non-trivial result about $PA$. (See Hajek/Pudlak, 1993, Metamathematics of First-Order Arithmetic, p. 108.) It is intimately related to the fact that $PA$ is reflexive - $PA$ proves the consistency of any of its finitely axiomatized subtheories. The proof of (iii) in Hajek/Pudlak uses partial truth definitions, first to show that $I\Sigma_k$ proves the consistency of all true $\Pi_{k+1}$-sentences.]

So,

(iv) $PA \vdash \neg(A \rightarrow B) \rightarrow \mathbf{Con}(\neg(A \rightarrow B))$.

So,

(v) $PA \vdash \neg \mathbf{Con}(\neg(A \rightarrow B)) \rightarrow (A \rightarrow B)$.

The validity of the inference in logic from $A$ to $B$ can be expressed by saying that the sentence $\neg (A \rightarrow B)$ is not consistent. This in fact can be proved in $PA$ itself,

(vi) $PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner) \leftrightarrow \neg \mathbf{Con}(\neg (A \rightarrow B))$.

So, we get a version of the scheme (V-Out):

• (V-Out) $PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner) \rightarrow (A \rightarrow B)$.

[Relatedly, $PA$ proves the local reflection scheme for logic: if $\mathbf{Prov}_{\emptyset}(x)$ means "$x$ is a theorem of logic", then $PA$ proves all instances of $\mathbf{Prov}_{\emptyset}(\ulcorner A \urcorner) \rightarrow A$.]

So, $PA$ itself is a consistent theory that already contains a theory of validity with versions of (V-Intro), (V-Elim) and (V-Out).

Application to Curry's Paradox:
The example discussed in Beall & Murzi concerns a validity-Curry sentence, a sentence $C$ which says "I am inconsistent". In the case of $PA$, choose $C$ such that,

(vii) $PA \vdash C \leftrightarrow \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$.

where $\bot$ is some contradiction (e.g., $0 \neq 0$). Using property (V-Out), we get:

(viii) $PA \vdash C \rightarrow (C \rightarrow \bot)$.

[Note: this is where we are about to use something like "contraction", as $C \rightarrow (C \rightarrow \bot)$ is equivalent in classical logic to $C \rightarrow \bot$.]

Thus,

(ix) $PA \vdash \neg C$.

So, since $PA$ is sound, $C$ is not true. This tells us that $\mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$ is not true. In other words, $C$ is consistent. In particular, it is not the case that $\bot$ is derivable in logic from $C$. This is why we cannot apply (V-Intro). Rather, $\bot$ is derivable in $PA$ itself from $C$, and $PA$ is stronger than logic. From (vii) and (ix), $PA \vdash \neg \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$. So:

(x) $PA \vdash \mathbf{Con}(C)$.

Beall & Murzi (ms) give a derivation of a contradiction from a sentence like $C$, but their derivation uses a different version of (V-Intro). Suppose $V$ is a theory of validity (including arithmetic) such that:

• $V$ permits diagonalization.
• $V$ proves each instance of the scheme (V-Out).
• $V$ has the following form of the (V-Intro) rule:
• (V-Intro)* $\text{If } V, A \vdash B, \text{ then } V \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$.

Then, following Beall & Murzi's derivation, $V$ is inconsistent:

1. $V \vdash C \leftrightarrow \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$.
2. $V \vdash \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner) \rightarrow (C \rightarrow \bot)$.
3. $V, C \vdash \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$.
4. $V, C \vdash C \rightarrow \bot$.
5. $V, C \vdash \bot$.
6. $V \vdash \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$.
7. $V \vdash C$.
8. $V \vdash \bot$.

The crucial step that might be considered problematic is (6), which invokes the strong introduction rule (V-Intro)* to infer $\mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$ from a derivation of $\bot$ from $C$ in the theory $V$ itself. But the derivation of $\bot$ from $C$ inside $V$ surely doesn't imply that the inference of $C$ to $\bot$ is logically valid.

Abstracting from the interpretation of $\mathbf{Val}$, this seems to me to be closely related to a version of Montague's Paradox: a theory which contains an "absolute knowability" predicate satisfying an (Intro) rule and an (Out) scheme.

[Update 1, 16 April: LaTeX-ified.]

[Update 2, 24 April: Since the issue of logical derivability is crucial here, I've changed occurrences of $0=1$ (which is normally used in discussion of consistency for systems of arithmetic) to $\bot$, which stands for a genuine contradiction, say $0 \neq 0$.]