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:
) is a statement that there is no ZF-proof of contradiction with length =< n.
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 phi 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.
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 phi 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.