I’ve been searching google scholar and haven’t found these exact results. Most of the related papers measure proof length in terms of steps instead of symbols.
Exceptions which I’m still reviewing are
P. Pudlágk, “On the length of proofs of finitistic consistency statements in first order theories”: www.math.cas.cz/~pudlak/fin-con.pdf
R. Parikh, “Existence and feasibility in arithmetic”, which I can’t find, and
Your first link seems to be almost exactly what I wanted, and the bounded Löb’s theorem should be a simple corollary. Thanks! This really simplifies the task of explaining Löbian cooperation =)
I’ve been searching google scholar and haven’t found these exact results. Most of the related papers measure proof length in terms of steps instead of symbols.
Exceptions which I’m still reviewing are
P. Pudlágk, “On the length of proofs of finitistic consistency statements in first order theories”: www.math.cas.cz/~pudlak/fin-con.pdf
R. Parikh, “Existence and feasibility in arithmetic”, which I can’t find, and
S. Buss, “Bounded Arithmetic, Proof Complexity and Two Papers of Parikh”: www.math.ucsd.edu/~sbuss/ResearchWeb/parikh/paper.pdf , which reviews the previous Parikh paper and mentions some derived work.
Your first link seems to be almost exactly what I wanted, and the bounded Löb’s theorem should be a simple corollary. Thanks! This really simplifies the task of explaining Löbian cooperation =)
Cool, thanks for the links!