Completeness and decidability

[Giovanni Lagnese]

The point is that, despite the great freedom with nonstandard elements in
Q, it doesn't seem so easy to build a counter-model. This is odd.


On Fri, Nov 26, 2021 at 11:22 PM Richard Kimberly Heck <
richard_heck at brown.edu> wrote:

> 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/20211127/003b1848/attachment.html>