Propositional calculus - Semantic Proof Methods

Proof Systems Introduction A proof system is a method for determining whether a logical argument is valid. In essence, we want to know: given a set of premises, does a conclusion necessarily follow? There are two fundamentally different approaches to answering this question: semantic proof systems and syntactic proof systems. The key distinction is this: Semantic methods work with the meanings of formulas (their truth conditions) Syntactic methods work with the forms of formulas (their structure and rules) Both approaches aim to establish the same thing—validity—but they take different paths to get there. Semantic Proof Systems Semantic proof systems determine validity by examining what the formulas mean. Specifically, they use semantic consequence, denoted by the symbol ⊧ (pronounced "entails" or "models"). We say that a set of premises semantically entails a conclusion (written $\Gamma \vDash \phi$) when: every truth assignment that makes all the premises true also makes the conclusion true. In other words, there's no possible way for the premises to be true and the conclusion to be false. Truth Tables as a Semantic Proof Method The most straightforward semantic method is the truth table. A truth table exhaustively lists all possible truth-value assignments (combinations of true/false values) for the propositional variables in a formula. By examining every row, you can determine whether a formula is valid or whether a conclusion follows from premises. How truth tables establish validity: For an argument with premises $\phi1, \phi2, \ldots, \phin$ and conclusion $\psi$, you create a truth table with all variables. Then you: Check each row where all premises are true Verify that the conclusion is also true in each such row If yes, the argument is valid; if you find even one row where all premises are true but the conclusion is false, the argument is invalid This method is reliable but becomes computationally burdensome with many variables (a formula with $n$ variables requires $2^n$ rows). Analytic Tableaux (Semantic Trees) Analytic tableaux (also called semantic trees) offer a more elegant semantic approach. Rather than checking all truth assignments at once, tableaux systematically explore what truth assignments are possible given a set of formulas. How tableaux work: The core idea is that a branch (a path through the tableau) represents a possible truth assignment. The technique attempts to find a truth assignment that makes all formulas true. A branch closes when it contains both a formula and its negation—because no truth assignment can satisfy both simultaneously. Proving validity with tableaux: To prove an argument valid using a tableau: Assume the premises are true and the conclusion is false Build the tableau by decomposing these formulas according to logical rules If every branch closes, then no truth assignment can satisfy the premises while making the conclusion false Therefore, the argument is valid When every branch closes, we've proven the original set of formulas is contradictory, which establishes the validity of the original argument. Syntactic Proof Systems While semantic systems focus on meaning, syntactic proof systems focus on the structure of formulas. They use syntactic consequence, denoted by ⊢ (pronounced "proves" or "derives"). We say a set of premises syntactically entails a conclusion (written $\Gamma \vdash \phi$) when the conclusion can be derived from the premises using purely mechanical rules that operate on the form of the formulas, without needing to think about what they mean. The crucial insight is that syntactic consequence should align with semantic consequence. When they do, the proof system is sound (syntactic consequence implies semantic consequence) and ideally complete (semantic consequence implies syntactic consequence). Axiomatic Systems An axiomatic system establishes validity through axioms and deduction rules. Axioms are formulas that are assumed to be true without proof. They represent basic logical truths. For example, the tautology $\phi \to (\psi \to \phi)$ might be an axiom. Deduction rules allow you to derive new formulas (theorems) from existing ones. The most common is modus ponens: from formulas $\phi$ and $\phi \to \psi$, you may derive $\psi$. To prove an argument: Start with the premises Apply deduction rules repeatedly to derive new formulas If you can derive the conclusion, the argument is valid Axiomatic systems are elegant and mirror mathematical proof, but constructing proofs can be difficult because the path from premises to conclusion isn't always obvious. Natural Deduction Natural deduction is a more intuitive syntactic approach. Rather than starting with axioms, it provides introduction rules and elimination rules for each logical connective. Introduction rules tell you how to introduce a connective into your proof. For example, the conjunction introduction rule says: if you've proven $\phi$ and you've proven $\psi$, then you may derive $\phi \land \psi$. Elimination rules tell you what you can conclude from a connective. For example, the conjunction elimination rule says: from $\phi \land \psi$, you may derive $\phi$ (or $\psi$). The advantage of natural deduction is that the rules mirror intuitive reasoning. To prove a conditional $\phi \to \psi$, you assume $\phi$ and then derive $\psi$; once you do, you can discharge the assumption and conclude $\phi \to \psi$. This matches how mathematicians naturally construct arguments. Connecting Semantic and Syntactic Approaches An important relationship holds between the two systems: if $\Gamma \vdash \phi$ (we can syntactically derive the conclusion), then $\Gamma \vDash \phi$ (the conclusion is a semantic consequence of the premises). This is soundness—syntactic systems don't let us prove anything invalid. Conversely, completeness means that if $\Gamma \vDash \phi$ (the conclusion semantically follows), then $\Gamma \vdash \phi$ (we can syntactically derive it). A complete proof system can prove everything that is logically valid. For classical propositional logic, both truth tables and analytic tableaux are complete semantic methods, and both axiomatic systems and natural deduction are complete syntactic systems.