University Seminar- Computability, Complexity, and Algebraic Structure

Time: Wednesday, February 21, 11:15am – 12:15pm

Place: Phillips Hall, Room 109

Speaker:  Hunter Monroe, IMF

Title:  Characterizing hard-to-prove tautologies in undecidable theories

Abstract:  If the ordering over undecidable theories by their efficiency at proving tautologies exactly coincides with some logical strength measure, our deep understanding of when one theory cannot prove the consistency of or interpret another would, we show, fully characterize theories’ hard-to-prove tautology families. The finest-grained possible conjecture of this form is “theory S is less efficient at proving tautologies than S+phi if and only if S does not efficiently interpret S+phi”. This conjecture translates independence results (“phi is independent of S”) into hard tautologies (“S+phi lacks a length n proof of 0 =1”). A more powerful variant rolls up several open questions in complexity theory into one.