When faced with a question of the sort, "Is schema X valid in class of frames C?", we usually go about proving or disproving this by assuming the antecedent of X and showing that the consequent follows from the relations that characterize C. Simply enough.

However, I am faced with proving that the schema □(□A -> A) is valid in the class of all secondary reflexive frames and am not sure about how to proceed, as there is no simple antecedent to assume or consequent to aim for. I have thought about using K to decompose the above but that would allow for only a partial proof.

Note: I am not looking for a proof but rather for an explanation of methodology.

  • Your antecedent is empty in this case since X is not a conditional, other than that the methodology is the same. Assume nothing and aim for □(□A -> A) based on the secondary-reflexive relation. You need to show that □A -> A holds in every accessible world.
    – Conifold
    Nov 11 '19 at 6:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.