Logic Seminar

Thursday, June 25, 2015 2:00 pm - 2:00 pm EDT (GMT -04:00)

David Belanger, Cornell University


Π1 conservation theorems and RCA0

A formula φ is Π1-conservative over a theory T if every Π1 formula provable from T + φ is already provable from T . This gives us a good deal of information: for instance, such a T +φ has the same first- order part as the corresponding T . The prototypical example is Harrington’s well-known, unpublished theorem that Weak Konig’s Lemma is Π1 conservative over RCA0. More recently, in connection with work on Ramsey’s theorem for pairs, Chong, Slaman, and Yang have shown that the Cohesiveness Principle COH is Π1 conservative over RCA0 + BΣ2.

We will present a new, essentially recursion-theoretic proof of this latter result, and show how to extend it to any RCA0 + BΣn or RCA0 + IΣn for n 2. Our methods are peculiar in that much of our work takes place in the very weak system RCA0 rather than RCA0.

M3-4206