Basic Notions In Logic Including Sat

Basic Notions in Logic including SAT

• This Section is on propositional logic, first-order logic, and modern Boolean satisfiability methods. In particular, we will prove the undecidability of the validity of first-order logic sentences. Boolean satisfiability is discussed in sufficient detail to ensure that the reader is well motivated to study the theory of NP-completeness.
• Mathematical logic is central to formalizing the notion of assertions and proofs. Classical logics include propositional (zeroth-order), firstorder, and higher-order logics. Most logics separate the notion of proof and truth. A proof is a sequence of theorems where each theorem is either an axiom or is obtained from previous theorems by applying a rule of inference.
• Informally speaking, it is intended that all theorems are “true.” This is formalized through the notion of a meaning function or interpretation which maps a well-formed formula (a syntactically correct formula, often abbreviated wff) to its truth value. If a wff is true under all interpretations, it is called a tautology (or equivalently, it is called valid).
• Therefore, when we later mention the term, “the validity problem of first-order logic,” we refer to the problem of deciding whether a given first-order logic formula is valid (this problem is later shown to be only semi-decidable, or equivalently TR or RE).
• A logical system consisting of a collection of axioms1 and rules of inference is sound if every theorem is a tautology. A logical system is complete if every tautology is a theorem. A logical system has independent rules of inference if omitting any rule prevents certain theorems from being derived.
• One uses the terminology of “order” when talking about logics. Propositional (zeroth-order) logic includes Boolean variables that range over true and false (or 1 and 0), Boolean connectives, and Boolean rules of inference. Predicate (first-order) logic additionally allows the use of individuals such as integers and strings that constitute infinite sets, variables that are quantified over such sets, as well as predicate and function constants. Second (and higher) order logics allow quantifications to occur over function and predicate spaces also. For example, if we present two principles of induction, namely arithmetic and complete; the formal statement of both these induction principles constitutes examples of higher order logic. There are also special classes of logics that vary according to the kinds of models (interpretations) possible: these include temporal logic. In these logics, notions such as validity tend to acquire specialized connotations, such as validity under a certain model. In this chapter, however, we will stick to the classical view of these notions.
• A Hilbert style axiomatization of propositional logic due to Church. An example involving “quacks and doctors,” presents examples of interpretations for formulas, and closes off with a proof for the fact that the validity problem of first-order logic is undecidable, but semi-decidable (or equivalently, RE or TR).
• We then turn our attention to the topic of satisfiability in the setting of propositional logic in Section 18.3. We approach the subject based on notions (and notation) popular in hardware verification - following how “Boolean logic” is treated in those settings (a model theoretic approach). We first examine two normal forms, namely the conjunctive and the disjunctive normal forms, and discuss converting one to the other. We then examine related topics such as -satisfiability, 2- satisfiability, and satisfiability-preserving transformations.