Completeness and decidability

[Richard Kimberly Heck]

On 11/26/21 16:50, Giovanni Lagnese wrote:
> Obviously, your argument for the left-to-right direction holds not 
> only for PA but also for Q.

Well, PA could prove this for Q, but I suspect that Q itself will not 
formalize that argument. That's just because (as far as anyone knows) Q 
cannot formalize the proof of the first incompleteness theorem, the 
reason being that induction is all over that argument. That said, some 
form of the argument presumably can be formalized in I\Delta_0 + 
\Omega_1, since, as Wilkie and Paris showed in the bounded induction 
paper, you can do G2 there. And that theory is interpretable in Q, even 
if it is (in another sense) much stronger than 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?

No, no ideas at the moment, but the usual proof that first-order logic 
is undecidable surely uses induction, so that proof will not go through 
in Q. (Cuts will not help there.) Probably someone knows what sort of 
theory we need to prove that first-order logic is undecidable?

At first glance, it seems like the proof I gave also uses something like 
\Sigma_1 completeness, which again Q has no hope of proving. I suspect a 
counter-model is readily available. You have such freedom with the 
non-standard elements in models of Q. That's why it's so easy to build 
counter-models to commutativity, etc.

Riki


> On Fri, Nov 26, 2021, 16:55 Richard Kimberly Heck 
> <richard_heck at brown.edu> wrote:
>
>     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
>

-- 
----------------------------
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211126/6991d008/attachment-0001.html>