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. We also stipulate that the provability relation satisfy the following:

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

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

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

R4. if $\vdash \neg T(\ulcorner \phi \urcorner)$, then $\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 our axioms), or any other rules of inference of any sort related to $T$. All we are adding 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. 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$ ?