The modal logic of forcing

A set theoretical assertion ψ ψ is forceable or possible , written ◊ ψ ψ , if ψ ψ holds in some forcing extension, and necessary , written ◻ ψ ψ , if ψ ψ holds in all forcing extensions. In this forcing interpretation of modal logic, we establish that if ZFC is consistent, then the ZFC-provable principles of forcing are exactly those in the modal theory S 4.2 S4.2 .