Timeline for Does the Feferman-Schutte analysis give a precise characterization of Predicative Second-Order Arithmetic?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 26, 2013 at 15:06 | comment | added | Keshav Srinivasan | @AndreasBlass Thanks, I didn't notice that part. So now the question becomes, does $ATR_0$ exhaust the set of statements that are predicatively acceptable? In other words, is $ATR_0$ "maximally" locally predicatively justifiable, or is there a larger system that is maximal? | |
| Sep 26, 2013 at 15:00 | comment | added | Andreas Blass | At the bottom of page 18, Feferman says that $ATR_0$ is locally predicatively justifiable, which, according to the definition on page 16, would imply that each individual theorem is predicatively justifiable, but not necessarily that a predicativist would see the whole system as justified. | |
| Sep 26, 2013 at 14:57 | comment | added | Keshav Srinivasan | @AndreasBlass Yes, you may be right. So in that case do you think all the theorems of $ATR_0$ are predicatively acceptable? | |
| Sep 26, 2013 at 14:49 | comment | added | Andreas Blass | @KeshavSrinivasan The passage you quoted isn't the whole sentence; Feferman precedes it with "It turns out in practice that". I suspect he is making a distinction here between mathematical facts (the subject of this sentence) and metamathematical facts like Con(PA) (or the well-foundedness of $\varepsilon_0$ or the existence of a truth predicate for first-order arithmetic). The next sentence reformulates the claim in terms of "everyday mathematics", and the sentence after that says that there is no theorem that can establish this. | |
| Sep 26, 2013 at 14:39 | comment | added | Keshav Srinivasan | @AndreasBlass Then why does Feferman say "if a known mathematical result can be established predicatively, it can already be done in a system conservative over Peano Arithmetic (PA)" on page 19 of this paper: math.stanford.edu/~feferman/papers/predicativity.pdf | |
| Sep 26, 2013 at 14:20 | comment | added | Andreas Blass | @KeshavSrinivasan It seems to me that a predicativist, who (as you assumed in the question) accepts all the ordinals below $\Gamma_0$ and thus in particular accepts $\varepsilon_0$, would also accept Gentzen's consistency proof for PA. In fact, I would expect predicativists to also accept the truth predicate for first-order sentences of arithmetic and thus to accept the "obvious" proof that PA is consistent because all its axioms are true. | |
| Sep 26, 2013 at 12:55 | comment | added | Keshav Srinivasan | How does that quote answer my question? I want to know how to characterize the second-order statements that are predicatively provable. By the way, how can he say that $ATR_0$ proves the same first-order truths as a predicative system? Doesn't it prove $Con(ACA_0)$ and thus $Con(PA)$? And isn't it not possible to predicatively prove any statement of first-order arithmetic not already provable in $PA$? | |
| Sep 26, 2013 at 6:31 | history | answered | alexod | CC BY-SA 3.0 |