Pointwise hereditary majorization and some applications (Q805612): Difference between revisions

A pointwise version of the Howard-Bezem notion of hereditary majorization is introduced, which has various advantages, and its relation to the usual notion of majorization is discussed. This pointwise majorization of primitive recursive functionals (in the sense of Gödel's T as well as Kleene/Feferman's PR) is applied to systems of intuitionistic and classical arithmetic (H and \(H^ c)\) in all finite types with full induction, as well as to the corresponding systems with restricted induction \(\hat H\upharpoonright\) and \(\hat H\upharpoonright^ c.\) 1) H and \(\hat H\upharpoonright\) are closed under a generalized fan-rule. For a restricted class of formulae this also holds for \(H^ c\) and \(\hat H\upharpoonright^ c.\) 2) We give a new and very perspicuous proof that for each \(\Phi^ 2\in T(PR)\) one can construct a functional \({\tilde \Phi}{}^ 2\in T(PR)\) such that \({\tilde \Phi}\alpha\) is a modulus of uniform continuity for \(\Phi\) on \(\{\beta^ 1|\bigwedge n(\beta n\leq \alpha n)\}\). Such a modulus can also be obtained by majorizing any modulus of pointwise continuity for \(\Phi\). 3) The type structure \({\mathcal M}\) of all pointwise majorizable set- theoretical functionals of finite type is used to give a short proof that quantifier-free ``choice'' with uniqueness \((AC!)^{1,0}\)-qf. is not provable within classical arithmetic in all finite types plus comprehension (given by the scheme \((C)^{\rho}:\bigvee y^{0\rho}\bigwedge x^{\rho}(yx=0\leftrightarrow A(x))\) for arbitrary A), dependent \(\omega\)-choice and bounded choice. Furthermore \({\mathcal M}\) separates several \(\mu\)-operators.