Theory Completeness

theory Completeness
  imports Soundness "HOL-Library.Countable_Set"
begin

section ‹Completeness›

text ‹Henkin completeness via the model-existence / abstract-consistency method
  of BKK Section 6 (Corollary 7.7), with the term model realised as a
  term evaluation (BKK Definition 3.35) --- then strengthened to arbitrary infinite value
  carriers, signatures with infinitely many parameters, and open formulas.›

subsection ‹Model existence and completeness (BKK Section 6, Corollary 7.7)›

text ‹We build a Henkin term model from a maximal consistent, saturated set of sentences, following
  BKK's model-existence route (BKK Section 6).  This file develops ‹NK›-consistency and its
  closure properties (BKK Lemma 7.5), the maximal saturated extension (BKK Lemma 6.32), the term
  model with its truth lemma (BKK Theorem 6.33), and the completeness theorem itself
  (BKK Corollary 7.7).›

subsubsection ‹Consistency (BKK Definition 7.4)›

text ‹A set of sentences is @{emph ‹NK-consistent›} (BKK Definition 7.4) if falsity is not derivable
  from it.›

definition con :: "'p tm set ⇒ bool" where "con Φ ⟷ ¬ (Φ ⊢ ❙⊥)"
lemma con_I: "(Φ ⊢ ❙⊥ ⟹ False) ⟹ con Φ" by (auto simp: con_def)

text ‹Subsets of a consistent set are consistent (using weakening).›

lemma con_mono: "con Ψ ⟹ Φ ⊆ Ψ ⟹ freep Ψ ⟹ con Φ" unfolding con_def
    using bprov_weaken by blast

text ‹Consistency is of finite character (compactness, BKK Definition 6.1): a set is consistent
  as soon as all its finite subsets are.›

lemma con_compact:
  "(⋀Φ0::'p::infinite tm set. finite Φ0 ⟹ Φ0 ⊆ Φ ⟹ con Φ0) ⟹ con Φ"
  using bprov_finite unfolding con_def by blast

text ‹The central step of a maximal-consistent extension (the ‹∇⇩s⇩a⇩t› case of BKK Lemma 7.5;
  property ‹∇⇩s⇩a⇩t› is BKK Definition 6.5): from a consistent set, adding a proposition or its
  negation keeps it consistent.›

lemma con_split: assumes "con Φ" and "wff⇘𝗈⇙(A)"
  shows "con (insert A Φ) ∨ con (insert (❙¬ A) Φ)"
proof (rule ccontr)
  assume "¬?thesis"
  hence "Φ ∪ {A} ⊢ ❙⊥" and "Φ ∪ {❙¬ A} ⊢ ❙⊥" by (auto simp: con_def)
  from ‹Φ ∪ {A} ⊢ ❙⊥› have "Φ ⊢ ❙¬ A" using assms(2)
      by (rule bprov.NegI)
  moreover from ‹Φ ∪ {❙¬ A} ⊢ ❙⊥› have "Φ ⊢ A" using assms(2)
      by (rule bprov.Contr)
  ultimately have "Φ ⊢ ❙⊥" using wff_FalseB by (rule bprov.NegE)
  thus False using assms(1) by (simp add: con_def)
qed

text ‹A consistent set does not contain both a proposition and its negation.›

lemma con_not_both: "con Φ ⟹ A ∈ Φ ⟹ ❙¬ A ∈ Φ ⟹ wff⇘𝗈⇙(A) ⟹ False"
  by (metis con_def wff_FalseB NegE Hyp)

subsubsection ‹Some admissible rules›

lemma freep_un: "freep Φ ⟹ freep (Φ ∪ {A})"
  by (metis freep_add Un_insert_right sup_bot.right_neutral)

text ‹Double-negation elimination (derivable from the classical rule ‹NK(Contr)›).›

lemma dneg: "Φ ⊢ ❙¬ (Neg ❙⋅ X) ⟹ wff⇘𝗈⇙(X) ⟹ freep Φ ⟹ Φ ⊢ X"
  by (metis (no_types, lifting) Contr Hyp NegE Un_insert_right bprov_weaken
            freep_add insertI1 subset_insertI sup_bot.right_neutral wff_FalseB)

text ‹Excluded middle and implication introduction (derivable in the classical calculus).›

lemma bprov_em: assumes wA: "wff⇘𝗈⇙(A)" shows "Φ ⊢ (❙¬ A) ❙∨ A"
proof -
  let ?D = "(❙¬ A) ❙∨ A"
  have wnA: "wff⇘𝗈⇙(❙¬ A)" using wA by (rule wff_Not)
  have wD: "wff⇘𝗈⇙(?D)" using wnA wA by (rule wff_Or)
  have "Φ ∪ {❙¬ ?D} ⊢ ❙¬ A"
  proof (rule bprov.NegI[OF _ wA])
    have "(Φ ∪ {❙¬ ?D}) ∪ {A} ⊢ A" by (auto intro: bprov.Hyp)
    hence "(Φ ∪ {❙¬ ?D}) ∪ {A} ⊢ ?D" using wnA by (rule bprov.DisIR)
    moreover have "(Φ ∪ {❙¬ ?D}) ∪ {A} ⊢ ❙¬ ?D"
        by (auto intro: bprov.Hyp)
    ultimately show "(Φ ∪ {❙¬ ?D}) ∪ {A} ⊢ ❙⊥" using wff_FalseB
        by (metis bprov.NegE)
  qed
  hence "Φ ∪ {❙¬ ?D} ⊢ ?D" using wA by (rule bprov.DisIL)
  moreover have "Φ ∪ {❙¬ ?D} ⊢ ❙¬ ?D" by (auto intro: bprov.Hyp)
  ultimately have "Φ ∪ {❙¬ ?D} ⊢ ❙⊥" using wff_FalseB by (metis bprov.NegE)
  thus ?thesis using wD by (rule bprov.Contr)
qed
lemma bprov_ImpE: assumes AB: "Φ ⊢ A ❙⊃ B" and A: "Φ ⊢ A"
    and fp: "freep Φ"
    and wA: "wff⇘𝗈⇙(A)" and wB: "wff⇘𝗈⇙(B)" shows "Φ ⊢ B"
proof -
  have wnA: "wff⇘𝗈⇙(❙¬ A)" using wA by (rule wff_Not)
  have disj: "Φ ⊢ (❙¬ A) ❙∨ B" using AB by (simp add: ImpB_def)
  have b1: "Φ ∪ {❙¬ A} ⊢ B"
    by (meson A Hyp NegE bprov_weaken fp freep_un inf_sup_ord(4) insertCI sup_ge1 wB)
  have b2: "Φ ∪ {B} ⊢ B" by (auto intro: bprov.Hyp)
  show ?thesis by (rule bprov.DisE[OF disj b1 b2 wnA wB])
qed
lemma bprov_TrueB: "Φ ⊢ ❙⊤" by (simp add: Hyp TrueB_def bprov.intros(3))

subsubsection ‹Witnessing a false universal
  (BKK property ‹∇⇩∃›, Definition 6.5; the ‹∇⇩∃› case of Lemma 7.5)›

text ‹If ‹¬Π⇘α⇙ G› is consistent with ‹Φ›, then it stays consistent when we add a witness
  ‹¬ (G c)› for a fresh parameter ‹c›.  This is the key step for making the extension saturated.›

lemma con_witness:
  assumes con: "con (insert (❙¬ ((Pi α) ❙⋅ G)) Φ)"
      and wG: "wff⇘α❙⇒𝗈⇙(G)" and fp: "freep Φ"
      and c: "c ∉ usedp Φ" "c ∉ pars G"
    shows "con (insert (❙¬ (G ❙⋅ (c⇧p⇘α⇙))) (insert (❙¬ ((Pi α) ❙⋅ G)) Φ))"
proof (rule con_I)
  define Γ where "Γ = Φ ∪ {❙¬ ((Pi α) ❙⋅ G)}"
  have fpG: "freep Γ" unfolding Γ_def by (rule freep_un[OF fp])
  assume "insert (❙¬ (G ❙⋅ (c⇧p⇘α⇙))) (insert (❙¬ ((Pi α) ❙⋅ G)) Φ) ⊢ ❙⊥"
  hence "Γ ∪ {❙¬ (G ❙⋅ (c⇧p⇘α⇙))} ⊢ ❙⊥" by (simp add: Γ_def insert_commute)
  hence "Γ ⊢ ❙¬ (Neg ❙⋅ (G ❙⋅ (c⇧p⇘α⇙)))"
    using wff_Not[OF wff_App[OF wG wff_Par]] by (rule bprov.NegI)
  hence "Γ ⊢ G ❙⋅ (c⇧p⇘α⇙)"
    using wff_App[OF wG wff_Par] fpG by (rule dneg)
  moreover have "c ∉ pars G" and "∀D ∈ Γ. c ∉ pars D" using c
    by (auto simp: Γ_def usedp_def)
  ultimately have piG: "Γ ⊢ (Pi α) ❙⋅ G" using wG
    by (blast intro: bprov.PiI)
  have "Γ ⊢ ❙¬ ((Pi α) ❙⋅ G)" by (auto simp: Γ_def intro: bprov.Hyp)
  from this piG have "Γ ⊢ ❙⊥" using wff_FalseB by (rule bprov.NegE)
  thus False using con by (simp add: con_def Γ_def)
qed

subsubsection ‹Maximal consistent, saturated extension (BKK's abstract extension lemma 6.32)›

text ‹We enumerate the (countably many) sentences and, step by step, decide each one or its
  negation (‹con_split›), immediately adding a Henkin witness for a decided negated universal
  (‹con_witness›).  The union of the chain is a maximal consistent, saturated set.›

definition freshc :: "'p tm set ⇒ 'p tm ⇒ 'p" where
 "freshc S G ≡ SOME c. c ∉ usedp S ∧ c ∉ pars G"

lemma freshc_fresh: "freep S ⟹ freshc S G ∉ usedp S ∧ freshc S G ∉ pars G"
  by (metis (lifting) finite_pars freep_fresh freshc_def someI_ex)

fun wit :: "'p tm set ⇒ 'p tm ⇒ 'p tm set" where
  ‹wit S (❙¬App (Pi α) G) = {❙¬ (G ❙⋅ ((freshc S G)⇧p⇘α⇙))}›
| ‹wit _ _ = {}›

lemma wit_cases: "wit S A = {} ∨ (∃α G. A = ❙¬ ((Pi α) ❙⋅ G) ∧
   wit S A = {❙¬ (G ❙⋅ ((freshc S G)⇧p⇘α⇙))})"
  by (induct S A rule: wit.induct) auto
lemma finite_wit: "finite (wit S A)"
  by (induct S A rule: wit.induct) auto
definition step :: "'p tm set ⇒ 'p tm ⇒ 'p tm set" where
  "step S A ≡ if cwff 𝗈 A
   then (if con (insert A S) then insert A S ∪ wit S A else insert (❙¬ A) S)
   else S"

primrec ext :: "'p::{countable,infinite} tm set ⇒ nat ⇒ 'p tm set" where
  "ext Φ 0 = Φ"
| "ext Φ (Suc n) = step (ext Φ n) (from_nat n)"

definition Hset :: "'p::{countable,infinite} tm set ⇒ 'p tm set" where
  "Hset Φ = (⋃n. ext Φ n)"

text ‹The chain is increasing and each stage stays finite-in-parameters and consistent.›

lemma ext_mono: "ext Φ n ⊆ ext Φ (Suc n)"
  by (induct n) (auto simp: step_def)
lemma ext_mono': "m ≤ n ⟹ ext Φ m ⊆ ext Φ n"
    using ext_mono lift_Suc_mono_le by blast
lemma freep_un_finite: "freep S ⟹ finite T ⟹ freep (S ∪ T)"
proof -
  assume "freep S" "finite T"
  hence "finite (usedp T)" by (auto simp: usedp_def)
  moreover have "- usedp (S ∪ T) = - usedp S - usedp T"
    by (auto simp: usedp_def)
  ultimately show ?thesis using ‹freep S›
    by (metis freep_def Diff_infinite_finite)
qed
lemma freep_step: "freep S ⟹ freep (step S A)"
  by (simp add: finite_wit freep_add freep_un_finite step_def)
lemma freep_ext: "freep Φ ⟹ freep (ext Φ n)"
  by (induction n) (auto simp: freep_step)
lemma con_step: assumes "con S" and "freep S" shows "con (step S A)"
proof (cases "cwff 𝗈 A")
  case False
  with assms(1) show ?thesis by (auto simp: step_def)
next case True
  show ?thesis 
  proof (cases "con (insert A S)")
    case False
    hence "con (insert (❙¬ A) S)"
      using con_split[OF assms(1)] cwff_wff[OF True] by blast
    thus ?thesis using False True by (simp add: step_def)
  next
    case True
    have "con (insert A S ∪ wit S A)" using wit_cases[of S A]  
    proof
      assume "wit S A = {}" thus ?thesis using True by simp
    next
      assume "∃α G. A = ❙¬ ((Pi α) ❙⋅ G) ∧ wit S A = {❙¬ (G ❙⋅ ((freshc S G)⇧p⇘α⇙))}"
      then obtain α G where AG: "A = ❙¬ ((Pi α) ❙⋅ G)"
        and w: "wit S A = {❙¬ (G ❙⋅ ((freshc S G)⇧p⇘α⇙))}" by blast
      have wG: "wff⇘α❙⇒𝗈⇙(G)" using cwff_wff[OF ‹cwff 𝗈 A›] AG
        by (auto dest: wff_unique)
      have fr: "freshc S G ∉ usedp S" "freshc S G ∉ pars G"
        using freshc_fresh[OF assms(2)] by auto
      have "con (insert (❙¬ (G ❙⋅ ((freshc S G)⇧p⇘α⇙))) (insert A S))"
        by (metis AG True assms(2) con_witness fr(1,2) wG)
      thus ?thesis using w by simp
    qed
    thus ?thesis using True ‹cwff 𝗈 A› by (simp add: step_def)
  qed
qed
lemma con_ext: "con Φ ⟹ freep Φ ⟹ con (ext Φ n)"
  by (induction n) (auto simp: con_step freep_ext)

text ‹‹Hset Φ› extends ‹Φ› and, by compactness, is consistent.›

lemma Phi_sub_Hset: "Φ ⊆ Hset Φ" unfolding Hset_def using ext.simps(1)
  by blast
lemma finite_sub_ext: "finite F ⟹ F ⊆ Hset Φ ⟹ ∃N. F ⊆ ext Φ N"
proof (induction F rule: finite_induct)
  case empty thus ?case by blast
next
  case (insert x F)
  then obtain N where N: "F ⊆ ext Φ N" by auto
  from insert.prems obtain M where M: "x ∈ ext Φ M"
    by (auto simp: Hset_def)
  have "insert x F ⊆ ext Φ (max N M)"
    using N M ext_mono'[of N "max N M" Φ] ext_mono'[of M "max N M" Φ] by auto
  thus ?case by blast
