Derived from

204104511 LM410 THEOREMS IN LOGIC 1  Module A in Mathematics LM40 MAIELI ROBERTO
(syllabus)
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"owenheimSkolem's theorem.
Part 3: Towards prooftheory: the cutelimination theorem. The cutelimination procedure. Definition of the elementary steps of cutelimination. First proof strategy (big reduction steps). Second proof strategy (reversion of derivations). The complexity of the cutelimination procedure (sketch). Some immediate consequences of the cutelimination theorem.
(reference books)
V. Michele Abrusci e Lorenzo Tortora de Falco, Logica. Vol. 1 Dimostrazioni e modelli al primo ordine, Springer, 2014 https://sites.google.com/view/lm410/home
