Degrees of sensible lambda theories

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


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



    Upload a copy of this work     Papers currently archived: 93,642

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

Existence of Some Sparse Sets of Nonstandard Natural Numbers.Renling Jin - 2001 - Journal of Symbolic Logic 66 (2):959-973.
Existence of some sparse sets of nonstandard natural numbers.Renling Jin - 2001 - Journal of Symbolic Logic 66 (2):959-973.
The Pure Part of $mathrm{HYP}(mathscr{M}$).Mark Nadel & Jonathan Stavi - 1977 - Journal of Symbolic Logic 42 (1):33-46.
On dedekind complete o-minimal structures.Anand Pillay & Charles Steinhorn - 1987 - Journal of Symbolic Logic 52 (1):156-164.
The complexity of the core model.William J. Mitchell - 1998 - Journal of Symbolic Logic 63 (4):1393-1398.
$t$-convexity And Tame Extensions.Lou van den Dries & Adam H. Lewenberg - 1995 - Journal of Symbolic Logic 60 (1):74-102.
Cantor’s Theorem May Fail for Finitary Partitions.Guozhen Shen - forthcoming - Journal of Symbolic Logic:1-18.


Added to PP

12 (#1,115,280)

6 months
55 (#88,440)

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 (ed.), Handbook of mathematical logic. New York: North-Holland. pp. 1091--1132.

Add more references