Why Cut-Free Is Needed
Nonconstructive proofs of realization apparently have a broader scope than constructive versions. All known constructive realization proofs build on some cut-free proof system: sequents, tableaus, hypersequents, nested sequents, and so on.
Why not axiom systems? After all, many more modal logics have axiomatic characterizations than are known to have one that is cut-free. One might think it would be relatively easy to extract a realization from an axiomatic proof, as we did in the previous section. Just work line by line. But, nobody knows how to do this in general. The problem is with modus ponens. In this section we discuss just what that problem is.
If we make the “wrong” choice for a realizer, it is possible that we block modus ponens applications. How do we know this can be avoided, that a “right” choice is always possible? In Wang (2011b, 2014) noncircular axiomatic proofs are introduced. Roughly, these are the ones for which a right choice is guaranteed. But no general methodology is known for constructively
showing noncircular proofs for modal logics always exist or for deciding which logics always have such proofs. In fact, this is something that is guaranteed by the existence of a cut-free proof system for a modal logic, and we are back to where we started.