Timeline for What restriction(s) of Goedel's primitive recursive functionals is (are) necessary and sufficient to prove the consistency of $PRA$
Current License: CC BY-SA 3.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 29, 2016 at 12:23 | vote | accept | Thomas Benjamin | ||
| Jan 29, 2016 at 4:23 | answer | added | Ulrik Buchholtz | timeline score: 4 | |
| Jan 21, 2016 at 15:45 | comment | added | Andrej Bauer | To go from probably to certainly I would like to see a proof. As to your other question, it ought to be similar to the reasoning done by Gödel in Dialectica: if there were a term corresponding to a proof of $\bot$ then there would also exist a normal term corresponding to $\bot$, but there isn't one. | |
| Jan 21, 2016 at 14:12 | comment | added | Thomas Benjamin | @AndrejBauer: what 'extra' would you need to turn that "probably" into "certainly" in your latest comment? If I understand correctly, strong normalization of a term means that it will terminate in a finite number of steps when reduced. What is to prevent a primitive recursive function from terminating in a finite number of steps with $\bot$ (as Prof. Nelson believed)? | |
| Jan 21, 2016 at 13:56 | comment | added | Andrej Bauer | The proof ordinal of PRA is $\omega^\omega$, so what @Ulrik is suggesting seems about right. That is: if you know that all primitive recursive functions normalize (terminate) then you can (probably) conclude that PRA is consistent. | |
| Jan 21, 2016 at 13:19 | comment | added | Thomas Benjamin | @AndrejBauer: Yes, thanks for helping me clarify that point. The question is, can System $T$ be so restricted so that the strong normalization of the restricted system implies the consistency of $PRA$ but no stronger system (e.g. $PA$)? | |
| Jan 21, 2016 at 11:01 | comment | added | Andrej Bauer | What the OP probably means to say is that strong normalization of System $T$ implies consistency of $PA$. And so the question is how to restrict System $T$ so that strong normalization of the restricted system implies consistency of $PRA$ but is too weak to imply consistency of $PA$. | |
| Jan 19, 2016 at 17:05 | comment | added | Ulrik Buchholtz | @ThomasBenjamin, OK, I've had a busy couple of days, but I'll put something up tomorrow. | |
| Jan 19, 2016 at 12:48 | comment | added | Thomas Benjamin | @Ulrik: Please take cody's advice. I would accept such an answer as it would be helpful to me. | |
| Jan 14, 2016 at 20:45 | comment | added | Thomas Benjamin | @Ulrik: Can the fragment of System $T$ you mention in your comment be used to prove the consistency of $PRA$? Though you say that System $T$ interprets $PA$ but does not prove $Con(PA)$, Shoenfield, in his text Mathematical Logic (pp. 214--222) claims to have used Goedel's primitive recursive function of finite type to prove the consistency of $PA$, so you might want to include why he believed he did this in your answer as well. I, myself, am just after the fragment (restriction) of System $T$ that just proves the consistency of $PRA$, nothing more. | |
| Jan 14, 2016 at 18:05 | comment | added | cody | @Ulrik: I think it is: it would be worthwhile, I think, to clarify the connection between "provably total functionals" and consistency strength, and turn your comment into an answer. | |
| Jan 14, 2016 at 18:01 | comment | added | Ulrik Buchholtz | System T interprets PA; it doesn't prove Con(PA). They are in this sense of equivalent strength: the recursive functions N→N represented by terms of System T are precisely the provably recursive functions of PA. A simple way to restrict System T so that you get just the primitive recursive functions is to allow only recursions with target type N (that is, you can still explicitly define and compose higher type functionals, but you cannot define those by recursion). Is that what you're after? | |
| Jan 14, 2016 at 16:57 | comment | added | Thomas Benjamin | @NoahSchweber: You're right--I am asking "how weak a theory with a certain form [the "theory" being Goedel's Dialectica interpretation using his primitive recursive functionals of finite type to interpret Heyting arithmetic] which proves that $PRA$ is consistent can be [that is, to just prove that $PRA$ is consistent, nothing more]." Does this explanation help at all? | |
| Jan 14, 2016 at 14:38 | review | Close votes | |||
| Jan 21, 2016 at 15:03 | |||||
| Jan 14, 2016 at 13:08 | comment | added | Noah Schweber | Thanks, but that doesn't help me very much - can you define precisely what you mean? It sounds like you're asking how weak a theory with a certain form which proves that PRA is consistent can be; is this right? If so, what's that form? | |
| Jan 14, 2016 at 13:04 | comment | added | Thomas Benjamin | @NoahSchweber: I mean using the techniques Goedel used to prove the consistency of $PA$ in his Dialectica paper and finding out what sorts of restrictions are needed so these techniques only prove the consistency of Primitive Recursive Arithmetic (you can use Shoenfield's use of Goedel's primitive recursive functionals in Mathematical Logic for his proof of the consistency of Peano Arithmetic as a guide). | |
| Jan 14, 2016 at 9:41 | comment | added | Noah Schweber | I don't really understand what you're asking. What does it mean that a class of functionals proves that a theory is consistent? | |
| Jan 14, 2016 at 7:40 | history | asked | Thomas Benjamin | CC BY-SA 3.0 |