CODEWITHSUNDEEP
booleanlambda-calculus
Francis Yip
Francis Yip

Reputation: 23

Proving NOT TRUE in Lambda Calculus

FALSE = λxy.y TRUE = λxy.x

We can define the NOT operation as follows: NOT = λx.x FALSE TRUE

I can prove NOT FALSE by doing this:

`NOT FALSE = λx.x (λxy.y) (λxy.x) (λxy.y)

 -  x = x
 -  M = x (λxy.y) (λxy.x)
 -  N = (λxy.y)

(λxy.y) (λxy.y) (λxy.x)

-   x = x
-   M = λy.y
-   N = λxy.y

λy.y {x --> λxy.y} = λy.y

(λy.y)(λxy.x)

-   x = y
-   M = y
-   N = λxy.x

y { y --> λxy.x) = λxy.x which is TRUE`

How can I prove NOT TRUE is FALSE using beta reductions?

Upvotes: 1

Views: 128

Answers (1)

Francis Yip
Francis Yip

Reputation: 23

I figured out the answer was to leave TRUE and FALSE as they were.

NOT TRUE = λx.x (λxy.y) (λxy.x) (λxy.x)

-   x = x
-   M = x (λxy.y) (λxy.x)
-   N = (λxy.y)

(λxy.x) (λxy.y) (λxy.x) TRUE FALSE TRUE

(λxy.x) FALSE TRUE

-   x = x
-   M = λy.x
-   N = λxy.y

λy.x {x --> λxy.y} = λy.(λxy.y)

λy. (λxy.y) (λxy.x) λy. FALSE TRUE

-   x = λy
-   M = λxy.y (FALSE)
-   N = λxy.x (TRUE)

FALSE {y --> (λxy.x)} = (λxy.y)

λxy.y which is False

Upvotes: 0

Related Questions