Project Page Index Table of Contents
  • Syntax of IEL
    • Size
    • Countability
  • Natural Deduction for IEL
    • Natural Deduction
    • Weakening
    • Admissibility for theories
    • Modal shifting lemma
    • Prime theories and contexts
      • Lindenbaum Lemma
      • Subset properties
      • Primeness properties
    • Truth Conditions and Derivations
    • Equivalence between IEL and IELm
  • Kripke-Models
    • Kripke Models
  • Classical Strong Completeness
    • Canonical models
    • Strong Completeness
      • Truth-Lemma
  • Sequent Calculus for IEL
    • Generic Structural Properties
    • Height-bounded sequent calculus
    • Inversion Results
    • Cut-Elimination
    • Equivalence between ND and SC
    • Disjunction Property
  • Decidability of IEL
    • Subformulas
    • Step Function
  • Structural Properties for Permutation-based sequent calculi
  • Permutation Based Cut-elimination for K
    • Cut Elimination
  • Case study: The classical modal logic K
    • Sequent Calculus for K
    • Inversion Results for K
    • Cut-Elimination for K
    • Decidability for K
  • Miscellaneous
    • Functions for dealing with contexts and lemmas about them
    • Induction principles
  • Additional Lemmas about Permutations
    • Map and Permutation
  • Constructive Completeness
  • Constructive Finite Model Property
      • Compute the candidate list
    • Admissibility
  • Semantic Cut-Elimination (following Su & Sano )
    • Semantic Cut-Elimination
  • Completeness for classical modal logics assuming dec
    • Option 1: Define unK with A \/ Box A
  • Completeness for classical modal logics assuming dec
    • Option 1: Define unK with A \/ Box A
Generated by coqdoc and improved with CoqdocJS