Programme

Part 1: Some preliminary notions.
Order relations and trees, inductive definitions, proofs by induction, axiom of choice and Kőnig's lemma.

Part 2: Provability and satisyability.
First order formal language: alphabet, terms, formulas, sequents. Structures for first order languages: structures, terms and formulas with parameters in a structure, value of terms, formulas and sequents. The calculus of sequents for first order logic: Gentzen's LK. Derivable sequents and derivations. Correctness of the rules of LK. Canonical analysis and fundamental theorem: construction of the canonical analysis (with and without cuts) and proof of the fundamental theorem of the canonical analysis. Consequences of the fundamental theorem: completeness theorem, compactness theorem, eliminability of cuts, L"owenheim-Skolem's theorem.

Part 3: Towards proof-theory: the cut-elimination theorem.
The cut-elimination procedure. Definition of the elementary steps of cut-elimination. First proof strategy (big reduction steps). Second proof strategy (reversion of derivations). The complexity of the cut-elimination procedure (sketch). Some immediate consequences of the cut-elimination theorem.

Core Documentation

V.M. Abrusci, L. Tortora de Falco, Logica Volume 1- Dimostrazioni e modelli al primo
ordine. Springer, (2014).

Type of delivery of the course

The course includes Face-to-face lectures; Discussions with students and debates on the discussed topics; Exercices; Attendance is not mandatory but strongly recommended.

Type of evaluation

Oral exam, of a duration usually between 45 and 60 minutes.