Logic seminar

Some remarks on Herbrand's Theorem

In [3] I proved Proposition 4.3 about the impossibility of certain forms of the formulas in Herbrand's Theorem. This is seemingly in contradiction with Theorem 6 of Buss, Kolodzieczyk and Thapen [1], and a more recent Theorem 3.2 of Li and Oliveira of [2]. Nevertheless, all theorems hold true. In the lecture I will explain the differences and prove my Proposition with an explicit formula, which is not in [3].

[1] Buss, Kolodzieczyk and Thapen: Fragments of approximate counting, JSL 79.
[2] Li, Igor Carboni Oliveira: Unprovability of strong complexity lower bounds in bounded arithmetic. ECCC~TR23-022.
[3] P. Pudlak: Consistency and games - in search of new combinatorial principles. Proc. Logic Colloquium'03.