qed
lemma con_Hset: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes "con Φ" and "freep Φ"
  shows "con (Hset Φ)"
  by (metis assms(1,2) con_compact con_ext con_mono finite_sub_ext freep_ext)

text ‹Crucially, ‹freep (Hset Φ)› fails (a maximal set uses every parameter), so we never weaken
  @{emph ‹to›} ‹Hset›.  Instead we use that every @{emph ‹finite›} subset of ‹Hset› is consistent
      ---
  finite contexts are always ‹freep›, which is all the proof rules need.›

lemma Hset_finite_con: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes "con Φ" and "freep Φ" and "finite F" and "F ⊆ Hset Φ"
  shows "con F" 
  by (meson assms(1,2,3,4) con_ext con_mono finite_sub_ext freep_ext)

text ‹‹Hset› decides every sentence --- BKK call this @{emph ‹saturated›}, property ‹⇩~∇⇩s⇩a⇩t›
  (BKK Definition 6.24) --- and has the Henkin witness property ‹⇩~∇⇩∃› (BKK Definition 6.19).
  We call the former @{emph ‹maximality›} and reserve @{emph ‹saturation›} for the witness
  property; the lemma names below follow this convention.›

lemma Hset_maximal: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes c: "cwff 𝗈 A" shows "A ∈ Hset Φ ∨ ❙¬ A ∈ Hset Φ"
proof -
  have "A ∈ ext Φ (Suc (to_nat A)) ∨ ❙¬ A ∈ ext Φ (Suc (to_nat A))"
    using c by (auto simp: step_def)
  thus ?thesis unfolding Hset_def by blast
qed
lemma Hset_saturated: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes conΦ: "con Φ" and fp: "freep Φ"
  and cA: "cwff 𝗈 (❙¬ ((Pi α) ❙⋅ G))" and inH: "❙¬ ((Pi α) ❙⋅ G) ∈ Hset Φ"
shows "∃c. ❙¬ (G ❙⋅ (c⇧p⇘α⇙)) ∈ Hset Φ"
proof -
  note wA = cwff_wff[OF cA] and fvsA = cwff_closed[OF cA]
  let ?A = "❙¬ ((Pi α) ❙⋅ G)"
  let ?S = "ext Φ (to_nat ?A)"
  have step: "ext Φ (Suc (to_nat ?A)) = step ?S ?A"
    by simp
  have "con (insert ?A ?S)"
  proof (rule ccontr)
    assume "¬ con (insert ?A ?S)"
    hence "❙¬ ?A ∈ ext Φ (Suc (to_nat ?A))" using cA step
        by (auto simp: step_def)
    hence "❙¬ ?A ∈ Hset Φ" unfolding Hset_def by blast
    thus False using con_not_both[OF con_Hset[OF conΦ fp] inH _ wA]
        by blast
  qed
  hence "wit ?S ?A ⊆ ext Φ (Suc (to_nat ?A))" using cA step
    by (auto simp: step_def)
  moreover have "wit ?S ?A = {❙¬ (G ❙⋅ ((freshc ?S G)⇧p⇘α⇙))}"
    by simp
  ultimately have "❙¬ (G ❙⋅ ((freshc ?S G)⇧p⇘α⇙)) ∈ Hset Φ"
    unfolding Hset_def by blast
  thus ?thesis by blast
qed

subsubsection ‹Leibniz equality is reflexive (BKK property ‹∇⇩r›, Lemma 6.25)›

lemma leib_refl: assumes fp: "freep Φ" and wa: "wff⇘α⇙(A)"
  shows "Φ ⊢ A ❙≐⇘α⇙ A" by (simp add: EqL EqR wa)

text ‹Leibniz substitution (the substitutivity built into BKK's Leibniz equality, Section 2.2;
cf.\ the ‹∇›-properties of BKK Lemma 6.12): equals may replace equals
in any predicate.  Instantiating ‹P› with suitable predicates yields symmetry, transitivity
and congruence.›

lemma leib_subst:
  assumes AB: "Φ ⊢ A ❙≐⇘α⇙ B" and fp: "freep Φ" and wa: "wff⇘α⇙(A)" and wb: "wff⇘α⇙(B)"
      and wP: "wff⇘α❙⇒𝗈⇙(P)" and PA: "Φ ⊢ P ❙⋅ A"
    shows "Φ ⊢ P ❙⋅ B"
proof -
  let ?body = "(Bnd 0) ❙⋅ A ❙⊃ (Bnd 0) ❙⋅ B"
  have "Φ ⊢ ❙Π⇘α❙⇒𝗈⇙ ?body"
    using Leib_beq[OF wa wb] AB by (rule bprov.Beta)
  hence "Φ ⊢ (Pi (α ❙⇒ 𝗈)) ❙⋅ (❙Λ⇘α ❙⇒ 𝗈⇙ ?body)" by (simp add: Forall_def)
  hence P: "Φ ⊢ (❙Λ⇘α ❙⇒ 𝗈⇙ ?body) ❙⋅ P" using wP by (rule bprov.PiE)
  have wAbs: "wff⇘(α❙⇒𝗈)❙⇒𝗈⇙(❙Λ⇘α ❙⇒ 𝗈⇙ ?body)"
    by (auto simp: opn_lc[OF wff_lc[OF wa]] opn_lc[OF wff_lc[OF wb]]
             intro!: wff_App wff_Fre wa wb wff_AbsI)
  have "(❙Λ⇘α ❙⇒ 𝗈⇙ ?body) ❙⋅ P ≈⇘𝗈⇙ P ❙⋅ A ❙⊃ P ❙⋅ B"
  proof -
    have "(❙Λ⇘α ❙⇒ 𝗈⇙ ?body) ❙⋅ P ≈⇘𝗈⇙ ?body❙⟨P❙⟩"
      by (rule beq.beta[OF wAbs wP])
    thus ?thesis
      by (simp add: opn_lc[OF wff_lc[OF wa]] opn_lc[OF wff_lc[OF wb]])
  qed
  from bprov.Beta[OF this P] have "Φ ⊢ P ❙⋅ A ❙⊃ P ❙⋅ B".
  moreover have "wff⇘𝗈⇙(P ❙⋅ A)" by (rule wff_App[OF wP wa])
  moreover have "wff⇘𝗈⇙(P ❙⋅ B)" by (rule wff_App[OF wP wb])
  ultimately show ?thesis using PA fp by (metis bprov_ImpE)
qed
lemma leib_sym:
  assumes AB: "Φ ⊢ A ❙≐⇘α⇙ B" and fp: "freep Φ" and wa: "wff⇘α⇙(A)" and wb: "wff⇘α⇙(B)"
  shows "Φ ⊢ B ❙≐⇘α⇙ A"
proof -
  have lcA: "lc A" using wa by (rule wff_lc)
  let ?P = "❙Λ⇘α⇙ (((Leib α) ❙⋅ (Bnd 0)) ❙⋅ A)" ― ‹the predicate ‹λx. x ❙≐ A››
  have wP: "wff⇘α❙⇒𝗈⇙(?P)" by (auto simp: opn_lc[OF lcA] intro!: wff_Fre wa wff_AbsI)
  have PbA: "?P ❙⋅ A ≈⇘𝗈⇙ (A ❙≐⇘α⇙ A)"
    using beq.beta[OF wP wa] by (simp add: opn_lc[OF lcA])
  have PbB: "?P ❙⋅ B ≈⇘𝗈⇙ (B ❙≐⇘α⇙ A)"
    using beq.beta[OF wP wb] by (simp add: opn_lc[OF lcA])
  have "Φ ⊢ A ❙≐⇘α⇙ A" using fp wa by (rule leib_refl)
  hence "Φ ⊢ ?P ❙⋅ A"
    using beq.sym[OF PbA] by (rule bprov.Beta[rotated])
  hence "Φ ⊢ ?P ❙⋅ B" using leib_subst[OF AB fp wa wb wP] by auto
  thus ?thesis by (rule bprov.Beta[OF PbB])
qed
lemma leib_trans:
  assumes AB: "Φ ⊢ A ❙≐⇘α⇙ B" and BC: "Φ ⊢ B ❙≐⇘α⇙ C" and fp: "freep Φ"
      and wa: "wff⇘α⇙(A)" and wb: "wff⇘α⇙(B)" and wc: "wff⇘α⇙(C)"
    shows "Φ ⊢ A ❙≐⇘α⇙ C"
proof -
  have lcA: "lc A" using wa by (rule wff_lc)
  let ?P = "❙Λ⇘α⇙ (((Leib α) ❙⋅ A) ❙⋅ (Bnd 0))" ― ‹the predicate ‹λx. A ❙≐ x››
  have wP: "wff⇘α❙⇒𝗈⇙(?P)"
    by (auto simp: opn_lc[OF lcA] intro!: wff_Fre wa wff_AbsI)
  have PbB: "?P ❙⋅ B ≈⇘𝗈⇙ (A ❙≐⇘α⇙ B)"
    using beq.beta[OF wP wb] by (simp add: opn_lc[OF lcA])
  have PbC: "?P ❙⋅ C ≈⇘𝗈⇙ (A ❙≐⇘α⇙ C)"
    using beq.beta[OF wP wc] by (simp add: opn_lc[OF lcA])
  from AB have "Φ ⊢ ?P ❙⋅ B" by (rule bprov.Beta[OF beq.sym[OF PbB]])
  hence "Φ ⊢ ?P ❙⋅ C" using leib_subst[OF BC fp wb wc wP] by auto
  thus ?thesis by (rule bprov.Beta[OF PbC])
qed
lemma leib_cong2:
  assumes AA: "Φ ⊢ A ❙≐⇘α⇙ A'" and fp: "freep Φ"
  and wa: "wff⇘α⇙(A)" and wa': "wff⇘α⇙(A')" and wC: "wff⇘α❙⇒β⇙(C)"
  shows "Φ ⊢ (C ❙⋅ A) ❙≐⇘β⇙ (C ❙⋅ A')"
