>>> >>>

-

..
-ӻ
.

Next

(i) x -    ├    x - .
(ii) A, B -    ├    (AB) - .
(iii) .


λ -

(i) x -    ├    x - .
(ii) 1. A, B -    ├    (AB) - .
     2. A -    ├    (λx.A) - .
(iii) .
λ- Λ, λ- – Λ0.

(α) λx.A = λy.(A [y / x]).
(β) (λx.A) B = A [B / x].
(μ) A = B    ├    CA = CB.
(ν) A = B    ├    AC = BC.
(ξ) A = B    ├    λx.A = λx.B.
(ρ) A = A.
(σ) A = B    ├    B = A.
(τ) A = B, B = C    ├    A = C.

(η) λx.Ax = A.

Next

, , " ".

( 12 2010 .)