Applied Proof Theory: Proof Interpretations and their Use in Mathematics

摘要: Preface.- Introduction.- Unwinding of proofs ('Proof Mining').- Intuitionistic and classical arithmetic in all finite types.- Representation Polish metric spaces.- Modified realizability.- Majorizability the fan rule.- Semi-intuitionistic systems monotone modified Godel's functional ('Dialectica') interpretation.- Systems based on logic Functional interpretation full analysis.- A non-standard principle uniform boundedness.- Elimination Skolem functions.- The Friedman-Dragalin A-translation.- Applications to analysis: general metatheorems I.- Case study I: Uniqueness approximation theory.- II.- II: fixed point theory nonexpansive mappings.- Final comments.- References.- Index.