# Lambda calculus: How to define a function that simulates $\neg p\vee q$?

I am making my first steps in lambda calculus, so please bear with me.
I want to create a lambda function, that given two boolean expressions (either $F$ or $T$ - defined below), simulates the formula $\neg p\vee q$ where the $p$ is its first argument and $q$ is the second.

Here is my attempt and how it fails:
The definitions are:
$T=\lambda xy.x$
$F=\lambda xy.y$
$\bigvee_{or}=\lambda xy.xTy$
$\neg_{negaion}=\lambda x.xFT$

Considering the above definitions, I tried:

$$\overbrace{\lambda st. \underbrace{(\lambda x.xFT)s}_\text{negates first arg}Tt}^{\text{represents }\neg p\vee q}$$

using $\beta$ reductions, I get:

$\lambda st.(\lambda x.xFT)sTt=_{\beta}\lambda st.sFTTt=_{\beta}\lambda st.sTt$

The problem is, as you probably notice - I get the logical $\bigvee_{or}$ again... which obviously does not produce the truth table I want.
What am I doing wrong?

$$f = \lambda st.\ sFTTt=\lambda st.\ (((sF)T)T)t\neq_{\beta}\lambda st.\ sTt$$

hence

$$f\ T =_\beta \lambda t.\ FTt =_\beta \lambda t.\ t$$

and

$$f\ F =_\beta \lambda t.\ TTt =_\beta \lambda t.\ T$$

I hope this helps $\ddot\smile$

• Ohh! Is that because function application is left associative? – so.very.tired Dec 5 '14 at 22:39