Logic course (2019-2020)

mondays 10:15-11:45, room 5440@MIMUW

Teaching material

Remote learning

Rocket.Chat:

(L)earning points

Labs

Outline

week lecture date lecture topics tutorials
0 24.02 organisation; historical context; introduction to propositional logic, tautology is coNP-complete, P1.2.3 (functionally complete set of connectives); multi-valued logics [slides] sec. 1.1 (warm-up), P1.2.2 (normal forms: NNF, CNF, DNF), P1.2.3 (functionally complete set of connectives), P1.2.4 (equisatisfiable CNF); P1.3.1-1.3.4 (complexity of SAT)
1 02.03 Hilbert’s proof system for propositional logic, soundness, deduction theorem, completeness (weak and strong); compactness; interpolation, Beth definability [slides] proof examples, P1.5.2 (compactness => König’s lemma), P1.5.3 (De Bruijn-Erdős’ theorem), P1.5.4, P2.9.2 (compactness w.r.t. finite satisfiability/logical consequence), weak completeness implies strong completeness
2 09.03 resolution (soundness, refutation completeness, hardness of pigeon-hole formulas, polynomial interpolants P1.7.6); SAT solving (DP, DPLL, phase transition); success of SAT solvers [slides] P1.3.5 (self-reducibility of SAT), P1.4.3 (exponential lower bound on equivalent CNF), P1.7.2 (interpolation), P1.7.3 (Beth definability), P1.7.4 (infinite extension of interpolation)
3 16.03 intuitionistic propositional logic: law of excluded middle, natural deduction, Curry-Howard correspondence (simply-typed lambda-calculus), models, tautology is PSPACE-complete [live stream] [video] [slides] P1.9.1 (examples), P1.9.2 (monotonicity of natural deduction), P1.9.3 (Kripke models with one world), P1.9.4 (monotonicity of Kripke semantics), P1.9.5 (soundness), P1.9.7 (examples of intuitionistic non-tautologies), P1.9.8 (linear models), P1.9.9 (disjunction property)
4 23.03 first-order logic: syntax, semantics, examples, Codd’s theorem, evaluation in AC0 for fixed formula, normal forms (NNF, PNF, SNF), Herbrand’s theorem [live stream] [slides] P2.1.2, P2.1.6-9 (definability examples), P2.2.1-2 (NNF, PNF), P2.3.1-3 (satisfaction relation), P2.6.1-2 (logical consequence), P2.14.1 (relational algebra)
5 30.03 Hilbert’s proof system for first-order logic, soundness, completeness [live stream] [slides] expressing properties in first-order logic: spectrum (P2.8.2-2.8.9) and its closure properties (P2.8.10-13); infiniteness (P2.3.4-7)
6 06.04 intuitionistic first-order logic: tautology examples, natural deduction, dependent types, lambdaP1 calculus, Kripke models, negative translation [live stream] [slides] more on spectrum: P2.8.15 (semilinear sets), P2.8.21-22 (spectra of existential and universal sentences), P2.8.29 (spectra are in NEXPTIME), P2.8.25-26 (counting spectrum); no exercises for IFOL (covered by the labs)
7 13.04 (EASTER MONDAY)  
8 20.04 compactness, Skolem-Löwenheim theorem, nonaxiomatisability [live stream] [slides] non-axiomatisability via compactness: P2.9.6, P2.9.7, P2.9.9, P2.9.10, P2.9.14, P2.9.15, P2.9.16 (done in the lecture); applications of Skolem-Löwenheim: P2.10.2 (done in the lecture), P2.10.7
9 27.04 MIDTERM EXAM more compactness (P2.9.4, P2.9.5, P2.9.18, P2.9.22) and Skolem-Löwenheim (P2.10.4, P2.10.9, P2.10.10, P2.10.11)
10 04.05 (NO LECTURE, Friday schedule on this Monday)  
11 11.05 relational homomorphisms, isomorphisms, Ehrenfeucht-Fraïssé games, application to non-definability and non-axiomatisability [live stream] [slides] P2.11.7 (isomorphism); P2.11.12, P2.12.4, P2.12.5, P2.12.6 (elementary equivalence), P2.12.10 (distinguishing sentences), P2.12.13 (infinite EF game)
12 18.05 the decision problem: semidecidability of validity and finite satifiability; decidable theories: finite model property (restriction on quantifier prefix, signature), quantifier elimination (equality, dense order, linear arithmetic, Presburger arithmetic, Tarski’s algebra) [live stream] [slides] P2.12.22-23 (inexpressibility via EF-games); P4.1.3-4 (small model property); P4.2.4, P4.2.6 (quantifier elimination)
13 25.05 undecidability of validity (Church-Turing) and finite satisfiability (Trakhtenbrot) [live stream] [slides] P2.12.11 (the hypercube), P2.12.27 (non-axiomatisability of the Church-Rosser property), P4.2.8-11 (quantifier elimination), P4.3.3 (decidability via interpretation)
14 01.06 second-order logic: expressiveness, failures (compactness, Skolem-Löwenheim theorems), nonaxiomatisability, Fagin’s theorem (finite model theory), monadic second-order logic (word models, Büchi-Elgot-Trakhtenbrot’s theorem) [live tream] [slides] P3.1.2 (countability), P3.1.5-8 (reachability, connectivity, Eulerian and Hamiltonian cycles of infinite and finite graphs), P3.1.9 (colourability), P3.2.1 (compactness and SO), P3.2.2 (Skolem-Löwenheim and SO), P3.3.5 (star-free regular languages in FO)
15 08.06 arithmetic and Gödel’s incompleteness theorem [live stream] [slides] P5.1.3-4 (expressing numeric functions in arithmetic), P5.1.5 (Collatz), P5.2.1-4 (recognising languages in arithmetic), P5.2.7 (undecidability of the integers), P5.3.2 (elimination of weak second-order quantifiers in arithmetic)
16 19.06 EXAM 10am-1pm (3 hrs)  
< ∞ 05.09 2nd TAKE EXAM [subscription form]  

[sources]