0
$\begingroup$

If $T$ is a consistent theory of arithmetic able to represent all computable functions, and in particular the $Proof(y,x)$ relation on natural numbers where $y$ is an encoding of a proof terminating in the formula with number $x$. I.e. if the relation holds on numbers $m,n$ then $T\vdash Proof(\underline{m},\underline{n})$ and otherwise $T\vdash \neg Proof(\underline{m},\underline{n})$. Ambiguity about the distinction between the relation and the formula for the relation is permitted. Suppose in $T$ the $Neg(y,x)$ relation, where $x$ is the number of the formula which is the negation of the formula for $y$. Moreover suppose for every formula $\varphi$,

$$T\vdash Neg(\varphi,v)\leftrightarrow v = \ulcorner\neg\varphi\urcorner$$ $$T\vdash Neg(v,\varphi)\rightarrow v<\ulcorner\varphi\urcorner$$

I take it this implies that we can universally generalize these formulae.

If we further define $Proof^{**}(y,x)$ as

$$Proof(y,x)\land \forall z<y\forall v([Neg(v,x)\lor Neg(x,v)]\rightarrow \neg Proof(z,x)$$

I have just shown that $T\vdash Proof^{**}(\underline{n},\ulcorner\varphi\urcorner)\leftrightarrow Proof(\underline{n},\ulcorner\varphi\urcorner)$. If we next define $Prv^{**}(x)$ as $\exists y Proof^{**}(y,x)$ then I need to prove

$$T\vdash Prv^{**}(\ulcorner\varphi\urcorner)\rightarrow \neg Prv^{**}(\ulcorner\neg\varphi\urcorner)$$

If $\varphi$ has proof coded $n$ then by consistency it doesn't have a proof of $\neg\varphi$ and by representability, $T\vdash \neg Proof^{**}(\underline{0},\ulcorner\neg\varphi\urcorner)\land ...\land \neg Proof^{**}(\underline{n-1},\neg\varphi) $ from which the provability follows. If $\varphi$ doesn't have a proof, though, I think what I should be trying to do is show $T\vdash \neg Prv^{**}(\ulcorner \varphi\urcorner)$ but this is equivalent to proving an unbounded universally quantified sentence, and I'm not sure how that could be possible. On the other hand we know that there are some sentences neither provable nor disprovable, so if $\varphi$ is one such sentence then showing this might be impossible. Perhaps somehow I still need to show the conditional without necessarily showing any one part of it? ... But I'm quite lost about how that might go.

$\endgroup$
1
  • $\begingroup$ $T \vdash Proof(n,\ulcorner \varphi \urcorner) \leftrightarrow Proof^{**}(n,\ulcorner \varphi \urcorner)$ doesn’t seem right. If it were, then $T \vdash (Prv(n) \leftrightarrow Prv^{**}(n))$, which can’t be since $T \not \vdash Prv(\ulcorner \phi \urcorner) \to \neg Prv(\ulcorner \neg \phi \urcorner)$. $\endgroup$
    – PW_246
    Jul 8 at 16:42

1 Answer 1

Reset to default
2
$\begingroup$

For simplicity, let's conflate objects and their codes (obviously this isn't allowed when writing the proof, but it can be useful for coming up with the proof). Intuitively, $Prv^{**}(p)$ says "there is a proof of $p$ shorter than any disproof of $p$." I don't quite mean "shorter," of course, but rather "of smaller Goedel number," but that's a bit of a mouthful. So (reasoning in $T$) suppose for a contradiction that the statement "$Prv^{**}(p)\wedge Prv^{**}(\neg p)$" held. Then there is a proof $a$ of $p$ with no shorter disproof of $p$, but also a disproof $b$ of $p$ with no shorter proof of $p$. OK - is $a<b$ or is $b<a$?

$\endgroup$
6
  • $\begingroup$ This sounds kind of like a semantic argument, though, no? Wouldn't this just show that a certain sentence is unprovable rather than is negation being provable? $\endgroup$
    – Addem
    Apr 20, 2017 at 4:02
  • 1
    $\begingroup$ @Addem No, the point is that "$Prv^{**}$" isn't just a provability predicate - it also constrains the possible proofs of the negation of the sentence in question. If $Prv^{**}(p)$ holds, then there is some $a$ such that $a$ is a proof of $p$ and no smaller $b$ is a proof of $\neg p$ (or of $q$, if $p=\neg q$). So suppose $Prv^{**}$ held, as witnessed by $a$; then for any proof $c$ of $\neg p$ (or of $q$, if $p=\neg q$), we must have $c>a$; but this means $\neg Prv^{**}(\neg p)$. Note that the conclusion is not that $\neg p$ is unprovable, just that it's not quickly provable. $\endgroup$
    – Noah Schweber
    Apr 20, 2017 at 4:12
  • $\begingroup$ As far as $T$ knows, we could quite easily have $Prv^{**}(p)$ and $Prv(\neg p)$ (where "$Prv(\neg p)$" just says that there is a proof of $\neg p$); it's just that the proof of $\neg p$ would have to come after the first proof of $p$. $T$ isn't sure that $Prv^{**}(p)$ means $p$ isn't disprovable, but $T$ is sure that $Prv^{**}(p)$ means that it's "easier" to prove $p$ than to disprove $p$. (Rosser's trick uses this shift to excellent effect.) $\endgroup$
    – Noah Schweber
    Apr 20, 2017 at 4:15
  • $\begingroup$ Oh, you know, I think I see it--you're saying "suppose for contradiction" as an actual move within $T$ rather than a semantic, metalanguage proof. So the argument goes, since $T \vdash (Prv^{**}(p)\land Prv^{**}(\neg p) )\rightarrow \bot$, basically, then it proves the given conditional sentence. I get it now, thank you! $\endgroup$
    – Addem
    Apr 21, 2017 at 2:37
  • $\begingroup$ @Addem Exactly - everything necessary can be done inside $T$. $\endgroup$
    – Noah Schweber
    Apr 21, 2017 at 3:19

You must log in to answer this question.

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