Unprovability of sharp versions of Friedman’s sine-principle

Abstract:

For every $n\geq 1$ and every function $F$ of one argument, we introduce the statement $\mathrm {SP}_F^n$: “for all $m$, there is $N$ such that for any set $A=\{a_1, a_2, \ldots , a_N\}$ of rational numbers, there is $H\subseteq A$ of size $m$ such that for any two $n$-element subsets $a_{i_1}< a_{i_2}<\cdots < a_{i_n}$ and $a_{i_1}< a_{k_2}< \cdots < a_{k_n}$ in $H$, we have \[ |\sin (a_{i_1}\cdot a_{i_2} \cdots a_{i_n}) - \sin (a_{i_1}\cdot a_{k_2} \cdots a_{k_n} )|< F(i_1)". \] We prove that for $n\geq 2$ and any function $F(x)$ eventually dominated by $({2 \over 3})^{\log ^{(n-1)}(x)}$, the principle $\mathrm {SP}_F^{n+1}$ is not provable in $I\Sigma _n$. In particular, the statement $\forall n \mathrm {SP}_{({2 \over 3})^{\log ^{(n-1)}}}^n$ is not provable in Peano Arithmetic. In dimension 2, the result is: $I\Sigma _1$ does not prove $\mathrm {SP}^2_F$, where $F(x)=({2 \over 3})^{\sqrt [A^{-1}(x)]{x}}$ and $A^{-1}$ is the inverse of the Ackermann function.