P. Pudlak's lectures at the
Fall school(Sept.'04)

Hard principles based on games

This will be a continuation of my last year School, or of my talk at the EMS Weekend. I will show that the principle $B_4$ is tractable (provable in $S^1_2$ and decidable in polynomial time). It is a result of Hastad (obtained at the last year School). The aim of this research is to find principles that would play a role in proof complexity similar to the role of Sipser functions in computational complexity.