[Caveat lector: I don’t know that much about this, but that’s how I see it at the moment.]
The amount of information required to find a proof of a proposition given all the information implicit in (the statement of) the proposition depends on the system doing the proof search. The system’s search order can be seen as a prior over proofs (and over potentially useful intermediate proof steps, auxiliary definitions, etc). Additional info can update the prior, so that you find the proof faster, or using fewer resources in general (or misupdate and find the proof later, or in a more costly way, or never at all).
So I think you’re right, but there are caveats.
Although it’s also possible that there’s some well-behaved class of proof-finding systems such that for any two of them, those caveats become irrelevant in the limit (of proposition/proof complexity or something?). (Logical inductors?)
[Caveat lector: I don’t know that much about this, but that’s how I see it at the moment.]
The amount of information required to find a proof of a proposition given all the information implicit in (the statement of) the proposition depends on the system doing the proof search. The system’s search order can be seen as a prior over proofs (and over potentially useful intermediate proof steps, auxiliary definitions, etc). Additional info can update the prior, so that you find the proof faster, or using fewer resources in general (or misupdate and find the proof later, or in a more costly way, or never at all).
So I think you’re right, but there are caveats.
Although it’s also possible that there’s some well-behaved class of proof-finding systems such that for any two of them, those caveats become irrelevant in the limit (of proposition/proof complexity or something?). (Logical inductors?)