一句话：将 Church 布尔编码推广到无穷 λ-演算，用 ⊥ 标识不可解项，从而编码 McCarthy 三值逻辑并可细化到四、五值逻辑。
本文研究如何在 λ-演算中表示多值逻辑。已知 Church 编码可将布尔逻辑嵌入 λ-演算；作者将其推广到合适的无穷 λ-演算，引入新常量 ⊥ 并将所有不可解项等同，从而给出 McCarthy 三值逻辑的编码。该编码可进一步细化为四值和五值逻辑，并且同样的思路也适用于 Church 最初的 λI-演算。作为动机，文章讨论 Russell 悖论，并利用该编码在无穷设定下计算无穷闭命题的真值。这表明 λ-演算的编码技术能统一处理多值真值与无穷命题。
We will extend the well-known Church encoding of Boolean logic into $\lambda$-calculus to an encoding of McCarthy's $3$-valued logic into a suitable infinitary extension of $\lambda$-calculus that identifies all unsolvables by $\bot$, where $\bot$ is a fresh constant. This encoding refines to $n$-valued logic for $n\in\{4,5\}$. Such encodings also exist for Church's original $\lambda\mathbf{I}$-calculus. By way of motivation we consider Russell's paradox, exploiting the fact that the same encoding allows us also to calculate truth values of infinite closed propositions in this infinitary setting.