I have looked in your notes on your homepage and as far I understand, the proof doesn't require transfinite induction.

With this result I can show that PA (and $ACA_0$) is a conservative extension of Primitive Closure Arithmetic, which I designed, see mathoverflow.net/questions/208696/primitive-closure-arithmetic. This is a very simple system closely related to computation

Many thanks. I will study is, can't judge it immediately. I think this is a very notable result, for several reasons. In reverse mathematics PA and $ACA_0$ are in the same class. Now this range is extended to a system that is less expressive. Also, since $\Pi_2$ has far stronger relation with computation than PA in general, this makes logic and computability theory stronger linked.

@JoelDavidHamkins and Emil Thanks for the replies, but I have difficulty to follow this, but I will see what I can find in my books and on the internet. But the last few weeks I had quite a progress in my proof. For any $\Pi^0_2$ theorem that has a proof that contains sentences not $\Pi^0_2$ I have several rewriting steps. One with Herbrandization, where I later replace the Herbrand functions. This does not work for induction, but I think I found a solution for that. But of course, until I completely worked it out, it can have a terrible flaw.

@AndreasBlass Interesting. Then the question is if that bound can not be calculated in practice or in theory. If the bound can be given in theory, than you would have a $\Pi^0_2$ sentence again. If it can't then we have a truly non-constructive proof. I have almost no knowledge about Diophantine equations, maybe I will raise a question about this, first on Mathematica.

@CarlMummert I have edited my question, I hope this is more clear. My idea is to throw out all sentences that are not $\Pi^0_2$ and then to see whether you loose strength. With $\Sigma^0_2$ I meant not $\Pi^0_2$, I corrected that. $ACA_0$ which allows $\Pi^1_2$ sentences but which is restricted in induction axiom, is a conservative extension over PA. If I prove that PA is a conservative extension over a system limited to $\Pi^0_2$ then $ACA_0$ is also conservative over that system.

It is not the same as CNF, because the sub-formulas on the right and the left can be of any complexity, as long as it doesn't contain 'not'.

Good answer! I would like to add that the mathematical and logic community should value good tools in this perspective. I think it is very hard to get a PhD on an improved tool. For a computer scientist a language like C is quite different than for instance Python. For mathematician/logician they are just a variant on the Turing machine. With such view the tools won't become better.

@LSpice The question was not about improving readability.

In your question you used 11 times 'I', do the same in your work.

@Goldstern Sorry, for the misunderstanding, I mean you don't have the full predicate logic. I will search on "primitive positive". What I try to achieve is something simpler than FOL + PA, because I think FOL + PA misses elegance, the elegance you normally find in math. Second step would be to find out the relation between PCA and FOL + PA. I hope the relative consistency between those two can be proven within PCA. The discussion in this question mathoverflow.net/questions/47150/…, suggests that it is possible, but I might misunderstood.

Goldstein, thanks for the comment. Using closure or fixed points for loops or recursion is not new. What I want to show is that you can do without FOL. That is also why I make the comparison to PRA.

Joel, I hope this will make things more clear.