Completeness and decidability

Giovanni Lagnese giov.lagn at
Fri Nov 26 16:50:53 EST 2021

Obviously, your argument for the left-to-right direction holds not only for
PA but also for Q. The right-to-left direction (for Q) seems an interesting
question to me. Do you think the answer is probably no? Do you have any
ideas in mind to build a model of Q that shows it?

On Fri, Nov 26, 2021, 16:55 Richard Kimberly Heck <richard_heck at>

> On 11/24/21 03:36, Giovanni Lagnese wrote:
> > Does Q prove
> > "Q is syntactically complete" <--> "for any Sigma_1 definition phi(x)
> > there is a Sigma_1 definition phi'(x) such that Q proves
> > phi'(x)<-->not-phi(x)"
> > ?
> I'd be very surprised if Q proved this, though Q can be surprisingly
> powerful. (See e.g. Visser's proof that Q can do arithmetized
> completeness, via cuts.) But I've thought about it a while, and I'm
> curious what kind of informal proof you have in mind.
> PA does seem to prove the corresponding thing about itself, but the only
> proof I've managed to produce is very indirect. Here's an argument. I am
> reasonably certainly this works.
> PA proves that first-order logic is undecidable; but the set of
> first-order validities is \Sigma_1 definable, and if it were also \Pi_1
> definable, then it would be decidable (and PA can prove that). Hence the
> formula defining the set of first-order validities is PA-verifiably a
> counter-example to the right-hand side. So the right-to-left direction
> follows.
> For the other direction, reason in PA. If PA is inconsistent, then of
> course the right-hand side holds. So suppose PA is consistent. Then PA
> is incomplete (by the formalization of the proof of G1 that lies at the
> heart of G2). So the left-to-right direction holds.
> Certainly Q will not formalize any such argument. I would suppose that
> I\Sigma_1 could do this. Presumably much weaker theories can as well.
> Note also that the same argument, in PA, proves the claim about Q.
> Is there a more direct sort of argument? The equivalence is certainly
> true, but a more 'direct' proof seems hard to come by, at least to me.
> Left to right, what's the obvious choice for \phi'(x)? It's something
> like Bew(\neg\phi(x)). But I don't see how to show in PA, assuming that
> PA is complete, that this is equivalent to \phi(x). The first step of
> the proof is roughly: Suppose \phi(n) and Bew(\neg\phi(n)). There's
> nothing obviously wrong with that, from inside PA: We can't infer
> Bew(\phi(n)), and we can't infer \neg\phi(n). Completeness can't help,
> because we've already assumed that \neg\phi(n) is provable.
> Riki
> --
> ----------------------------
> Richard Kimberly (Riki) Heck
> Professor of Philosophy
> Brown University
> Office Hours: Thursday, 11-12
> Link:
> Personal link:
> Pronouns: they/them/their
> Email:           rikiheck at
> Website:
> Blog:  
> Amazon:
> Google Scholar:
> Research Gate:
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211126/c1ab76ca/attachment-0001.html>

More information about the FOM mailing list