Many-valued logics inside {\lambda}-calculus: Church's rescue of Russell with B{\"}ohm trees
Fer-Jan de Vries · arXiv (Cornell University) · 2018
We extend the Church encoding of the Booleans and two-valued Boolean Logic in $\lambda$-calculus to encodings of $n$-valued sequential propositional logic (for $3\leq n\leq 5$) in well-chosen infinitary extensions in $\lambda$-calculus. In case of three-valued logic we use the infinitary extension of the finite lambda calculus in which all terms have a unique normal form in which their Bohm tree can be recognised. The construction can be refined for $n\in\{4,5\}$. The three $n$-valued logics so obtained are variants of McCarthy's left-sequential three-valued proposition calculus. The four-valued logic has been described by Bergstra. The five-valued logic seems new, but closely related to a five-valued logic proposed by Bergstra and Ponse in the context of Process Algebras. The encodings of these $n$-valued logics are of interest because they can be used to calculate the truth values of infinite closed propositions. With a novel application of McCarthy's three-valued logic we can now resolve Russell's paradox. We make the speculation that Church could have found a similar encoding of three-valued logic in his own $\lambda$I-calculus, because of the simplifying fact that Bohm trees are always finite in $\lambda$I-calculus.