Predicate logic - Proof Theory and Deductive Systems

Proof Theory and Deductive Systems Introduction Proof theory studies how we can formally derive conclusions from assumptions using syntactic rules. Rather than checking whether a formula is true in every interpretation (the semantic approach), proof theory asks: Can we construct a formal proof? This distinction between proof (syntax) and validity (semantics) is central to understanding deductive systems. What a Deductive System Is A deductive system is a formal framework with two essential components: axioms and inference rules. The axioms are assumed to be true, and the inference rules specify how to derive new formulas from existing ones. A deduction (or proof) is a finite sequence of formulas where each formula in the sequence either: Is an axiom or an assumed hypothesis, or Follows from earlier formulas in the sequence by applying an inference rule Think of a deduction like a chain of logical steps, where you start with what you know (axioms and hypotheses) and work toward your conclusion by following rigid, mechanical rules. The key point is that a deduction is entirely syntactic—it's about manipulating symbols according to formal rules, not about interpreting what those symbols mean. Rules of Inference A rule of inference allows you to derive a conclusion formula from one or more hypothesis formulas. The simplest and most famous rule is Modus Ponens, which says: from $\varphi$ and $\varphi \to \psi$, you may derive $\psi$. Soundness of Rules A rule of inference is sound when it preserves truth: every interpretation that satisfies all the hypotheses must also satisfy the conclusion. In other words, you can never use a sound rule to derive something false from true premises. Modus Ponens is sound: if both $\varphi$ and $\varphi \to \psi$ are true, then $\psi$ must be true. The Substitution Rule and Variable Capture When working with quantifiers and variables, a crucial rule is the substitution rule, which allows you to substitute a term $t$ for a variable $x$ in a formula $\varphi$ to obtain $\varphi[t/x]$. However, there's an important restriction: variable capture must be avoided. Suppose you have the formula $\exists y(x < y)$ and you want to substitute the term $y + 1$ for $x$. If you naively perform the substitution, you get $\exists y(y + 1 < y)$—but now the $y$ in "$y + 1$" is bound by the existential quantifier, which is not what was intended. The original formula said "there exists a $y$ larger than $x$," but the substituted formula says "there exists a $y$ larger than $y + 1$," which is completely different. To avoid variable capture, you must rename the bound variable in the formula before substituting. In our example, you would first rewrite $\exists y(x < y)$ as $\exists z(x < z)$, and then substitute to get $\exists z(y + 1 < z)$. Now the meaning is preserved correctly. Major Deductive Systems The outline of proof theory involves several important deductive systems. Each provides a different way to structure proofs, but all are designed to be both sound and complete for first-order logic. Hilbert-Style Systems Hilbert-style deductive systems use a small number of inference rules (typically just Modus Ponens) combined with many axioms. The axioms come in infinite schemas of logically valid formulas that capture the truths of propositional logic and quantification. A Hilbert-style deduction is simply a list of formulas where each line is either: A logical axiom An assumed hypothesis, or Derived from earlier lines by Modus Ponens Hilbert systems are elegant in their minimalism (few rules), but proofs tend to be long and unintuitive because you must rely on numerous axioms. Natural Deduction Natural deduction takes the opposite approach: it has no logical axioms, only inference rules. Instead, it provides introduction and elimination rules for each logical connective and quantifier. For example: To introduce a conditional ($\to$-intro), you assume the antecedent and derive the consequent To eliminate a conjunction ($\land$-elim), you can extract either conjunct Natural deduction mirrors informal mathematical reasoning more closely than Hilbert systems, making proofs more readable and intuitive. Sequent Calculus The sequent calculus works with objects called sequents, written as $\Gamma \vdash \Delta$. Here, $\Gamma$ and $\Delta$ are collections of formulas, and the sequent expresses: "the conjunction of formulas in $\Gamma$ implies the disjunction of formulas in $\Delta$." Sequent calculus includes structural rules that manipulate the collections: Weakening allows you to add a formula to either side Contraction allows you to remove duplicate formulas Cut eliminates an intermediate formula from a proof Sequent calculus is particularly useful for theoretical analysis because it has a special property: it admits cut elimination, meaning any proof using the cut rule can be transformed into one without it. Tableaux Method The tableaux method (or truth tables method) proves a formula $A$ indirectly. You start with the negation $\lnot A$ at the root of a tree and systematically apply rules that break down formulas into simpler components. The goal is to show that every branch of the tree "closes"—that is, every branch reaches a contradiction. When all branches close, you've shown that $\lnot A$ is unsatisfiable, which means $A$ must be valid. This method is highly algorithmic and well-suited to computer implementation. Resolution Method The resolution method is the workhorse of automated theorem proving. It first converts the formula into a normal form called clause form, where a clause is a disjunction of literals (atomic formulas or their negations). Resolution uses a single powerful inference rule: from clauses $C1 \lor \varphi$ and $C2 \lor \lnot \varphi$, derive $C1 \lor C2$. The method repeatedly applies resolution until the empty clause (a contradiction) is derived, showing that the original formula's negation is unsatisfiable. Soundness and Completeness Two fundamental properties characterize the quality of a deductive system. Soundness means the system never lies: every formula that can be derived within the system is logically valid. In other words, if $\vdash \varphi$ (you can prove $\varphi$), then $\models \varphi$ (the formula is valid in every interpretation). Completeness means the system is powerful enough: every logically valid formula can be derived. In other words, if $\models \varphi$ (the formula is valid), then $\vdash \varphi$ (you can prove it). The remarkable fact is that all major deductive systems for first-order logic—Hilbert-style, natural deduction, sequent calculus, tableaux, and resolution—are both sound and complete. This means that syntax and semantics align perfectly: a formula is provable if and only if it is valid. This alignment is not guaranteed for stronger logics. For instance, second-order logic cannot have a complete deductive system, which is why first-order logic is so fundamental in mathematical logic and automated reasoning. Decidability and Semidecidability An important limitation of first-order logic concerns decidability. The logical consequence relation for first-order logic is semidecidable: If a sentence $A$ entails a sentence $B$ (that is, $A \models B$), then a deductive system will eventually find a proof, so the relation is semidecidable. However, there is no algorithm that always halts when $A$ does not entail $B$. The algorithm might search forever without finding a proof, and you cannot know when to give up. This is a fundamental limitation discovered by Church and Turing. Contrast this with propositional logic, which is fully decidable: there is an algorithm (like truth tables) that always terminates with a yes-or-no answer. Despite this limitation, the semidecidability of first-order logic makes it suitable for automated theorem proving, since the prover can be set to work until a proof is found. <extrainfo> Automated Theorem Proving First-order logic is the foundation for many practical automated theorem provers because its proof systems can be mechanized. Systems like resolution and the tableaux method have been successfully implemented in computer programs that can automatically find proofs for complex logical formulas. This makes first-order logic not just a theoretical tool but a practical one for computer science and artificial intelligence. </extrainfo>