Pointwise hereditary majorization and some applications
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.
- Moment problems in hereditary function spaces
- Haar inequality in hereditary setting and applications
- Majorization methods on hyperplanes and their applications
- Some results on majorization and their applications
- scientific article; zbMATH DE number 2091976
- Point-wise multipliers of Herz-type Besov spaces and their applications
- Hereditary properties of matrices with cut-points
- Pointwise versions of the maximum theorem with applications in optimization
- Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
- Extensional Gödel functional interpretation. A consistency proof of classical analysis
- Gödelsche Funktionalinterpretation für Eine Erweiterung der Klassischen Analysis
- scientific article; zbMATH DE number 51623 (Why is no real title available?)
- scientific article; zbMATH DE number 3231083 (Why is no real title available?)
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Note on the fan theorem
- Recursive Functionals and Quantifiers of Finite Types I
- Some models for intuitionistic finite type arithmetic with fan functional
- Spielquantorinterpretation unstetiger Funktionale der höheren Analysis
- Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Monotone majorizable functionals
- On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness
- Functional interpretation of Aczel's constructive set theory
- The FAN principle and weak König's lemma in Herbrandized second-order arithmetic
- Bounded functional interpretation
- Proof interpretations with truth
- Light monotone Dialectica methods for proof mining
- Confined modified realizability
- Compact and majorizable functionals of finite type
- Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
- Relative constructivity
- Some logical metatheorems with applications in functional analysis
- A syntactic approach to continuity of T-definable functionals
- Classical provability of uniform versions and intuitionistic provability
- A Look at the Generalized Heron Problem through the Lens of Majorization-Minimization
- Proof mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions
- A Gentzen-style monadic translation of Gödel's system T
- Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
- Proof mining and probability theory
- Logical metatheorems for abstract spaces axiomatized in positive bounded logic
This page was built for publication: Pointwise hereditary majorization and some applications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q805612)
