In ‘An Introduction to Mathematical Logic through Type Theory’, Andrews describes a way of translating sentences in higher order logic into lambda terms in his version of the typed lambda calculus (see §51.) I am wondering if there is a uniform, neat way to do the opposite – convert a lambda term $X$ in his system back into a sentence of higher order logic (I’m happy to restrict attention to cases in which $X$ has type $o$.)

Basically, I am trying to figure out whether every expression (of type $o$) in the version of the typed lambda calculus in question can be read as an ordinary sentence of higher order logic in a natural and uniform way.

Some more information on Andrews’ setup: he has constants $Q_{((o alpha) alpha)}$ for each type $alpha$ and a constant $iota_{(i(oi))}$. (Here $i$ is the type of individuals and $o$ the type of truth values.) He then defines:

$$begin{array}{lcl}

A_{alpha} = B_{alpha} & mbox{stands for} & Q_{((o alpha) alpha)} A_{alpha} B_{alpha} \

A_{o} leftrightarrow B_{o} & mbox{stands for} & Q_{((oo)o)} A B \

T_{o} & mbox{stands for} & Q_{((oo)o)}=Q_{((oo)o)} \

F_{o} & mbox{stands for} & lambda x_{o} T = lambda x_{o} x_{o} \

Pi_{(o(o alpha))} & mbox{stands for} & Q_{(o(o alpha)(o alpha))} lambda x_{alpha} T_o \

forall x_{alpha} A_o & mbox{stands for} & Pi_{(o(o alpha))} lambda x_{alpha} T_o \

wedge_{(o(oo))} & mbox{stands for} & lambda v_1 lambda v_2 (lambda x_{(o(oo))} (x_{(o(oo))}TT) = lambda x_{(o(oo))} (x_{(o(oo))} v_1 v_2)) \

A_o wedge B_o & mbox{stands for} & wedge_{(o(oo))} A_o B_o \

supset_{(o(oo))} & mbox{stands for} & lambda x_0 lambda y_0 (x_0 = (x_0 wedge y_0)) \

A_o supset B_o & mbox{stands for} & supset_{(o(oo))} A_o B_o \

neg_{(oo)} & mbox{stands for} & Q_{(o(oo))} F \

vee_{(o(oo))} & mbox{stands for} & lambda x_0 lambda y_0 neg((neg x_0) wedge (neg y_0)) \

A_o vee B_o & mbox{stands for} & vee_{(o(oo))} A_o B_o \

exists x_{alpha} A & mbox{stands for} & neg forall x_{alpha} neg A \

A_{alpha} neq B_{alpha} & mbox{stands for} & neg (A_{alpha} = B_{alpha}) \

end{array}$$

Having spelled all that out, I should say that I don’t particularly care what formulation of the typed lambda calculus is used.