Completeness and decidability

[Richard Kimberly Heck]

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: https://brown.zoom.us/j/94571455010
Personal link: https://brown.zoom.us/my/rikiheck

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
Google Scholar:  https://scholar.google.com/citations?user=QUKBG6EAAAAJ
ORCID:           http://orcid.org/0000-0002-2961-2663
Research Gate:   https://www.researchgate.net/profile/Richard_Heck