Timeline for Natural $\Pi_1$ sentence independent of PA
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 10, 2020 at 9:59 | answer | added | Mohammad Golshani | timeline score: 4 | |
| May 9, 2020 at 0:19 | comment | added | none | @user76284, tbh if you write down a not-too-large system of integer diophantine equations and ask if it has a solution, that seems to wash away the metamathematicality enough that you could possibly convince an unsuspecting 19th century mathematician that it came up in some other context. But of course for suitable coefficients, the insolubility can be unprovable in PA (MRDP theorem). | |
| May 6, 2020 at 20:29 | comment | added | Ulrik Buchholtz | As a step in this direction (giving a natural-looking scheme rather than a single sentence), look at Anton Freund's recent A mathematical commitment without computational strength. | |
| May 6, 2020 at 19:54 | history | edited | user76284 | CC BY-SA 4.0 |
deleted 7 characters in body
|
| May 5, 2020 at 2:19 | comment | added | user44143 | @FrançoisG.Dorais, the OP might also be looking for an example with a proof. | |
| May 4, 2020 at 22:59 | comment | added | François G. Dorais | Considering that Harvey's goal is to achieve simple and natural examples of undecidability, perhaps you have found the right source already. | |
| May 4, 2020 at 19:33 | comment | added | Hermann Gruber | My answer was bad, so I will delete it. But I wanted to save the two enlighting comments to my answer: Goodstein's theorem is a statement of the form $\forall\exists$ (i.e. $\Pi_2$) so unfortunately it's not $\Pi_1$. – user76284 The standard combinatorial statements from the 80s can all be stated as claims that some recursive function is total. Any such statement is $\Pi_2$, and all the famous examples of this kind are properly $\Pi_2$. – Andrés E. Caicedo | |
| May 4, 2020 at 18:09 | comment | added | none | I would say that the word problem for finitely presented groups is not metamathematical, although it asks for an algorithm. Its history goes back to before anyone was thinking about undecidability much. Its specific instances are $\Pi_1$ and some of them are undecidable. Whether concocting a specific undecidable one is natural is up to you, I guess. Same with Hilbert's tenth problem. | |
| May 3, 2020 at 17:25 | history | asked | user76284 | CC BY-SA 4.0 |