= 27d567bc2d48d9f40e9ccc20ea370b15)
Zetetic comments on A model of UDT without proof limits - 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 (37)
I found myself wondering if there are any results about the length of the shortest proof in which a proof system can reach a contradiction, and found the following papers:
Paper 1 talks about partial consistency. We have statements of the following form:
The paper claims that this is provable in ZF for each n. The paper then discusses results about the proof length of the partial consistency statements is polynomial in n. The author goes on to derive analogous results pertaining to frege proof systems weaker than ZF.
From these results it may be possible to have the agent's proof system produce a partial consistency result for a stipulated length.
Paper 2 shows that the question of whether a formula
has a proof of length no more than k is undecidable.
Both papers seem relevant, but I don't presently have the time to think them through carefully.
There's stuff like that in Ch. 2 of Lindstrom's Aspects of Incompleteness, apparently elementary within the area.
Thanks to you and Nesov for the references. I didn't know this stuff and it looks like it might come in handy.