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ć.