Proving using Beta Reductions (Lambda Calculus)

Question

I am working on proving something by using Lambda Calculus and Beta Reductions, and I was following along a tutorial on another problem and attempted to carry over the knowledge onto a different problem and I am a little confused on the last step.

The problem is to prove $\textbf{or true false}$.

Here are my steps: (if there are any improvements or errors please let me know)

Step 1: Begin writing the identity for OR along with the parameters true and false.

$(\lambda x. \lambda y.(x ~ true ~ y)) ~ true false$

Step 2: Replace the $x$ terms with true.

$(\lambda y.(true ~ true ~ y)) ~ false $

Step 3: Replace the $y$ terms with false.

$ true ~ true ~ false \equiv (true ~ true) false $

Step 4: (I am a little shaky on this step, however I saw it done this way). Expand on one of the terms by replacing with it's identity. So we break true into:

$ (\lambda x. \lambda y. x) true ~ false $

Step 5: Again, replace x with true.

$(\lambda y.true) ~ false$

Step 6: $\textbf{this is the step i am most confused on}$ It looks as if since there is no way we can distribute the false to the y we simply just drop both of them since it is not an applicable function. Which then returns you with true, which stands to reason that true or false is true.

Can anyone shed light on Step 6? Or if I am correct and thats the rationale please let me know!

Answer 1

First let: $$ true = \lambda x ~ y . x $$ $$ false = \lambda x ~ y . y$$ $$ or = \lambda x ~ y .((x ~ true) y) $$

So this is what you wrote:

$$or ~ true ~ false \rhd_{\beta} true$$

$$ \Bigg ( \Big( \lambda x ~ y . (x ~ true) y \Big) true \Bigg) ~ false $$ $$ \Bigg ( \lambda y. \Big ((true ~ true) y \Big) \Bigg) false $$ $$ ((true ~ true) ~ false) $$

Unwrap $true$.

$$ \Big( (\lambda x ~ y . x) ~ true) \Big) ~ false $$ $$ \color{red}{(\lambda y . true) ~ false } \rhd true $$

In the red step, which is what's burdening you, you're just consuming the $false$, why? Because there are no free $y$ variables in $true \equiv (\lambda x~ y. x)$. This is rule-(e) for substitution.

Definition 1.12 (Substitution) For any $M, N, x$, define $[N/x]M$ to be the result of substituting $N$ for every free occurrence of $x$ in $M$, and changing bound variables to avoid clashes. The precise definition is by induction on $M$, as follows (after [CF58, p.94]).

(a) $[N/x]x \equiv N$

(b) $[N/x]a \equiv a$ for all atoms $a \not \equiv x$

(c) $[N/x](PQ) \equiv ([N/x]P)([N/x]Q)$

(d) $[N/x](\lambda x.P) \equiv (\lambda x.P)$

(e) $[N/x](\lambda y.P) \equiv P$ if $x \not \in FV(P)$.

(f) $[N/x](\lambda y.P) \equiv \lambda y. [N/x]P$ if $x \in FV(P)$ and $y \not \in FV(N)$.

(g) $[N/x](\lambda y.P) \equiv \lambda z. [N/x][z/y]P$ if $x \in FV(P)$ and $y \in FV(N)$.

Note: $FV(P)$ stands for the set of free variables of $P$.