Proof Complexity studies lengths of mathematical proofs. Both First Order Logic and Propositional Logic are in the scope of the theory, and the scholars are recently putting much more focus on propositional proof complexity, motivated by its tight relation to Computational Complexity.
One of the strongest lower-bound results in propositional proof complexity is Ajtai’s theorem, stating that the pigeonhole principle needs exponentially large proofs in the constant-depth fragments of Sequent Calculus (with Cut). In this talk, together with a brief introduction to proof complexity, we overview several successful tools (or, “quantitative” model theory) for showing Ajtai’s theorem and its variants; namely, pebble game, k-evaluation (assignments of shallow decision trees), and Nullstellensatz proof system. Then we cast some interesting (and possibly interdisciplinary) open problems; this includes a brief presentation of my recent trials: Uniform Counting Principle v.s. the injective pigeonhole principle, pebble games with backtracking options for depth-(2+1/2) fragment of Sequent Calculus v.s. the pigeonhole principle, and those for the ordinal analysis of PA.