To acquire a good knowledge of first order classical logic and its fundamental theorems
teacher profile teaching materials
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.
ordine. Springer, (2014).
Fruizione: 20710016 TEOREMI SULLA LOGICA 1 in Filosofia L-5 TORTORA DE FALCO LORENZO
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 primoordine. 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.