[FOM] bounds on proofs

[Sara L. Uckelman]

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


-- 
Dr. Sara L. Uckelman
Department of Philosophy
Durham University
https://www.dur.ac.uk/philosophy/staff/?id=12928

The Dictionary of Medieval Names from European Sources
http://dmnes.org/