Skip to content

Nicer soundness statements for the base_logic

Robbert Krebbers requested to merge robbert/base_logic_soundness into master

This MR introduces the following primitive soundness statements:

  • Soundness of pure propositions ⌜ φ ⌝%I → φ.
  • Soundness of later (▷ P)%I → P.

The old soundness statement, (▷^n ⌜ φ ⌝)%I → φ is now a derived form.

I think having (▷ P)%I → P is quite common in modal logic, so it's nice that we it too.

Edited by Robbert Krebbers

Merge request reports