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

Jan A. Bergstra
University of Amsterdam
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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2271947
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,464
Through your library

References found in this work BETA

The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
Theory of Recursive Functions and Effective Computability.Hartley Rogers - 1971 - Journal of Symbolic Logic 36 (1):141-146.
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

Citations of this work BETA

No citations found.

Add more citations

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.


Added to PP index

Total views
41 ( #278,827 of 2,520,788 )

Recent downloads (6 months)
1 ( #405,623 of 2,520,788 )

How can I increase my downloads?


My notes