北京雁栖湖应用数学研究院

2024年06月03日 至 07月11日

Day 1 Introduction
• History and purpose of logic.
• Boolean algebras.
Inductively defined sets (Ch. 3 of Carlström)
• Motivation: What is formal syntax?  What are formulas?
• The natural numbers; recursion and induction principles
• General inductively defined sets; their recursion and induction principles
• Example: binary trees
Suggested Exercises: Carlström exercises 3.2.28, 3.2.29.

Day 2 Propositional logic (Ch. 4)
• Syntax: the inductively defined set of propositional formulas
• Interpretation of formulas as truth-value
• Semantics: valuations, interpretations, tautologies
• Logical equivalence and entailment.
Suggested exercises: Any from Ch. 4, especially 4.1.6, 4.2.32, 4.2.34, 4.2.37, 4.2.41

Day 3 Natural deduction (Ch. 5)
• Rules of natural deduction
• Notation: φ1, φ2, … φn ⊢ ψ
• Formal definition of derivations, derivability;
Suggested exercises: any from Ch. 5, especially 5.2.4, 5.2.7, 5.3.6–10, 5.4.4, 5.6.1, 5.6.3, and 5.6.6 (this one is a bit more challenging than the rest).

Day 4 Soundness Theorem (Ch. 6)
• Statement of Soundness Theorem (6.1.5): connection between derivability and validity in interpretations
• Proof of soundness
Suggested exercises: any from Ch.6, especially 6.1.22, 6.1.25, 6.1.28, 6.1.34, 6.1.38, 6.3.4

Day 5 Applications of Soundness (Ch. 6)
• Theories and consistency
• Proofs vs countermodels
Suggested exercises: any from Ch.6, especially 6.1.22, 6.1.25, 6.1.28, 6.1.34, 6.1.38, 6.3.4  
NOTE: For now, we’re skipping Ch.7, Normalization.  We may come back to it later in the course, if time allows

Day 6 Completeness (Ch. 8)
• Statement of completeness
• Statement of model existence lemma
• Roadmap to proof of completeness
• Maximal consistency
Suggested exercises: 8.1.3, 8.1.14, 8.1.17, 8.2.1, 8.2.6, 8.2.7

Day 7 Predicate Logic (Ch.9)
• Concept, examples: languages/theories of groups, posets, arithmetic
• Arity types (aka signatures, etc.)
• Terms, Formulas
• Substitution
• Free/bound occurrences of variables
Suggested exercises: 9.1.15, 9.1.17, 9.1.19, 9.2.7.

Day 8 Semantics (Ch. 10)
• Structures for signatures; valuations of variables. 
• NOTE: we define/notate interpretations slightly differently from Carlström — we consider the valuation of variables v as separate from the structure 𝒜, not a part of 𝒜 as in Carlström.
• Interpretation of terms and formulas, 
Suggested exercises: Any from Ch. 10

Day 9 Semantics (Ch. 10), cont’d
• Lemma: interpretation of a term/formula depends only on its free variables 
• Notations, terminology: A,v ⊨ φ, etc.
Simplifications (Ch. 11)
• Definition of “bound for”, “free for” (OBS: confusing terminology — this is completely different from “bound in”, “free in”!)
• Lemmas on interpretation of substitutions

Day 10 Natural deduction for predicate logic (Ch. 12)
• New rules for predicate logic
• Rules for equality
• Rules for quantifiers
• Heuristics for derivations in predicate logic
• Useful building-block derivations
Soundness for predicate logic (Ch. 13)
• Statement + proof outline
Suggested exercises: Any from Ch. 12; especially 12.1.6, 12.1.12, but also all from §12.2 are good.  For finding derivations: practice, practice, practice!

Day 11 Soundness (Ch. 13)
• Proof of soundness for predicate logic
• Adaptation of outline to predicate setting
• Cases for the new rules
Suggested exercises: Any from Ch. 13.

Day 12 Completeness (Ch. 14)
• Outline of proof: model existence lemma, constructing model from suitable theory
• Maximal consistency and the existence property
• Any maximally consistent theory with the existence property has a model
• Any consistent theory has (up to variable-renaming) a maximally consistent extension with the existence property
Suggested exercises: proof of 14.1.3, 14.1.4, 14.1.5, 14.1.15, 14.2.16.

公开

公开