Proof Theory - ALGV00012

• Title: Teorie důkazů
• Guaranteed by: Department of Logic (21-KLOG)
• Faculty: Faculty of Arts
• Actual: from 2024
• Semester: summer
• Points: 4
• E-Credits: 4
• Examination process: summer s.:
• Hours per week, examination: summer s.:2/0, Ex [HT]
• Capacity: unlimited / unknown (unknown)
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: taught
• Language: Czech
• Teaching methods: full-time
• Note: course can be enrolled in outside the study plan; enabled for web enrollment
• Guarantor: Bc. Jan Bydžovský, M.Sc., Ph.D.
• Teacher(s): Bc. Jan Bydžovský, M.Sc., Ph.D.

Annotation

English

Introductory course on Proof Theory

Last update: Bydžovský Jan, Bc., M.Sc., Ph.D. (02.02.2025)

Czech

Úvodní kurz do Teorie Důkazů

Last update: Bydžovský Jan, Bc., M.Sc., Ph.D. (02.02.2025)

Literature

English

Primary
Gaisi Takeuti. Proof Theory: Second Edition, Dover Publications, 2013

Secondary
A.S Troelstra and H. Schwichtenberg. Basic ProofTheory, Second Edition, Cambridge University Press, 2000

Feferman, Solomon, and others. 'On the completeness of the calculus of logic (1929)', in Solomon Feferman, and others (eds), Kurt Gödel Collected Works Volume I: Publications 1929–1936 (New York, NY, 2001; online edn, Oxford Academic, 31 Oct. 2023)

G. Kreisel, Finiteness Theorems in Arithmetic: An Application of Herbrand's Theorem For Σ2 - Formulas. Studies in Logic and the Foundations of Mathematics, Elsevier, Volume 107, 1982,

Harvey Friedman. The complexity of explicit definitions, Advances in Mathematics, Volume 20, Issue 1, 1976

Last update: Bydžovský Jan, Bc., M.Sc., Ph.D. (02.02.2025)

Czech

Primární
Gaisi Takeuti. Proof Theory: Second Edition, Dover Publications, 2013

Sekundární
A.S Troelstra and H. Schwichtenberg. Basic ProofTheory, Second Edition, Cambridge University Press, 2000

Feferman, Solomon, and others. 'On the completeness of the calculus of logic (1929)', in Solomon Feferman, and others (eds), Kurt Gödel Collected Works Volume I: Publications 1929–1936 (New York, NY, 2001; online edn, Oxford Academic, 31 Oct. 2023)

G. Kreisel, Finiteness Theorems in Arithmetic: An Application of Herbrand's Theorem For Σ2 - Formulas. Studies in Logic and the Foundations of Mathematics, Elsevier, Volume 107, 1982

Harvey Friedman. The complexity of explicit definitions, Advances in Mathematics, Volume 20, Issue 1, 1976

Last update: Bydžovský Jan, Bc., M.Sc., Ph.D. (02.02.2025)

Syllabus

English

This lecture will be given in english if requested. We will cover the Part I of Proof theory book by Gaisi Takeuti i.e.

- Cut-Elimination theorem
- Herbrand's teorem, Mid-sequent theorem, Beth's definability theorem, Interpolation theorem
- Witnessing theorems
- Completeness of predicate logic with equality
- Gentzen's proof of the consistency of PA.

Time permitting we will explore one of the following areas depending on the students interests
- Completeness of intuitionistic calculus LJ wrt to Heyting algebras,
- Proof Complexity

Last update: Bydžovský Jan, Bc., M.Sc., Ph.D. (05.02.2025)

Czech

Kurz bude volně kopírovat první část knihy Proof Theory od Gaisi Takeuti tj.

- Cut-Elimination theorem,
- Herbrand's teorem, Mid-sequent theorem, Beth's definability theorem, Interpolation theorem
- Witnessing theorems,
- Gentzen's proof of the consistency of PA.

Podle času a zájmu studentů se kurz rozvětví do jedné ze dvou následujících alternativ:
- úplnost intuicionistického kalkulu LJ vůči Heytingovým algebrám, nebo
- důkazová složitost.

Last update: Bydžovský Jan, Bc., M.Sc., Ph.D. (05.02.2025)