Theory HintikkaTheory
theory HintikkaTheory
imports MaximalSet
begin
section ‹ Hintikka Theorem ›
text ‹
The formalization of Hintikka's lemma is by induction on the structure of the formulas in a Hintikka
set $H$ by applying the technical theorem {\tt HintikkaP\_model\_aux}. This theorem applies a series
of lemmas to address the evaluation of all possible cases of formulas in $H$. Indeed, considering
the Boolean evaluation $IH$ that maps all propositional letters in $H$ to true and all other letters
to false, the most interesting cases of the inductive proof are those related to implicational
formulas in $H$ and the negation of arbitrary formulas in $H$. These cases are not straightforward
since implicational and negation formulas are not considered in the definition of Hintikka sets.
For an implicational formula, say $F_1 \longrightarrow F_2$, it is necessary to prove that if it
belongs to $H$, its evaluation by $IH$ is true. Also, whenever
$\neg(F_1 \longrightarrow F_2)$ belongs to $H$ its evaluation is false. The proof is obtained by
relating such formulas, respectively, with $\beta$ and $\alpha$ formulas (case P6).
The second interesting case is the one related to arbitrary negations. In this case, it is proved
that if $\neg F$ belongs to $H$, its evaluation by $IH$ is true, and in the case that
$\neg\neg F$ belongs to $H$, its evaluation by $IH$ is also true (Case P7).
›
locale HintikkaProp =
fixes H :: "'b formula set"
assumes "ClosedPredicate H
(λ H G . G ∈ H)
(λ H G . G ∈ H)
(λ H F G . F ∈ H ∧ G ∈ H)
(λ H F G . F ∈ H ∨ G ∈ H)"
fun IH :: "'b formula set ⇒ 'b ⇒ bool" where
"IH H P = (if atom P ∈ H then True else False)"
lemma (in HintikkaProp) HintikkaConj:
assumes "(F ∧. G) ∈ H"
shows "F ∈ H ∧ G ∈ H"
proof-
have "FormulaAlpha (F ∧. G)" by auto
have 1: "Comp1 (F ∧. G) = F"
by (simp add: Comp1_def)
have "Comp2 (F ∧. G) = G"
by (simp add: Comp2_def)
thus ?thesis using 1 assms AlphaPredicate_def ClosedPredicate_def HintikkaProp_def
by (metis (no_types, lifting) FormulaAlpha.simps(1) HintikkaProp_axioms)
qed
lemma (in HintikkaProp) HintikkaNegConj:
assumes "¬.(F ∧. G) ∈ H"
shows "¬.F ∈ H ∨ ¬.G ∈ H"
proof-
have 1: "FormulaBeta (¬. (F ∧. G))" by auto
have 2: "Comp1 (¬. (F ∧. G)) = ¬.F"
by (simp add: Comp1_def)
have "Comp2 (¬. (F ∧. G)) = ¬.G"
by (simp add: Comp2_def)
thus ?thesis using "1" "2" assms BetaPredicate_def ClosedPredicate_def
HintikkaProp_def
by (metis (lifting) HintikkaProp_axioms)
qed
lemma (in HintikkaProp) HintikkaDisj:
assumes "(F ∨. G) ∈ H"
shows "F ∈ H ∨ G ∈ H"
proof-
have 1: "FormulaBeta (F ∨. G)" by auto
have 2: "Comp1 (F ∨. G) = F"
by (simp add: Comp1_def)
have "Comp2 (F ∨. G) = G"
by (simp add: Comp2_def)
thus ?thesis using "1" "2" BetaPredicate_def ClosedPredicate_def HintikkaProp_axioms
HintikkaProp_def assms
by (metis (lifting))
qed
lemma (in HintikkaProp) HintikkaNegDisj:
assumes "¬.(F ∨. G) ∈ H"
shows "¬.F ∈ H ∧ ¬.G ∈ H"
proof-
have 1: "FormulaAlpha (¬.(F ∨. G))" by auto
have 2: "Comp1 (¬.(F ∨. G)) = ¬.F"
by (simp add: Comp1_def)
have "Comp2 (¬. (F ∨. G)) = ¬.G"
by (simp add: Comp2_def)
thus ?thesis using "1" "2" AlphaPredicate_def ClosedPredicate_def HintikkaProp_axioms
HintikkaProp_def assms
by (metis (no_types, lifting))
qed
lemma (in HintikkaProp) HintikkaImp:
assumes "(F1 →. F2) ∈ H"
shows "¬.F1 ∈ H ∨ F2 ∈ H"
proof-
have 1: "FormulaBeta (F1 →. F2)" by auto
have 2: "Comp1 (F1 →. F2) = ¬.F1"
by (simp add: Comp1_def)
have "Comp2 (F1 →. F2) = F2"
by (simp add: Comp2_def)
thus ?thesis
by (metis (no_types, lifting) "1" "2" BetaPredicate_def ClosedPredicate_def HintikkaProp_axioms
HintikkaProp_def assms)
qed
lemma (in HintikkaProp) HintikkaNegImp:
assumes "¬.(F1 →. F2) ∈ H"
shows "F1 ∈ H ∧ ¬.F2∈H"
proof-
have 1: "FormulaAlpha (¬.(F1 →. F2))" by auto
have 2: "Comp1 (¬.(F1 →. F2)) = F1"
by (simp add: Comp1_def)
have "Comp2 (¬.(F1 →. F2)) = ¬.F2"
by (simp add: Comp2_def)
thus ?thesis
by (metis (lifting) "1" "2" AlphaPredicate_def ClosedPredicate_def HintikkaProp_axioms HintikkaProp_def assms)
qed
lemma (in HintikkaProp) HintikkaP_model_aux:
shows "(F ∈ H ⟶ t_v_evaluation (IH H) F) ∧ (¬. F ∈ H ⟶ t_v_evaluation (IH H) (¬. F))"
proof(induction F)
case FF
then show ?case
using HintikkaProp_axioms HintikkaProp_def ClosedPredicate_def ConstPredicate_def
by fastforce
next
case TT
then show ?case
using HintikkaProp_axioms HintikkaProp_def ClosedPredicate_def ConstPredicate_def t_v_evaluation.simps(2)
by (metis (no_types, lifting))
next
case (atom x)
then show ?case
using HintikkaProp_axioms HintikkaProp_def AtomPredicate_def ClosedPredicate_def IH.elims(1) t_v_evaluation.simps(3,4)
by (metis (no_types, lifting))
next
case (Negation F)
then show ?case
using HintikkaProp_axioms HintikkaProp_def ClosedPredicate_def DNegPredicate_def
t_v_evaluation.simps(4)
by (metis (lifting))
next
case (Conjunction F1 F2)
then show ?case
by (metis HintikkaConj HintikkaNegConj t_v_evaluation.simps(4,5))
next
case (Disjunction F1 F2)
then show ?case
by (metis HintikkaDisj HintikkaNegDisj t_v_evaluation.simps(4,6))
next
case (Implication F1 F2)
then show ?case
by (metis HintikkaImp HintikkaNegImp t_v_evaluation.simps(4,7))
qed
corollary (in HintikkaProp) ModelHintikkaPa:
assumes "F ∈ H"
shows "t_v_evaluation (IH H) F"
using assms HintikkaP_model_aux by auto
corollary (in HintikkaProp) ModelHintikkaP:
shows "(IH H) model H"
proof (unfold model_def)
show "∀F∈H. t_v_evaluation (IH H) F"
proof (rule ballI)
fix F
assume "F ∈ H"
thus "t_v_evaluation (IH H) F" using ModelHintikkaPa by auto
qed
qed
corollary (in HintikkaProp) HintikkaSatisfiable:
shows "satisfiable H"
using ModelHintikkaP
by (unfold satisfiable_def, auto)
definition HintikkaP :: "'b formula set ⇒ bool" where
"HintikkaP H = ((∀P. ¬ (atom P ∈ H ∧ (¬.atom P) ∈ H)) ∧
⊥. ∉ H ∧ (¬.⊤.) ∉ H ∧
(∀F. (¬.¬.F) ∈ H ⟶ F ∈ H) ∧
(∀F. ((FormulaAlpha F) ∧ F ∈ H) ⟶
((Comp1 F) ∈ H ∧ (Comp2 F) ∈ H)) ∧
(∀F. ((FormulaBeta F) ∧ F ∈ H) ⟶
((Comp1 F) ∈ H ∨ (Comp2 F) ∈ H)))"
lemma HintikkaEq : "HintikkaP H = HintikkaProp H"
unfolding HintikkaP_def HintikkaProp_def AtomPredicate_def ConstPredicate_def
DNegPredicate_def AlphaPredicate_def BetaPredicate_def ClosedPredicate_def
by simp
end