On normalization of proofs in set theory

Lars Hallnäs. On normalization of proofs in set theory. Warszawa: Instytut Matematyczny Polskiej Akademi Nauk, 1988. <http://eudml.org/doc/268566>.

@book{LarsHallnäs1988,
abstract = {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.............................................................................................................................................95Errata Page: 6₂ For: r,s Read: r,t Page: 75² For: $ϕ_\{x∈t(x̅)\}$ Read: $ϕ_\{x∈r(x̅)\}$},
author = {Lars Hallnäs},
keywords = {naive set theory; partial normalization; Girard's method of computability predicates; intuitionistic systems; well-founded fragments; ZF; semiformal system SET describing the cumulative hierarchy; E-theorems},
language = {eng},
location = {Warszawa},
publisher = {Instytut Matematyczny Polskiej Akademi Nauk},
title = {On normalization of proofs in set theory},
url = {http://eudml.org/doc/268566},
year = {1988},
}

TY - BOOK
AU - Lars Hallnäs
TI - On normalization of proofs in set theory
PY - 1988
CY - Warszawa
PB - Instytut Matematyczny Polskiej Akademi Nauk
AB - 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.............................................................................................................................................95Errata Page: 6₂ For: r,s Read: r,t Page: 75² For: $ϕ_{x∈t(x̅)}$ Read: $ϕ_{x∈r(x̅)}$
LA - eng
KW - naive set theory; partial normalization; Girard's method of computability predicates; intuitionistic systems; well-founded fragments; ZF; semiformal system SET describing the cumulative hierarchy; E-theorems
UR - http://eudml.org/doc/268566
ER -