Assignments

Topics:

Mathematical Preliminaries: Set, Relations, Partial Orders, Well-ordered sets and principle of Noetherian induction, Structural induction, Cardinality of Sets.

Propositional Calculus:
    Syntax and semantics
    Hintikka's Lemma and Model Existence Theorem
    Model theory: Compactness, Lowenheim-skolem theorem, normal forms, functional completeness
    Semantic Tablaeux: soundness, completeness and decidability
    Hilbert style proof system, Sequent calculus

First-order logic:
    Syntax and semantics
    Hintikka's Lemma and model existence theorem
    First-order semantic Tableaux: soundness and completeness
    Hilbert style proof system for FOL, deduction theorem, Sequent calculus
    Prenex normal form, Resolution

First-order logic with equality:
    Canonical models, Model existence theorem
    Axiomatisation and completeness
    Upward and downward Lowenheim-Skolem Theorems

*** OMITTED Scope of First-order Logic:
    Axiomatisation of some mathematical structures
    ZFC set theory in FOL, Limitations of FOL

Decision procedures: quantifier-free formulae with uninterpreted functions with equality, theory of lists and arrays, First order real-arithmetic,  Fourier-Motzkin Variable Elimination

Basics of Modal and Program Logics: Kripke semantics, Correspondances, Axiomatisation: systems K, KT4, S5, completeness, decidability using filteration. Dynamic logic: axiomatisation and completeness.

Text Books

J.H. Gallier: Logic for computer science, John Wiley and Sons, 1987.

M. Fitting: First-order logic and automated theorem proving, Springer-Verlag, 1990.

H.D. Ebbinghaus, J. Flum, W. Thomas: Mathematical Logic, Springer-Verlag, 1984.

Assignments from last year's course

References and Links