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.