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.
https://sites.google.com/view/lm410/home
Fruizione: 20410451-1 LM410 -TEOREMI SULLA LOGICA 1 - MODULO A in Matematica LM-40 MAIELI ROBERTO
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. Michele Abrusci e Lorenzo Tortora de Falco, Logica. Vol. 1 Dimostrazioni e modelli al primo ordine, Springer, 2014https://sites.google.com/view/lm410/home
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. In case of health emergency due to COVID-19 the way lectures will be given will depend on the conditions. In such a potential framework all the possible efforts will be done to limit the unavoidable damages related to the necessity to switch to online courses and interaction during the lessons will be preserved as much as possible. Lessons held in classroom will be streamed in real time but not recorded.Type of evaluation
Written and/or oral exam, of a duration usually between 45 and 60 minutes. In case of health emergency due to COVID-19 the way exams will be held will depend on the conditions. In such a potential framework all the possible efforts will be done to limit the unavoidable damages related to the necessity to switch to online exams.