Question

Consider the following definitions given to you for Boolean logic:

not = λx.((x false) true)
true = λx.λy.x
false = λx.λy.y

Show that not (not true) evaluates to true. Your steps must use proper substitutions and each step must be accompanied with a brief explanation (e.g., "replacing the bound x with false", etc.).

You can use "L" for the lambda symbol in your answer.

Answer 1

not = λx.((x false) true)
true = λx.λy.x
false = λx.λy.y

Lambda calculus
(Lx . + x 1) means that function of x that adds x to 1

not (not true) = true

true is select first
false is select second

Boolean Logic:

There is no “True” or “False” in lambda calculus. There isn’t even a 1 or 0.

Instead:

T is represented by: λx.λy.x
F is represented by: λx.λy.y

First, we can define an “if” function λbtf that returns t if b is True and f if b is False

IF is equivalent to: λb.λt.λf.b t f

Using IF, we can define the basic boolean logic operators:
a AND b is equivalent to: λab.IF a b F

a OR b is equivalent to: λab.IF a T b

NOT a is equivalent to: λa.IF a F T

so, as per the definition of not a mentioned above,

not true is equivalent to: λtrue.IF true false true --> So it returns false
not (not true) is equivalent to not (false) as we have already proved not true = false
not false is equivalent to: λfalse.IF false false true -> So it returns true

Hence not (not true) evaluates to true