在 Lambda 演算中证明不正确

Question

假 = λxy.y 真 = λxy.x

我们可以将 NOT 运算定义如下： NOT = λx.x 假 真

我可以通过这样做来证明不是假的：

`非假 = λ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 这是 TRUE`

如何使用 beta 缩减来证明 NOT TRUE 是 FALSE？

Answer 1

我发现答案是保持 TRUE 和 FALSE 不变。

不正确 = λ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) 正确 错误 正确

(λxy.x) 假 真

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

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

λy。 (λxy.y) (λxy.x) λy。假是真

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

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

λxy.y 为 False