This article looks at Propositional Logic, also called Statement Calculus, from a combinatorial and algebraic point of view (Sections 3-6), its implementation in software (Section 7), and its application to digital electronics (Section 10). Historical sections cover the shift in viewpoint from classical logic based on Aristotle’s syllogism to modern symbolic logic (Section 2) and the axiomatization of logic (Section 9). (See logic sourcebook for the original source papers (1830-1881) that drove this shift.)

In Section 7, we implement the grammar of the statement calculus in the Symbolic Logic Simulator (SLS), a program written in 28 lines of Forth code, that allows computer-aided verification of any theorem in Propositional Logic (see Appendix 1 for source code). The program makes it straight-forward to explore non-obvious logical identities, and verify any propositional logic theorem or conjecture, in particular see Appendix 2 for key identities in the statement calculus (duality, algebraic, and canonical identities).

The concept of linguistic adequacy is developed in Section 8 and the NAND Adequacy Theorem is proved showing that NAND can generate all logical operations. A corollary is that any digital logic circuit can be built up entirely using NAND gates, illustrated using the free Digital Works software.

Continue reading this article…