Theory Hintikka

section ‹Hintikka sets for SeCaV›

theory Hintikka
  imports Prover
begin

text ‹In this theory, we define the concept of a Hintikka set for SeCaV formulas.
  The definition mirrors the SeCaV proof system such that Hintikka sets are downwards closed with
  respect to the proof system.›

text ‹This defines the set of all terms in a set of formulas (containing ‹Fun 0 []› if it would
  otherwise be empty).›
definition
  ‹terms H ≡ if (⋃p ∈ H. set (subtermFm p)) = {} then {Fun 0 []}
    else (⋃p ∈ H. set (subtermFm p))›

locale Hintikka =
  fixes H :: ‹fm set›
  assumes
    Basic: ‹Pre n ts ∈ H ⟹ Neg (Pre n ts) ∉ H› and
    AlphaDis: ‹Dis p q ∈ H ⟹ p ∈ H ∧ q ∈ H› and
    AlphaImp: ‹Imp p q ∈ H ⟹ Neg p ∈ H ∧ q ∈ H› and
    AlphaCon: ‹Neg (Con p q) ∈ H ⟹ Neg p ∈ H ∧ Neg q ∈ H› and
    BetaCon: ‹Con p q ∈ H ⟹ p ∈ H ∨ q ∈ H› and
    BetaImp: ‹Neg (Imp p q) ∈ H ⟹ p ∈ H ∨ Neg q ∈ H› and
    BetaDis: ‹Neg (Dis p q) ∈ H ⟹ Neg p ∈ H ∨ Neg q ∈ H› and
    GammaExi: ‹Exi p ∈ H ⟹ ∀t ∈ terms H. sub 0 t p ∈ H› and
    GammaUni: ‹Neg (Uni p) ∈ H ⟹ ∀t ∈ terms H. Neg (sub 0 t p) ∈ H› and
    DeltaUni: ‹Uni p ∈ H ⟹ ∃t ∈ terms H. sub 0 t p ∈ H› and
    DeltaExi: ‹Neg (Exi p) ∈ H ⟹ ∃t ∈ terms H. Neg (sub 0 t p) ∈ H› and
    Neg: ‹Neg (Neg p) ∈ H ⟹ p ∈ H›

end