= 27d567bc2d48d9f40e9ccc20ea370b15)
HamletHenna comments on Formalising cousin_it's bounded versions of Gödel's theorem - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (4)
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!