# 'Logically symmetric' expressions in lambda calculus

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?

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$.