# Theory Usemantics

```section ‹Bounded semantics›

theory Usemantics imports SeCaV begin

text ‹In this theory, we define an alternative semantics for SeCaV formulas where the quantifiers
are bounded to terms in a specific set.
This is needed to construct a countermodel from a Hintikka set.›

text ‹This function defines the semantics, which are bounded by the set ‹u›.›
primrec usemantics where
‹usemantics u e f g (Pre i l) = g i (semantics_list e f l)›
| ‹usemantics u e f g (Imp p q) = (usemantics u e f g p ⟶ usemantics u e f g q)›
| ‹usemantics u e f g (Dis p q) = (usemantics u e f g p ∨ usemantics u e f g q)›
| ‹usemantics u e f g (Con p q) = (usemantics u e f g p ∧ usemantics u e f g q)›
| ‹usemantics u e f g (Exi p) = (∃x ∈ u. usemantics u (SeCaV.shift e 0 x) f g p)›
| ‹usemantics u e f g (Uni p) = (∀x ∈ u. usemantics u (SeCaV.shift e 0 x) f g p)›
| ‹usemantics u e f g (Neg p) = (¬ usemantics u e f g p)›

text ‹An environment is well-formed if the variables are actually in the quantifier set ‹u›.›
definition is_env :: ‹'a set ⇒ (nat ⇒ 'a) ⇒ bool› where
‹is_env u e ≡ ∀n. e n ∈ u›

text ‹A function interpretation is well-formed if it is closed in the quantifier set ‹u›.›
definition is_fdenot :: ‹'a set ⇒ (nat ⇒ 'a list ⇒ 'a) ⇒ bool› where
‹is_fdenot u f ≡ ∀i l. list_all (λx. x ∈ u) l ⟶ f i l ∈ u›

text ‹If we choose to quantify over the universal set, we obtain the usual semantics›
lemma usemantics_UNIV: ‹usemantics UNIV e f g p ⟷ semantics e f g p›
by (induct p arbitrary: e) auto

text ‹If a function name ‹n› is not in a formula, it does not matter whether it is in
the function interpretation or not.›
lemma uupd_lemma [iff]: ‹n ∉ params p ⟹ usemantics u e (f(n := x)) g p ⟷ usemantics u e f g p›
by (induct p arbitrary: e) simp_all

text ‹The semantics of substituting variable i by term t in formula a are well-defined›
lemma usubst_lemma [iff]:
‹usemantics u e f g (subst a t i) ⟷ usemantics u (SeCaV.shift e i (semantics_term e f t)) f g a›
by (induct a arbitrary: e i t) simp_all

subsubsection ‹Soundness of SeCaV with regards to the bounded semantics›
text ‹We would like to prove that the SeCaV proof system is sound under the bounded semantics.›

text ‹If the environment and the function interpretation are well-formed, the semantics of terms
are in the quantifier set ‹u›.›
lemma usemantics_term [simp]:
assumes ‹is_env u e› ‹is_fdenot u f›
shows ‹semantics_term e f t ∈ u› ‹list_all (λx. x ∈ u) (semantics_list e f ts)›
using assms by (induct t and ts rule: semantics_term.induct semantics_list.induct)

text ‹If a function interpretation is well-formed, replacing the value by one in the quantifier set
results in a well-formed function interpretation.›
lemma is_fdenot_shift [simp]: ‹is_fdenot u f ⟹ x ∈ u ⟹ is_fdenot u (f(i := λ_. x))›
unfolding is_fdenot_def SeCaV.shift_def by simp

text ‹If a sequent is provable in the SeCaV proof system and the environment
and function interpretation are well-formed, the sequent is valid under the bounded semantics.›
theorem sound_usemantics:
assumes ‹⊩ z› and ‹is_env u e› and ‹is_fdenot u f›
shows ‹∃p ∈ set z. usemantics u e f g p›
using assms
proof (induct arbitrary: f rule: sequent_calculus.induct)
case (10 i p z)
then show ?case
proof (cases ‹∀x ∈ u. usemantics u e (f(i := λ_. x)) g (sub 0 (Fun i []) p)›)
case False
moreover have ‹∀x ∈ u. ∃p ∈ set (sub 0 (Fun i []) p # z). usemantics u e (f(i := λ_. x)) g p›
using 10 is_fdenot_shift by metis
ultimately have ‹∃x ∈ u. ∃p ∈ set z. usemantics u e (f(i := λ_. x)) g p›
by fastforce
moreover have ‹list_all (λp. i ∉ params p) z›
using 10 by simp
ultimately show ?thesis
using 10 Ball_set insert_iff list.set(2) uupd_lemma by metis
qed simp
next
case (11 i p z)
then show ?case
proof (cases ‹∀x ∈ u. usemantics u e (f(i := λ_. x)) g (Neg (sub 0 (Fun i []) p))›)
case False
moreover have
‹∀x ∈ u. ∃p ∈ set (Neg (sub 0 (Fun i []) p) # z). usemantics u e (f(i := λ_. x)) g p›
using 11 is_fdenot_shift by metis
ultimately have ‹∃x ∈ u. ∃p ∈ set z. usemantics u e (f(i := λ_. x)) g p›
by fastforce
moreover have ‹list_all (λp. i ∉ params p) z›
using 11 by simp
ultimately show ?thesis
using 11 Ball_set insert_iff list.set(2) uupd_lemma by metis
qed simp
qed fastforce+

end
```