On Constructive Interpretation of Predicative Mathematics

1*-consistent 18 provable a₁ alternand argument axioms B₁ B₂ binding degree class variables consistency proof cut formula cut-free deduction theorem defined definition derivation elementary number theory Ex₁ finitary finite follows Formelbund free function variables free variables func function symbols given proof Gödel number Herbrand alternation Herbrand interpretation Herbrand's theorem Hilbert hypothesis of induction infinite induction interpretation Kreisel lemma ln(a natural numbers no-counter-example number variables obtain a proof ordinal recursive functionals otherwise P₁ predicate calculus premiss prime formulae primitive recursive function proof in RA(S proof of lemma propositional calculus provable in F prove quantifier-free formula quantifiers RA(Z ramified analysis recursion equations recursive number theory reduced proof replacing Schütte's subformula substitution Suppose t₁ theorem 13 theory with induction tion top degree transfinite induction true universal quantification w-consistency W₁ w₂ x₁