Poslední úprava: Bydžovský Jan, Bc., M.Sc., Ph.D. (02.02.2025)
Introductory course on Proof Theory
Poslední úprava: Bydžovský Jan, Bc., M.Sc., Ph.D. (02.02.2025)
Literatura -
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
Poslední úprava: Bydžovský Jan, Bc., M.Sc., Ph.D. (02.02.2025)
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
Poslední úprava: Bydžovský Jan, Bc., M.Sc., Ph.D. (02.02.2025)
Sylabus -
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.
Poslední úprava: Bydžovský Jan, Bc., M.Sc., Ph.D. (05.02.2025)
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
Poslední úprava: Bydžovský Jan, Bc., M.Sc., Ph.D. (05.02.2025)
