# 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
```