= 27d567bc2d48d9f40e9ccc20ea370b15)
bogus 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)
Are these results actually novel? Proof complexity is a fairly well-established field in logic, and related results definitely exist, starting with Gödel's own Speedup theorem (which informally states that "simple" theorems exist with very long proofs, and that such proofs can be shortened by shifting to a more powerful system.)
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!