8
$\begingroup$

I am new to lambda calculus and definability theory, and I am trying to clarify my understanding of the relationship among the following concepts:

  1. An element $a$ in the domain of a type $A_\sigma$ is $\lambda$-definable if it is the denotation of a closed lambda-term
  2. A subset $X$ is definable, in the model-theoretic sense, if it is the denotation of some formulas in the background language
  3. Let $L^+$ be an extension of a ground langauge $L$ with a new signature term $r$. We say $r$ is explicitly definable in $L$ if it is extensionally equivalent to a formula in $L$, i.e.~there is $\varphi(x)$ in $L$ such that $\forall x(r(x)\leftrightarrow \varphi(x))$ (if $r$ is a constant, then $r(x)$ stands for $x=r$).
  4. The axiom of restricted comprehension/specification says, roughly, for every formula and a given set, there is a subset of that set specified by that formula.

Is it right to think that 1. comprehension and $\lambda$-definability are inversions of each other: the former says, given a description there is a denotation of that description, whereas the latter asks, given a term is it denotated by some description (I have also read somewhere that $\lambda$-abstraction is tantamount to comprehension principles-is it correct?) 2. model-theoretic explicit definability and $\lambda$-definability are largely orthogonal to each other. The former is strictly a question about the relative expressiveness of two languagues, whereas the latter concerns the syntax-semantic interface. On this note, I am also wondering if there has been any work on the relationship between explicit definability in the model-theoretic sense, and definability by $\lambda$-abstraction. For instance, assuming $\beta$-conversion, if $X\equiv\lambda x:\sigma. \varphi(x)$, then $\varphi(x)$ is automatically an explicit definition for $X$ (assuming, of course that we have $\forall^\sigma$ in our language). But we also know that explicit and implicit definability come apart in higher-order logic. Is there a precise definition of implicit definability in type-theoretic terms?

Many thanks in advance.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.