- Shawn Hedman, A First Course in Logic: An Introduction to
Model Theory, Proof Theory, Computability and Complexity , Reprinted in 2006,
Oxford Texts in Logic, Oxford University Press (Text for course) .
- Peter B. Andrews, An Introduction to Mathematical Logic
and Type Theory: To Truth Through Proof, 2nd edition, Springer, 2002
(Reference)
- B. A. Davey and H. A. Priestley, Introduction to
Lattices and Orders, Second edition, Cambridge University Press,
2001 (Text for course)
- L. Libkin, Elements of Finite Model Theory, Springer, 2004
(Reference)
- D. Kroening and O. Strichman, Decision Procedures:
An Algorithmic Point of View , Springer, 2008
(Reference)
Current Reading List
- Chapters 1, 2 and 3 of A First Course in Logic: ... by
Shawn Hedman.
Lecture Schedule
| Date | Topics details | |
|---|
| Jul 22 | Course overview, prerequisites and logistics.
Quick introduction to propositional logic and a
proof system for propositional logic. |
Clarification from lecture |
| Jul 26 | Notions of soundness and completeness of a
proof system for propositional logic.
Compactness theorem for propositional logic,
its proof and an application |
|
| Jul 29 | Revisiting compactness theorem for propositional
logic, introduction to first order logic syntax
and semantics, notion of structures in semantics of
first order logic. | |
| Aug 2 | Tutorial session by Rahul Srinivasan |
|
| Aug 5 | Structures and semantics of first order
logic, validity and satisfiability of first
order logic formulae and sentences, inherent
difficulty in checking
validity/satisfiability in first order logic
vis-a-vis propositional logic. Resolution
as a technique for proving unsatisfiability:
soundness and completeness of resolution for
propositional logic |
|
| Aug 9 | Notion of equisatisfiability. Prenex and
Skolem normal forms (PNF and SNF) in first
order logic. Skolem functions and
constants. Equisatisfiability of a formula
and its SNF variant, relations between their
models. Use of SNF in resolution techniques
for first order logic. |
|
| Aug 12 | Lecture by Abhisekh Sankaran:
Computing most general unifiers: existence,
algorithm and proof of the unifier being most
general, use in first order logic resolution
| |
| Aug 16 | Resolution in first order logic, role
of unifiers in finding resolvents.
Soundness of resolution in first order
logic. Herbrand structures and models.
| |
| Aug 19 | More on Herbrand structures, models and
unsatisfiable first order sentences.
A procedure for checking unsatisfiability
of first order sentences based on Herbrand's
theorem. Completeness of resolution for
first order logic. |
|
| Aug 23 | Compactness Theorem for first order logic:
proof and applications. Using compactness
theorem to prove 4-colorability of infinite
planar graphs from 4-colorability result
of finite planar graphs. Using compactness
theorem to show that certain properties of
graphs are not expressible in first order
logic.
|
|
| Aug 24 | Compensation class for Aug 26:
Completeness Theorem for FOL. Compactness,
completeness and Herbrand's unsatisfiability
theorems: moving from one to the other.
Embeddings and elementary embeddings of
first-order structures, onto embeddings as
elementary embeddings, illustrations. |
|
|