[FOM] bounds on proofs

[Alasdair Urquhart]

Pavel Hrubes has some very good results on this question.
In particular, he proved exponential lower bounds on the
size of proofs in K, S4 and some other systems.

"Lower Bounds for modal logics", JSL 72 (2007), 941-958.


On Wed, 18 May 2016, Sara L. Uckelman wrote:

> This isn't exactly a FOM question but hopefully it's enough on topic to
> be admissable.  A student of mine wrote this morning asking about
> known results regarding bounds on proofs, particularly proofs in modal
> systems:
>
> "for, for example, the systems of modal logic we studied, and which we
> proved were complete, can we then put a bound on the length of the
> proof of a theorem?  If not, are there systems in which we can
> construct such a bound?"
>
> Chapter 5 of Hughes & Cresswell give a constructive method for showing
> the completeness of S5, with a procedure for mechanically generating a
> proof of any theorem, and I suspect that without too much difficulty a
> bound could be put on these.  But I'll admit, my knowledge of other such
> constructive proof procedures is limited, so I simply don't know of any
> of the relevant results in this area.
>
> References would be appreciate by both my student and myself!
>
> Cheers,
> -Sara