Formal system Study Guide

📖 Core Concepts Formal system – An abstract framework that uses a formal language (symbols + grammar) and a deductive apparatus (inference rules) to derive theorems from axioms. Formal language – Consists of syntax (rules for forming strings) and semantics (the meanings assigned to those strings). Well‑formed formula (wff) – Any string that obeys the grammar; wffs are the only objects that can be axioms or premises. Deductive system – The pair “axioms + inference rules”; it works independently of any interpretation. Proof system – A deductive system where theorems are established by finite formal proofs (a sequence of wffs). Model – A structure assigning meanings to symbols such that all (non‑logical) axioms are true. Soundness – Every provable formula is true in all models. Semantic completeness – Every formula true in all models is provable. Recursive / effective – A formal system whose axioms and rules are decidable (algorithmically checkable). Recursively enumerable – A system where axioms/rules are semidecidable (algorithm can list them, but may not halt on non‑members). Gödel’s Incompleteness – Any consistent formal system strong enough for basic arithmetic cannot be both complete and prove its own consistency. --- 📌 Must Remember A formal system needs (1) formal language, (2) deductive apparatus; an inductive apparatus is optional. Soundness ≠ Completeness: sound → provable ⇒ true; complete → true ⇒ provable. Recursive ⇒ both axiom set and rule set are decidable; recursively enumerable ⇒ only semidecidable. Gödel (1931): No consistent arithmetic system can prove its own completeness (or consistency). Hilbert’s Program aimed for a complete, consistent, and decidable formalization of mathematics – refuted by Gödel. Formal proof = finite sequence of wffs; each line is either an axiom or follows from earlier lines by a rule. Metamathematics uses a metalanguage to talk about the object language of a formal system. --- 🔄 Key Processes Building a Formal System Choose an alphabet → define a grammar → generate well‑formed formulas. Select a set of axioms (decidable if recursive). Specify inference rules (e.g., modus ponens). Deriving a Theorem (formal proof) Start with axioms (and previously proved theorems). Apply an inference rule to earlier lines → produce a new wff. Continue until the desired formula appears; the sequence is the proof. Checking Soundness For each rule, verify that if premises are true in a model, the conclusion is also true in that model. Testing Completeness (semantic) Show that for any formula \( \varphi \), if \( \varphi \) holds in every model, there exists a formal proof of \( \varphi \). Gödel‑style Incompleteness Construction Encode statements as numbers (arithmetization). Build a self‑referential sentence \( G \) that says “\( G \) is not provable”. Prove: if the system is consistent, \( G \) is true but unprovable ⇒ incompleteness. --- 🔍 Key Comparisons Recursive vs. Recursively Enumerable Recursive: membership can be decided (yes/no in finite time). Recursively enumerable: can list members; may run forever on non‑members. Sound vs. Complete Sound: all provable statements are true. Complete: all true statements are provable. Formal system vs. Model Formal system: syntactic objects (symbols, rules). Model: semantic interpretation that gives truth values. Proof system vs. Deductive system Deductive system: axioms + rules (abstract). Proof system: a deductive system used to produce finite formal proofs. --- ⚠️ Common Misunderstandings “If a formula is a theorem, it must be true in the real world.” Truth is relative to a model; a theorem is only guaranteed true in all models when the system is sound. “Recursive = decidable for every question.” Recursiveness applies to the sets of axioms/rules, not to the theoremhood problem (which is generally undecidable). “Gödel proved a system is inconsistent.” Gödel proved incompleteness (there are true but unprovable statements) provided the system is consistent. “A model is the same as an interpretation.” An interpretation maps symbols to meanings; a model is an interpretation that satisfies all axioms. --- 🧠 Mental Models / Intuition “Syntax → Semantics” pipeline: Think of a formal language as a grammar‑checker (syntax). Once a string passes, a dictionary (semantics) tells you what it means in a model. Proof as a Lego tower: Each block (wff) must sit on previously placed blocks according to the rules (gravity). The top block is the theorem you want. Recursive vs. Enumerable as “door lock vs. visitor list”: A recursive set has a lock that instantly tells you “in” or “out”. An enumerable set just has a list you can scan; you may never know if an absent name is truly not there. --- 🚩 Exceptions & Edge Cases Non‑standard models (e.g., of Peano Arithmetic) satisfy the same axioms but contain “extra” elements; they show that categoricity fails for many systems. Effective but incomplete: Many useful formal systems (e.g., PA) are recursive yet not semantically complete because of Gödel’s theorem. Inductive apparatus: Not required for a formal system, but appears in systems that need proof by induction (e.g., arithmetic). --- 📍 When to Use Which Choose a recursive system when you need an algorithmic check for membership (e.g., automated theorem provers). Use a proof system for constructing explicit derivations (e.g., in homework or formal verification). Employ a metalanguage when you are reasoning about the formal system itself (metamathematics, proving soundness/completeness). Select a model to test semantic properties (soundness) or to illustrate non‑standard behavior. --- 👀 Patterns to Recognize “Every line depends only on earlier lines” → classic sign of a formal proof. “Axioms appear without justification” → look for the base of any derivation. “Rule of inference applied to premises” → spot the modus ponens pattern: from \(P\) and \(P \rightarrow Q\) infer \(Q\). “All true in every model ⇒ provable?” → triggers the semantic completeness test. --- 🗂️ Exam Traps Distractor: “If a system is recursive, its theoremhood problem is decidable.” – Wrong: recursion refers to axioms/rules, not to theoremhood (undecidable for arithmetic). Distractor: “Gödel showed that any consistent system is incomplete and unsound.” – Wrong: Gödel’s theorem does not affect soundness; a system can be sound yet incomplete. Distractor: “A model is a proof of consistency.” – Wrong: a model shows relative consistency (if the model exists, the axioms cannot be contradictory), but does not itself constitute a proof inside the system. Distractor: “Inductive apparatus is required for all formal systems.” – Wrong: it is optional; many systems (e.g., propositional logic) lack induction. ---