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
  • Embedding IEL into IPC
  • Shallow Embedding type-based nd into Coq
    • Consistency of nd, if lifted to type
  • Classical Strong Completeness
    • Kripke Models
    • Canonical models
    • Strong Completeness
      • Truth-Lemma
    • Classical Admissability Results
      • Admissibility of reflection
      • Disjunction property
      • Disjunction Property for verifications
  • Constructive Strong Quasi-Completeness
    • Kripke Models
    • Modified Entailment Relation
    • Canonical models
      • Strong Quasi-Completeness
    • Completeness
      • Soundness (using LEM)
  • 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
  • Permutation-based Cut-Elimination for IEL
  • Structural Properties for Permutation-based sequent calculi
  • Case study: The classical modal logic K
    • Sequent Calculus for K
    • Inversion Results for K
    • Cut-Elimination for K
    • Decidability for K
  • Permutation Based Cut-elimination for K
    • Cut Elimination
  • Additional Lemmas about Permutations
    • Map and Permutation
  • IEL and the knowability paradox
    • Church-Fitch
    • Percivals Criticism of intuitionistic reflection
  • Miscellaneous
    • Functions for dealing with contexts and lemmas about them
    • Induction principles
Generated by coqdoc and improved with CoqdocJS