I didn’t yet read the paper, but it occurs to me that the direction he seems to want to go in (based on your summary) would be better achieved not by directly weakening/removing induction, but by removing axiom 2.
This would “cut off” induction after a certain point while being more directly in the spirit of ultrafinitism. Also, it seems less “brain breaking” to me. (I don’t reject axiom 2, but the notion of rejecting 2 seems less WTF to me then rejecting 5.)
I didn’t yet read the paper, but it occurs to me that the direction he seems to want to go in (based on your summary) would be better achieved not by directly weakening/removing induction, but by removing axiom 2.
This would “cut off” induction after a certain point while being more directly in the spirit of ultrafinitism. Also, it seems less “brain breaking” to me. (I don’t reject axiom 2, but the notion of rejecting 2 seems less WTF to me then rejecting 5.)