Propositional Logic#
Author: Alexander Kurz
The purpose of this note is to introduce the simplest logic that will appear throughout the book. It is known as propositional logic, or classical propositional logic (as opposed to variants such as intuitionistic logic) or Boolean logic (to honor George Boole and as opposed to other algebraic logics.)
In class, we used mostly the text on Propositional Logic by the Open Logic Project as our reference. In the following, I will give a quick rundown of the most important concepts.
Chapter 1.2: A formula is built from propositional variables and logical connectives such as \(\wedge\) (AND), \(\vee\) (OR), \(\neg\) (NOT).
Chapter 1.5: A valuation assigns to each propositional variable a truth value. (I like to write truth values as \(0\) and \(1\), in the book it is \(\mathbb F\) and \(\mathbb T\).) For each connective there is a truth table, so that one can define inductively the notion of satisfaction of a formula \(\phi\) by a valuation.
Chapter 1.6: A formula is satisfiable if it is satisfied by some valuation and a formula is a tautology if it is satisfied by all valuations.
Chapter 4: Natural deduction plays a major role in interactive theorem provers such as Lean and Isabelle and more generally in proof theory and type theory. We only skimmed this chapter and came back to it later when discussing the Lean Intro to Logic (which may be the best starting point to learn and practice proofs in the calculus of Natural Deduction).
Chapter 5: We spend more time on tableaux than on natural deduction because tableaux made their way into many logic-based reasoning tools including SAT-solvers and model checkers. We worked through the Examples in 5.4.
The Introduction to Logic contains an overview and summary of the most important big ideas in logic that we need.