Joel, I am not quite following your comment. As said, I am quite convinced that Goodman can be proven in FOL + PA + COR, (but it is a more than year ago that I have thought about it). Are you saying that this is incorrect or that this is similar to transfinite induction?

Note, that Goodstein can be proven in second order logic. So, if the sets are defined by predicates and you allow quantification over it, you have effectively a second order system. The proof in such system might however become close to the transfinite proof.

Access to the book again. The problem is that the first lemma of 6.4 is a lemma that can not be expressed as a lemma in FOL+PA (therefore not formally proven). If you want something that can be expressed in FOL+PA, one should have a sequence like construction, where you prove that the sequence can be extended with a new element. Such as theorem 1.9ii of the piece of Jaap van Oosten. Consequence is that Shoenfield only proves informally that certain functions are recursive, but is insufficient shown that recursiveability is provable in PA. I don't know if any theorems in the book depend on it.

If the answer is yes, then the next question is if it is NPC.

I agree with you that a fully formal proof would make a book unreadable (although, in these times you can put it on the internet and give a reference in the book :-). However, one can adopt a style of writing, where it is very clear how theorems (so, not proofs) could be writtten formaly. The referenced piece of Jaap van Oosten follows this style, and leaves many proofs to the reader (which I consider okay). The Shoenfield book doesn't follow this style. The sequences pop up in informal mathematics, without proper link to the formal part.

Note, that the proof is not required for the remaining part of the book. It is necessary to show that you can do basic mathematics (whatever that is) in FOL+PA. The book only addresses that FOL+PA can define certain things, such as computable functions. Still, I consider it an omission. My question popped up, because I was looking at rather simple systems where you could do some real mathematics, without the complexity of ZFC or type theory. If you start with a closure operator and a successor operator, you don't need the + and x of PA and it is a better prequal to 2nd order logic.

Andreas, I don't have the book by hand, because I am typing from a different location. But I do not agree with you that the proof was designed to be easily formalizable. The informal proof starts with an sequence. In the formal part, you are just trying to prove the basic properties of sequence. So, that is a no go. If you look to the reference I gave of Jaap van Oosten, you will see that the proof contains several non trivial induction step. You need to prove that a sequence can be extended. This is not trivial, when it is encoded with prime number, because you need to choose a new one.

@Andrew, although it is often mentioned that PA or PRA suffices, it is very hard to find the right material that tells how. There are some tricks to go from numbers to more complex datastructures and proves of that. Loops in programs can be rather easily expressed in closures. But, then you need the basic properties of closures. See for a detailed build of theorems: staff.science.uu.nl/~ooste110/syllabi/peanomoeder.pdf

There is always the problem with probabilistic or statistical methods, that you may not ignore knowledge. In mathematical proof you may ignore info, that you don't need. If value c is determined, but someone comes with a good argument that the c is incorrect in this particular case, then you may not ignore that argument. That makes any answer obtained by this method, instable due to future knowledge.

Henry, thanks for pointing this out. I mean second order logic as in reverse math. So, where functions and predicates are just objects and with full comprehension principle. For my question it is only relevant, that we have a stronger logic that FOL + PA, that is capable of proving the consistency of FOL + PA. As far I know (but I could be wrong), second order logic in the sense of reverse math, is capable of that. For any consistent system that is capable of proving consistency of FOL + PA, it is not possible to prove relative consistency in that system. So, why does that proof fail?

Schoppenhauer, thanks for the answer. But this is not exactly what I was looking for. You extend the second order logic with additional axioms. But, I just want, without extending the logic, a theorem in second order logic, for which the proof does not reduce to a trivial first order logic theorem, when all variables are filled in. As I explained in my question, I think such theorem must exists, because if it does not exist the logic could prove its own consistency.

Neil, thanks for answer. I have learned some HOL-light. HOL, Isabelle and Coq (I don't know Agda), are type theory, I thought it would be simpler to restrict it to second order logic. If I indeed want to make such algorithm, then you are right that I need to be more specific. However, in general I can say, that such algorithm won't work, because it would ultimo mean that the logic could prove it's own consistency if it can prove the termination of the algorithm. Since, I can do these things manually, I don't understand which cases are intrinsically hard. I think these cases are in all sys.

Noah, thanks for reading my question. With 'proof' I mean the whole derivation tree of a theorem. For second order logic, I mean a logic where I can quantify over functions or predicates. I don't know what you mean that second-order logic has no good proof system. At least I can say, in informal mathematics, a proof that requires quantification over functions or predicates. For the proof reduction, it is difficult to be more clear, because I failed to make the precise algorithm. It is an attempt to automate the things I can do manually, but I want to understand better, why I failed.