Course - Logic and Proof MT24

• Course Webpage
• Lecture Notes
  • 0, Propositional logic preliminaries: notes
  • 1, Polynomial time formula classes: notes, slides
  • 2, Resolution and interpolation: notes, slides
  • 3, Lower bounds for resolution: notes, slides
  • 4, Cutting planes: notes, slides
  • From the previous year:
    • 1, Introduction: notes, slides
    • 2, Propositional logic: notes, slides
    • 3, Equivalence and normal forms: notes, slides
    • 4, Polynomial time formula classes: notes, slides
    • 5, Resolution: notes, slides
    • 6, DPLL algorithm: notes, slides
    • 7, Lower bounds for resolution: notes
    • 8, Compactness theorem: notes, slides
    • 9, First-order logic: notes, slides
    • 10, Normal forms for first-order logic: notes, slides
    • 11, Herbrand’s theorem and ground resolution: notes, slides
    • 12, Examples of ground resolution proofs: notes
    • 13, Undecidability of validity and satisfiability: notes, slides
    • 14, Resolution for predicate logic: notes, slides
    • 15, Decidable theories: notes
    • 16, Compactness theorem and Vaught’s test: notes, slides
• Related: [[Course - Logic MT24]]^U
• Other courses this term: [[Courses MT24]]^U
• Other resources:
  • Slides on Ehrenfeucht-Fraïssé games

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

• [[Notes - Logic and Proof MT24, Basic definitions for propositional logic]]^U
• [[Notes - Logic and Proof MT24, Horn formulas]]^U
• [[Notes - Logic and Proof MT24, 2-CNF formulas]]^U
• [[Notes - Logic and Proof MT24, Walk-SAT]]^U
• [[Notes - Logic and Proof MT24, 3-CNF formulas]]^U
• [[Notes - Logic and Proof MT24, XOR-Clauses]]^U
• [[Notes - Logic and Proof MT24, Boolean circuits]]^U
• [[Notes - Logic and Proof MT24, Resolution]]^U
• [[Notes - Logic and Proof MT24, Cutting planes]]^U
• [[Notes - Logic and Proof MT24, Compactness theorem]]^U
• [[Notes - Logic and Proof MT24, First-order logic]]^U
• [[Notes - Logic and Proof MT24, Logical theories]]^U
• [[Notes - Logic and Proof MT24, Decidable theories]]^U
• [[Notes - Logic and Proof MT24, Unbounded dense linear orders]]^U
• [[Notes - Logic and Proof MT24, Rado graph]]^U
• [[Notes - Logic and Proof MT24, Regular languages]]^U
• [[Notes - Logic and Proof MT24, Presburger arithmetic]]^U
• [[Notes - Logic and Proof MT24, Algebraically closed fields]]^U
• [[Notes - Logic and Proof MT24, Ehrenfeucht-Fraïssé games]]^U

Problem Sheets

• Sheet 1
• Sheet 2
• From the previous year:
  • Sheet 1
  • Sheet 2, solutions
  • Sheet 3
  • Sheet 4
  • Sheet 5

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$?)