Course - Logic and Proof MT24


Timetable

  • Monday 9AM-10AM, weeks 1-8 (lecture)
  • Tuesday 9AM-10AM, weeks 1-8 (lecture)
  • Tuesday 3PM-4PM, weeks 3,5,7,8 (class)

Notes

Problem Sheets

To-do List

  • Go over notes on [[Notes - Logic and Proof MT24, Walk-SAT]]U and improve analysis my modelling as a “random walk on line $\{0, \ldots, n\}$ with absorbing barrier $0$ and reflecting barrier $n$”, and details for the 2-CNF case in which case the randomised algorithm only takes polynomial time
  • Non constructive proof of the existence of interpolant in [[Notes - Logic and Proof MT24, Resolution]]U
  • Constructive proof of the existence of interpolant in [[Notes - Logic and Proof MT24, Resolution]]U, also use extra notes made during lecture 3 and 4, “unzipping the original proof”
  • Proof for lower bounds on resolution in [[Notes - Logic and Proof MT24, Resolution]]U
  • Proof for lower bounds on resolution based on results about circuit lower bounds
  • Example applications of compactness theorem
  • Decidability of unbounded dense linear orders
  • Decidability of ordered divisible Abelian groups
    • Make it more concrete using $\mathbb R$ with rational multiplication as an example
  • Decidability of $\pmb T _ {RG}$
  • Definition of a model
  • Winning strategies in some [[Notes - Logic and Proof MT24, Ehrenfeucht-Fraïssé games]]U
  • Previous years notes would also be good to look at, e.g. the final 2023 lecture contains more material on [[Notes - Logic and Proof MT24, Ehrenfeucht-Fraïssé games]]U, especially the last proof that there is no first-order formula over the signature of graphs that represents the property of a graph being connected
  • Better notes on using EF games to show completeness, etc.
  • Slides give another proof for two graphs that can’t be distinguished where one is connected and the other is not, I think there is a typo in the notes where it says $2^{k}-1$ instead of $2^{k-1}$ (or maybe even $\ge 2^{k-1}+1$?)
  • “Skolemization” spelling consistency?
  • Proof of soundness in lecture 13
  • High-level explanation of unification and resolution
  • Proofs for completeness of first-order resolution
  • Go over problem sheet solutions
  • Lecturer said he likes ground resolution questions
  • Compactness theorem for first order logic
  • Vaught’s test, sufficient conditions for a theory to be complete (Theorem 10.6 in Logic)
  • Proof of Ax-Grothendieck theorem using completeness of algebraically closed fields



Related posts