Propositional calculus Study Guide

📖 Core Concepts Propositional calculus – Logic of whole statements (propositions) that are true (T) or false (F). No predicates or quantifiers. Propositional variable – Symbol (e.g., \(p, q\)) standing for an atomic proposition. Well‑formed formula (wff) – Built from variables and logical connectives (\(\land, \lor, \lnot, \rightarrow, \leftrightarrow\)) according to the formation grammar. Interpretation / valuation – Assignment of T/F to every variable; for \(n\) variables there are \(2^{n}\) possible interpretations. Truth‑functional – The truth value of a compound wff depends only on the truth values of its parts (captured by truth tables). Tautology / valid formula – True under every interpretation (semantic consequence of the empty set). Contradiction – False under every interpretation. Consistent set – At least one interpretation makes all formulas true. Validity of an argument – No interpretation makes all premises true while the conclusion false (no counter‑example). Soundness – Argument is valid and all its premises are actually true. Functional completeness – A single connective (e.g., NAND “\(\uparrow\)” or NOR “\(\downarrow\)”) can express all others. Proof systems – Semantic (truth tables, analytic tableaux) use meaning of formulas. Syntactic (axiomatic systems, natural deduction) use formal inference rules (\(\vdash\)). Natural‑deduction rules – Introduction (∧I, ∨I, →I, ¬I) and elimination (∧E, ∨E, →E, ¬E) rules for each connective. Axiomatic system (Łukasiewicz / System P2) – Three axiom schemata plus modus ponens (and substitution) generate all theorems. SAT problem – “Is a propositional formula satisfiable?” – decidable, but NP‑complete. --- 📌 Must Remember Bivalence & Law of Excluded Middle: Every wff is either T or F, never both. Number of interpretations: For \(n\) distinct variables, \(2^{n}\). Derived connectives: \(p \rightarrow q \equiv \lnot p \lor q\) \(p \lor q \equiv \lnot(\lnot p \land \lnot q)\) Functional completeness: NAND (\(p \uparrow q \equiv \lnot(p \land q)\)) and NOR (\(p \downarrow q \equiv \lnot(p \lor q)\)) each suffice to define all others. Classic valid argument forms (remember the pattern): Modus Ponens (MP): \(p,\;p\rightarrow q\; \vdash\; q\) Modus Tollens (MT): \(\lnot q,\;p\rightarrow q\; \vdash\; \lnot p\) Disjunctive Syllogism (DS): \(p\lor q,\;\lnot p\; \vdash\; q\) Hypothetical Syllogism (HS): \(p\rightarrow q,\;q\rightarrow r\; \vdash\; p\rightarrow r\) Constructive Dilemma (CD): \(p\rightarrow q,\;r\rightarrow s,\;p\lor r\; \vdash\; q\lor s\) Destructive Dilemma (DD): \(p\rightarrow q,\;r\rightarrow s,\;\lnot q\lor \lnot s\; \vdash\; \lnot p\lor \lnot r\) Natural‑deduction essentials: ∧I: From \(p\) and \(q\) infer \(p\land q\). ∧E: From \(p\land q\) infer \(p\) (or \(q\)). →I: Assume \(p\), derive \(q\), then infer \(p\rightarrow q\) (discharge). →E (MP): From \(p\rightarrow q\) and \(p\) infer \(q\). ¬I: Assume \(p\), derive contradiction, infer \(\lnot p\). ¬E (RAA): From \(\lnot\lnot p\) infer \(p\). Łukasiewicz axioms (System P2): \((A\rightarrow (B\rightarrow A))\) \(((A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C)))\) \(((\lnot A\rightarrow \lnot B)\rightarrow (B\rightarrow A))\) SAT complexity: NP‑complete → no known polynomial‑time algorithm; use DPLL / modern SAT solvers in practice. --- 🔄 Key Processes Truth‑Table Validity Test List all distinct variables. Write all \(2^{n}\) rows of T/F assignments. Compute the truth value of each sub‑formula column‑wise. Valid if the conclusion column is T in every row where all premises are T (or equivalently, the negation of the whole argument is a contradiction). Analytic Tableau (Semantic Tree) Write the set of premises plus the negated conclusion at the root. Apply tableau expansion rules for each connective (e.g., split a \(\lor\) into two branches). A branch closes when it contains a formula and its negation. If all branches close → the original argument is valid. Natural‑Deduction Proof (Fitch style) List premises. Open a sub‑proof (assumption) when an introduction rule needs it (e.g., for →I). Derive the desired conclusion using the appropriate introduction/elimination rules. Discharge assumptions when the rule’s condition is met. Deriving a Theorem in System P2 Choose an axiom instance matching the target pattern. Apply modus ponens repeatedly to combine axioms. Example: From Axiom 1 and Axiom 2 obtain \(A\rightarrow A\). DPLL SAT Solver (high‑level) Unit propagation – assign values forced by unit clauses. Pure‑literal elimination – assign truth to literals that appear with only one polarity. Choose a variable, branch on T/F, recurse. Backtrack on conflict; if all branches close → unsatisfiable. --- 🔍 Key Comparisons Semantic vs. Syntactic proof Semantic: Uses meanings (truth tables, tableaux). Directly shows no counter‑example. Syntactic: Manipulates symbols with formal rules (natural deduction, axioms). Shows derivability (\(\vdash\)). Truth table vs. Analytic tableau Truth table: Exhaustive, good for ≤4 variables; mechanical but can be large. Tableau: Branches only as needed; often more efficient for showing unsatisfiability. NAND vs. NOR (functional completeness) NAND: \(\uparrow\) alone can define \(\lnot, \land, \lor, \rightarrow\). NOR: \(\downarrow\) also sufficient; choose whichever the problem explicitly mentions. Validity vs. Soundness Validity: Logical form guarantees conclusion true if premises are true. Soundness: Adds the factual premise that the premises are true. Derived rule vs. Primitive rule Derived: e.g., Material transposition (MTT) can be proved from MP + RAA. Primitive: Rules listed in the system’s inference set (e.g., →I, ¬I). --- ⚠️ Common Misunderstandings “True because antecedent false” – Material implication \(p\rightarrow q\) is true when \(p\) is false, even if everyday “if … then …” feels different. Confusing consistency with validity – A set can be consistent (has a model) yet not entail a particular formula. Assuming any connective can serve as a primitive – Only NAND or NOR are functionally complete; others need definitions. Thinking substitution is always needed – In axiom schemata, each substitution instance is itself an axiom, so an explicit substitution rule can be omitted. Double‑negation elimination works only in classical propositional logic, not in intuitionistic variants. --- 🧠 Mental Models / Intuition Truth table = “enumerate every possible world.” Imagine each row as a distinct universe; if the conclusion ever fails while premises hold, you’ve found a counter‑example. Tableau = “search for a contradiction.” Start with premises + ¬conclusion; each branch explores a possible world. If every world collapses (contains \(p\) and \(\lnot p\)), the argument must be valid. Natural deduction = “building a house with scaffolding.” Assumptions are temporary scaffolds (boxes); once the roof (desired formula) is in place, remove the scaffolding (discharge). NAND/NOR = “the Swiss‑army knife of logic.” Remember: NAND = NOT (AND), NOR = NOT (OR) – you can always “undo” the AND/OR to get the other connectives. --- 🚩 Exceptions & Edge Cases Infinite formulas are excluded by the closure clause – only finitely generated wffs count. Material implication ≠ causal implication – no notion of “cause” in truth‑functional semantics. Double‑negation elimination fails in non‑classical logics (e.g., intuitionistic). Derived rules (e.g., material transposition) are not primitive; they must be proved before use. SAT solvers may return “unknown” on pathological instances (e.g., extremely large formulas with pathological structure). --- 📍 When to Use Which | Situation | Best Tool | Why | |-----------|-----------|-----| | ≤ 4 variables, need quick check | Truth table | Simple, exhaustive, minimal steps. | | ≥ 5 variables, want to show unsatisfiability | Analytic tableau or DPLL SAT solver | Branching avoids full enumeration. | | Formal proof required (e.g., exam question) | Natural deduction (Fitch) | Shows each inference step; easy to read. | | Metatheoretic proof (completeness, consistency) | Axiomatic system (Łukasiewicz/P2) | Works with axiom schemata & modus ponens. | | Large industrial verification | SAT/SMT solver | Handles thousands of variables efficiently. | | Need to replace all connectives with a single operator | NAND/NOR | Functional completeness guarantees expressibility. | --- 👀 Patterns to Recognize Both \(p\) and \(\lnot p\) appear → Immediate inconsistency → branch closes. A premise of the form \(p \rightarrow q\) together with \(p\) → Spot MP pattern → infer \(q\). A disjunction together with a negated conjunct → Spot DS pattern → infer the other disjunct. Repeated sub‑formula (e.g., \(A\rightarrow B\) appearing twice) → Likely a place to apply →I or →E without re‑deriving. A tableau node with a conjunction → Split into two separate nodes on the same branch (no branching). --- 🗂️ Exam Traps Choosing MT instead of MP – “From \(p\) and \(p\rightarrow q\) infer \(\lnot p\)” is wrong; MT needs \(\lnot q\). Treating NAND as “not AND” but forgetting the outer negation – \(p \uparrow q\) is \(\lnot(p\land q)\), not simply “\(p\) and not \(q\)”. Assuming any set of premises is automatically consistent – A set like \(\{p, \lnot p\}\) is inconsistent; watch for hidden contradictions. Misreading “valid” as “true” – A formula can be valid (tautology) but not true in a given interpretation (trivial, but the wording matters). Forgetting to discharge assumptions in natural deduction – Leaving an open assumption makes the proof invalid. Using derived rule (material transposition) without justification – If the exam only allows primitive rules, you must first derive it. ---