Timeline for What are key $\Sigma^0_2$ or $\Pi^0_3$ theorems?
Current License: CC BY-SA 3.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 28, 2015 at 10:15 | vote | accept | Lucas K. | ||
| Aug 23, 2015 at 13:13 | answer | added | Henry Towsner | timeline score: 7 | |
| Aug 23, 2015 at 11:25 | comment | added | Lucas K. | @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. | |
| Aug 23, 2015 at 10:17 | comment | added | Emil Jeřábek | Even better, the $\Pi^0_2$ fragment of PA is axiomatized by the uniform $\Sigma_1$ reflection schema for finite subtheries of PA (that is, for the theories $I\Sigma_n$) | |
| Aug 23, 2015 at 9:54 | comment | added | Joel David Hamkins | PA proves the consistency of the $\Sigma^0_n$ fragment of PA, and this is a $\Pi^0_1$ assertion, and hence $\Sigma^0_2$. Does your system prove the consistency of all these fragments of PA? This would be required for your conservativity result. | |
| Aug 23, 2015 at 9:45 | history | edited | Lucas K. | CC BY-SA 3.0 |
edited body
|
| Aug 23, 2015 at 9:38 | comment | added | Lucas K. | @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. | |
| Aug 23, 2015 at 9:30 | comment | added | Lucas K. | @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. | |
| Aug 23, 2015 at 9:11 | history | edited | Lucas K. | CC BY-SA 3.0 |
Explained it better.
|
| Aug 23, 2015 at 8:36 | comment | added | Andreas Blass | Although I'm not a number theorist and therefore can't immediately give you details, I believe that there are some important results saying that certain Diophantine equations have only finitely many solutions, without giving an explicit bound for those solutions. The natural formalization of such a statement would be a $\Sigma^0_2$ sentence. | |
| Aug 23, 2015 at 0:11 | comment | added | Carl Mummert | I don't completely understand the first paragraph. $\text{Con}(\text{PA})$ is a $\Sigma^0_2$ sentence that does add strength to PA. At the same time, many theorems in the literature are $\Pi^1_1$ or $\Pi^1_2$, rather than arithmetical. If no set parameters are allowed, then it is hard to state most ordinary theorems. | |
| Aug 22, 2015 at 22:17 | history | asked | Lucas K. | CC BY-SA 3.0 |