Degrees of sensible lambda theories

Journal of Symbolic Logic 43 (1):45-55 (1978)
  Copy   BIBTEX

Abstract

A λ-theory T is a consistent set of equations between λ-terms closed under derivability. The degree of T is the degree of the set of Godel numbers of its elements. H is the $\lamda$ -theory axiomatized by the set {M = N ∣ M, N unsolvable. A $\lamda$ -theory is sensible $\operatorname{iff} T \supset \mathscr{H}$ , for a motivation see [6] and [4]. In § it is proved that the theory H is ∑ 0 2 -complete. We present Wadsworth's proof that its unique maximal consistent extention $\mathscr{H}^\ast (= \mathrm{T}(D_\infty))$ is Π 0 2 -complete. In $\S2$ it is proved that $\mathscr{H}_\eta(= \lambda_\eta-\text{Calculus} + \mathscr{H})$ is not closed under the ω-rule (see [1]). In $\S3$ arguments are given to conjecture that $\mathscr{H}\omega (= \lambda + \mathscr{H} + omega-rule)$ is Π 1 1 -complete. This is done by representing recursive sets of sequence numbers as λ-terms and by connecting wellfoundedness of trees with provability in Hω. In $\S4$ an infinite set of equations independent over H η will be constructed. From this it follows that there are 2^{ℵ_0 sensible theories T such that $\mathscr{H} \subset T \subset \mathscr{H}^\ast$ and 2 ℵ 0 sensible hard models of arbitrarily high degrees. In $\S5$ some nonprovability results needed in $\S\S1$ and 2 are established. For this purpose one uses the theory H η extended with a reduction relation for which the Church-Rosser theorem holds. The concept of Gross reduction is used in order to show that certain terms have no common reduct

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 89,528

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Larger cardinals in cichoń's diagram.Jörg Brendle - 1991 - Journal of Symbolic Logic 56 (3):795-810.
On the t-degrees of partial functions.Paolo Casalegno - 1985 - Journal of Symbolic Logic 50 (3):580-588.
Consequences of arithmetic for set theory.Lorenz Halbeisen & Saharon Shelah - 1994 - Journal of Symbolic Logic 59 (1):30-40.
Existence of some sparse sets of nonstandard natural numbers.Renling Jin - 2001 - Journal of Symbolic Logic 66 (2):959-973.
Normality and p(κ)/j.R. Zrotowski - 1991 - Journal of Symbolic Logic 56 (3):1064-1067.
The reals in core models.Philip Welch - 1987 - Journal of Symbolic Logic 52 (1):64-67.

Analytics

Added to PP
2009-01-28

Downloads
43 (#320,151)

6 months
1 (#1,009,728)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Jan A. Bergstra
University of Amsterdam

Citations of this work

No citations found.

Add more citations

References found in this work

Theory of Recursive Functions and Effective Computability.Hartley Rogers - 1971 - Journal of Symbolic Logic 36 (1):141-146.
The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
Typed lambda calculus.Henk P. Barendregt, Wil Dekkers & Richard Statman - 1977 - In Jon Barwise & H. Jerome Keisler (eds.), Handbook of Mathematical Logic. North-Holland Pub. Co.. pp. 1091--1132.

Add more references