On p-Optimal Proof Systems and Logics for PTIME

摘要

We prove that TAUT has a p-optimal proof system if and only if a logic related to least fixed-point logic captures polynomial time on all finite structures. Furthermore, we show that TAUT has no effective p-optimal proof system if NTIME(h~(o(1))) ￠ DTIME(h~(o(log h))) for every time constructible and increasing function h.