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›
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
