[FOM] the notion of "effectively complete"

[Rupert McCallum]

Dear FOM-ers,
I have been trying to get clear in my mind in what sense PA^2+\{Det( boldface \Pi^1_n ) : n \in \omega \} is "effectively complete", and I was wondering if we have some kind of handle on how much consistency strength you need to be "effectively complete" for first-order arithmetic. Given that Harvey Friedman's finite form of Kruskal's theorem is unprovable in predicative analysis, it seems that predicative analysis is not enough to be "effectively complete" for first-order arithmetic. Is there some level of consistency strength, such as maybe \Pi^1_1-CA_0 or \Pi^1_2-CA_0 where in some sense we can safely say that from this point on there are no more examples of incompleteness at the level of first-order arithmetic except for Goedel-type ones, or is that not known or maybe even not really possible to precisely state?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180918/076e6992/attachment.html>