proof -
  have lcC: "lc C" using wC by (rule wff_lc)
  have lcA: "lc A" using wa by (rule wff_lc)
  let ?P = "❙Λ⇘α⇙ (C ❙⋅ A ❙≐⇘β⇙ C ❙⋅ (Bnd 0))"   ― ‹‹λx. (C A) ❙≐ (C x)››
  have wP: "wff⇘α❙⇒𝗈⇙(?P)"
    by (auto simp: opn_lc[OF lcC] opn_lc[OF lcA]
             intro!: wff_AbsI wff_App wff_Fre wC wa wff_App[OF wC wa])
  have PbA: "?P ❙⋅ A ≈⇘𝗈⇙ (C ❙⋅ A ❙≐⇘β⇙ C ❙⋅ A)"
    using beq.beta[OF wP wa] by (simp add: opn_lc[OF lcC] opn_lc[OF lcA])
  have PbA': "?P ❙⋅ A' ≈⇘𝗈⇙ (C ❙⋅ A ❙≐⇘β⇙ C ❙⋅ A')"
    using beq.beta[OF wP wa'] by (simp add: opn_lc[OF lcC] opn_lc[OF lcA])
  have "Φ ⊢ C ❙⋅ A ❙≐⇘β⇙ C ❙⋅ A" using fp wff_App[OF wC wa]
      by (rule leib_refl)
  hence "Φ ⊢ ?P ❙⋅ A" by (rule bprov.Beta[OF beq.sym[OF PbA]])
  hence "Φ ⊢ ?P ❙⋅ A'" using leib_subst[OF AA fp wa wa' wP] by auto
  thus ?thesis by (rule bprov.Beta[OF PbA'])
qed
lemma leib_cong1:
  assumes CC: "Φ ⊢ C ❙≐⇘α❙⇒β⇙ C'" and fp: "freep Φ"
      and wC: "wff⇘α❙⇒β⇙(C)" and wC': "wff⇘α❙⇒β⇙(C')" and wa: "wff⇘α⇙(A)"
    shows "Φ ⊢ (C ❙⋅ A) ❙≐⇘β⇙ (C' ❙⋅ A)"
proof -
  have lcC: "lc C" using wC by (rule wff_lc)
  have lcA: "lc A" using wa by (rule wff_lc)
  let ?P = "❙Λ⇘α ❙⇒ β⇙ (C ❙⋅ A ❙≐⇘β⇙ (Bnd 0) ❙⋅ A)"   ― ‹‹λf. (C A) ❙≐ (f A)››
  have wP: "wff⇘(α❙⇒β)❙⇒𝗈⇙(?P)"
    by (auto simp: opn_lc[OF lcC] opn_lc[OF lcA]
             intro!: wff_AbsI wff_App wff_Fre wC wa wff_App[OF wC wa])
  have PbC: "?P ❙⋅ C ≈⇘𝗈⇙ (C ❙⋅ A ❙≐⇘β⇙ C ❙⋅ A)"
    using beq.beta[OF wP wC] by (simp add: opn_lc[OF lcC] opn_lc[OF lcA])
  have PbC': "?P ❙⋅ C' ≈⇘𝗈⇙ (C ❙⋅ A ❙≐⇘β⇙ C' ❙⋅ A)"
    using beq.beta[OF wP wC'] by (simp add: opn_lc[OF lcC] opn_lc[OF lcA])
  have "Φ ⊢ C ❙⋅ A ❙≐⇘β⇙ C ❙⋅ A"
    using fp wff_App[OF wC wa] by (rule leib_refl)
  hence "Φ ⊢ ?P ❙⋅ C" by (rule bprov.Beta[OF beq.sym[OF PbC]])
  hence "Φ ⊢ ?P ❙⋅ C'" using leib_subst[OF CC fp wC wC' wP] by auto
  thus ?thesis by (rule bprov.Beta[OF PbC'])
qed

subsubsection ‹Deductive closure of the Hintikka set›

text ‹Since ‹Hset› is maximal and each of its finite subsets is consistent, every sentence
    provable from a finite subset already belongs to ‹Hset› (deductive closure --- a consequence
    of the maximality of the extension, BKK Lemma 6.32).›

lemma Hset_deduct: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes conΦ: "con Φ" and fpΦ: "freep Φ"
      and finF: "finite F" and subF: "F ⊆ Hset Φ" and FS: "F ⊢ S"
      and cS: "cwff 𝗈 S" shows "S ∈ Hset Φ"
proof (rule ccontr)
  assume "S ∉ Hset Φ"
  hence negS: "❙¬ S ∈ Hset Φ" using Hset_maximal[OF cS] by blast
  have fin': "finite (insert (❙¬ S) F)" using finF by simp
  have sub': "insert (❙¬ S) F ⊆ Hset Φ" using negS subF by auto
  have "insert (❙¬ S) F ⊢ ❙⊥"
    by (meson FS Hyp NegE bprov_weaken fin' freep_finite insertCI subset_insertI wff_FalseB)
  moreover have "con (insert (❙¬ S) F)"
      by (rule Hset_finite_con[OF conΦ fpΦ fin' sub'])
  ultimately show False by (simp add: con_def)
qed

text ‹In particular, Leibniz equality is reflexive on ‹Hset› --- BKK's property ‹∇⇩r›
  for saturated Hintikka sets (Lemma 6.25; Lemma 6.23 gives the negative form
  ‹⇩~∇⇩=⇩r›); symmetry, transitivity and congruence follow below.›

lemma Hset_leib_refl: fixes Φ :: "'p::{countable,infinite} tm set" 
  assumes conΦ: "con Φ" and fpΦ: "freep Φ" and ca: "cwff α A"
  shows "(A ❙≐⇘α⇙ A) ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ, of "{}"])
  note wa = cwff_wff[OF ca] and cA = cwff_closed[OF ca]
  show "finite {}" by simp
  show "{} ⊆ Hset Φ" by simp
  show "{} ⊢ A ❙≐⇘α⇙ A"
    by (rule leib_refl[OF freep_finite[OF finite.emptyI] wa])
  show "cwff 𝗈 (A ❙≐⇘α⇙ A)"
    by (rule cwffI[OF wff_LeibE[OF wa wa]]) (simp add: Leib_def cA)
qed
lemma Hset_leib_sym: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes conΦ: "con Φ" and fpΦ: "freep Φ"
    and ca: "cwff α A" and cb: "cwff α B" and AB: "(A ❙≐⇘α⇙ B) ∈ Hset Φ"
  shows "(B ❙≐⇘α⇙ A) ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ])
  note wa = cwff_wff[OF ca] and cA = cwff_closed[OF ca] and
       wb = cwff_wff[OF cb] and cB = cwff_closed[OF cb]
  show "finite {A ❙≐⇘α⇙ B}" by simp
  show "{A ❙≐⇘α⇙ B} ⊆ Hset Φ" using AB by simp
  show "{A ❙≐⇘α⇙ B} ⊢ B ❙≐⇘α⇙ A"
    by (simp add: Hyp freep_finite leib_sym wa wb)
  show "cwff 𝗈 (B ❙≐⇘α⇙ A)"
    by (rule cwffI[OF wff_LeibE[OF wb wa]]) (simp add: Leib_def cA cB)
qed
lemma Hset_leib_trans: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes conΦ: "con Φ" and fpΦ: "freep Φ"
  and ca: "cwff α A" and wb: "wff⇘α⇙(B)" and cc: "cwff α C"
  and AB: "(A ❙≐⇘α⇙ B) ∈ Hset Φ" and BC: "(B ❙≐⇘α⇙ C) ∈ Hset Φ"
  shows "(A ❙≐⇘α⇙ C) ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ])
  note wa = cwff_wff[OF ca] and cA = cwff_closed[OF ca] and
       wc = cwff_wff[OF cc] and cC = cwff_closed[OF cc]
  let ?F = "{A ❙≐⇘α⇙ B, B ❙≐⇘α⇙ C}"
  show "finite ?F" by simp
  show "?F ⊆ Hset Φ" using AB BC by simp
  show "?F ⊢ A ❙≐⇘α⇙ C"
    by (meson Hyp ‹finite {A ❙≐⇘α⇙ B, B ❙≐⇘α⇙ C}› freep_finite insertCI
        leib_trans wa wb wc)
  show "cwff 𝗈 (A ❙≐⇘α⇙ C)"
    by (rule cwffI[OF wff_LeibE[OF wa wc]]) (simp add: Leib_def cA cC)
qed
lemma Hset_leib_cong: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes conΦ: "con Φ" and fpΦ: "freep Φ"
      and cc: "cwff (α❙⇒β) C" and cc': "cwff (α❙⇒β) C'" and ca: "cwff α A"
      and ca': "cwff α A'"
      and CC: "(C ❙≐⇘α❙⇒β⇙ C') ∈ Hset Φ" and AA: "(A ❙≐⇘α⇙ A') ∈ Hset Φ"
    shows "((C ❙⋅ A) ❙≐⇘β⇙ (C' ❙⋅ A')) ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ])
  note wC = cwff_wff[OF cc] and cC = cwff_closed[OF cc] and
       wC' = cwff_wff[OF cc'] and cC' = cwff_closed[OF cc'] and
       wA = cwff_wff[OF ca] and cA = cwff_closed[OF ca] and
       wA' = cwff_wff[OF ca'] and cA' = cwff_closed[OF ca']
  let ?F = "{C ❙≐⇘α❙⇒β⇙ C', A ❙≐⇘α⇙ A'}"
  have fp: "freep ?F" using freep_finite[of ?F] by simp
  show "finite ?F" by simp
  show "?F ⊆ Hset Φ" using CC AA by simp
  show "?F ⊢ (C ❙⋅ A) ❙≐⇘β⇙ (C' ❙⋅ A')"
    by (meson Hyp fp insertCI leib_cong1 leib_cong2 leib_trans wA wA' wC wC' 
              wff_App[OF wC' wA] wff_App[OF wC' wA'] wff_App[OF wC wA])
  show "cwff 𝗈 ((C ❙⋅ A) ❙≐⇘β⇙ (C' ❙⋅ A'))"
    by (rule cwffI[OF wff_LeibE[OF wff_App[OF wC wA] wff_App[OF wC' wA']]])
       (simp add: Leib_def cC cA cC' cA')
qed

text ‹Leibniz-equal propositions have the same truth (membership transfers along ‹∼› at type ‹𝗈›);
proved by Leibniz substitution with the identity predicate.›

lemma Hset_leib_mp: fixes Φ :: "'p::{countable,infinite} tm set"
  assumes conΦ: "con Φ" and fpΦ: "freep Φ"
      and ca: "cwff 𝗈 A" and cb: "cwff 𝗈 B" and AB: "(A ❙≐⇘𝗈⇙ B) ∈ Hset Φ"
      and A: "A ∈ Hset Φ"
    shows "B ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ _ _ _ cb])
  note wA = cwff_wff[OF ca] and cA = cwff_closed[OF ca] and
       wB = cwff_wff[OF cb] and cB = cwff_closed[OF cb]
  let ?F = "{A ❙≐⇘𝗈⇙ B, A}"
  let ?P = "❙Λ⇘𝗈⇙ (Bnd 0)"   ― ‹the identity predicate›
  have wP: "wff⇘𝗈❙⇒𝗈⇙(?P)" by (rule wff_AbsI) (simp add: wff_Fre)
  have fp: "freep ?F" using freep_finite[of ?F] by simp
  have PA: "?P ❙⋅ A ≈⇘𝗈⇙ A" using beq.beta[OF wP wA] by simp
  have PB: "?P ❙⋅ B ≈⇘𝗈⇙ B" using beq.beta[OF wP wB] by simp
  show "finite ?F" by simp
  show "?F ⊆ Hset Φ" using AB A by simp
  have s1: "?F ⊢ A ❙≐⇘𝗈⇙ B" by (auto intro: bprov.Hyp)
  have s2: "?F ⊢ ?P ❙⋅ A"
    by (rule bprov.Beta[OF beq.sym[OF PA]]) (auto intro: bprov.Hyp)
  have "?F ⊢ ?P ❙⋅ B" by (rule leib_subst[OF s1 fp wA wB wP s2])
  thus "?F ⊢ B" by (rule bprov.Beta[OF PB])
qed

subsection ‹The term model (BKK Section 6, the Hintikka lemma)›

text ‹Fix a consistent, parameter-rich set ‹Φ›; its Hintikka extension ‹H› is maximal, consistent
  and saturated.  The @{emph ‹term model›} has as its domain the closed well-formed terms quotiented
  by provable Leibniz equality ‹A ∼ B ≡ (A ❙≐ B) ∈ H›; this quotient is what forces property q.›

locale hintikka_model = fixes Φ :: "'p::{countable,infinite} tm set"
  assumes conΦ: "con Φ" and fpΦ: "freep Φ"
begin

text ‹The ‹∼›-equivalence classes of closed well-formed terms (@{const cwff} from
  Section 2): ‹A ∼ B ≡ (A ❙≐⇘σ⇙ B) ∈ H› --- the Leibniz quotient of BKK's model-existence proof
  (BKK Theorem 6.33); the ‹⇩~∇›-properties of Leibniz equality in ‹H› are BKK Lemma 6.23.›

definition cls :: "'p tm ⇒ 'p tm set" where
  "cls A ≡ {B. ∃σ. cwff σ A ∧ cwff σ B ∧ (A ❙≐⇘σ⇙ B) ∈ Hset Φ}"
lemma cls_self: "cwff σ A ⟹ A ∈ cls A"
  using Hset_leib_refl[OF conΦ fpΦ] by (auto simp: cls_def cwff_def)
lemma leib_sym':
  "cwff σ A ⟹ cwff σ B ⟹ (A ❙≐⇘σ⇙ B) ∈ Hset Φ ⟹ (B ❙≐⇘σ⇙ A) ∈ Hset Φ" 
  using Hset_leib_sym[OF conΦ fpΦ] by (auto simp: cwff_def)
lemma leib_trans':
  "cwff σ A ⟹ cwff σ B ⟹ cwff σ C ⟹ (A ❙≐⇘σ⇙ B) ∈ Hset Φ
    ⟹ (B ❙≐⇘σ⇙ C) ∈ Hset Φ ⟹ (A ❙≐⇘σ⇙ C) ∈ Hset Φ"
  using Hset_leib_trans[OF conΦ fpΦ] by (auto simp: cwff_def)

text ‹The quotient is faithful: two classes coincide exactly when the terms are Leibniz-equal in
  ‹H›.  This is what will give property q in the model.›

lemma cls_eq_iff:
  assumes wA: "cwff σ A" and wB: "cwff σ B"
    shows "(cls A = cls B) ⟷ (A ❙≐⇘σ⇙ B) ∈ Hset Φ" 
  by (smt (verit, best) Collect_cong cls_def cls_self cwff_unique
      leib_sym' leib_trans' mem_Collect_eq wA wB)

lemma cls_rep:
  assumes "cwff σ A"
  shows "cwff σ (SOME B. B ∈ cls A) ∧ (A ❙≐⇘σ⇙ (SOME B. B ∈ cls A)) ∈ Hset Φ"
proof -
  have "(SOME B. B ∈ cls A) ∈ cls A" using cls_self[OF assms]
    by (metis someI)
  then obtain τ where t: "cwff τ A" "cwff τ (SOME B. B ∈ cls A)"
    "(A ❙≐⇘τ⇙ (SOME B. B ∈ cls A)) ∈ Hset Φ" by (auto simp: cls_def)
  have "τ = σ" using cwff_unique[OF t(1) assms].
  thus ?thesis using t(2,3) by simp
qed

text ‹The applicative structure of the term model (BKK Definition 3.1): the domain of type ‹σ›
  consists of the classes of closed terms of type ‹σ›, and application is term application.›

definition Dm :: "ty ⇒ 'p tm set ⇒ bool" where "Dm σ X ≡ ∃A. cwff σ A ∧ X = cls A"
definition Ap :: "'p tm set ⇒ 'p tm set ⇒ 'p tm set" where
  "Ap X Y ≡ cls ((SOME A. A ∈ X) ❙⋅ (SOME B. B ∈ Y))"
lemma Ap_cls:
  assumes wA: "cwff (α ❙⇒ β) A" and wB: "cwff α B"
    shows "Ap (cls A) (cls B) = cls (A ❙⋅ B)"
proof -
  have a: "cwff (α ❙⇒ β) (SOME A'. A' ∈ cls A)" "(A ❙≐⇘α❙⇒β⇙ (SOME A'. A' ∈ cls A)) ∈ Hset Φ" 
    using cls_rep[OF wA] by auto
  have b: "cwff α (SOME B'. B' ∈ cls B)" "(B ❙≐⇘α⇙ (SOME B'. B' ∈ cls B)) ∈ Hset Φ"
    using cls_rep[OF wB] by auto
  have wAB: "cwff β (A ❙⋅ B)" using wA wB
    by (auto simp: cwff_def intro: wff_App)
  have "((A ❙⋅ B) ❙≐⇘β⇙ ((SOME A'. A' ∈ cls A) ❙⋅ (SOME B'. B' ∈ cls B))) ∈ Hset Φ"
    using Hset_leib_cong[OF conΦ fpΦ] wA a(1) wB b(1) a(2) b(2) by (auto simp: cwff_def)
  moreover have "cwff β ((SOME A'. A' ∈ cls A) ❙⋅ (SOME B'. B' ∈ cls B))" 
    using a(1) b(1) cwff_App by blast 
  ultimately have "cls (A ❙⋅ B) = cls ((SOME A'. A' ∈ cls A) ❙⋅ (SOME B'. B' ∈ cls B))"
    using cls_eq_iff wAB by blast
  thus ?thesis by (simp add: Ap_def)
qed
lemma Dm_cls: "cwff σ A ⟹ Dm σ (cls A)" by (auto simp: Dm_def)
lemma Ap_dom: "Dm (α ❙⇒ β) X ⟹ Dm α Y ⟹ Dm β (Ap X Y)" 
  by (auto simp: Dm_def Ap_cls cwff_def intro: wff_App)

text ‹Truth and falsity behave (the analogue of BKK Lemma 3.43 / property b): ‹❙⊤ ∈ H›, ‹❙⊥ ∉ H›,
  so ‹cls ❙⊤ ≠ cls ❙⊥›.›

lemma Hset_TrueB: "❙⊤ ∈ Hset Φ"
  using Hset_deduct bprov_TrueB conΦ cwff_TrueB fpΦ by blast 
lemma Hset_not_FalseB: "❙⊥ ∉ Hset Φ"
  by (metis hintikka_model_axioms Hyp con_def con_Hset hintikka_model_def)
lemma TF: "cls ❙⊤ ≠ cls ❙⊥"
  using Hset_TrueB Hset_leib_mp Hset_not_FalseB cls_eq_iff conΦ
        cwff_FalseB cwff_TrueB fpΦ by blast

subsubsection ‹Satisfaction bridges: membership in ‹H› as truth
  (BKK Lemma 6.21, Lemmas 6.25--6.26)›

text ‹‹H› never contains both ‹φ› and ‹❙¬φ› (BKK's property ‹⇩~∇⇩c›, Definition 6.19,
  here for arbitrary sentences via Lemma 6.10).›

lemma Hset_notboth: "wff⇘𝗈⇙(φ) ⟹ φ ∈ Hset Φ ⟹ ❙¬ φ ∉ Hset Φ"
    using conΦ con_Hset con_not_both fpΦ by auto

text ‹Boolean extensionality inside ‹H› (via the rule ‹NK(b)›; the saturated-sets lemma for
  property b, BKK Lemma 6.26): a member of ‹H› is Leibniz-equal to ‹❙⊤›, a non-member
  to ‹❙⊥›.›

lemma Hset_eq_TrueB:
  assumes p: "φ ∈ Hset Φ" and w: "cwff 𝗈 φ"
  shows "(φ ❙≐⇘𝗈⇙ ❙⊤) ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ, of "{φ}"])
  show "finite {φ}" by simp
  show "{φ} ⊆ Hset Φ" using p by simp
  show "{φ} ⊢ φ ❙≐⇘𝗈⇙ ❙⊤"
    by (metis BoolE Hyp bprov_TrueB cwff_def insertCI insert_is_Un w wff_TrueB)
  show "cwff 𝗈 (φ ❙≐⇘𝗈⇙ ❙⊤)"
    by (metis cwff_App cwff_TrueB cwff_def fvs_defs(5) w wff_Leib)   
qed

lemma Hset_eq_FalseB: assumes np: "❙¬ φ ∈ Hset Φ" and w: "cwff 𝗈 φ"
  shows "(φ ❙≐⇘𝗈⇙ ❙⊥) ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ, of "{❙¬ φ}"])
  show "finite {❙¬ φ}" by simp
  show "{❙¬ φ} ⊆ Hset Φ" using np by simp
  show "{❙¬ φ} ⊢ φ ❙≐⇘𝗈⇙ ❙⊥" 
    by (metis BoolE Hyp NegE TrueB_def Un_empty_right
        Un_insert_right bprov_TrueB cwff_wff insertCI w wff_FalseB)
  show "cwff 𝗈 (φ ❙≐⇘𝗈⇙ ❙⊥)" 
    by (metis w cwff_def cwff_FalseB cwff_App wff_Leib fvs_defs(5)) 
qed

text ‹Sentences with the same truth value in ‹H› are Leibniz-equal in ‹H› (the general form
  of the ‹NK(b)› bridge, cf.\ BKK Lemma 6.26).›

lemma Hset_iff_eq:
  assumes wp: "cwff 𝗈 φ" and wq: "cwff 𝗈 ψ"
      and iff: "φ ∈ Hset Φ ⟷ ψ ∈ Hset Φ" 
  shows "(φ ❙≐⇘𝗈⇙ ψ) ∈ Hset Φ" 
  by (metis Hset_eq_FalseB Hset_eq_TrueB Hset_maximal cls_eq_iff
      cwff_FalseB cwff_TrueB iff wp wq)

text ‹THE satisfaction bridge: a sentence's class is the class of ‹❙⊤› exactly when it is
  in ‹H› (the ‹υ›-valuation of the term model in the proof of BKK Theorem 6.33).›

lemma cls_TrueB_iff: "cwff 𝗈 φ ⟹ cls φ = cls ❙⊤ ⟷ φ ∈ Hset Φ" 
  by (metis Hset_eq_FalseB Hset_eq_TrueB Hset_maximal TF cls_eq_iff cwff_FalseB cwff_TrueB)

text ‹Property b at the class level: the boolean domain has exactly the classes of ‹❙⊤›
  and ‹❙⊥› (BKK Definition 3.46).›

lemma cls_bool: "cwff 𝗈 φ ⟹ cls φ = cls ❙⊤ ∨ cls φ = cls ❙⊥" 
  by (metis TF cls_eq_iff cwff_FalseB cls_TrueB_iff Hset_iff_eq)
lemma cls_FalseB_iff: "cwff 𝗈 φ ⟹ cls φ = cls ❙⊥ ⟷ φ ∉ Hset Φ" 
  by (metis cls_eq_iff cwff_FalseB TF Hset_iff_eq cls_TrueB_iff)

subsubsection ‹The evaluation and logical conditions of the term model›

text ‹The ‹β›-condition (BKK Definition 3.18(4)) inside ‹H›: a ‹β›-redex is Leibniz-equal to
  its reduct, via the rule ‹NK(β)› applied to reflexivity.›

lemma Hset_beta:
  assumes wAbs: "cwff (σ❙⇒τ) (❙Λ⇘σ⇙ b)" and wa: "cwff σ a"
    shows "((❙Λ⇘σ⇙ b) ❙⋅ a ❙≐⇘τ⇙ b❙⟨a❙⟩) ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ, of "{}"])
  let ?A = "(❙Λ⇘σ⇙ b) ❙⋅ a"  let ?B = "b❙⟨a❙⟩"
  have wA: "wff⇘τ⇙(?A)"
    using cwff_wff[OF wAbs] cwff_wff[OF wa] by (auto intro: wff_App)
  have step: "(?B ❙≐⇘τ⇙ ?B) ≈⇘𝗈⇙ (?A ❙≐⇘τ⇙ ?B)" 
    by (meson appL appR beq.sym beta cwff_wff wAbs wa wff_Leib wff_opn)
  show "{} ⊢ ?A ❙≐⇘τ⇙ ?B"
    by (meson Beta cwff_def finite.emptyI freep_finite leib_refl local.step wAbs wa wff_opn) 
  show "finite {}" by simp
  show "{} ⊆ Hset Φ" by simp
  show "cwff 𝗈 (?A ❙≐⇘τ⇙ ?B)"
    by (meson cwff_App cwff_def cwff_opn fvs_defs(5) wAbs wa wff_Leib)
qed

text ‹The ‹L⇘¬⇙› condition (BKK Figure 2) at the class level, from maximality
  and consistency of ‹H›.›

lemma cls_neg: "cwff 𝗈 φ ⟹ cls (❙¬ φ) = (if cls φ = cls ❙⊤ then cls ❙⊥ else cls ❙⊤)"
  by (meson Hset_maximal Hset_notboth cwff_App cwff_Neg cwff_def
            cls_FalseB_iff cls_TrueB_iff)

text ‹The ‹L⇘∨⇙› condition: ‹H› treats disjunction disjunctively (BKK ‹∇⇩∨›, Definition 6.19).›

lemma Hset_dis_iff:
  assumes wp: "cwff 𝗈 φ" and wq: "cwff 𝗈 ψ"
    shows "φ ❙∨ ψ ∈ Hset Φ ⟷ φ ∈ Hset Φ ∨ ψ ∈ Hset Φ" 
proof
  assume d: "φ ❙∨ ψ ∈ Hset Φ"
  show "φ ∈ Hset Φ ∨ ψ ∈ Hset Φ"
  proof (rule ccontr)
    assume "¬ (φ ∈ Hset Φ ∨ ψ ∈ Hset Φ)"
    hence np: "❙¬ φ ∈ Hset Φ" and nq: "❙¬ ψ ∈ Hset Φ"
        using Hset_maximal[OF wp] Hset_maximal[OF wq] by blast+
    let ?F = "{φ ❙∨ ψ, ❙¬ φ, ❙¬ ψ}"
    have "?F ⊢ φ ❙∨ ψ" by (auto intro: bprov.Hyp)
    moreover have "?F ∪ {φ} ⊢ ❙⊥"
      by (metis Hyp NegE insertCI insert_is_Un sup.commute wff_FalseB)   
    moreover have "?F ∪ {ψ} ⊢ ❙⊥"
      by (metis Hyp NegE Un_insert_right insertCI insert_subset sup_ge1 wff_FalseB)
    ultimately have "?F ⊢ ❙⊥"
      using cwff_wff[OF wp] cwff_wff[OF wq] by (metis bprov.DisE)
    moreover have "con ?F"
      by (meson Hset_finite_con conΦ d empty_subsetI finite.emptyI finite.insertI
                fpΦ insert_subsetI np nq)
    ultimately show False by (simp add: con_def)
  qed
next
  show "φ ∈ Hset Φ ∨ ψ ∈ Hset Φ ⟹ φ ❙∨ ψ ∈ Hset Φ" 
    by (meson DisIL DisIR Hset_deduct Hyp bprov_finite conΦ cwff_App
        cwff_Dis cwff_def fpΦ wp wq)
qed

lemma cls_dis:
  assumes wp: "cwff 𝗈 φ" and wq: "cwff 𝗈 ψ"
  shows "cls (φ ❙∨ ψ) = (if cls φ = cls ❙⊤ ∨ cls ψ = cls ❙⊤ then cls ❙⊤ else cls ❙⊥)"
proof -
  have wd: "cwff 𝗈 (φ ❙∨ ψ)" using wp wq by (auto simp: cwff_def)
  show ?thesis by (simp add: Hset_dis_iff cls_FalseB_iff cls_TrueB_iff wd wp wq)
qed

text ‹The ‹L⇧σ⇘∀⇙› condition: ‹H› treats the quantifier universally --- ‹NK(ΠE)› gives one
  direction, the witness property ‹⇩~∇⇩∃› (BKK Definition 6.19) together with maximality the
  other.›

lemma Hset_pi_iff:
  assumes wf: "cwff (σ❙⇒𝗈) f"
    shows "(Pi σ) ❙⋅ f ∈ Hset Φ ⟷ (∀a. cwff σ a ⟶ f ❙⋅ a ∈ Hset Φ)"
proof
  assume pf: "(Pi σ) ❙⋅ f ∈ Hset Φ"
  have step: "f ❙⋅ a ∈ Hset Φ" if wa: "cwff σ a" for a
    by (meson Hset_maximal Hyp NegE PiE conΦ con_Hset con_def
              cwff_App cwff_def fpΦ local.wf pf wa wff_FalseB)
  thus "∀a. cwff σ a ⟶ f ❙⋅ a ∈ Hset Φ" by blast
next
  assume all: "∀a. cwff σ a ⟶ f ❙⋅ a ∈ Hset Φ"
  show "(Pi σ) ❙⋅ f ∈ Hset Φ"
  proof (rule ccontr)
    assume npf: "(Pi σ) ❙⋅ f ∉ Hset Φ"
    have wPf: "wff⇘𝗈⇙((Pi σ) ❙⋅ f)"
      using cwff_wff[OF wf] by (auto intro: wff_App wff_Pi)
    have cPf: "fvs ((Pi σ) ❙⋅ f) = {}"
      using cwff_closed[OF wf] by simp
    have n: "❙¬ ((Pi σ) ❙⋅ f) ∈ Hset Φ"
        using Hset_maximal[OF cwffI[OF wPf cPf]] npf by blast
    have wn: "wff⇘𝗈⇙(❙¬ ((Pi σ) ❙⋅ f))" using wPf by (rule wff_Not)
    have cn: "fvs (❙¬ ((Pi σ) ❙⋅ f)) = {}" using cPf by simp
    obtain c where nc: "❙¬ (f ❙⋅ (c⇧p⇘σ⇙)) ∈ Hset Φ"
      using Hset_saturated[OF conΦ fpΦ cwffI[OF wn cn] n] by blast
    have inc: "f ❙⋅ (c⇧p⇘σ⇙) ∈ Hset Φ"
      using all[rule_format, of "c⇧p⇘σ⇙"] cwff_Par[of σ c] by simp
    show False
      using Hset_notboth[OF wff_App[OF cwff_wff[OF wf] wff_Par] inc] nc by simp
  qed
qed

lemma cls_pi:
  assumes wf: "cwff (σ❙⇒𝗈) f"
  shows "cls ((Pi σ) ❙⋅ f) = (if (∀a. cwff σ a ⟶ Ap (cls f) (cls a) = cls ❙⊤)
                             then cls ❙⊤ else cls ❙⊥)"
proof -
  have wPf: "cwff 𝗈 ((Pi σ) ❙⋅ f)"
    using wf by (auto simp: cwff_def intro: wff_App wff_Pi)
  have e: "(Ap (cls f) (cls a) = cls ❙⊤) = (f ❙⋅ a ∈ Hset Φ)" if a: "cwff σ a" for a
    using Ap_cls[OF wf a] cls_TrueB_iff[OF cwff_App[OF wf a]] by simp
  have inner: "(∀a. cwff σ a ⟶ Ap (cls f) (cls a) = cls ❙⊤)
      = (∀a. cwff σ a ⟶ App f a ∈ Hset Φ)" using e by blast
  show ?thesis
    using cls_TrueB_iff[OF wPf] cls_FalseB_iff[OF wPf] Hset_pi_iff[OF wf] inner
    by (cases "∀a. cwff σ a ⟶ f ❙⋅ a ∈ Hset Φ") auto
qed

text ‹The ‹β›-condition transfers membership: a redex of type ‹𝗈› is in ‹H› exactly when its
  reduct is (via the Leibniz bridge).›

lemma Hset_beta_iff:
  assumes "cwff (σ❙⇒𝗈) (❙Λ⇘σ⇙ b)" and "cwff σ a"
  shows "(❙Λ⇘σ⇙ b) ❙⋅ a ∈ Hset Φ ⟷ b❙⟨a❙⟩ ∈ Hset Φ"
  by (meson Hset_beta Hset_leib_mp Hset_leib_sym conΦ cwff_App cwff_opn fpΦ assms)

text ‹Type uniqueness of the classes (BKK: the domains are disjoint by type).›

lemma cls_type:
  "cwff σ s ⟹ cwff τ t ⟹ cls s = cls t ⟹ σ = τ" 
  by (smt (verit, ccfv_SIG) cls_def cls_self cwff_unique mem_Collect_eq)

text ‹Property q (BKK Definition 3.46): the Leibniz combinator itself is the identity
  relation of the term model, by @{thm cls_eq_iff}.›

lemma cwff_Leib: "cwff (σ❙⇒σ❙⇒𝗈) (Leib σ)" by (simp add: cwff_def)

text ‹Property f (functionality, BKK Definition 3.46) via the rule ‹NK(f)›: two functions
  that agree on every class are Leibniz-equal in ‹H›.  Saturation enters through
  @{thm Hset_pi_iff} to establish the ‹Π›-premise of ‹NK(f)›.›

lemma cls_ext:
  assumes wg: "cwff (σ❙⇒τ) g" and wh: "cwff (σ❙⇒τ) h"
      and ag: "⋀a. cwff σ a ⟹ Ap (cls g) (cls a) = Ap (cls h) (cls a)"
    shows "cls g = cls h"
proof -
  have lcg: "lc g" and lch: "lc h" using wg wh
    by (auto intro: cwff_lc)
  let ?body = "g ❙⋅ (Bnd 0) ❙≐⇘τ⇙ h ❙⋅ (Bnd 0)"
  have opnb: "?body❙⟨u❙⟩ = (g ❙⋅ u ❙≐⇘τ⇙ h ❙⋅ u)" for u using lcg lch
    by simp
  ― ‹the abstracted body is a closed well-formed predicate›
  have wB: "cwff (σ❙⇒𝗈) (❙Λ⇘σ⇙ ?body)"
  proof -
    have "wff⇘𝗈⇙(?body❙⟨x⇧f⇘σ⇙❙⟩)" for x unfolding opnb
      using cwff_wff[OF wg] cwff_wff[OF wh]
      by (auto intro: wff_App wff_Fre)
    hence "wff⇘σ❙⇒𝗈⇙(❙Λ⇘σ⇙ ?body)" by (rule wff_AbsI)
    moreover have "fvs (❙Λ⇘σ⇙ ?body) = {}"
      using cwff_closed[OF wg] cwff_closed[OF wh]
      by (simp add: Leib_def)
    ultimately show ?thesis by (simp add: cwff_def)
  qed
  ― ‹pointwise agreement puts every instance of the body in ‹H››
  have inst: "(❙Λ⇘σ⇙ ?body) ❙⋅ a ∈ Hset Φ" if a: "cwff σ a" for a
    by (smt (verit, ccfv_threshold) Ap_cls Hset_beta_iff ag
        cls_eq_iff cwff_App opnb that wB wg wh)
  ― ‹hence the ‹Π›-sentence is in ‹H›, and ‹NK(f)› yields the equation›
  have PiH: "(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body) ∈ Hset Φ"
      using Hset_pi_iff[OF wB] inst by blast
  have "(g ❙≐⇘σ❙⇒τ⇙ h) ∈ Hset Φ"
  proof (rule Hset_deduct[OF conΦ fpΦ, of "{(Pi σ) ❙⋅ (❙Λ⇘σ⇙
      ?body)}"])
    show "finite {(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body)}" by simp
    show "{(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body)} ⊆ Hset Φ" using PiH by simp
    have "{(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body)} ⊢ ❙Π⇘σ⇙ ?body"
      by (auto intro: bprov.Hyp simp: Forall_def)
    thus "{(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body)} ⊢ g ❙≐⇘σ❙⇒τ⇙ h"
      using FuncE cwff_wff wg wh by blast
    show "cwff 𝗈 (g ❙≐⇘σ❙⇒τ⇙ h)" by (metis cwff_App wg wh cwff_Leib)
 qed
  thus ?thesis using cls_eq_iff[OF wg wh] by simp
qed

text ‹The description condition of the term model (beyond BKK; cf.\ Andrews 1972): a class
that provably behaves as the singleton of ‹a› is mapped by ‹Iota σ› to the class of ‹a›.
Functional extensionality ‹NK(f)› reduces the pointwise hypothesis to a Leibniz equation
with the literal singleton ‹(Leib σ) ❙⋅ a›, which the axiom ‹NK(ι)› describes.›

lemma cls_desc:
  assumes wf: "cwff (σ❙⇒𝗈) f" and wa: "cwff σ a"
      and sing: "⋀b. cwff σ b ⟹ (Ap (cls f) (cls b) = cls ❙⊤) = (cls b = cls a)"
    shows "cls ((Iota σ) ❙⋅ f) = cls a"
proof -
  have lcf: "lc f" and lca: "lc a" using wf wa
    by (auto intro: cwff_lc)
  let ?body = "f ❙⋅ (Bnd 0) ❙≐⇘𝗈⇙ ((Leib σ) ❙⋅ a) ❙⋅ (Bnd 0)"
  have opnb: "?body❙⟨u❙⟩ = (f ❙⋅ u ❙≐⇘𝗈⇙ ((Leib σ) ❙⋅ a) ❙⋅ u)" for u
    using lcf lca by simp
  have wB: "cwff (σ❙⇒𝗈) (❙Λ⇘σ⇙ ?body)"
  proof -
    have "wff⇘𝗈⇙(?body❙⟨x⇧f⇘σ⇙❙⟩)" for x unfolding opnb
      using cwff_wff[OF wf] cwff_wff[OF wa]
      by (auto intro: wff_App wff_Fre)
    hence "wff⇘σ❙⇒𝗈⇙(❙Λ⇘σ⇙ ?body)" by (rule wff_AbsI)
    moreover have "fvs (❙Λ⇘σ⇙ ?body) = {}" using cwff_def local.wf wa
      by auto
    ultimately show ?thesis by (simp add: cwff_def)
  qed
  ― ‹the pointwise singleton facts land in ‹H››
  have inst: "(❙Λ⇘σ⇙ ?body) ❙⋅ b ∈ Hset Φ" if b: "cwff σ b" for b
    by (metis (no_types, opaque_lifting) Ap_cls Hset_beta_iff Hset_iff_eq cls_TrueB_iff
              cls_eq_iff cwff_App cwff_Leib local.wf opnb sing that wB wa)
  have PiH: "(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body) ∈ Hset Φ"
    using Hset_pi_iff[OF wB] inst by blast
  ― ‹‹NK(f)› reduces to the literal singleton, ‹NK(ι)› describes it›
  have "(((Iota σ) ❙⋅ f) ❙≐⇘σ⇙ a) ∈ Hset Φ"
  proof (rule Hset_deduct[OF conΦ fpΦ, of "{(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body)}"])
    show "finite {(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body)}" by simp
    show "{(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body)} ⊆ Hset Φ" using PiH by simp
    let ?F = "{(Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?body)}"
    have fpF: "freep ?F" by (rule freep_finite) simp
    have PiD: "?F ⊢ ❙Π⇘σ⇙ ?body"
      by (auto intro: bprov.Hyp simp: Forall_def)
    show "?F ⊢ (Iota σ) ❙⋅ f ❙≐⇘σ⇙ a"
      by (rule leib_trans[OF
        leib_cong2[OF bprov.FuncE[OF PiD cwff_wff[OF wf] 
                cwff_wff[OF cwff_App[OF cwff_Leib wa]]] fpF
                    cwff_wff[OF wf] cwff_wff[OF cwff_App[OF
                    cwff_Leib wa]] 
              wff_Iota] bprov.Desc[OF cwff_wff[OF wa]] fpF
                  wff_App[OF wff_Iota cwff_wff[OF wf]] 
            wff_App[OF wff_Iota cwff_wff[OF cwff_App[OF cwff_Leib
                wa]]] cwff_wff[OF wa]])
    show "cwff 𝗈 ((Iota σ) ❙⋅ f ❙≐⇘σ⇙ a)" 
      by (metis wa cwff_App local.wf cwff_Leib cwff_Iota)
  qed
  thus ?thesis
    using cls_eq_iff[OF cwff_App[OF cwff_Iota wf] wa] by simp
qed

text ‹Primitive equality in ‹H› (BKK Remark 7.9): reflexivity is ‹∇⇘=⇩r⇙› via ‹NK(=⇩r)›, and
primitive and Leibniz equality coincide in ‹H› --- ‹→› via ‹NK(=⇩l)› (‹∇⇘=⇩≐⇙›), ‹←› by
Leibniz substitution into ‹λx. a ❙=⇘σ⇙ x› from reflexivity.›

lemma Hset_peq_iff:
  assumes wa: "cwff σ a" and wb: "cwff σ b"
    shows "(a ❙=⇘σ⇙ b) ∈ Hset Φ ⟷ (a ❙≐⇘σ⇙ b) ∈ Hset Φ"
proof
  assume p: "(a ❙=⇘σ⇙ b) ∈ Hset Φ" show "(a ❙≐⇘σ⇙ b) ∈ Hset Φ"
  proof (rule Hset_deduct[OF conΦ fpΦ, of "{a ❙=⇘σ⇙ b}"])
    show "finite {a ❙=⇘σ⇙ b}" by simp
    show "{a ❙=⇘σ⇙ b} ⊆ Hset Φ" using p by simp
    show "{a ❙=⇘σ⇙ b} ⊢ a ❙≐⇘σ⇙ b"
      by (auto intro: bprov.EqL bprov.Hyp)
    show "cwff 𝗈 (a ❙≐⇘σ⇙ b)"
      using cwff_App cwff_Leib wa wb by blast
  qed
next
  assume l: "(a ❙≐⇘σ⇙ b) ∈ Hset Φ" show "(a ❙=⇘σ⇙ b) ∈ Hset Φ"
  proof (rule Hset_deduct[OF conΦ fpΦ, of "{a ❙≐⇘σ⇙ b}"])
    show "finite {a ❙≐⇘σ⇙ b}" by simp
    show "{a ❙≐⇘σ⇙ b} ⊆ Hset Φ" using l by simp
    let ?F = "{a ❙≐⇘σ⇙ b}"  let ?P = "❙Λ⇘σ⇙ (a ❙=⇘σ⇙ Bnd 0)"
    have lca: "lc a" using wa by (rule cwff_lc)
    have wP: "wff⇘σ❙⇒𝗈⇙(?P)"
      by (rule wff_AbsI)
         (auto simp: opn_lc[OF lca] intro: cwff_wff[OF wa] wff_Fre)
    have fpF: "freep ?F" by (rule freep_finite) simp
    have hyp: "?F ⊢ a ❙≐⇘σ⇙ b" by (auto intro: bprov.Hyp)
    have PA: "?P ❙⋅ a ≈⇘𝗈⇙ (a ❙=⇘σ⇙ a)"
      using beq.beta[OF wP cwff_wff[OF wa]] by (simp add: opn_lc[OF lca])
    have PB: "?P ❙⋅ b ≈⇘𝗈⇙ (a ❙=⇘σ⇙ b)"
      using beq.beta[OF wP cwff_wff[OF wb]] by (simp add: opn_lc[OF lca])
    have "?F ⊢ a ❙=⇘σ⇙ a" by (rule bprov.EqR[OF cwff_wff[OF wa]])
    hence "?F ⊢ ?P ❙⋅ a" by (rule bprov.Beta[OF beq.sym[OF PA]])
    hence "?F ⊢ ?P ❙⋅ b"
      by (rule leib_subst[OF hyp fpF cwff_wff[OF wa] cwff_wff[OF wb] wP])
    thus "?F ⊢ a ❙=⇘σ⇙ b" by (rule bprov.Beta[OF PB])
    show "cwff 𝗈 (a ❙=⇘σ⇙ b)"
      using cwff_wff[OF wa] cwff_wff[OF wb] cwff_closed[OF wa] cwff_closed[OF wb] 
      by (auto simp: cwff_def)
  qed
qed

end

subsubsection ‹Model existence (BKK Lemma 7.5 / Theorem 7.6)›

text ‹The Hintikka set induces a term evaluation: the class map ‹cls› together with the term-model
  domains and application satisfies every @{locale valuation} condition.  Via the bridge
  ‹valuation ⊆ bkk_model› of Section 2, every ‹NK›-consistent set of sentences therefore
  has a model in the class ‹ℳ⇘βfb⇙› --- BKK's model-existence theorem.›

sublocale hintikka_model ⊆ V: valuation Dm Ap cls
proof
  show "cwff (σ❙⇒τ) (❙Λ⇘σ⇙ b) ⟹ cwff σ a ⟹ Ap (cls (❙Λ⇘σ⇙ b)) (cls a) = cls (b❙⟨a❙⟩)"
    for σ τ b a by (metis (no_types, lifting) Ap_cls Hset_beta cls_eq_iff cwff_App cwff_opn)
  show "cwff (σ❙⇒τ) g ⟹ cwff (σ❙⇒τ) h ⟹ (⋀a. cwff σ a
      ⟹ Ap (cls g) (cls a) = Ap (cls h) (cls a)) ⟹ cls g = cls h"
    for σ τ g h by (rule cls_ext)
  show "cwff σ a ⟹ cwff σ b ⟹ (Ap (Ap (cls (Eq σ)) (cls a)) (cls b)
      = cls ❙⊤) = (cls a = cls b)" for σ a b
  proof -
    assume wa: "cwff σ a" and wb: "cwff σ b"
    have 2: "Ap (cls ((Eq σ) ❙⋅ a)) (cls b) = cls (a ❙=⇘σ⇙ b)"
      using Ap_cls[OF cwff_App[OF cwff_Eq wa] wb] by simp
    have wab: "cwff 𝗈 (a ❙=⇘σ⇙ b)"
      using cwff_App[OF cwff_App[OF cwff_Eq wa] wb] by simp
    show "(Ap (Ap (cls (Eq σ)) (cls a)) (cls b) = cls ❙⊤) = (cls a = cls b)"
      using Ap_cls[OF cwff_Eq wa] 2 cls_TrueB_iff[OF wab]
            Hset_peq_iff[OF wa wb] cls_eq_iff[OF wa wb] by simp
  qed
qed(auto simp: Ap_cls Dm_def cls_type TF cls_desc cls_pi cls_dis cls_neg cls_bool)

subsubsection ‹The truth lemma›

context hintikka_model
begin

text ‹THE TRUTH LEMMA (the satisfaction claim of BKK Theorem 6.33; the underlying Hintikka
  properties are BKK Lemma 6.21): under any domain-respecting assignment a
  sentence denotes its own class, and it denotes the truth value ‹cls ❙⊤› of the term model
  exactly when it belongs to ‹H›.›

theorem truth_lemma:
  "cwff 𝗈 φ ⟹ V.vresp ξ ⟹ V.Ev ξ φ = cls ❙⊤ ⟷ φ ∈ Hset Φ"
  using cls_TrueB_iff msub_closed cwff_closed V.Ev_def by metis

end

subsubsection ‹Completeness (BKK Corollary 7.7)›

text ‹‹NK⇩β⇩f⇩b› with ‹NK(ι)› is complete for the class ‹ℳ⇘βfb⇙› of ‹Σ›-models with
  description (the description-enriched ‹ℳ⇩β⇩f⇩b›, cf.\ Andrews 1972): a sentence that is
  valid in every such model of a sufficiently ‹Σ›-pure (‹freep›, BKK Definition 6.3) set of
  sentences ‹Φ› (it suffices to assume validity over the models carried by ‹'p tm set› --- in
  particular the term model) is derivable from ‹Φ›.  Unlike BKK, who allow signatures of any
  infinite cardinality ‹ℵ⇩s› (BKK Remark 3.16), we fix a countable type of parameter names
  (‹'p :: {countable, infinite}›); the enumeration of sentences in the extension lemma rests
  on it.  The proof
  is by contraposition, BKK's argument: if ‹Φ ⊢ A› fails then ‹Φ ∪ {❙¬A}› is ‹NK›-consistent
  (‹NK(Contr)›), extends to a maximal saturated set (BKK's abstract extension lemma 6.32),
      and its term model --- a general model by
  model existence --- satisfies ‹Φ› but refutes ‹A›, contradicting validity.›

lemma fp0: "freep ({} :: 'p::{countable,infinite} tm set)"
  by (rule freep_finite[OF finite.emptyI])

theorem completeness:
  fixes Φ :: "'p::{countable,infinite} tm set" and A :: "'p tm" 
  assumes c: "cwff 𝗈 A" and fp: "freep Φ"
      and valid: "⊨('p tm set) A"
      and sen: "⋀B. B ∈ Φ ⟹ cwff 𝗈 B" 
  shows "Φ ⊢ A"
proof (rule ccontr)
  assume nd: "¬ Φ ⊢ A"
  note wA = cwff_wff[OF c] and cA = cwff_closed[OF c]
  let ?Ψ = "insert (❙¬ A) Φ"
  have conΨ: "con ?Ψ" using bprov.simps con_def nd wA by fastforce
  have fpΨ: "freep ?Ψ" by (rule freep_add[OF fp])
  interpret H: hintikka_model ?Ψ by unfold_locales (rule conΨ fpΨ)+
  ― ‹a domain-respecting assignment for the term model›
  define ξ :: "nat ⇒ ty ⇒ 'p tm set" where
    "ξ ≡ λn τ. H.cls (undefined⇧p⇘τ⇙)"
  have r: "H.V.vresp ξ"
    by (auto simp: ξ_def H.V.vresp_def intro: H.Dm_cls cwff_Par)
  have ra: "app_struct.asg H.Dm ξ" using r
    by (simp add: H.V.bkkA.asg_def H.V.vresp_def)
  have bm: "bkk_model H.Dm H.Ap H.V.Ev (λa. a = H.cls ❙⊤)"
    by intro_locales
  ― ‹the term model satisfies ‹Φ› by the truth lemma›
  have sat: "∀B∈Φ. H.V.Ev ξ B = H.cls ❙⊤"
    using H.truth_lemma[OF _ r] sen Phi_sub_Hset[of ?Ψ]
    by (auto simp: cwff_def)
  ― ‹validity at the term model forces ‹A ∈ H››
  have "H.V.Ev ξ A = H.cls ❙⊤"
    using valid unfolding bkk_valid_def rel_truth_def using bm ra sat by blast
  hence AH: "A ∈ Hset ?Ψ" using H.truth_lemma[OF _ r] wA cA
    by (simp add: cwff_def)
  ― ‹but ‹❙¬A ∈ Ψ ⊆ H› --- contradiction with consistency of ‹H››
  have "❙¬ A ∈ Hset ?Ψ" using Phi_sub_Hset[of ?Ψ] by auto
  thus False using H.Hset_notboth[OF wA AH] by simp
qed

text ‹Soundness (BKK Theorem 7.3) and completeness (BKK Corollary 7.7) are statements about the
  @{emph ‹same›} class of models, so together they characterise derivability semantically: a
  sentence is derivable from ‹Φ› exactly when it holds in every model of ‹Φ› in the class
  ‹ℳ⇘βfb⇙› over the term carrier.›

text ‹The semantic characterisation of derivability from the empty hypothesis set
  (BKK Corollary 7.7 at ‹Φ = {}›, combined with Theorem 7.3): a sentence is derivable
  iff it is valid in every ‹Σ›-model of the class ‹ℳ⇘βfb⇙› (over the carrier of the
  term model; the general hypothesis-set form is @{thm [source] completeness}).  The
  soundness direction is @{thm [source] soundness_bkk}; the completeness direction only
  shrinks the quantification to the canonical models via the sublocale bridge.›

theorem derivable_iff_valid:
  fixes A :: "'p::{countable,infinite} tm"
  assumes "cwff 𝗈 A"
  shows "⊢ A ⟷ ⊨('p tm set) A"
  by (metis (mono_tags, lifting) assms bkk_valid_def completeness empty_iff fp0
            rel_truth_def soundness_bkk)

subsubsection ‹Further derived Leibniz rules›

text ‹Leibniz modus ponens: transport a theorem along a proven Leibniz equation
  (via ‹NK(β)› and Leibniz substitution into the identity predicate).›

lemma leib_mp:
  assumes AB: "Φ ⊢ A ❙≐⇘𝗈⇙ B" and A: "Φ ⊢ A" and fp: "freep Φ"
      and wA: "wff⇘𝗈⇙(A)" and wB: "wff⇘𝗈⇙(B)"
    shows "Φ ⊢ B"
proof -
  let ?P = "❙Λ⇘𝗈⇙ (Bnd 0) :: 'p tm"
  have wP: "wff⇘𝗈❙⇒𝗈⇙(?P)" by (rule wff_AbsI) (simp add: wff_Fre)
  have bA: "?P ❙⋅ A ≈⇘𝗈⇙ A" using beq.beta[OF wP wA] by simp
  have bB: "?P ❙⋅ B ≈⇘𝗈⇙ B" using beq.beta[OF wP wB] by simp
  have "Φ ⊢ ?P ❙⋅ A" by (rule bprov.Beta[OF beq.sym[OF bA] A])
  hence "Φ ⊢ ?P ❙⋅ B" by (rule leib_subst[OF AB fp wA wB wP])
  thus ?thesis by (rule bprov.Beta[OF bB])
qed

text ‹From Leibniz to primitive equality (BKK Remark 7.9; by Leibniz substitution
  into ‹❙Λx. A ❙=⇘α⇙ x› from ‹NK(=⇩r)›-reflexivity; the converse is the rule ‹NK(=⇩l)›).›

lemma leib_to_peq:
  assumes AB: "Φ ⊢ A ❙≐⇘α⇙ B" and fp: "freep Φ"
      and wA: "wff⇘α⇙(A)" and wB: "wff⇘α⇙(B)"
    shows "Φ ⊢ A ❙=⇘α⇙ B"
proof -
  let ?P = "❙Λ⇘α⇙ (A ❙=⇘α⇙ Bnd 0)"
  have wP: "wff⇘α ❙⇒ 𝗈⇙(?P)"
    by (rule wff_AbsI) (auto simp: opn_lc[OF wff_lc[OF wA]] intro!:  wA wff_Fre)
  have bA: "?P ❙⋅ A ≈⇘𝗈⇙ (A ❙=⇘α⇙ A)"
    using beq.beta[OF wP wA] by (simp add: opn_lc[OF wff_lc[OF wA]])
  have bB: "?P ❙⋅ B ≈⇘𝗈⇙ (A ❙=⇘α⇙ B)"
    using beq.beta[OF wP wB] by (simp add: opn_lc[OF wff_lc[OF wA]])
  have "Φ ⊢ A ❙=⇘α⇙ A" by (rule bprov.EqR[OF wA])
  hence "Φ ⊢ ?P ❙⋅ A" by (rule bprov.Beta[OF beq.sym[OF bA]])
  hence "Φ ⊢ ?P ❙⋅ B" by (rule leib_subst[OF AB fp wA wB wP])
  thus ?thesis by (rule bprov.Beta[OF bB])
qed

text ‹The diagonal contradiction: a proposition Leibniz-equal to its own negation
  refutes the context (by excluded middle and Leibniz modus ponens).›

lemma leib_neg_contra:
  assumes E: "Φ ⊢ A ❙≐⇘𝗈⇙ (❙¬ A)" and fp: "freep Φ" and wA: "wff⇘𝗈⇙(A)"
  shows "Φ ⊢ ❙⊥"
proof -
  have br1: "Φ ∪ {❙¬ A} ⊢ ❙⊥"
  proof -
    have fp1: "freep (Φ ∪ {❙¬ A})" using freep_add[OF fp] by simp
    have hy: "Φ ∪ {❙¬ A} ⊢ ❙¬ A" by (auto intro: bprov.Hyp)
    have e: "Φ ∪ {❙¬ A} ⊢ A ❙≐⇘𝗈⇙ (❙¬ A)"
      by (rule bprov_weaken[OF E _ fp1]) auto
    have "Φ ∪ {❙¬ A} ⊢ (❙¬ A) ❙≐⇘𝗈⇙ A"
      by (rule leib_sym[OF e fp1 wA wff_Not[OF wA]])
    hence "Φ ∪ {❙¬ A} ⊢ A"
      by (rule leib_mp[OF _ hy fp1 wff_Not[OF wA] wA])
    thus ?thesis by (rule bprov.NegE[OF hy _ wff_FalseB])
  qed
  have br2: "Φ ∪ {A} ⊢ ❙⊥"
  proof -
    have fp2: "freep (Φ ∪ {A})" using freep_add[OF fp] by simp
    have hy: "Φ ∪ {A} ⊢ A" by (auto intro: bprov.Hyp)
    have e: "Φ ∪ {A} ⊢ A ❙≐⇘𝗈⇙ (❙¬ A)"
      by (rule bprov_weaken[OF E _ fp2]) auto
    have "Φ ∪ {A} ⊢ ❙¬ A"
      by (rule leib_mp[OF e hy fp2 wA wff_Not[OF wA]])
    thus ?thesis by (rule bprov.NegE[OF _ hy wff_FalseB])
  qed
  show ?thesis
    by (rule bprov.DisE[OF bprov_em[OF wA] br1 br2 wff_Not[OF wA] wA])
qed

text ‹Application of a primitive equation, and ‹β›-reduction on the right of ‹❙≐›.›

lemma peq_app: "Φ ⊢ C ❙=⇘α ❙⇒ β⇙ D ⟹ freep Φ ⟹ wff⇘α ❙⇒ β⇙(C) ⟹ wff⇘α ❙⇒ β⇙(D)
    ⟹ wff⇘α⇙(A) ⟹ Φ ⊢ (C ❙⋅ A) ❙≐⇘β⇙ (D ❙⋅ A)"
  by (rule leib_cong1[OF bprov.EqL])
lemma leib_reduce_right: "Φ ⊢ A ❙≐⇘𝗈⇙ B ⟹ B ≈⇘𝗈⇙ B' ⟹ wff⇘𝗈⇙(A) ⟹ Φ ⊢ A ❙≐⇘𝗈⇙ B'" 
  by (metis beq.appR bprov.Beta wff_App wff_Leib)

text ‹The same three steps for @{emph ‹primitive›} equality (via ‹NK(=⇩l)› in and
  ‹leib_to_peq› out): application to an argument, ‹β›-reduction on the right, and
  the diagonal contradiction ‹A ❙= ❙¬ A ⟹ ❙⊥›.›
subsection ‹Completeness at every signature and carrier›

text ‹This part strengthens the completeness theorem from the term-model carrier to
  @{emph ‹arbitrary›} infinite value carriers, by an explicit model-embedding
  construction: every ‹Σ›-model of the class ‹ℳ⇘βfb⇙› whose total domain embeds
  injectively into a carrier ‹'u› has an isomorphic copy on ‹'u›, and satisfaction is
  invariant under the embedding.  Since the term model has a countable total domain
  (the language is countable), it embeds into every infinite carrier, so validity
  over any infinite carrier suffices for derivability.  Completeness is then
  extended further, to open formulas and to signatures with infinitely
  many parameters, and the development closes with the main theorems stated in
  self-contained notation.›

subsubsection ‹A countermodel for every underivable sentence›

text ‹The completeness construction, packaged as an explicit countermodel: if a
  sentence is not derivable, the Hintikka term model refutes it.  The total domain
  of the term model is countable --- the domains are ‹∼›-classes of closed wffs.›

lemma refuting_term_model:
  fixes A :: "'p::{countable,infinite} tm"
  assumes c: "cwff 𝗈 A" and nd: "¬⊢ A"
  obtains Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set" and vl ξ
  where "bkk_model Dm Ap Ee vl" "countable {x. ∃τ. Dm τ x}"
        "app_struct.asg Dm ξ" "¬ vl (Ee ξ A)"
proof -
  note wA = cwff_wff[OF c] and cA = cwff_closed[OF c]
  have conΨ: "con {❙¬ A}" using bprov.simps con_def nd wA by fastforce
  have fpΨ: "freep {❙¬ A}" by (intro freep_finite) simp
  interpret H: hintikka_model "{❙¬ A}"
    by unfold_locales (rule conΨ fpΨ)+
  define ξ :: "nat ⇒ ty ⇒ 'p tm set" where
    "ξ ≡ λn τ. H.cls (undefined⇧p⇘τ⇙)"
  have r: "H.V.vresp ξ"
    by (auto simp: ξ_def H.V.vresp_def intro: H.Dm_cls cwff_Par)
  have ra: "app_struct.asg H.Dm ξ"
    using r by (simp add: H.V.bkkA.asg_def H.V.vresp_def)
  have bm: "bkk_model H.Dm H.Ap H.V.Ev (λa. a = H.cls ❙⊤)"
    by intro_locales
  ― ‹the model refutes ‹A›: ‹❙¬A ∈ H›, so ‹A ∉ H›, so the truth lemma denies ‹A››
  have "❙¬A ∈ Hset {❙¬ A}" using Phi_sub_Hset[of "{❙¬ A}"] by auto
  hence "A ∉ Hset {❙¬ A}" using H.Hset_notboth[OF wA] by blast
  hence ref: "H.V.Ev ξ A ≠ H.cls ❙⊤" using H.truth_lemma[OF c r] by simp
  ― ‹the total domain is contained in the countable range of ‹cls››
  have "{x. ∃τ. H.Dm τ x} ⊆ range H.cls" by (auto simp: H.Dm_def)
  hence cnt: "countable {x. ∃τ. H.Dm τ x}"
    by (rule countable_subset) simp
  show ?thesis by (rule that[OF bm cnt ra]) (use ref in simp)
qed

subsubsection ‹Model embedding: satisfaction is carrier-independent›

text ‹A ‹Σ›-model over a carrier ‹'v› whose total domain maps injectively into a
  carrier ‹'u› has an isomorphic copy over ‹'u›; every refutation transfers.  All
  model conditions are pointwise, so the transfer needs no induction on terms.›

lemma bkk_model_embed:
  fixes Dm :: "ty ⇒ 'v ⇒ bool" and i :: "'v ⇒ 'u"
    and A :: "'p tm"
  assumes M: "bkk_model Dm Ap Ee vl"
     and inj: "inj_on i {x. ∃τ. Dm τ x}"
     and wA: "wff⇘𝗈⇙(A)"
     and xi: "app_struct.asg Dm ξ" and nA: "¬ vl (Ee ξ A)"
  obtains Dm' Ap' and Ee' :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" and vl' ξ'
  where "bkk_model Dm' Ap' Ee' vl'" "app_struct.asg Dm' ξ'" "¬ vl' (Ee' ξ' A)"
proof -
  interpret M: bkk_model Dm Ap Ee vl by (rule M)
  define D where "D = {x. ∃τ. Dm τ x}"
  have DmD: "Dm τ x ⟹ x ∈ D" for τ x by (auto simp: D_def)
  have iinj: "x ∈ D ⟹ y ∈ D ⟹ i x = i y ⟹ x = y" for x y
    using inj by (auto simp: D_def inj_on_def)
  define bk where "bk = (λu. SOME x. x ∈ D ∧ i x = u)"
  have cancel: "x ∈ D ⟹ bk (i x) = x" for x
    unfolding bk_def by (rule some_equality) (auto intro: iinj)
  define Dm' where "Dm' = (λτ u. ∃x. Dm τ x ∧ u = i x)"
  have Dm'I: "Dm τ x ⟹ Dm' τ (i x)" for τ x by (auto simp: Dm'_def)
  define pull :: "(nat ⇒ ty ⇒ 'u) ⇒ nat ⇒ ty ⇒ 'v" where
    "pull ≡ λξ' n τ. if ∃x. Dm τ x ∧ i x = ξ' n τ
                     then SOME x. Dm τ x ∧ i x = ξ' n τ
                     else SOME x. Dm τ x"
  have pull_asg: "M.asg (pull ξ')" for ξ'
    unfolding M.asg_def pull_def
    by (auto intro: someI_ex M.as_nonempty someI2_ex)
  have pull_agree: "Dm' τ (ξ' n τ) ⟹ i (pull ξ' n τ) = ξ' n τ"
    for ξ' n τ
    unfolding pull_def Dm'_def by (auto intro: someI2_ex)
  have pull_push: "pull (λn τ. i (ξ n τ)) = ξ"
  proof (intro ext)
    fix n τ
    have d: "Dm τ (ξ n τ)" using xi by (simp add: M.asg_def)
    have "∃x. Dm τ x ∧ i x = i (ξ n τ)" using d by blast
    moreover have "⋀x. Dm τ x ⟹ i x = i (ξ n τ) ⟹ x = ξ n τ"
      by (auto intro: iinj DmD d)
    ultimately show "pull (λn τ. i (ξ n τ)) n τ = ξ n τ"
      unfolding pull_def by auto
  qed
  define Ap' where "Ap' ≡ λu v. i (Ap (bk u) (bk v))"
  define Ee' where "Ee' ≡ λξ' B. i (Ee (pull ξ') B)"
  define vl' where "vl' ≡ λu. vl (bk u)"
  have Ap'I: "x ∈ D ⟹ y ∈ D ⟹ Ap' (i x) (i y) = i (Ap x y)" for x y
    by (simp add: Ap'_def cancel)
  have vl'I: "x ∈ D ⟹ vl' (i x) ⟷ vl x" for x
    by (simp add: vl'_def cancel)
  have EeD: "wff⇘τ⇙(B) ⟹ Ee (pull ξ') B ∈ D" for τ B ξ'
    by (auto intro: DmD M.ev_type[OF _ pull_asg])
  have ApD: "Dm (α ❙⇒ β) f ⟹ Dm α a ⟹ Ap f a ∈ D" for α β f a
    by (auto intro: DmD M.as_appTy)
― ‹the image is an applicative structure; interpreting it makes the specialised ‹asg› equation
    available›
  have AS': "app_struct Dm' Ap'"
  proof (unfold_locales, goal_cases)
    case (1 α) show ?case using M.as_nonempty Dm'I by (metis Dm'_def)
  next
    case (2 α β f a) thus ?case
      by (auto simp: Dm'_def Ap'I DmD intro: M.as_appTy)
  qed
  interpret A': app_struct Dm' Ap' by (rule AS')
  ― ‹the image is a model: every condition transfers pointwise›
  have BM: "bkk_model Dm' Ap' Ee' vl'"
  proof (unfold_locales, goal_cases)
    case 1 thus ?case
      by (auto simp: Ee'_def intro: Dm'I M.ev_type[OF _ pull_asg])
  next
    case (2 ξ' n σ)
    hence "Dm' σ (ξ' n σ)" by (simp add: A'.asg_def)
    thus ?case by (simp add: Ee'_def M.ev_var[OF pull_asg] pull_agree)
  next
    case 3 thus ?case
      by (simp add: Ee'_def M.ev_app[OF _ _ pull_asg]
          Ap'I[OF EeD EeD])
  next
    case (4 τ B ξ' ξ'')
    have "pull ξ' n σ = pull ξ'' n σ" if "(n, σ) ∈ occ B" for n σ
      using 4(4)[OF that] by (auto simp: pull_def)
    thus ?case unfolding Ee'_def
      by (intro arg_cong[of _ _ i] M.ev_coin[OF 4(1) pull_asg pull_asg])
  next
    case 5 thus ?case
      by (simp add: Ee'_def M.ev_beta[OF _ pull_asg])
  next
    case (6 ξ' a')
    then obtain a where a: "Dm 𝗈 a" "a' = i a" by (auto simp: Dm'_def)
    have "vl' (Ap' (Ee' ξ' Neg) a') = vl (Ap (Ee (pull ξ') Neg) a)"
      by (simp add: a Ee'_def Ap'I[OF EeD[OF wff_Neg] DmD[OF a(1)]]
          vl'I[OF ApD[OF M.ev_type[OF wff_Neg pull_asg] a(1)]])
    thus ?case
      by (simp add: a M.vl_neg[OF pull_asg a(1)] vl'I[OF DmD[OF a(1)]])
  next
    case (7 ξ' a' b')
    then obtain a b where ab: "Dm 𝗈 a" "a' = i a" "Dm 𝗈 b" "b' = i b"
      by (auto simp: Dm'_def)
    have dsD: "Ap (Ee (pull ξ') Dis) a ∈ D"
      by (rule ApD[OF M.ev_type[OF wff_Dis pull_asg] ab(1)])
    have ds2: "Dm (𝗈 ❙⇒ 𝗈) (Ap (Ee (pull ξ') Dis) a)"
      by (rule M.as_appTy[OF M.ev_type[OF wff_Dis pull_asg] ab(1)])
    have "vl' (Ap' (Ap' (Ee' ξ' Dis) a') b')
            = vl (Ap (Ap (Ee (pull ξ') Dis) a) b)"
      by (simp add: ab Ee'_def Ap'I[OF EeD[OF wff_Dis] DmD[OF ab(1)]]
          Ap'I[OF dsD DmD[OF ab(3)]] vl'I[OF ApD[OF ds2 ab(3)]])
    thus ?case
      by (simp add: ab M.vl_dis[OF pull_asg ab(1) ab(3)]
          vl'I[OF DmD[OF ab(1)]] vl'I[OF DmD[OF ab(3)]])
  next
    case (8 ξ' σ f')
    then obtain f where f: "Dm (σ ❙⇒ 𝗈) f" "f' = i f"
        by (auto simp: Dm'_def)
    have piD: "Dm ((σ ❙⇒ 𝗈) ❙⇒ 𝗈) (Ee (pull ξ') (Pi σ))"
      by (rule M.ev_type[OF wff_Pi pull_asg])
    have l: "vl' (Ap' (Ee' ξ' (Pi σ)) f')
               = vl (Ap (Ee (pull ξ') (Pi σ)) f)"
      by (simp add: f Ee'_def Ap'I[OF EeD[OF wff_Pi] DmD[OF f(1)]]
          vl'I[OF ApD[OF piD f(1)]])
    have r: "(∀d'. Dm' σ d' ⟶ vl' (Ap' f' d'))
               = (∀d. Dm σ d ⟶ vl (Ap f d))"
      by (auto simp: Dm'_def f Ap'I[OF DmD[OF f(1)] DmD]
          vl'I[OF ApD[OF f(1)]])
    show ?case using l r M.vl_pi[OF pull_asg f(1)] by simp
  next
    case (9 ξ' σ a' b')
    then obtain a b where ab: "Dm σ a" "a' = i a" "Dm σ b" "b' = i b"
      by (auto simp: Dm'_def)
    have eqD: "Ap (Ee (pull ξ') (Eq σ)) a ∈ D"
      by (rule ApD[OF M.ev_type[OF wff_Eq pull_asg] ab(1)])
    have eq2: "Dm (σ ❙⇒ 𝗈) (Ap (Ee (pull ξ') (Eq σ)) a)"
      by (rule M.as_appTy[OF M.ev_type[OF wff_Eq pull_asg] ab(1)])
    have "vl' (Ap' (Ap' (Ee' ξ' (Eq σ)) a') b')
            = vl (Ap (Ap (Ee (pull ξ') (Eq σ)) a) b)"
      by (simp add: ab Ee'_def Ap'I[OF EeD[OF wff_Eq] DmD[OF ab(1)]]
          Ap'I[OF eqD DmD[OF ab(3)]] vl'I[OF ApD[OF eq2 ab(3)]])
    thus ?case
      using M.vl_eq[OF pull_asg ab(1) ab(3)] iinj[OF DmD DmD] ab
      by (auto simp: DmD)
  next
    case (10 ξ' σ f' a')
    then obtain f a where fa: "Dm (σ ❙⇒ 𝗈) f" "f' = i f" "Dm σ a" "a' = i a"
      by (auto simp: Dm'_def)
    have sing: "vl (Ap f b) ⟷ b = a" if b: "Dm σ b" for b
    proof -
      have "vl' (Ap' f' (i b)) ⟷ i b = a'"
        using 10(4)[OF Dm'I[OF b]] by simp
      thus ?thesis
        using b fa iinj[OF DmD DmD]
        by (auto simp: Ap'I[OF DmD[OF fa(1)] DmD[OF b]]
            vl'I[OF ApD[OF fa(1) b]] DmD)
    qed
    have "Ap (Ee (pull ξ') (Iota σ)) f = a"
      by (rule M.vl_iota[OF pull_asg fa(1) fa(3)]) (rule sing)
    thus ?case
      by (simp add: fa Ee'_def Ap'I[OF EeD[OF wff_Iota] DmD[OF fa(1)]])
  next
    case 11
    show ?case
      unfolding A'.functional_def
    proof (intro allI impI)
      fix α β f' g'
      assume f': "Dm' (α ❙⇒ β) f'" and g': "Dm' (α ❙⇒ β) g'"
        and agree: "∀a'. Dm' α a' ⟶ Ap' f' a' = Ap' g' a'"
      obtain f g where fg: "Dm (α ❙⇒ β) f" "f' = i f" "Dm (α ❙⇒ β) g" "g' = i g"
        using f' g' by (auto simp: Dm'_def)
      have "Ap f a = Ap g a" if a: "Dm α a" for a
      proof -
        have "i (Ap f a) = i (Ap g a)"
          using agree[THEN spec, of "i a"] Dm'I[OF a]
          by (simp add: fg Ap'I[OF DmD[OF fg(1)] DmD[OF a]]
              Ap'I[OF DmD[OF fg(3)] DmD[OF a]])
        thus ?thesis by (rule iinj[OF ApD ApD, OF fg(1) a fg(3) a])
      qed
      hence "f = g"
        using M.prop_f fg unfolding M.functional_def by blast
      thus "f' = g'" by (simp add: fg)
    qed
  next
    case (12 a' b')
    then obtain a b where ab: "Dm 𝗈 a" "a' = i a" "Dm 𝗈 b" "b' = i b"
      by (auto simp: Dm'_def)
    thus ?case
      using 12(3) M.prop_b[OF ab(1) ab(3)] vl'I[OF DmD[OF ab(1)]]
        vl'I[OF DmD[OF ab(3)]] by simp
  qed
  ― ‹the pushed assignment refutes ‹A› in the image model›
  define ξ' where "ξ' ≡ λn τ. i (ξ n τ)"
  have asg': "app_struct.asg Dm' ξ'"
    using xi unfolding M.asg_def ξ'_def A'.asg_def
    by (auto intro: Dm'I)
  have "Ee' ξ' A = i (Ee ξ A)" by (simp add: Ee'_def ξ'_def pull_push)
  hence "¬ vl' (Ee' ξ' A)"
    using nA vl'I[OF DmD[OF M.ev_type[OF wA xi]]] by simp
  thus ?thesis using BM asg' that by simp
qed

subsubsection ‹Completeness at every infinite carrier›

text ‹The strengthened form of BKK Corollary 7.7: validity over the models of
  ‹ℳ⇘βfb⇙› at @{emph ‹any›} infinite value carrier implies derivability.  The term
  carrier plays no special role: it only needs to embed into the given carrier,
  which its countability guarantees.›

theorem completeness_at_any_carrier:
  fixes A :: "'p::{countable,infinite} tm"
  assumes c: "cwff 𝗈 A"
    and valid: "⊨('u::infinite) A"
  shows "⊢ A"
proof (rule ccontr)
  assume nd: "¬⊢ A"
  obtain Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set" and vl ξ
    where M: "bkk_model Dm Ap Ee vl" and cnt: "countable {x. ∃τ. Dm τ x}"
      and xi: "app_struct.asg Dm ξ" and nA: "¬ vl (Ee ξ A)"
    by (rule refuting_term_model[OF c nd])
  ― ‹embed the countable total domain into the infinite carrier ‹'u››
  obtain f :: "'p tm set ⇒ nat" where f: "inj_on f {x. ∃τ. Dm τ x}"
    using cnt by (auto simp: countable_def)
  obtain g :: "nat ⇒ 'u" where g: "inj g"
    using infinite_UNIV infinite_countable_subset by blast
  have inj: "inj_on (g ∘ f) {x. ∃τ. Dm τ x}"
    using f g by (rule comp_inj_on[OF _ inj_on_subset]) auto
  obtain Dm' Ap' and Ee' :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" and vl' ξ'
    where "bkk_model Dm' Ap' Ee' vl'" "app_struct.asg Dm' ξ'" "¬ vl' (Ee' ξ' A)"
    using bkk_model_embed M inj cwff_wff[OF c] xi nA by blast
  thus False using valid unfolding bkk_valid_def rel_truth_def by blast
qed

subsubsection ‹Completeness for open formulas›

text ‹Completeness does not require closed sentences: assignments interpret the free
  variables.  The bridge is a substitution-value law for @{emph ‹abstract›}
  ‹Σ›-evaluations (the abstract form of BKK Lemma 3.20, one variable at a time),
  proved without any term induction: substitution is expressed through closing,
  ‹β›-conversion and the evaluation conditions.  On the syntactic side a free
  variable is generalised through a fresh parameter by the rule chain
  ‹NK(β)›--‹NK(ΠI)›--‹NK(ΠE)›--‹NK(β)›.›

lemma opn_clos_sub: "opn k v t = t ⟹ opn k v (clos k x σ t) = fsub x σ v t"
  by (induction t arbitrary: k) auto

lemma fsub_id: "fsub x σ (x⇧f⇘σ⇙) t = t"
  by (induction t) auto

lemma occ_clos: "(x, σ) ∉ occ (clos k x σ t)"
  by (induction t arbitrary: k) auto

lemma pars_clos [simp]: "pars (clos k x σ t) = pars t"
  by (induction t arbitrary: k) auto

lemma finite_occ: "finite (occ t)"
  by (induction t) auto

lemma occ_fsub_closed: "occ u = {} ⟹ occ (fsub x σ u t) = occ t - {(x, σ)}"
  by (induction t) auto

text ‹The sharpened ‹β›-application law: the fresh-name condition only concerns the
  typed occurrence ‹(x, σ)›, not the bare name (a name may occur at several types).›

lemma (in sigma_eval) ev_abs_app_occ:
  assumes wb: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)" and xi: "asg ξ"
    and x: "(x, σ) ∉ occ b" and d: "Dm σ d"
  shows "Ap (Ee ξ (❙Λ⇘σ⇙ b)) d = Ee (ξ(x⇘σ⇙ := d)) (b❙⟨x⇧f⇘σ⇙❙⟩)"
proof -
  have xi': "asg (ξ(x⇘σ⇙ := d))" by (rule asg_upd[OF xi d])
  have "Ee (ξ(x⇘σ⇙ := d)) (b❙⟨x⇧f⇘σ⇙❙⟩) = Ee (ξ(x⇘σ⇙ := d)) ((❙Λ⇘σ⇙ b) ❙⋅ (x⇧f⇘σ⇙))"
    by (rule ev_beta[OF beq.sym[OF beq.beta[OF wb wff_Fre]] xi'])
  also have "… = Ap (Ee (ξ(x⇘σ⇙ := d)) (❙Λ⇘σ⇙ b)) (Ee (ξ(x⇘σ⇙ := d)) (x⇧f⇘σ⇙))"
    by (rule ev_app[OF wb wff_Fre xi'])
  also have "… = Ap (Ee (ξ(x⇘σ⇙ := d)) (❙Λ⇘σ⇙ b)) d"
    using ev_var[OF xi', of x σ] by (simp add: upd_def)
  also have "… = Ap (Ee ξ (❙Λ⇘σ⇙ b)) d"
    using x by (intro arg_cong2[of _ _ d d Ap] refl
        ev_coin[OF wb xi' xi]) (auto simp: upd_def)
  finally show ?thesis ..
qed

text ‹The substitution-value law for abstract ‹Σ›-evaluations (BKK Lemma 3.20 for a
  single free variable): substituting @{emph ‹any›} well-formed term equals updating
  the assignment with its value.›

lemma (in sigma_eval) ev_fsub_one:
  assumes wA: "wff⇘τ⇙(A)" and wu: "wff⇘σ⇙(u)" and xi: "asg ξ"
  shows "Ee ξ (fsub x σ u A) = Ee (ξ(x⇘σ⇙ := Ee ξ u)) A"
proof -
  have opnA: "opn 0 v A = A" for v by (simp add: wff_lc[OF wA])
  let ?B = "clos 0 x σ A"
  have wAbs: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ ?B)"
    by (rule wff_AbsI) (simp add: opn_clos_sub[OF opnA] wff_fsub[OF wA
        wff_Fre])
  have du: "Dm σ (Ee ξ u)" by (rule ev_type[OF wu xi])
  have "Ee ξ (fsub x σ u A) = Ee ξ ((❙Λ⇘σ⇙ ?B) ❙⋅ u)"
    unfolding opn_clos_sub[OF opnA, symmetric]
    by (rule ev_beta[OF beq.sym[OF beq.beta[OF wAbs wu]] xi])
  also have "… = Ap (Ee ξ (❙Λ⇘σ⇙ ?B)) (Ee ξ u)"
    by (rule ev_app[OF wAbs wu xi])
  also have "… = Ee (ξ(x⇘σ⇙ := Ee ξ u)) (?B❙⟨x⇧f⇘σ⇙❙⟩)"
    by (rule ev_abs_app_occ[OF wAbs xi occ_clos du])
  also have "?B❙⟨x⇧f⇘σ⇙❙⟩ = A"
    by (simp add: opn_clos_sub[OF opnA] fsub_id)
  finally show ?thesis .
qed

text ‹Syntactic generalisation: a fresh parameter substituted for a free variable can
  be quantified away and re-instantiated, recovering the open formula.›

lemma bprov_generalize_par:
  assumes wA: "wff⇘𝗈⇙(A)" and p: "p ∉ pars A"
    and d: "⊢ fsub x σ (p⇧p⇘σ⇙) A"
  shows "⊢ A"
proof -
  have opnA: "opn 0 v A = A" for v :: "'a tm"
    by (simp add: wff_lc[OF wA])
  let ?B = "clos 0 x σ A"
  have wAbs: "wff⇘σ❙⇒𝗈⇙(❙Λ⇘σ⇙ ?B)"
    by (rule wff_AbsI)
       (simp add: opn_clos_sub[OF opnA] wff_fsub[OF wA wff_Fre])
  have bq1: "(❙Λ⇘σ⇙ ?B) ❙⋅ (p⇧p⇘σ⇙) ≈⇘𝗈⇙ fsub x σ (p⇧p⇘σ⇙) A"
    using beq.beta[OF wAbs wff_Par] by (simp add: opn_clos_sub[OF opnA])
  have h2: "{} ⊢ (❙Λ⇘σ⇙ ?B) ❙⋅ (p⇧p⇘σ⇙)"
    by (rule bprov.Beta[OF beq.sym[OF bq1] d])
  have h3: "{} ⊢ (Pi σ) ❙⋅ (❙Λ⇘σ⇙ ?B)"
    by (rule bprov.PiI[OF h2 wAbs]) (use p in auto)
  have h4: "{} ⊢ (❙Λ⇘σ⇙ ?B) ❙⋅ (x⇧f⇘σ⇙)"
    by (rule bprov.PiE[OF h3 wff_Fre])
  have bq2: "(❙Λ⇘σ⇙ ?B) ❙⋅ (x⇧f⇘σ⇙) ≈⇘𝗈⇙ A"
  proof -
    have "(❙Λ⇘σ⇙ ?B) ❙⋅ (x⇧f⇘σ⇙) ≈⇘𝗈⇙ ?B❙⟨x⇧f⇘σ⇙❙⟩"
      by (rule beq.beta[OF wAbs wff_Fre])
    thus ?thesis by (simp add: opn_clos_sub[OF opnA] fsub_id)
  qed
  show ?thesis by (rule bprov.Beta[OF bq2 h4])
qed

text ‹Completeness for arbitrary (locally closed) well-formed formulas, by induction
  on the number of typed free occurrences: each occurrence is generalised through a
  fresh parameter, semantically justified by the substitution-value law.›

lemma completeness_open_aux:
  fixes A :: "'p::{countable,infinite} tm"
  shows "card (occ A) ≤ n ⟹ wff⇘𝗈⇙(A) ⟹ (⊨('p tm set) A) ⟹ ⊢ A"
proof (induction n arbitrary: A)
  case (0 A)
  hence "occ A = {}" by (simp add: finite_occ card_eq_0_iff)
  hence "cwff 𝗈 A" using 0(2) by (simp add: cwff_def fvs_eq_fst_occ)
  thus ?case using derivable_iff_valid 0(3) by blast
next
  case (Suc n A)
  show ?case
  proof (cases "occ A = {}")
    case True
    hence "cwff 𝗈 A"
      using Suc.prems(2) by (simp add: cwff_def fvs_eq_fst_occ)
    thus ?thesis using derivable_iff_valid Suc.prems(3) by blast
  next
    case False
    then obtain x σ where xs: "(x, σ) ∈ occ A" by auto
    obtain p :: 'p where p: "p ∉ pars A"
      by (meson ex_new_if_finite finite_pars infinite_UNIV)
    define A1 where "A1 = fsub x σ (p⇧p⇘σ⇙) A"
    have wA1: "wff⇘𝗈⇙(A1)"
      unfolding A1_def by (rule wff_fsub[OF Suc.prems(2) wff_Par])
    have occ1: "occ A1 = occ A - {(x, σ)}"
      unfolding A1_def by (rule occ_fsub_closed) simp
    have card1: "card (occ A1) ≤ n"
      using Suc.prems(1) xs finite_occ
      by (simp add: occ1 card_Diff_singleton)
    have valid1: "⊨('p tm set) A1"
      unfolding bkk_valid_def rel_truth_def
    proof (intro allI impI)
      fix Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set"
        and vl :: "'p tm set ⇒ bool" and ξ
      assume bm: "bkk_model Dm Ap Ee vl" and xi: "app_struct.asg Dm ξ"
      interpret M: bkk_model Dm Ap Ee vl by (rule bm)
      have eq: "Ee ξ A1 = Ee (ξ(x⇘σ⇙ := Ee ξ (p⇧p⇘σ⇙))) A"
        unfolding A1_def
        by (rule M.ev_fsub_one[OF Suc.prems(2) wff_Par xi])
      have asg': "app_struct.asg Dm (ξ(x⇘σ⇙ := Ee ξ (p⇧p⇘σ⇙)))"
        by (rule M.asg_upd[OF xi M.ev_type[OF wff_Par xi]])
      have v: "∀ξ. app_struct.asg Dm ξ ⟶ vl (Ee ξ A)"
        using Suc.prems(3) bm unfolding bkk_valid_def rel_truth_def by blast
      show "vl (Ee ξ A1)" using v[rule_format, OF asg']
          by (simp add: eq)
    qed
    have "⊢ A1" by (rule Suc.IH[OF card1 wA1 valid1])
    thus ?thesis
      unfolding A1_def
      by (rule bprov_generalize_par[OF Suc.prems(2) p, of x σ])
  qed
qed

theorem completeness_open:
  fixes A :: "'p::{countable,infinite} tm"
  assumes "wff⇘𝗈⇙(A)"
      and "⊨('p tm set) A"
    shows "⊢ A"
  using assms(1,2) completeness_open_aux by blast

lemma completeness_open_any_aux:
  fixes A :: "'p::{countable,infinite} tm"
  shows "card (occ A) ≤ n ⟹ wff⇘𝗈⇙(A) ⟹ ⊨('u::infinite) A ⟹ ⊢ A"
proof (induction n arbitrary: A)
  case (0 A)
  hence "occ A = {}" by (simp add: finite_occ card_eq_0_iff)
  hence "cwff 𝗈 A" using 0(2) by (simp add: cwff_def fvs_eq_fst_occ)
  thus ?case using completeness_at_any_carrier 0(3) by blast
next
  case (Suc n A)
  show ?case
  proof (cases "occ A = {}")
    case True
    hence "cwff 𝗈 A"
      using Suc.prems(2) by (simp add: cwff_def fvs_eq_fst_occ)
    thus ?thesis using completeness_at_any_carrier Suc.prems(3) by blast
  next
    case False
    then obtain x σ where xs: "(x, σ) ∈ occ A" by auto
    obtain p :: 'p where p: "p ∉ pars A"
      by (meson ex_new_if_finite finite_pars infinite_UNIV)
    define A1 where "A1 = fsub x σ (p⇧p⇘σ⇙) A"
    have wA1: "wff⇘𝗈⇙(A1)"
      unfolding A1_def by (rule wff_fsub[OF Suc.prems(2) wff_Par])
    have occ1: "occ A1 = occ A - {(x, σ)}"
      unfolding A1_def by (rule occ_fsub_closed) simp
    have card1: "card (occ A1) ≤ n"
      using Suc.prems(1) xs finite_occ
      by (simp add: occ1 card_Diff_singleton)
    have valid1: "⊨('u) A1"
      unfolding bkk_valid_def rel_truth_def
    proof (intro allI impI)
      fix Dm :: "ty ⇒ 'u ⇒ bool" and Ap
        and Ee :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" and vl ξ
      assume bm: "bkk_model Dm Ap Ee vl" and xi: "app_struct.asg Dm ξ"
      interpret M: bkk_model Dm Ap Ee vl by (rule bm)
      have eq: "Ee ξ A1 = Ee (ξ(x⇘σ⇙ := Ee ξ (p⇧p⇘σ⇙))) A"
        unfolding A1_def
        by (rule M.ev_fsub_one[OF Suc.prems(2) wff_Par xi])
      have asg': "app_struct.asg Dm (ξ(x⇘σ⇙ := Ee ξ (p⇧p⇘σ⇙)))"
        by (rule M.asg_upd[OF xi M.ev_type[OF wff_Par xi]])
      have v: "∀ξ. app_struct.asg Dm ξ ⟶ vl (Ee ξ A)"
        using Suc.prems(3) bm unfolding bkk_valid_def rel_truth_def by blast
      show "vl (Ee ξ A1)" using v[rule_format, OF asg']
        by (simp add: eq)
    qed
    have "⊢ A1" by (rule Suc.IH[OF card1 wA1 valid1])
    thus ?thesis unfolding A1_def
      by (rule bprov_generalize_par[OF Suc.prems(2) p, of x σ])
  qed
qed

theorem completeness_open_at_any_carrier:
  fixes A :: "'p::{countable,infinite} tm"
  assumes "wff⇘𝗈⇙(A)"
      and "⊨('u::infinite) A"
    shows "⊢ A"
  using completeness_open_any_aux assms by auto

subsubsection ‹Signature transport›

text ‹On the semantic side, maps of parameter names need @{emph ‹no›} injectivity:
  any ‹h :: 'p ⇒ 'q› turns a model for ‹'q› into a model for ‹'p› by
  evaluating through ‹prn h› --- the value conditions ‹vl⇩¬, …, vl⇩ι› only
  inspect ‹Ee› at the logical constants, which ‹prn› fixes.›

lemma prn_occ [simp]: "occ (prn f t) = occ t"
  by (induction t) auto

lemma bkk_model_reduct:
  fixes Ee :: "(nat ⇒ ty ⇒ 'u) ⇒ 'q tm ⇒ 'u" and h :: "'p ⇒ 'q"
  assumes "bkk_model Dm Ap Ee vl"
  shows "bkk_model Dm Ap (λξ t. Ee ξ (prn h t)) vl"
proof -
  interpret bkk_model Dm Ap Ee vl by (rule assms)
  show ?thesis
  proof (unfold_locales, goal_cases)
    case 3 thus ?case using ev_app by fastforce
    next case 4 thus ?case by (metis ev_coin prn_occ wff_prn)
    next case 5 thus ?case using ev_beta by blast
  qed(auto simp: vl_eq vl_pi vl_dis vl_neg vl_iota ev_var ev_type wff_prn prop_f prop_b)
qed

lemma bkk_valid_map:
  fixes h :: "'p ⇒ 'q"
  assumes v: "⊨('u) (A :: 'p tm)"
    shows "⊨('u) (prn h A :: 'q tm)"
  unfolding bkk_valid_def rel_truth_def
  by (metis bkk_model_reduct bkk_valid_def rel_truth_def v)

text ‹Completeness for every signature with infinitely many parameters: the
  finitely many parameters of ‹A› are relocated into a copy of ‹ℕ› inside ‹'p›,
  completeness over ‹ℕ› applies, and ‹bprov_rename› transports the derivation back.
  (With only finitely many parameters this route is barred: ‹NK(ΠI)› consumes fresh
  eigen-parameters, and an injection ‹ℕ ⇒ 'p› is exactly what supplies them.)›

theorem completeness_at_any_signature:
  fixes A :: "'p::infinite tm"
  assumes wA: "wff⇘𝗈⇙(A)" and v: "⊨('u::infinite) A"
  shows "⊢ A"
proof -
  obtain g0 :: "nat ⇒ 'p" where g0: "inj g0"
    using infinite_UNIV infinite_countable_subset by blast
  define B where "B = pars A ∪ range g0"
  have "inj_on (inv g0) (range g0)" by (rule inj_on_inv_into) simp
  hence rc: "countable (range g0)" by (rule countableI)
  have ri: "infinite (range g0)"
    using finite_imageD[of g0 UNIV] g0 infinite_UNIV_nat by auto
  have cB: "countable B" and iB: "infinite B"
    unfolding B_def using rc ri by (auto intro: countable_finite)
  define g where "g = from_nat_into B"
  have g: "inj g" and cover: "pars A ⊆ range g"
    using bij_betw_from_nat_into[OF cB iB]
    unfolding g_def bij_betw_def B_def by auto
  define h :: "'p ⇒ nat" where "h = (λp. SOME n. g n = p)"
  have gh: "g (h p) = p" if "p ∈ pars A" for p
  proof -
    from cover that obtain n where n: "g n = p" by auto
    from someI[of "λn. g n = p", OF n] show ?thesis by (simp add: h_def)
  qed
  have wN: "wff⇘𝗈⇙(prn h A)" by (rule wff_prn[OF wA])
  have dN: "⊢ (prn h A :: nat tm)"
    using bkk_valid_map completeness_open_at_any_carrier v wN by blast
  have "⊢ (prn g (prn h A) :: 'p tm)"
    using bprov_rename dN g by fastforce
  moreover have "prn g (prn h A) = A"
    by (simp add: gh prn_cong prn_prn)
  ultimately show ?thesis by simp
qed

end