Propositional calculus - Historical Axiomatic Systems and Computation

Formal Axiomatic Systems for Propositional Logic Introduction: From Frege to Modern Systems Propositional logic can be formalized in different ways. One important approach is through axiomatic systems, which start with a small set of logical truths (axioms) and use simple inference rules to derive all other theorems. This approach originated with Gottlob Frege's groundbreaking work in the 19th century, but was later simplified and standardized. Understanding these axiomatic systems is fundamental to studying formal logic, as they show how all of propositional reasoning can be reduced to a few simple building blocks. The Core Building Blocks: Axioms and Connectives Frege's original system used six axiom formulas, but mathematicians later discovered that many of these were redundant. Jan Łukasiewicz proved that Frege's six axioms could be reduced to just three axioms without losing any logical power. This simplified system became standard in logic, and Alonzo Church adopted it and named it System P2. The key insight is that we only need two logical connectives to build all of propositional logic: implication (denoted $\rightarrow$) and negation (denoted $\neg$). Every other logical connective (conjunction, disjunction, etc.) can be defined in terms of these two. The Three Axioms of System P2 System P2 is defined by three axiom schemata. The word "schema" is important here: each axiom is not just a single formula, but a pattern that can be instantiated with any propositional formulas. Axiom 1 captures a basic fact about implication: if $A$ is true, then $B$ implies $A$ (regardless of whether $B$ is actually true). $$A \rightarrow (B \rightarrow A)$$ Axiom 2 expresses the hypothetical syllogism principle. It says: if $A$ implies "$B$ implies $C$", then whenever $A$ implies $B$, we can conclude $A$ implies $C$. $$(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$$ Axiom 3 connects negation and implication. It says: if $\neg A$ implies $\neg B$, then $B$ implies $A$ (this is the contrapositive principle). $$(\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A)$$ Each of these axiom schemata is universally valid—true under every possible interpretation of the propositional variables. Inference Rules: How We Derive New Theorems To derive theorems from these axioms, System P2 employs just two rules: Modus Ponens is the primary inference rule. It states: if we have proved both a formula $\phi$ and a formula $\phi \rightarrow \psi$, then we may derive $\psi$. Symbolically: $$\frac{\phi, \quad \phi \rightarrow \psi}{\psi}$$ This rule captures the basic intuition that implication allows us to move from one true statement to another. Substitution is the second rule, though it was never formalized precisely. The idea is straightforward: if a formula is a theorem, then any substitution of formulas for its propositional variables yields another theorem. For example, if $(A \rightarrow A)$ is a theorem, then $(P \rightarrow P)$, $(Q \rightarrow Q)$, and $((A \rightarrow B) \rightarrow (A \rightarrow B))$ are all theorems. Key Insight: Axiom Schemata Eliminate the Need for Explicit Substitution Here's a subtle but important point: when we write "Axiom 1: $A \rightarrow (B \rightarrow A)$", we're not specifying a single formula. Instead, we're giving a schema that stands for infinitely many axiom instances. Each instance is obtained by substituting concrete formulas for $A$ and $B$. For instance, all of the following are axiom instances: $P \rightarrow (Q \rightarrow P)$ $(P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))$ $\neg P \rightarrow (P \rightarrow \neg P)$ By formalizing axioms as schemata rather than single formulas, we can generate infinitely many axioms without needing a separate substitution rule. Each substitution instance is itself an axiom, ready to use. Derivation Example: Proving $(A \rightarrow A)$ Let's walk through a concrete example to see how the system works. We'll derive $(A \rightarrow A)$—the theorem that any proposition implies itself. Step 1: Instantiate Axiom 2 with $B = (A \rightarrow A)$ and $C = A$: $$(A \rightarrow ((A \rightarrow A) \rightarrow A)) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A))$$ Step 2: Instantiate Axiom 1 with $A = A$ and $B = A$: $$A \rightarrow (A \rightarrow A)$$ Step 3: Apply modus ponens using Axiom 1 from Step 2 as the minor premise and an appropriate instantiation of Axiom 1 as the major premise to derive: $$A \rightarrow ((A \rightarrow A) \rightarrow A)$$ Step 4: Now apply modus ponens to the formula from Step 1 and Step 3 to derive: $$(A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)$$ Step 5: Apply modus ponens one more time using the result from Step 4 and the formula from Step 2: $$A \rightarrow A$$ This derivation demonstrates that the three axioms and modus ponens are sufficient to prove that every proposition implies itself. This is our first theorem in System P2. Computational Aspects: Decidability and Complexity The Satisfiability Problem While axiomatic systems show us how to prove theorems, there's another fundamental question in propositional logic: Is a given formula satisfiable? That is, does there exist an assignment of truth values to the propositional variables that makes the formula true? For example, the formula $(P \vee \neg P)$ is satisfiable (it's true under all assignments), whereas $(P \wedge \neg P)$ is not satisfiable (it's false under all assignments). A key fact: the satisfiability problem for propositional logic is decidable. This means there exists an algorithm that, given any propositional formula, can determine in finite time whether the formula is satisfiable. One simple algorithm is truth-table checking: enumerate all possible truth assignments and check if at least one makes the formula true. Computational Complexity: NP-Completeness While the satisfiability problem is decidable, determining the complexity of solving it reveals something important: the satisfiability problem is NP-complete. This means: It belongs to the class NP: if a formula is satisfiable, this fact can be verified quickly (in polynomial time) by checking whether a proposed truth assignment makes the formula true. It is NP-hard: if we could solve SAT (the satisfiability problem) efficiently, we could solve every problem in NP efficiently. Many researchers believe this is computationally impossible. In practical terms, NP-completeness means that while small to moderate-sized instances are solvable, worst-case instances may require exponential time. Practical SAT Solving Algorithms Despite the theoretical worst-case hardness, modern SAT solvers work remarkably well on real-world problems. Two historically important algorithms are: The Davis–Putnam–Logemann–Loveland (DPLL) algorithm (1962) is the foundational approach that most modern SAT solvers build upon. It uses: Unit propagation: if a clause reduces to a single literal, that literal must be true. Pure literal elimination: if a variable appears with only one polarity across all clauses, assign it accordingly. Backtracking: when conflicts arise, undo assignments and try alternatives. The Chaff algorithm (2001) improved upon DPLL by introducing: Better heuristics for choosing which variable to assign next. More efficient conflict analysis and backtracking strategies. Dynamic memory management. These algorithms, though worst-case exponential, perform efficiently on many practical instances encountered in real applications like hardware verification, software testing, and artificial intelligence planning. <extrainfo> Extension to SMT Solvers Modern logic systems have extended SAT solving to handle more expressive logics. Satisfiability Modulo Theories (SMT) solvers combine SAT solving techniques with decision procedures for arithmetic (and other theories). For example, an SMT solver can determine whether a formula like $(x > 5) \wedge (x < 3)$ is satisfiable by using SAT solving at the propositional level and arithmetic reasoning for the constraints. These solvers are crucial for automated reasoning in areas like program verification and formal methods. </extrainfo>