# Adding a truth-like predicate to PA

It is well known that adding a truth predicate to arithmetic in the most natural way leads to a contradiction.

Suppose as usual that we add a one place relation T to the language of arithmetic, and define some system of Godel numbering $\ulcorner \cdot \urcorner$ for this expanded language. Given a set of axioms A in this language (e.g., PA), we extend the usual provability relation $A \vdash \phi$ by demanding that it satisfy the following:

R1. if $A \vdash \phi$, then $A \vdash T(\ulcorner \phi \urcorner)$

R2. if $A \vdash T(\ulcorner \phi \urcorner)$, then $A \vdash \phi$

R3. if $A \vdash \neg \phi$, then $A \vdash \neg T(\ulcorner \phi \urcorner)$

R4. if $A \vdash \neg T(\ulcorner \phi \urcorner)$, then $A \vdash \neg \phi$

Notes:

• We are not adding any new axioms (in particular, we are not adding any Tarski biconditionals $\phi \leftrightarrow T(\ulcorner \phi \urcorner)$ to A), or any other rules of inference of any sort related to $T$. All we are adding to A are the above rules.

• Requirements R1-R4 are different from adding rules of inference. Obviously, adding rules of inference that tell that us we can go from $\phi$ to $T(\ulcorner \phi \urcorner)$ and back, and $\neg \phi$ to $\neg T(\ulcorner \phi \urcorner)$ and back, would be too strong and lead to contradictions in well known ways if A is sufficiently strong. Loosely speaking, with R1-R4, we can't reason hypothetically about truth, though we can talk about the truth or falsity of something when we've actually established its truth or falsity.

Question: Given the above requirements, do we nevertheless have $PA \vdash \bot$ ?

• Could you clarify a little what you mean? Your requirements all have empty left-hand side (that is, there is no theory preceding $\vdash$), but then later you refer to $PA\vdash\perp$. Do you intend that R1 etc. hold also with respect to any theory, or are you only requiring them for the empty theory, or what? Jan 27, 2016 at 2:14
• I intend that these rules apply to whatever theory we are working with (in my case, PA). I will edit accordingly. Jan 27, 2016 at 2:25

Obviously, adding rules of inference that tell that us we can go from $\phi$ to $T(\ulcorner\phi\urcorner)$ and back, and $\neg\phi$ to $\neg T(\ulcorner\phi\urcorner)$ and back, would be too strong and lead to contradictions in well known ways.
Actually, that's not correct. According to a theorem of Friedman and Sheard these rules (denoted by them "$T$-intro", "$T$-elim", "$\neg T$-intro", and "$\neg T$-elim") can be consistently added to PA. (See part D of their main theorem.) [Edit: to clarify, this is in the context of Hilbert-style deduction. If these rules of inference were included in a natural deduction system then they could be converted to implications using $\to$-introduction, and then you would get the Tarski biconditionals and a liar paradox.]
I may add that I have formulated an extension $S$ of Peano arithmetic which is consistent, includes the capture scheme $\phi \to T(\ulcorner \phi\urcorner)$ for every sentence $\phi$, and for which $T(\ulcorner T(\ulcorner \cdots \ulcorner\phi\urcorner \cdots \urcorner)\urcorner)$ is not a theorem, for any false arithmetical sentence $\phi$. Thus if the release scheme "infer $\phi$ from $T(\ulcorner \phi\urcorner)$" were added it would still be consistent. Incidentally, this system has the remarkable property that it proves its own soundness and consistency in the sense that it proves the sentences $$(\forall n)({\rm Prov}_S(n) \to T(n))$$ and $$T(\ulcorner{\rm Con}(S)\urcorner).$$ See this paper or my book. (Note that my system uses intuitionistic logic, although it includes the law of excluded middle for every sentence of arithmetic.)
• Well, if you can prove $\phi$ then you can infer $T(\ulcorner\phi\urcorner)$, and then $\phi \leftrightarrow T(\ulcorner\phi\urcorner)$ follows trivially, but there's no technique for proving biconditionals generally. You explained why yourself: we can't reason hypothetically about truth, we can only talk about the truth or falsity of something when we've actually established its truth or falsity. Jan 27, 2016 at 4:02
• ... $T$-intro etc. are deduction rules, not axiom schemes. Jan 27, 2016 at 4:02