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

Completeness properties of classical theories of finite type and the normal form theorem

Seria

Rozprawy Matematyczne tom/nr w serii: 207 wydano: 1983

Zawartość

Warianty tytułu

Abstrakty

EN

CONTENTS
Introduction........................................................................................................................................................................................................................5
0. Terminology and preliminaries......................................................................................................................................................................................12
1. The extent of cut elimination by absorption..................................................................................................................................................................17
2. ∏¹-completeness of second order logic and a new proof of the normal form theorem.................................................................................................24
3. Weak models and proper three-valued models of second order theories....................................................................................................................31
4. Model theoretic proofs of the normal form theorem for higher order systems: comparison with the literature..............................................................39
5. Completeness of the systems $JT^n$ and $∏^n$-completeness of $∑^n$-theories.....................................................................................................43
6. ∀-analytical completeness of the systems $JPRE^n$ and poor completeness of the theories $PRE^n$ of primitive recursive equations....................48
7. ∀¹ ∃⁰-completeness of PRE² and König's Lemma for primitive recursive 0-1-trees......................................................................................................56
References.......................................................................................................................................................................................................................62

Słowa kluczowe

Tematy

Miejsce publikacji

Warszawa

Copyright

Seria

Rozprawy Matematyczne tom/nr w serii: 207

Liczba stron

62

Liczba rozdzia³ów

Opis fizyczny

Dissertationes Mathematicae, Tom CCVII

Daty

wydano
1983

Twórcy

  • Universität Hannover

Bibliografia

  • [1] H. Friedman, Provable equality in primitive recursive arithmetic with and without induction, Pacific Journal Math. 57 (1975), 379-392.
  • [2] G. Gentzen, Untersuchungen über das logische Schliessen. I., Math. Zeitschrift 39 (1935), 176-210.
  • [3] J. Y. Girard, Three-valued logic and cut-elimination: The actual meaning of Takeuti's conjecture, Diss. Math. 136, Warszawa 1976.
  • [4] R. L. Goodstein. Recursive number theory, Amsterdam 1957.
  • [5] G. Kreisel and G. Takeuti, Formally self-referential propositions for cut free classical analysis and related systems, Diss. Math. 118, Warszawa 1974.
  • [6] P. Päppinghaus, Existentiell schwache Vollständigkeit der Logik zweiter Stufe und Schnittelimination, Dissertation, Univ. Heidelberg, Heidelberg 1977.
  • [7] D. Prawitz, Completeness and Hauptsatz for second order logic, Theoria 33 (1967), 246-253.
  • [8] D. Prawitz, Hauptsatz for higher order logic, JSL 33 (1968), 452-457.
  • [9] D. Prawitz, Some results for intuitionistic logic with second order quantification rules, in: A. Kino, J. Myhill, R. E. Vesley (eds.), Intuitionism and proof theory. Proc. of the summer conf. at Buffalo N. Y. 1968, Amsterdam 1970, 259-269.
  • [10] K. Schütte, Syntactical and semantical properties of simple type theory, JSL 25 (1960), 305-326.
  • [11] J. R. Shoenfield, Mathematical logic, Reading, Mass. 1967.
  • [12] W. W. Tait, A non-constructive proof of Gentzen's Hauptsatz for second order predicate logic, Bull. AMS 72 (1966), 980-983.
  • [13] M. Takahashi, A proof of cut-elimination theorem in simple type theory, J. Math. Soc. Japan 19 (1967), 399-410.
  • [14] M. Takahashi, Review of [12], JSL 33 (1968), 289-290.
  • [15] M. Takahashi, A system of simple type theory of Gentzen style with inference on extensionality, and the cut-elimination in it, Comment, math. Univ. Sancti Pauli 18 (1969), 129-147.
  • [16] G. Takeuti, On a generalized logical calculus, Jap. J. Math. 23 (1953), 39-96.
  • [17] G. Takeuti, Proof theory, Amsterdam 1975.
  • [18] A. S. Troelstra, Metamathematical investigation of intuitionistic arithmetic and analysis, Berlin-Heidelberg-New York 1973.
  • [19] H. Wolter, Über Mengen von Ausdrücken der Logik höherer Stufe, für die der Endlichkeitssatz und der Satz von Löwenheim-Skolem gelten, Zeitschr. f. math. Logik und Grundlagen d. Math. 18 (1972), 13-18.

Języki publikacji

EN

Uwagi

Identyfikator YADDA

bwmeta1.element.zamlynska-ea62dbfc-3044-4b08-8dc8-3ed809a7fb93

Identyfikatory

ISBN
83-01-02639-1
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ć.