I am attempting to back two claims in this problem:

I use $\textbf{Q}$ to denote minimal arithmetic for this post.

I use the term 'rudimentary sentence' to denote formulas built using only negation, conjunction, disjunction, and bounded quantifications. It has been pointed out to me that these are more formally called $\Delta_0$ sentences. Additionally, '$\exists$-rudimentary' refers to $\Sigma_1$ sentences.

A theory $T$ is 1-consistent if for all $\exists$-rudimentary sentences of the form $\exists x$ $F(x)$ , if $T\vdash \neg F(0)$, $T\vdash \neg F(1)$, $T\vdash \neg F(2)$,... then $T\not\vdash\exists x$ $F(x)$.

To show: If $T$ is 1-consistent, then $T$ is consistent.


From this point on, I assume that $T$ is a 1-consistent theory.

I use a function now $Prv_T(x)$ to mean $\vdash_T A$ if and only if the sentence $Prv(\ulcorner A\urcorner )$ is correct under the standard interpretation.

Let $T$ now be a 1-consistent ($\Sigma_1$-sound) theory extending minimal arithmetic.

I let $G$ be such that

$T \vdash G \leftrightarrow Prv(\ulcorner G\urcorner)$.

To show: $T\not\vdash \neg G$.

I apologize in advance if this is unclear, I am not yet totally comfortable communicating this material.

  • $\begingroup$ Is "rudimentary sentence" your own word? It sounds like you're defining what is usually called $\Delta_0$ sentences, and your "$\exists$-rudimentary sentences" must be $\Sigma_1$ sentences. $\endgroup$ May 13 '16 at 7:17
  • $\begingroup$ @HenningMakholm It is probably an informalism, I am following Boolos, Burgess, and Jeffrey, Computability and Logic. I apologize for this, I'll add it in. $\endgroup$
    – faux
    May 13 '16 at 7:21
  • $\begingroup$ By the way, the natural continuation of your $G$-based reasoning is Löb's theorem which says (under suitable assumptions) that if $T\vdash G\leftrightarrow Prv(\ulcorner G\urcorner)$ then $T\vdash G$. But in order to get the last step from $T\vdash G$ to $T\not\vdash \neg G$, you need to already know that $T$ is consistent, so I don't think you'll actually make progress that way. $\endgroup$ May 13 '16 at 7:33
  • $\begingroup$ @HenningMakholm I apologize! You are very correct on that - for the second part, I am to operate under the assumption that $T$ is a 1-consistent ($\Sigma_1$-sound) theory extending minimal arithmetic (I will add that in now). Would Löb's theorem now apply? $\endgroup$
    – faux
    May 13 '16 at 7:39
  • $\begingroup$ x @faux: I think Löb's theorem applies (if you have enough machinery available to construct your $G$ in the first place, which I'll assume) -- I'm just doubting that it's helpful for your goal of proving $T$ consistent. $\endgroup$ May 13 '16 at 7:43

Your diagonalization ansatz seems to be overkill for this purpose.

Instead simply consider that in an inconsistent theory everything is provable. So if $T$ is inconsistent, you can let $F$ be any formula whatsoever; the premise of your definition of "1-consistent" will then be satisfied but the conclusion is not. So it is impossible for a theory to be inconsistent yet 1-consistent.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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