# Equality in the untyped lambda calculus without extensionality

Raymond Turner (in p.66 of "Truth and Modality for Knowledge Representation") elaborates a combinatory logic, $PT$, whose language $L2$ is the following language of terms (together with a language of wffs which will be introduced below). The language of terms consists of the pure untyped lambda calculus enriched with logical combinators:

$\textbf{Basic intensional vocabulary of the language of term:}$

$\text{individual variables}$ $$\hspace{2cm} x, y, z,...$$ $\text{individual constants}$ $$\hspace{2cm} c, d, e,...$$ $\text{logical constants}$ $$\hspace{2cm} \land_{int}, \lor_{int}, \neg_{int}, \Rightarrow, \Leftrightarrow, \Xi, \theta, \approx$$

$$(\text{\Xi and \theta are the universal and existential quantifiers, respectively, with \approx the identity symbol})$$

$\textbf{Inductive definition of terms:}$

(i) $$\text{Every variable or constant is a term}$$
(ii) $$\text{If t is a term and x a variable, then (\lambda x.t) it a term.}$$ (iii) $$\text{If t and t' are terms than (tt') is a term.}$$

$\textbf{Axioms of the language of terms:}$

(i) $$\lambda x.t = \lambda y. t [y/t]$$ $$\text{for y not free in t}$$ (ii) $$(\lambda x. t)t' = t [t'/x]$$

He writes that $\eta$ does not hold in his system.

$L2$ consists of the above language of terms and in addition a language of wffs (see below). The language of terms does not allow us to express that a term is a proposition, nor that it is a true proposition. In order to do this, the language of wffs (a first order language) is provided, with a separate set of extensional connectives $\{\&, \lor, \rightarrow \}$, quantifiers and identity. The terms of this second language are variables and constants taken from the first language, and act as arguments to predicates and as entities over which quantifiers of the second language may range. The wffs are defined recursively as follows:

$$\textit{Inductive definition of wff:}$$ (i) $$\text{If t and s are terms, then s =t, P(t) and T(t) are atomic wffs.}$$ $$\text{(P(t) asserts that t is a proposition and T(t) asserts that t is a true proposition)}$$ (ii) $$\text{If \Phi and \Phi' are wff, then \neg \Phi and \Phi \circ \Phi' are wff, for \circ \in \{\&, \lor, \rightarrow \}}$$ (iii) $$\text{If \Phi is a wff and x a variable, then \exists x \Phi and \forall \Phi are wffs.}$$

Turner writes, "to the reader unfamiliar with combinatory logic this language may appear somewhat strange. The language of terms contains, in addition to the constructors of the pure Lambda Calculus, the logical combinators...these are the intensional analogues of the connectives and quantifiers... the term intensional is not innappropriate here since the equality relation on terms is that of the Lambda Calculus and two terms which can be taken to be propositions will only be equal when this is derivable within the Lambda Calculus."

He writes that the equality relation in the untyped lambda calculus is such that, where $T$ is a truth predicate, (1) does not imply (2):

(1) $$T(t) \Leftrightarrow T(s)$$ (2) $$t=s$$

He is I think talking about models of the untyped lambda calculus without the following axiom of extensionality:

(3) $$\forall x \thinspace (tx = sx)\rightarrow (t = s)$$

He writes 'it is perfectly possible for two Lambda abstracts to yield the same truth values for all arguments without being equal as terms."

My question is this: semantically what is the notion of equality in the untyped lambda calculus without extensionality if it does not reduce to bi-implication? Is it syntactic identity?

Is the notion of derivability in the pure untyped Lambda calculus without extensionality a preorder (since antisymmetry would presumably fail)?

Edit:
Hurkl writes: "You aren't consistent in your symbols; e.g. you use both $\land$ and $\&$, and you use both $\Xi$ and $\forall$. Are these typos?" No. I explicitly said "the language of wffs (a first order language) is provided, with a $\textit{separate set of extensional connectives$\{\&, \lor, \rightarrow \}$, quantifiers and identity}$. $\forall$ is the extensional universal quantifier.

• You aren't consistent in your symbols; e.g. you use both $\wedge$ and $\&$, and you use both $\Xi$ and $\forall$. Are these typos?
– user14972
Commented Sep 26, 2016 at 9:06
• One of the most natural interpretations of equality, without extensionality, is syntactic equality. However, in a particular model, equality could be interpreted as some equivalence relation between extensional equality (which, intuitively, makes the most things equal) and syntactic equality (which, intuitively, makes the fewest things equal). In particular, if additional axioms of equality are added, then the equality relation may need to be more than just intensional equality, even if not enough axioms are added to make it extensional equality. Commented Sep 26, 2016 at 10:36

An interpretation provides a set $M$ of elements. Some of its elements are called propositions. We do not require that those elements be set-theoretic relations on $M$ — that is, if $t \in M$ is a proposition, we do not require $t \subseteq M$, or $t \in \{\text{true}, \text{false}\}^M$ or any equivalent such thing.