 The above correspondence result immediately shows that GL is modally sound with respect to the class of possible worlds models on transitive conversely well-founded frames, because all axioms and rules of GL are valid on such models. The question is whether completeness also holds: for example, the formula \(\Box A \rightarrow \Box\Box A\), which is valid on all transitive frames, is indeed provable in GL, as was mentioned in  Section 1.  But is every formula that is valid on all transitive conversely well-founded frames also provable in GL?