What people are saying - Write a review
We haven't found any reviews in the usual places.
consider the current state of constructive foundations of classical analysis
of Vol I and Section VI by V A Howard Section V and Appendices
ination of the Xoperator
1 other sections not shown
Appendix argument assume assumption axiom of bar axiom of choice bar induction applied bar recursion Brouwer's characteristic functional Church's thesis classical analysis comprehension axiom consider consistency proof constants constructive functions continuous functionals cp(u cut free decidable defined denote Dialectica interpretation equations equivalent extended extensionality finite sequences finite type follows free choice sequences free ips variables free variables freely chosen function variables functional of type functionals of finite given Godel's Hence higher type objects hyperarithmetic impredicative induction of type inductive definitions intuitionistic logic Kleene Kleene's Kreisel Lemma lh(c mathematics means natural numbers notation notion number theoretic functions obtained predicate logic primitive recursive functionals principle provable proved quantifier-free quantifiers R-founded recursion of type reducible replaced restricted result rules satisfies schema second order arithmetic Section set theory subformula Suppose term of type transfinite induction transfinite recursion type symbols verify