Completeness and decidability

Richard Kimberly Heck richard_heck at brown.edu
Fri Nov 26 10:54:57 EST 2021

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

Pronouns: they/them/their

Email:           rikiheck at brown.edu
Website:         http://rkheck.frege.org/
Blog:            http://rikiheck.blogspot.com/
Amazon:          http://amazon.com/author/richardgheckjr