A popular idea among philosophers is that facts are built out of fundamental entities in something like the way that sentences are built out of elementary expressions. My question is motivated by a certain strategy for making some implications of this idea formally precise using the lambda-calculus.

Consider the simply typed lambda calculus with a single base type $t$ and a type $\alpha\to\beta$ for every pair of types $\alpha$ and $\beta$. Our language contains infinitely many variables $v_i^\alpha$ of each type $\alpha$. Variables are terms; $(fa)$ is a term of type $\beta$ for terms $f$ and $a$ respectively of types $\alpha\to\beta$ and $\alpha$; $(\lambda v_i^\alpha.b)$ is a term of type $\alpha\to\beta$ for any term $b$ of type $\beta$; nothing else is a term. $D_t:=\{0,1\}$ and $D_{\alpha\to\beta}:={D_\alpha}^{D_\beta}$. For any assignment function $g$ mapping every variable $v_i^\alpha$ to a member of $D_\alpha$, we define the interpretation function $[[\cdot]]^g$ mapping every term of type $\alpha$ to a member of $D_\alpha$ as follows: $[[v_i^\alpha]]^g = g(v_i^\alpha)$, $[[(fa)]]^g = [[f]]^g([[a]]^g)$, and $[[(\lambda v_i^\alpha. b)]]^g(a) = [[b]]^{g[v_i^\alpha\mapsto a]}$ for all $a\in D_\alpha$, where $g[v_i^\alpha\mapsto a]$ is the function mapping $v_i^\alpha$ to $a$ and otherwise agreeing with $g$. A substitution $\sigma$ is any type-respecting function from variables to terms; a term $a$ admits $\sigma$ if, for all variables $v$ and $v'$, no free occurrence of $v'$ in $\sigma(v)$ becomes bound when $\sigma(v)$ is substituted for a free occurrence of $v$ in $a$. Let $\sigma^*a$ be the result of simultaneously substituting an occurrence of $\sigma(v)$ for every free occurrence of $v$ in $a$, for all variables $v$. We adopt standard abbreviations where it causes no confusion.

Definition 1. A term $R$ of type $t\to(t\to t)$ is logically symmetric := $[[\sigma^*R]]^g=[[\sigma^*(\lambda xy.Ryx)]]^g$, for all assignment functions $g$, variables $x,y$ of type $t$ not free in $R$, and substitutions $\sigma$ admitted by $R$.

Example $(\lambda xy.z)$ is logically symmetric for all pairwise-distinct variables $x,y,z$ of type $t$.

Question 1. Does $R$ being logically symmetric imply that $[[R]]^g$ is a constant function?

(The philosophical idea behind this question is that relations like conjunction should be identical to their converses, in which case a positive answer is arguably incompatible with their being structured out of fundamental constituents in anything like the way that complex terms are constructed from their elementary constituents.)

Definition 2. $a$ is a $\lambda I$-term := every occurrence of $\lambda v$ in $a$ takes scope over a free occurrence of $v$

Question 2. Are there any logically symmetric $\lambda I$-terms?


The answer to Question 1 is yes. The answer does not depend on the interpretation being boolean.

Suppose the term is nonconstant. Since this calculus has only terminating terms, first normalize the expression to be only applications of variables. The term must have that either $x$ or $y$ (w.l.o.g, let it be $x$) appears earliest within the term. Starting from the earliest occurence and moving backwards, assign each variable to the constant function picking out the term containing $x$.

For example, if the term is $f (i h x) (y z (j m)) k$, assign $i := \lambda a b. b$ and $f := \lambda a b c. a$.

Then $[[R]]^g$ = $\lambda x y. x$ for our assignment of $g$, and this is obviously not preserved under swapping, so no term containing $x$ or $y$ in its definition meets the criterion. Hence all such terms are constant in $x$ and $y$.

Question 2 is negative. All logically symmetric terms do not contain $x$ or $y$.

  • $\begingroup$ What about non-constant terms that don't normalize to applications of variables, like λab.da(λc.c), for a,b,c of type t and d of type t→(t→t)→t? EDIT: Oh, I see, applications of variables is all we need, not applications of variables to variables. $\endgroup$ – Jeremy Mar 6 '18 at 0:18
  • $\begingroup$ Yeah, not all the applications must be to variables. If any variable is applied to x or y, then you can use this, otherwise normalize until you either can, or x and y disappear. $\endgroup$ – Jason Carr Mar 6 '18 at 17:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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