Syllabus for J. Krajicek's lectures at the
I will discuss two complementary tasks: How to construct strong proof systems for propositional logic, able to prove many propositional tautologies by short proofs, and how to construct hard tautologies, formulas that require long proofs in many (possibly all) proofs systems.
Fall school (Sept.'03)
Strong proof systems and hard tautologies
Proof systems are quasi-ordered by the relation of (polynomial) simulation and it is unknown if there exists an optimal proof system, i.e. a maximal element of the quasi-ordering. This question is quite foundational and is related to the two tasks above.
I plan to recall few basic facts known for some time and then present some more recent thoughts about the problems.
A general background can be found in my book, in parts of Chapters 9, 10 and 14, in particular. However, the presentation will be self-contained and centered around my recent paper.