Article contents
Completeness, invariance and λ-definability
Published online by Cambridge University Press: 12 March 2014
Extract
In [4] Gordon Plotkin considers the problem of characterizing the λ-definable functionals in full type structures. A plausible, but, as we shall see, quite false, conjecture is that a functional is λ-definable ⇔ it is invariant in the sense of Fraenkel and Mostowski. A better guess might be that the set of λ-definable functionals of type σ has a uniform (in σ) definition in type theory over all full type structures (Plotkin explicitly considers a certain sort of definition by means of “logical relations”). More or less generally, one may ask if the following question is decidable.
Given: a functional F in a full type structure over a finite ground domain.
Question: is Fλ-definable?
We call the statement that this question is decidable Plotkin's λ-definability conjecture. We do not know if Plotkin's conjecture is true.
In this note we consider several questions which quickly arise from Plotkin's conjecture. In §1, we ask which type structures satisfy λ-definability = invariance. We construct for each consistent set of equations a model satisfying this equality. From consideration of these models we obtain a number of syntactic corollaries including a reduction of βη-conversion to βη-conversion at a single type (Theorem 3), an “ω-rule” for βη-conversion (Proposition 6) and consistency with βη-conversion (Proposition 8), definability and indefinability results for versions of Kronecker's δ (Propositions 10 and 11), and a decidability result for the problem of inter-definability among combinators.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1982
References
REFERENCES
- 65
- Cited by