What people are saying - Write a review
We haven't found any reviews in the usual places.
Technical notes to the introduction
Part A Regular theories and normalization
2 other sections not shown
Other editions - View all
3xEx 3zCz absoluteness ALGOL 60 arithmetical derivation arithmetical sentence bar induction Bar(d basing function calculus classical contradicting Crit(d.u d,u d,u defined E-atom E-Der(d E-sentence encodes equation Fd,u Final finitary finite first-order formula F GENTZEN Hence Heyting's implies improper reduction ind.hyp inference rules infinitary derivations infinitary proof figures intuitionistic intuitionistic arithmetic ISBN 90 Kleene's recursion theorem KREISEL language LEIVANT LEMMA metamathematical natural deduction Nmble Nmble(iji node normal derivation normalization proof normalization theorem notation NPrf occur parameters pd,u PRAWITZ 65 predicate logic prim prim.rec proof of theorem proof-tree propositional letters provable prove quantifiers regular theories replacing satisfies the subformula schema F schemata second order sequent stable strongly regular subcase subderivation subformula property substitutions tail(w theory of species tion transfinite induction trivially TROELSTRA 73 truth definition type theory uniform variables Vx3y well-founded well-foundedness well-ordering