On normalization of proofs in set theory
Lars Hallnäs
GDML_Books, (1988), p.

CONTENTSIntroduction..............................................................................................................................................5I. Naive set theory.....................................................................................................................................61. The formal system................................................................................................................................62. Inversion and reduction properties of the rules of inference..............................................................123. Rules of contraction...........................................................................................................................174. Normalizability.....................................................................................................................................225. Counter-examples to normalizability in set theory...............................................................................246. C-normalizability.................................................................................................................................287. Concepts of normalizability and C-normalizability for naive set theory with intuitionistic logic.............33II. Well-founded fragments of naive set theory........................................................................................331. Basic definitions, properties of C-normal deductions..........................................................................332. Axioms for set theory..........................................................................................................................373. The language SET..............................................................................................................................504. Semantical motivation for the rules of contraction..............................................................................54III. C-normalizability of deductions in well-founded fragments of naive set theory...................................621. Well-foundedness predicates and well-foundedness objects.............................................................632. ϕT(x̅)(α̅(t̅))..................................................................................................................................663. The substitution property....................................................................................................................844. Every deduction in N satisfies some negation closed W-predicate.....................................................875. C-normalizability for well-founded fragments of naive set theory with intuitionistic logic.....................926. Notes..................................................................................................................................................94References.............................................................................................................................................95

Errata Page: 6₂ For: r,s Read: r,t Page: 75² For: ϕx∈t(x̅) Read: ϕx∈r(x̅)

EUDML-ID : urn:eudml:doc:268566 
@book{bwmeta1.element.zamlynska-2e4a4d2f-6a08-47b6-8e9b-1f63f3aac438,
     author = {Lars Halln\"as},
     title = {On normalization of proofs in set theory},
     series = {GDML\_Books},
     publisher = {Instytut Matematyczny Polskiej Akademi Nauk},
     address = {Warszawa},
     year = {1988},
     zbl = {0667.03041},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.zamlynska-2e4a4d2f-6a08-47b6-8e9b-1f63f3aac438}
}

Lars Hallnäs. On normalization of proofs in set theory. GDML_Books (1988),  http://gdmltest.u-ga.fr/item/bwmeta1.element.zamlynska-2e4a4d2f-6a08-47b6-8e9b-1f63f3aac438/