Predicate logic Study Guide

📖 Core Concepts First‑order logic (FOL): Formal language with variables, predicates, function symbols, quantifiers ( ∀, ∃ ) that range over a domain of discourse (non‑empty set). Signature: Set of non‑logical symbols (constants, function symbols, predicate symbols) together with their arities. Term: Either a variable or a function symbol applied to terms (e.g., $f(t1,…,tn)$). Formula: Built from atomic formulas (predicates on terms, equality) using logical connectives and quantifiers. Sentence: Formula with no free variables; has a definite truth value under any interpretation. Interpretation (Structure): Pair ⟨ D, · ⟩ giving a domain $D$ and assigning meanings to each symbol: $f^I:D^n\to D$, $P^I\subseteq D^n$, $c^I\in D$. Satisfaction / Validity: $I\models\varphi$ means $\varphi$ is true in $I$. $\varphi$ is logically valid if $I\models\varphi$ for every $I$. Logical consequence: $\Gamma\models\psi$ iff every interpretation satisfying all $\Gamma$ also satisfies $\psi$. Deductive system: Set of syntactic inference rules (Hilbert, natural deduction, sequent calculus, tableaux, resolution) that produce proofs. Soundness: Anything provable is logically valid. Completeness: Anything logically valid has a proof. Semidecidability: Proof search will eventually succeed when a consequence holds, but may run forever otherwise. --- 📌 Must Remember Formation Rules: Variables → terms. If $f$ is $n$‑ary, $f(t1,…,tn)$ is a term. If $P$ is $n$‑ary, $P(t1,…,tn)$ is an atomic formula. $\lnot\varphi$, $(\varphi\land\psi)$, $(\varphi\lor\psi)$, $(\varphi\rightarrow\psi)$, $(\varphi\leftrightarrow\psi)$ are formulas. $\forall x\,\varphi$, $\exists x\,\varphi$ are formulas. Free vs. Bound: Variable inside the scope of its quantifier → bound; otherwise free. Equality axioms (with equality as logical symbol): Reflexivity: $\forall x\;(x=x)$. Substitution for functions: $x=y\rightarrow f(\dots ,x,\dots)=f(\dots ,y,\dots)$. Leibniz (substitution for predicates): $x=y\rightarrow(\varphi(x)\rightarrow\varphi(y))$. Key semantic results: Compactness: $\Sigma$ satisfiable ⇔ every finite $\Sigma0\subseteq\Sigma$ is satisfiable. Löwenheim–Skolem: If a theory has an infinite model, it has models of every infinite cardinal ≥ |signature|. Gödel Completeness: $\Gamma\models\varphi$ ⇔ there is a proof of $\varphi$ from $\Gamma$. Undecidability: No algorithm decides logical consequence for arbitrary FOL sentences (once a binary predicate is present). --- 🔄 Key Processes Evaluating a term $t$ under interpretation $I$ and assignment $\mu$: $$t^{I,\mu}= \begin{cases} \mu(x) & \text{if }t\text{ is variable }x\\ f^{I}\big(t1^{I,\mu},\dots,tn^{I,\mu}\big) & \text{if }t=f(t1,\dots,tn) \end{cases}$$ Evaluating an atomic formula $P(t1,\dots,tn)$: true iff $(t1^{I,\mu},\dots,tn^{I,\mu})\in P^{I}$. Quantifier evaluation: $\forall x\,\varphi$ true ⇔ for all $d\in D$, $\varphi$ true under $\mu[x:=d]$. $\exists x\,\varphi$ true ⇔ some $d\in D$ makes $\varphi$ true under $\mu[x:=d]$. Proof search (resolution): Convert to clause form (CNF). Apply resolution rule repeatedly; deriving the empty clause $\square$ shows unsatisfiability of the negated goal. Tableaux construction: Start with $\lnot A$. Expand using decomposition rules for connectives/quantifiers. Close a branch when a literal and its negation appear. All branches closed ⇒ $A$ is valid. --- 🔍 Key Comparisons First‑order vs. Propositional FOL: variables, predicates, quantifiers → can talk about objects individually. Propositional: only whole‑sentence atoms, no internal structure. Hilbert vs. Natural Deduction Hilbert: few inference rules, many axiom schemata; proofs are terse but less intuitive. Natural Deduction: introduction/elimination rules for each connective/quantifier; mirrors informal reasoning. Tableaux vs. Resolution Tableaux: builds a tree; good for finding counter‑models. Resolution: clause‑based, algorithmic; central to automated theorem proving. Equality as logical symbol vs. non‑logical predicate Logical: built‑in axioms (reflexivity, substitution). Non‑logical: must add axioms manually; can be defined by a binary predicate satisfying Leibniz’s law. --- ⚠️ Common Misunderstandings “All first‑order sentences are decidable.” Only restricted fragments (e.g., monadic, guarded) are decidable; full FOL is undecidable. “If a formula has a model, it is true in the real world.” Truth is relative to an interpretation; many non‑standard models exist (Löwenheim–Skolem). “Bound variables cannot be renamed.” They can be renamed (α‑conversion) as long as you avoid capture; this is essential for safe substitution. “∃!x P(x) is a primitive quantifier.” It is definable: $\exists x\,(P(x)\land\forall y\,(P(y)\rightarrow y=x))$. --- 🧠 Mental Models / Intuition Domain + Map: Think of an interpretation as a world that supplies a map from each symbol to a concrete object/function/relation in that world. Free vs. Bound as “open/closed doors”: A free variable is an open door (its value can vary); a bound variable is a closed door (its value is fixed by the quantifier). Compactness = “finite witness”: If every finite piece of a theory can be satisfied, the whole theory can be satisfied—no hidden infinite contradictions. Resolution = “clashing puzzle pieces”: Each clause is a piece; resolution finds a clash that forces the empty clause, proving inconsistency. --- 🚩 Exceptions & Edge Cases Empty domain: Standard FOL requires a non‑empty domain; many theorems (e.g., Löwenheim–Skolem) fail if emptiness is allowed. Equality omitted: Without equality as a logical symbol, you must explicitly add reflexivity, symmetry, transitivity, and substitution axioms if you need true equality. Higher‑order quantification: Not allowed in FOL; attempts to quantify over predicates break compactness and Löwenheim–Skolem. Non‑standard models: Even a theory like Peano arithmetic has models containing “infinite” natural numbers—cannot be ruled out by FOL alone. --- 📍 When to Use Which Choose Natural Deduction when you need a proof that mirrors informal reasoning (e.g., exam proofs, teaching). Pick Hilbert‑style for metatheoretic arguments (e.g., proving soundness/completeness). Use Tableaux for quickly checking satisfiability or constructing counter‑models. Apply Resolution in automated theorem proving or when working with clause normal form. Employ Compactness to prove existence of models for infinite theories by constructing finite approximations. Invoke Löwenheim–Skolem when you want to argue that a theory cannot be categorical (has models of many cardinalities). --- 👀 Patterns to Recognize Quantifier alternation (∃∀…) often signals higher complexity; many decidable fragments restrict alternation depth. Purely relational sentences (no function symbols) are easier to Skolemize for resolution. Repeated use of the same variable inside nested quantifiers → likely variable‑capture issue; look for needed α‑conversion. Clause sets containing both $P(t)$ and $\lnot P(t)$ → immediate closure in tableaux or resolution. Formulas of the shape $\forall x\,(P(x)\rightarrow Q(x))$ often rewrite to $\lnot\exists x\,(P(x)\land\lnot Q(x))$ for proof strategies. --- 🗂️ Exam Traps “All variables are bound” → forgetting a free variable makes a formula not a sentence; such a “sentence” cannot be assigned a truth value. Mis‑applying substitution: Ignoring the variable‑binding restriction leads to accidental capture; exam answers that ignore renaming are wrong. Assuming compactness ⇒ decidability: Compactness only guarantees existence of models, not an algorithm to find them. Treating equality as a predicate without axioms: Without reflexivity/substitution, proofs that rely on $=$ may fail. Confusing logical consequence with syntactic derivability: Only sound‑complete systems guarantee equivalence; a system lacking completeness (e.g., some restricted proof systems) can miss valid consequences. ---