MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Fix notation

Suppose that $Prf_1(m, n)$ is the numerical relation that holds when $m$ numbers a $T$-proof of the sentence numbered $n$, according to scheme 1 for numbering wffs and sequences of wffs. Likewise $Prf_2(m, n)$ is the relation that holds when $m$ numbers a $T$-proof of the sentence numbered $n$ according to a different numbering scheme 2.

Let $\mathsf{Prf_1}$ represent $Prf_1$ in $T$, and put $\Box_1\varphi =_{def}$ $\exists \mathsf{x}\mathsf{Prf_1(x,\overline{\ulcorner\varphi\urcorner})}$, where $\overline{\ulcorner\varphi\urcorner}$ is $T$'s standard numeral for the number for $\varphi$ under scheme 1. Similarly for $\Box_2\varphi$.


A) Is it known what are the (most general?) conditions on the relation between coding schemes 1 and 2 for which we have

$T \vdash \Box_1\varphi \leftrightarrow \Box_2\varphi$, for any sentence $\varphi$?

B) What are the nicest/weakest(?) "derivability conditions" on a box $\Box$ in $T$, which if satisfied by both $\Box_1$ and $\Box_2$, mean that $T$ can again prove that equivalence?

share|cite|improve this question
up vote 4 down vote accepted

$\DeclareMathOperator\prf{Prf}\DeclareMathOperator\con{Con}$ As for A, I don’t think there are any useful criteria known that would guarantee the provable equivalence of two proof predicates that would not beg the question.

As for B, no “derivability conditions” in the usual sense the word is used can do this, assuming the conditions hold at least for the standard construction of a proof predicate based on proofs in a common proof system for first-order logic together with a $\Delta^0_1$ list of axioms.

Consider the following construction. Let $\tau(x)$ be any $\Sigma^0_1$-formula defining an axiom set for $T$, and $\prf_\tau$ the associated proof predicate. Pick any $\Pi^0_1$-sentence $\pi=\forall x\\,\theta(x)$ with $\theta\in\Delta^0_0$ which is true in $\mathbb N$, but unprovable in $T+\con_\tau$. Define $\sigma(x)=(\tau(x)\lor\exists y\le x\\,\neg\theta(y))$, and let $\prf_\sigma$ be the corresponding proof predicate. Then $\prf_\sigma$ is a proof predicate for $T$ (since in $\mathbb N$, $\tau$ and $\sigma$ are equivalent), but $T$ does not prove $\Box_\sigma\bot\to\Box_\tau\bot$: indeed, reasoning in $T$, if $\pi$ fails, then every formula with a sufficiently large Gödel number is a $\sigma$-axiom, and plenty of such formulas are contradictions, hence $\Box_\sigma\bot$. Contrapositively, $T+\con_\sigma$ proves $\pi$, hence using our assuption on $\pi$, $T+\con_\tau$ cannot prove $\con_\sigma$.

share|cite|improve this answer
Thanks, this looks very promising! But (I'm no doubt being dim here) it would be helpful if you could spell out more of the proof of the final claim ...! – Peter Smith Jul 9 '12 at 20:00
I added some details, I hope it is more clear now. – Emil Jeřábek Jul 10 '12 at 11:40
Thanks for the extra details! – Peter Smith Jul 11 '12 at 6:33

OK, maybe the question is going right past me, I don't understand a thing, and this is a lame non-answer, and you have something in mind I don't begin to comprehend. But is T supposed to be a first-order theory? In this case it has a certain collection of models and these aren't related to the numbering scheme. The provable sentences are just the ones that are true in all the models, per the completeness / compactness theorem. Proving the compactness theorem as I understand it takes a rather powerful theory (I think it is a second order sentence in $\mathbb N$ and relies on a weak form of the axiom of choice). But if T is this powerful, doesn't it always prove what you are asking for every formula? Are you only interested in certain (weaker) classes of theories? I'd expect the theory matters and not just the formulas.

share|cite|improve this answer
There is no computably axiomatizable theory $T$ which proves what Peter is asking for every formula. Consider the stupid (but totally legitimate) definition $Prf_\psi(x, [\phi]):=Prf_1(x, [\phi])\vee \exists y(Prf_1(x, [\psi]))$ for some fixed $\psi$ not proved by $T$. $T$ clearly cannot prove the equivalence of $Prf_\psi$ and $Prf_1$ for all choices of $\psi$, since then $T_1$ would prove ``$T_1$ is inconsistent or $\psi$ is not provable from $T_1$". Particularly, if $T_1$ proved this for all $\psi$ and consisted of true sentences of arithmetic, we could compute a completion of $T_1$ (cont'd) – Noah Schweber Jul 9 '12 at 4:11
(cont'd) since we would know that $T_1$ proves $\chi$ iff $T_1$ does not prove ``If $T_1$ proves $\chi$, then $T_1$ is inconsistent." So in fact, given any subtheory of true arithmetic (and, I suspect, any sufficiently strong theory at all), there will be many proof predicates which are not provably equivalent. – Noah Schweber Jul 9 '12 at 4:12
Noah: Thanks for this -- and I suspect that my Qn A misfires (I was wondering about fiddling with coding schemes, forgetting to keep other things constant!). But with your construction, do we get the second half of the defn for representing a relation? If not-$\mathit{Prf}_1(m, n)$ we get $T \vdash \neg\mathsf{Prf_1(m, n)}$. And by your hypothesis, for all $m$ we get $T \vdash \neg\mathsf{Prf_1(m, [\psi])}$. But that won't give us that if not-$\mathit{Prf}_1(m, n)$ then $T \vdash \neg\mathsf{Prf_1(m, n)} \land \neg\mathsf{\exists x Prf_1(x, [\psi])}$ will it? – Peter Smith Jul 9 '12 at 6:48

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.