The Container Notation in the \(\lambda \) -Calculus (2): Propositional Logic

This chapter examines the application of the \(\lambda \) -calculus to classical propositional logic. Historically, this approach, based on the concept of combinator, is the culmination of an algorithmic view of logic proposed by Peirce and other logicians. The chapter starts defining the truth-combinator-values (or Church Booleans) t and f (this chapter introduces the terms “truth-combinator-values”, “truth-combinator-functions”, “truth-combinator-tables”, and “truth-combinator-logic”). The truth-combinator-values work as independent programs (combinators) that compute projection functions. Then, using the conditional statement from the C programming language, the truth-combinator-functions not (negation) and and (conjunction) are introduced. Moreover, each row in the corresponding truth-combinator-table is obtained by \(\beta \) -reduction under the interpretation provided by the container notation (for example, not \(t \quad \beta \) -reduces to f and not \(f \quad \beta \) -reduces to \(t)\) . Furthermore, notice that some of Ramsey’s most innovative philosophical views have a natural counterpart in truth-combinator-logic. For example, in his contribution to the debate on negative facts in Cambridge, he says that it is only an accident of our symbolism that we have the word “not” and the symbol “¬” at all. While this remark is completely natural and obvious in the context of the \(\lambda \) -calculus, it may seem counterintuitive in the context of, say, Principia Mathematica.