[FOM] bounds on proofs

Sara L. Uckelman s.l.uckelman at durham.ac.uk
Wed May 18 10:37:54 EDT 2016

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

"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!


Dr. Sara L. Uckelman
Department of Philosophy
Durham University

The Dictionary of Medieval Names from European Sources

More information about the FOM mailing list