agda-unimath icon indicating copy to clipboard operation
agda-unimath copied to clipboard

Published 20 hours ago • verified publisher icon UniMath

Modal logic

Open spcfox opened this issue 8 months ago • 1 comments

Module containing the formalization of normal modal logics. It includes:

  • Syntax and Kripke semantics of modal logics
  • Definition of modal logics K and S5
  • Constructive proofs of soundness and consistency
  • Classical proofs of completeness and finite approximability

The theorems proved are easily generalized to other normal modal logics.

The code is currently being refactored.

spcfox avatar May 31 '24 20:05 spcfox