3
$\begingroup$

In many references I find that the simply typed lambda calculus was introduced because the Kleene–Rosser paradox showed that pure/untyped lambda calculus was inconsistent. However, since it is untyped, the usual definition of inconsistency (i.e., that every type is inhabited) does not apply. Then, in what sense is pure lambda calculus inconsistent?

Even more confusingly, a couple of other references (e.g. Barendregt) defines consistency as the property that not all terms are $\beta$-equivalent, a property which pure lambda calculus has.

(This question may be related to How does the Y combinator exemplify "Lambda calculus inconsistency"?, but I believe is not a duplicate)

$\endgroup$

1 Answer 1

3
$\begingroup$

The short answer is that the "untyped lambda calculus" from 1932 is not the modern untyped lambda calculus. The modern one comes from a later (I think) realization that just the lambda/application part can be used as a computational system.

The calculus from 1932 was developed to be a logical system. There are additional terms that allow you to build up logical formulas, and the lambda calculus part that was later distilled out is handling the abstraction over and instantiation of variables, and the building of formulas/terms. The calculus is actually pretty complicated. It has:

  • 8 term formers. Abstraction and application are two, but also: $Π$, $Σ$, $\&$, ~, $ι$ and $A$.
    • $Π$ is like a combination of $∀$ and $⇒$ connectives
    • $Σ$ is similar to $∃$
    • $\&$ is $∧$
    • ~ is $¬$
    • $ι$ is like definite description/global choice (so, if $P$ is a predicate, then $ιP$ is a term such that $P(ιP)$ holds iff $∃x. P(x)$, or something along those lines)
    • I'm honestly not sure what $A$ is. Its description in the paper is unclear, but later it is said to be involved in defining 'classes' somehow.
  • 5 inference rules. One is the α rule, and two are β rules (one for reduction and one for expansion). The other two are like the rules for ∃ introduction and ∀/⇒ elimination in first-order logic.
  • 37 postulates. These are formulas that are assumed to be true as a starting point for deducing other formulas via the inference rules. For instance:
    • $Π(λp. Σ(λq. \&(p,q)),λp. p)$
    • The above is an encoding of: $p ∧ q ⇒ p$

Now, the untyped part is that there is nothing that requires you to use all these connectives in a way that actually makes sense given the above explanations. For instance, $\&$ is logical "and", and is supposed to be applied to at most two subformulas. But applying it to more than two is still considered a valid formula. Also, the variables managed by the lambda calculus are not (merely) like the variables in first-order logic, ranging over a 'domain of discourse.' They also sometimes serve the role of propositional/predicate (meta)variables, as in the $p ∧ q ⇒ p$ example. But there is nothing keeping track of which variables are which, and that they aren't used in incoherent ways.

Anyhow, with all this extra machinery, I imagine the notion of logical consistency is just the normal one: are there propositions that are not deducible from the (37) postulates? And in particular, is some designated 'false' proposition not deducible? I'm not familiar with the details, but the above incoherence lets us try some (now) standard tricks, like considering applications of predicates to themselves, and probably talking about the "predicate selecting predicates that don't hold for themselves." Then simple types render this impossible, because self-analyzing predicates would require their type to be infinite.

Edit: one sidenote: it probably won't be completely straightforward to do the diagonalization (if you track down the paper with the full rules). Church was already aware of various paradoxes when designing the system, and was trying to rule them out (this is mentioned in the paper). He just wasn't completely successful.

$\endgroup$
6
  • $\begingroup$ Do you have a reference for the 1932 calculus? Worth noting that there's a clever short version that is very similar to, e.g. the HOL light system, but untyped, based on an equational logic. Not sure if it was similar to the original system though. $\endgroup$
    – cody
    May 10, 2023 at 21:23
  • 1
    $\begingroup$ The paper is called "A Set of Postulates for the Foundation of Logic." I don't know if you can get it anywhere online, though. I happen to have a physical copy. $\endgroup$
    – Dan Doel
    May 11, 2023 at 14:51
  • 1
    $\begingroup$ Here is the paper. $\endgroup$ May 11, 2023 at 21:43
  • $\begingroup$ @cody could you share the one you meant? $\endgroup$ Jun 18, 2023 at 2:27
  • $\begingroup$ The Wikipedia article gives the rules: en.m.wikipedia.org/wiki/HOL_Light, but doesn't define the connectives. $\endgroup$
    – cody
    Jun 19, 2023 at 5:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.