6
$\begingroup$

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$ ?

Improve this question
$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – Joel David Hamkins
    Commented Jan 27, 2016 at 2:14
  • 1
    $\begingroup$ I intend that these rules apply to whatever theory we are working with (in my case, PA). I will edit accordingly. $\endgroup$
    – Cecilia Burrow
    Commented Jan 27, 2016 at 2:25

1 Answer 1

Reset to default
5
$\begingroup$

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

Improve this answer
$\endgroup$
9
  • 1
    $\begingroup$ Thanks, I'll look at all those materials, they sound fascinating. Still, I'm puzzled about the Friedman and Sheard result - if the rest of the logic is standard, and T-intro etc. mean what one would think, wouldn't one then able to prove every Tarksi biconditional, and thus get into trouble by considering Liar type sentences defined by the usual diagonalization method? $\endgroup$
    – Cecilia Burrow
    Commented Jan 27, 2016 at 3:19
  • 1
    $\begingroup$ 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. $\endgroup$
    – Nik Weaver
    Commented Jan 27, 2016 at 4:02
  • $\begingroup$ ... $T$-intro etc. are deduction rules, not axiom schemes. $\endgroup$
    – Nik Weaver
    Commented Jan 27, 2016 at 4:02
  • $\begingroup$ Yes, looking at their paper, T-intro etc. do seem to be just the rules R1-R4, rather than the more general sort of deduction rule that applies even in hypothetical reasoning. $\endgroup$
    – Cecilia Burrow
    Commented Jan 27, 2016 at 5:02
  • 1
    $\begingroup$ Just to clear up some confusions here and make it easy for the reader: we need to distinguish rules of inference that apply anywhere (even within hypothetical reasoning) from rules of inference of the form R1-R4, which only take complete proofs to complete proofs. I don't know that there is accepted terminology here, but let's call call the former a 'rule of inference' and the later a 'proof transformation rule.' $\endgroup$
    – Cecilia Burrow
    Commented Jan 27, 2016 at 17:02

You must log in to answer this question.

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