What is the proof of that self-application in the λ-calculus is not inconsistent?

Question

The SEP entry on lambda calculus discusses its consistency, surmising:

Early formulations of the idea of λ-calculus by A. Church were indeed inconsistent. The Church-Rosser theorem gives us, among other things, that the plain λ-calculus — that is, the theory λ of equations between λ-terms — is consistent.

Earlier in this article they say:

The syntax of λ-calculus is quite flexible. One can form all sorts of terms, even self-applications such as xx. Such terms appear at first blush to be suspicious; one might suspect that using such terms could lead to inconsistency, but in fact such terms do not lead to inconsistency and serve a useful purpose in the context of λ-calculus.

Is the proof that the self-application terms do not cause inconsistency based on the Church-Rosser theorem, or is there a separate proof for this?

I am interested in the self-reference/self-satisfaction distinction, so I would like to use the "self-application" aspect of lambda calculus to better understand if formulations like a "vow-in-itself" (a vow supposedly fulfilled just by swearing it) are logically consistent.

Answer 1

There is no separate proof for self-application. (It follows directly from Church Rosser, as proved in section 6 of your linked SEP).

I will assume familiarity with lambda terms throughout. We have different notions of equality at play:

• snytactic: when two terms have the same parse tree
• alpha: same up to bound variables
• beta: terms P, Q are beta equivalent iff one can be otained from the other via a finite series of beta reductions and expansions. *

The equational theory we are concerned with is that induced by beta equality. In more detail, we have a theory whose axioms are the following

• all terms are equal to themselves
• An application term (with the left term an abstraction) is equal to the terms obtained via beta reduction

The rules of inference are typical: we have symmetry, transitivity, and congruence rules. For example, if M = M', N = N', we can prove MN = M'N'. So we obtain a theory along with a deductive system for proving equality. It is straightforward to prove via induction that two terms are beta equal iff they can be proved equal via the system we have just sketched. Consistence for such an equational theory means that the theory is non-trivial (via analogy with first order logic, or any logic with ex falso).

Recall that beta normal forms have the computational interpretation of a program that has finished running. The combinators K, I are in beta normal form. If K=I was derivable from the theory, there would be an intermediate term M that beta reduces to both I, K. Then we can use diamond property of Church Rosser to find a term that both I, K reduce to. But I and K cannot be further reduced, so that they would have to be equal to each other and this is not the case. So K= I is not provable, ie, the theory is not trivial.

Notably, we have treated the consistency of the entire theory of equality for lambda calculus, including that of self application terms.

*Here, we can take beta reduction to be over the alpha-equivalence classes of terms.

Answer 2

This is a sketch of lambda calculus:

1. A set of lambda terms:

   • Variables: x, y, z, ... are lambda terms
   • If t is a lambda term and x is a variable, then (λx.t) is a lambda term
   • If t and s are lambda terms, then (t s) is a lambda term

2. The primary computation rule is beta-reduction: ((λx.t) s) → t[x := s] where t[x := s] denotes the substitution of s for free occurrences of x in t.

Church's earlier version of lambda calculus was meant to be a replacement for formal logic, so it was intended to have a semantics.

Alonzo Church first introduced the λ-calculus as "A set of postulates for the foundation of logic" in two papers of that title published in 1932 and 1933. Church believed that "the entities of formal logic are abstractions, invented because of their use in describing and systematizing facts of experience or observation, and their properties, determined in rough outline by this intended use, depend for their exact character on the arbitrary choice of the inventor".

The intended use of the formal system Church developed was function application. Intuitively, the expression (later called a term) λx.x2 corresponds to an anonymous definition of the mathematical function f(x) = x2. An "anonymous definition" of a function refers to a function defined without a name; in the current case, instead of defining a function "f", an anonymous definition corresponds to the mathematician's style of defining a function as a mapping, such as "x ↦ x2". Do note that the operation of squaring is not yet explicitly defined in the λ-calculus. Later, it will be shown how it can be. For our present purposes, the use of squaring is pedagogical.

By limiting the use of free variables and the law of excluded middle in his system in certain ways, Church hoped to escape paradoxes of transfinite set theory. The original formal system of 1932–1933 turned out, however, not to be consistent. In it, Church defined many symbols besides function definition and application: a two-place predicate for extensional equality, an existential quantifier, negation, conjunction, and the unique solution of a function.

In 1935, Church's students Kleene and Rosser, using this full range of symbols and Gödel's method of representing the syntax of a language numerically so that a system can express statements about itself, proved that any formula is provable in Church's original system. In 1935, Church isolated the portion of his formal system dealing solely with functions and proved the consistency of this system.

One idiosyncratic feature of the system of 1935 was eliminated in Church's 1936 paper, which introduced what is now known as the untyped λ-calculus. This 1936 paper also provides the first exposition of the Church-Turing thesis and a negative answer to Hilbert's famous problem of determining whether a given formula in a formal system is provable. We will discuss these results later.

- https://iep.utm.edu/lambda-calculi/

In the above, we read that Church's original formulation, available for download here, included more features, like a symbol for "extensional equality of terms", quantifiers, and other common logical connectives like negation and conjunction. Kleene and Rosser proved that that version of lambda calculus, including its deduction rules, could not serve the same purpose as logic, since it could be used to derive inconsistencies. Church then worked on a modified version called the simply typed lambda calculus. This version can be used as a logically consistent system. It has a semantics:

Broadly speaking, there are two different ways of assigning meaning to the simply typed lambda calculus, as to typed languages more generally, variously called intrinsic vs. extrinsic, ontological vs. semantical, or Church-style vs. Curry-style. An intrinsic semantics only assigns meaning to well-typed terms, or more precisely, assigns meaning directly to typing derivations. This has the effect that terms differing only by type annotations can nonetheless be assigned different meanings. For example, the identity term on integers and the identity term on booleans may mean different things. (The classic intended interpretations are the identity function on integers and the identity function on boolean values.) In contrast, an extrinsic semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language. In this view, λx : Int. x and λx : Bool. x mean the same thing (i.e., the same thing as λx. x).

The Church-Rosser theorem just says that every term in simply typed lambda calculus can be reduced to a single, canonical form - a "normal form". My guess is that this proof is not to be taken as a direct statement of the consistency of simply-typed lambda calculus, but rather, that it is used in the proof of the consistency, because you need to be able to reduce the huge multiplicity of terms to a more manageable collection of their normal forms. This also happens when you try to prove things about Boolean algebras, but Boolean algebras have two normal forms (disjunctive normal form and conjunctive normal form). There is apparently some deep connection between simply typed lambda calculus being "strongly normalizing" and it being consistent.

This history is described here:

Lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics. The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.

Subsequently, in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped lambda calculus. In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus.

Regarding your question about self-application, one of the ways simply typed lambda calculus avoids inconsistency is by not permitting unrestricted self-application.