Motivation, Introduction and Administrivia
Syntax and semantics of propositional logic;
Proving properties of formulas using structural induction;
Satisfiability and validity; relating satisfiability and validity;
Relevance lemma and other proofs by structural induction;
Decision problem for SAT is NP-complete;
Existence of practically efficient SAT solvers; using Z3
Compactness theorem and a purely model-theoretic proof of it using Koenig's Lemma; applications of compactness theorem including 4-color theorem for infinite planar graphs and showing certain properties cannot be expressed using FOL;
Proof system for propositional logic;
Soundness and completeness of the proof system; notion of consistency of formulas; Henkin's Lemma (consistency => satisfiability); maximal consistent sets; Lindenbaum's lemma;
Strong completeness theorem (using compactness and completeness); deduction theorem
Deciding SAT: the splitting method; conversion to equisatisfiable CNF formulas with linear blow-up;
Resolution and the resolution proof system; soundness and completeness proofs of resolution; using resolution for SAT;
Architecture of a SAT solver-- DPLL, resolution, learned clauses, heuristics.
Modeling mathematical structures using universes, relations and functions
Expressing properties of mathematical structures using relations/functions, quantification, and Boolean logic
Introduction to FOL; examples involving graphs, lists, numbers, groups, databases, programs, etc.
Syntax for FOL for any countable signature; free variables; sentences;
Semantics using models and interpretations of variables
Satisfiability and validity; relation between them
Henkin's reduction of FOL to propositional logic: prime formulas; Henkin's reduction by expanding signature using witnessing constants and adding axioms
Compactness theorem for FOL using Henkin's reduction and compactness for propopositional logic.
Lowenheim-Skolem theorem; proof using model construction above.
Proof system for FOL; soundness and Godel's (strong) completeness theorem.
Applications of compactness theorem to proving inexpressibility of FOL; FOL cannot express finiteness of models (but can express that a model has only n elements for a fixed n and can also ensure that all models are infinite); non-standard models of Presburger arithmetic exist (Skolem's theorem);
Computability theory: detour into Turing machines, computable functions, undecidability, recursively enumerable functions.
Decidiability of satisfiability and validity; validity is r.e.; satisfiability is not r.e.; Validity (and satisfiability) is undecidable (proof reducting halting of 2-counter machines to validity).
FO Theories: theory of a model; theory of a set of sentences; theory of a recursive set of sentences.
Consequences of major results: theory of a model, complete theories, complete recursive axiomatizations and decidability.
Various theories: Presburger arithmetic, Peano arithmetic, theory of equality, theory of rationals, theory of reals,
Godel's incompleteness theorem; proof using undecidability of the theory of numbers with addition and multiplication.
Quantifier Elimination for Linear Rationals
Deciding Quantifier-free theory of Equality
Midterm Exam
Quantifier Elimination for Linear Arithmetic (Presburger)
Nelson-Oppen Combination of Quantifier-free theories
Fusing models, arrangements, fusing models of different theories modulo common arrangement, the Nelson-Oppen procedure--- variable abstraction and ``guess-and-check'' decision procedure (nondeterministic version); proof using fusing of models.
Automatic Structures
Structures presented finitely using machines that rewrite words; automatic structures defined using synchronous regular languages; FO theory of automatic structures is decidable; examples: infinite omega sequence, infinte binary tree, the infinite grid, the configuration graph of a Turing machine; Presburger arithmetic.
Monadic Second-Order Logic
Second order logic, second order logic on (N, <) is undecidable, what about monadic SO?; MSO on finite words, equivalence with regular lagnuages; decidability of MSO on finite word models; MSO on trees, infinite words and infinite trees (without proof),
Interpretations
Interpreting FO of a structure in another structure; 1-tuple interpretations and k-tuple interpretations; MSO interpretations (only 1-tuple interpretations work). Examples: Interpreting FO on integers in natural numbers, FO over rationals in FO over natural numbers, MSO over k-ary trees using MSO on binary trees, MSO on rationals with < on MSO over the tree, MSO on pushdown graphs, how interpretations can prove decidability as well as undecidability.