Logic as a Tool

Chapter 2Deductive Reasoning in Propositional Logic

This chapter presents the deductive side of propositional logic: deductive systems and formal derivations of logical consequences in them. First, I explain the concept and purpose of a deductive system and provide some historical background. I then introduce, discuss, and illustrate with examples the most popular types of deductive systems for classical logic: Axiomatic Systems, Semantic Tableaux, Natural Deduction, and Resolution. In a supplementary section at the end of the chapter I sketch generic proofs of soundness and completeness of these deductive systems. In another supplementary section I discuss briefly the computational complexity of the Boolean satisfiability problem and the concept of NP-completeness.

The deductive systems introduced in this chapter are specifically designed for classical propositional logic, but the concept is universal and applies to almost all logical systems that have been introduced and studied. In Chapter 4 I extend each of these deductive systems with additional axioms and rules for the quantifiers, so that they also work for first-order logic.

2.1 Deductive systems: an overview

2.1.1 The concept and purpose of deductive systems

The fundamental concept in logic is that of logical consequence. It extends the concept of logical validity and is the basis of logically correct reasoning. Verifying logical consequence in propositional logic is conceptually simple and technically easy (although ...