Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Cover of the book
Tytuł książki

On normalization of proofs in set theory

Seria

Rozprawy Matematyczne tom/nr w serii: 261 wydano: 1988

Zawartość

Warianty tytułu

Abstrakty

EN

CONTENTS
Introduction..............................................................................................................................................5
I. Naive set theory.....................................................................................................................................6
1. The formal system................................................................................................................................6
2. Inversion and reduction properties of the rules of inference..............................................................12
3. Rules of contraction...........................................................................................................................17
4. Normalizability.....................................................................................................................................22
5. Counter-examples to normalizability in set theory...............................................................................24
6. C-normalizability.................................................................................................................................28
7. Concepts of normalizability and C-normalizability for naive set theory with intuitionistic logic.............33
II. Well-founded fragments of naive set theory........................................................................................33
1. Basic definitions, properties of C-normal deductions..........................................................................33
2. Axioms for set theory..........................................................................................................................37
3. The language SET..............................................................................................................................50
4. Semantical motivation for the rules of contraction..............................................................................54
III. C-normalizability of deductions in well-founded fragments of naive set theory...................................62
1. Well-foundedness predicates and well-foundedness objects.............................................................63
2. $ϕ_{T(x̅)}(α̅(t̅))$..................................................................................................................................66
3. The substitution property....................................................................................................................84
4. Every deduction in N satisfies some negation closed W-predicate.....................................................87
5. C-normalizability for well-founded fragments of naive set theory with intuitionistic logic.....................92
6. Notes..................................................................................................................................................94
References.............................................................................................................................................95

Słowa kluczowe

Tematy

Miejsce publikacji

Warszawa

Copyright

Seria

Rozprawy Matematyczne tom/nr w serii: 261

Liczba stron

95

Liczba rozdzia³ów

Opis fizyczny

Dissertationes Mathematicae, Tom CCLXI

Daty

wydano
1988

Twórcy

  • Filosofiska Institutionen, Stockholms Universitet, 106 91 Stockholm, Sweden

Bibliografia

  • [G] G. Gentzen, Untersuchungen über das logische Schliessen, Matematische Zeitschrift 39 (1934), 176-210 and 405-431.
  • [Gi] J. Y. Girard, Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupre dans l'analyse et la théorie des types, Proceedings of the second Scandinavian logic symposium, ed. J. E. Fenstad, North Holland, Amsterdam 1971.
  • [M1] P. Martin-Löf, Hauptsatz for the intuitionistic theory of iterated inductive definitions. Proceedings of the second Scandinavian logic symposium, ed. J. E. Fenstad, North Holland, Amsterdam 1971.
  • [M2] P. Martin-Löf, Hauptsatz for the theory of species, Proceedings of the second Scandinavian logic symposium, ed. J. E. Fenstad, North Holland, Amsterdam 1971.
  • [M3] P. Martin-Löf, Hauptsatz for intuitionistic simple type theory, in: Logic, methodology and philosophy of science IV, ed. P. Suppes, North Holland, Amsterdam 1973.
  • [M4] P. Martin-Löf and P. Hancock, Syntax and semantics of mathematical language (Manuscript).
  • [P] W. Powell, Normalization in ZF (abstract).
  • [Pr1] D. Prawitz, Natural deduction, Almqvist & Wicksell, Stockholm 1965.
  • [Pr2] D. Prawitz, Ideas and results in proof theory. Proceedings of the second Scandinavian logic symposium, ed. J. E. Fenstad, North Holland, Amsterdam 1971.
  • [Pr3] D. Prawitz, Towards a foundation of a general proof theory, in Logic, methodology and philosophy of science IV, ed. P. Suppes, North Holland, Amsterdam 1973.
  • [Pr4] D. Prawitz, On the idea of a general proof theory, Synthese 27 (1974), 63-77.
  • [Pr5] D. Prawitz, Validity and normalizability of proofs in first and second order classical and intuitionistic logic, Atti del congresso nazionale di logica, Bibliopolis, Neapel 1981.
  • [Sch] K. Schütte, Syntactical and semantical properties of simple type theory, Journal of Symbolic Logic 25 (1960), 305-326.
  • [T] W. Tait, Intentional interpretation of functional of finite type. Journal of Symbolic Logic 32 (1967), 198-212.

Języki publikacji

EN

Uwagi

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

Identyfikator YADDA

bwmeta1.element.zamlynska-2e4a4d2f-6a08-47b6-8e9b-1f63f3aac438

Identyfikatory

ISBN
83-01-07604-6
ISSN
0012-3862

Kolekcja

DML-PL
Zawartość książki

rozwiń roczniki

JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.