In light of the latter restriction, it is not possible to mimic the inductive form of the sorites argument in \(\mathsf{PA}^F\). But of course \(\mathsf{PA}^F\) is still inconsistent in virtue of the conditional form of the argument. Nonetheless, Parikh showed that for appropriate choices of \(\tau\), any proof of a contradiction in \(\mathsf{PA}^F\) must itself be very long.  For instance, if we consider the super-exponential function \(2 \Uparrow 0 = 1\) and \(2 \Uparrow (x+1) = 2^{2 \Uparrow x}\) and let \(\tau\) be the primitive recursive term \(2 \Uparrow 2^k\), it is a consequence of Parikh’s result that any proof of a contradiction in \(\mathsf{PA}^F\) must be on the order of \(2^k\) steps long. For example if \(\tau = 2 \Uparrow 2^{1000}\), then such a proof must be at least \(2^{1000}\) lines   long.[51]  This suggests the possibility of a two-part reply on behalf of the strict finitist to Dummett’s argument against strict   finitism:[52]