Theory Completeness

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

section ‹Completeness›

text ‹Henkin completeness for ‹NK›, with the term model realised as a term evaluation
  (BKK Definition 3.35).  The result is then strengthened to arbitrary infinite value
  carriers, signatures with infinitely many parameters, and open formulas, and extended to
  derivation from hypotheses --- up to arbitrary parameter-rich contexts of open formulas
  at any infinite signature cardinality; the carrier need only be at least as large as
  the signature.  For the hypothesis relation ‹⊩› of ‹Calculus› even the
  parameter-rich proviso disappears (‹completeness_fprov›).›

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).  ‹NK›-consistency and its closure properties
  (BKK Definition 7.4, Lemma 7.5) live in ‹Calculus›; here we develop the witnessing step,
  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 ‹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 ‹Signatures of arbitrary cardinality: the parameter reserve›

text ‹BKK run their extension lemma at any infinite signature cardinality ‹ℵ⇩s› (BKK
  Remark 3.16).  To follow them beyond countable signatures, the enumeration of sentences
  below walks a well-order of the @{emph ‹term type›} instead of ‹ℕ›, and the freshness
  argument becomes quantitative: the argument below needs a reserve of unused parameters as
  large as the @{emph ‹signature›}, not merely infinite (whether an infinite reserve would
  suffice is not settled here, see the closing remark).  The predicate ‹richp› ("parameter-rich")
  captures this, in the cardinal order ‹≤o› of the Isabelle/HOL library; over a countable
  signature it collapses to ‹freep› (@{emph ‹infinite›} reserve, BKK Definition 6.3).›

unbundle cardinal_syntax

definition richp :: "'p tm set ⇒ bool" where "richp Φ ≡ |UNIV :: 'p set| ≤o |- usedp Φ|"

lemma richp_freep:
  assumes "richp (Φ :: 'p::infinite tm set)" shows "freep Φ"
proof -
  have "|UNIV :: nat set| ≤o |UNIV :: 'p set|"
    using infinite_iff_card_of_nat infinite_UNIV by blast
  from ordLeq_transitive[OF this assms[unfolded richp_def]]
  show ?thesis unfolding freep_def using infinite_iff_card_of_nat by blast
qed

lemma richp_iff_freep:
  fixes Φ :: "'p::{countable,infinite} tm set"
  shows "richp Φ ⟷ freep Φ"
proof
  assume "richp Φ" thus "freep Φ" by (rule richp_freep)
next
  assume "freep Φ"
  hence n: "|UNIV :: nat set| ≤o |- usedp Φ|"
    unfolding freep_def using infinite_iff_card_of_nat by blast
  have "|UNIV :: 'p set| ≤o |UNIV :: nat set|"
    using card_of_ordLeq by fastforce
  thus "richp Φ" unfolding richp_def using n ordLeq_transitive by blast
qed

lemma infinite_tm_UNIV: "infinite (UNIV :: 'p tm set)"
proof -
  have "inj (Bnd :: nat ⇒ 'p tm)" by (simp add: inj_on_def)
  thus ?thesis by (metis finite_imageD infinite_UNIV_nat infinite_super top_greatest)
qed

text ‹Over an infinite signature there are at most as many terms as parameters: an infinite
  type absorbs pairing (‹|'p × 'p| =o |'p|›), so the whole term algebra encodes injectively
  into ‹'p› itself --- the nontrivial half of the identity ‹|'p tm| = max(ℵ⇩0, |'p|)›, and
  the only half needed here.
  The encoder ‹tmenc› tags each constructor and recurses through an injective pairing.›

primrec tmenc :: "('u × 'u ⇒ 'u) ⇒ (nat ⇒ 'u) ⇒ ('p ⇒ 'u) ⇒ 'p tm ⇒ 'u" where
  "tmenc pr2 nt pt (Bnd n) = pr2 (nt 0, nt n)"
| "tmenc pr2 nt pt (Fre n σ) = pr2 (nt 1, pr2 (nt n, nt (to_nat σ)))"
| "tmenc pr2 nt pt (Par p σ) = pr2 (nt 2, pr2 (pt p, nt (to_nat σ)))"
| "tmenc pr2 nt pt Neg = pr2 (nt 3, nt 0)"
| "tmenc pr2 nt pt Dis = pr2 (nt 4, nt 0)"
| "tmenc pr2 nt pt (Pi σ) = pr2 (nt 5, nt (to_nat σ))"
| "tmenc pr2 nt pt (Iota σ) = pr2 (nt 6, nt (to_nat σ))"
| "tmenc pr2 nt pt (Eq σ) = pr2 (nt 7, nt (to_nat σ))"
| "tmenc pr2 nt pt (App s t) = pr2 (nt 8, pr2 (tmenc pr2 nt pt s, tmenc pr2 nt pt t))"
| "tmenc pr2 nt pt (Abs σ b) = pr2 (nt 9, pr2 (nt (to_nat σ), tmenc pr2 nt pt b))"

lemma tmenc_inj:
  assumes p2: "inj pr2" and nt: "inj nt" and pt: "inj pt"
  shows "tmenc pr2 nt pt s = tmenc pr2 nt pt t ⟹ s = t"
  by (induction s arbitrary: t)
     (case_tac t; force dest!: injD[OF p2] injD[OF nt] injD[OF pt])+

lemma card_of_tm: "|UNIV :: 'p tm set| ≤o |UNIV :: 'p::infinite set|"
proof -
  have "|UNIV :: ('p × 'p) set| =o |UNIV :: 'p set|"
    using card_of_Times_same_infinite[OF infinite_UNIV] by simp
  hence "|UNIV :: ('p × 'p) set| ≤o |UNIV :: 'p set|"
    by (rule ordIso_imp_ordLeq)
  then obtain pr2 :: "'p × 'p ⇒ 'p" where p2: "inj pr2"
    by (meson card_of_ordLeq)
  obtain nt :: "nat ⇒ 'p" where nt: "inj nt"
    using infinite_UNIV infinite_countable_subset by blast
  have idp: "inj (id :: 'p ⇒ 'p)" by (simp add: inj_on_def)
  have "inj (tmenc pr2 nt id)"
    using tmenc_inj[OF p2 nt idp] by (auto intro: injI)
  thus ?thesis by (simp add: card_of_ordLeqI)
qed

lemma richp_reserve:
  assumes "richp (Φ :: 'p::infinite tm set)"
  shows "|UNIV :: 'p tm set| ≤o |- usedp Φ|"
  by (rule ordLeq_transitive[OF card_of_tm assms[unfolded richp_def]])

text ‹Two small counting facts: a finite set is strictly smaller than any infinite type, and
  over an infinite type ‹'k› a union of fewer-than-‹|'k|› finite sets stays strictly
  smaller than ‹|'k|› --- no regularity of the cardinal is needed, because the members are
  finite.›

lemma card_of_finite_infinite:
  assumes "finite (A :: 'a set)" and "infinite (B :: 'b set)"
  shows "|A| <o |B|"
  using assms
  by (intro finite_ordLess_infinite) (auto simp: Field_card_of card_of_well_order_on)

lemma card_of_UNION_finite_small:
  fixes F :: "'i ⇒ 'a set"
  assumes small: "|I| <o |UNIV :: 'k set|" and inf: "infinite (UNIV :: 'k set)"
      and fin: "⋀i. i ∈ I ⟹ finite (F i)"
  shows "|⋃i∈I. F i| <o |UNIV :: 'k set|"
proof (cases "finite I")
  case True
  hence "finite (⋃i∈I. F i)" using fin by blast
  thus ?thesis using inf by (rule card_of_finite_infinite)
next
  case False
  have "|⋃i∈I. F i| ≤o |I|"
  proof (rule card_of_UNION_ordLeq_infinite[OF False])
    show "|I| ≤o |I|" by (rule ordLeq_reflexive[OF card_of_Well_order])
    show "∀i∈I. |F i| ≤o |I|"
      using fin False by (blast intro: ordLess_imp_ordLeq card_of_finite_infinite)
  qed
  thus ?thesis using small by (rule ordLeq_ordLess_trans)
qed

text ‹A full-size reserve survives removing finitely many elements --- the workhorse
  behind the closure properties of ‹richp›.›

lemma card_of_diff_finite:
  assumes rich: "|UNIV :: 'a::infinite set| ≤o |R :: 'a set|" and fin: "finite F"
  shows "|UNIV :: 'a set| ≤o |R - F|"
proof (rule ccontr)
  assume "¬ |UNIV :: 'a set| ≤o |R - F|"
  hence l: "|R - F| <o |UNIV :: 'a set|"
    by (metis card_of_Well_order not_ordLeq_iff_ordLess)
  have "R ⊆ (R - F) ∪ F" by blast
  hence "|R| ≤o |(R - F) ∪ F|" by (rule card_of_mono1)
  moreover have "|(R - F) ∪ F| <o |UNIV :: 'a set|"
    by (rule card_of_Un_ordLess_infinite[OF infinite_UNIV l
          card_of_finite_infinite[OF fin infinite_UNIV]])
  ultimately show False
    using rich by (meson ordLeq_ordLess_trans ordLeq_transitive ordLess_irreflexive)
qed

text ‹Like ‹freep›, richness survives adding one formula: only finitely many parameters
  are lost.›

lemma richp_add:
  assumes "richp (Φ :: 'p::infinite tm set)" shows "richp (insert B Φ)"
proof -
  have "- usedp Φ - pars B ⊆ - usedp (insert B Φ)"
    by (auto simp: usedp_def)
  hence "|- usedp Φ - pars B| ≤o |- usedp (insert B Φ)|"
    by (rule card_of_mono1)
  thus ?thesis
    unfolding richp_def
    using card_of_diff_finite[OF assms[unfolded richp_def] finite_pars]
          ordLeq_transitive by blast
qed

text ‹Folding the signature into one half of itself: an injective renaming ‹h :: 'p ⇒ 'p›
  whose co-range is as large as the signature (‹|'p + 'p| = |'p|›).  The untouched half
  serves as a parameter reserve in ‹completeness_fprov› and in ‹NK_Infinity›.›

lemma signature_fold:
  "∃h :: 'p::infinite ⇒ 'p. inj h ∧ |UNIV :: 'p set| ≤o |- range h|"
proof -
  have "|(UNIV :: 'p set) <+> (UNIV :: 'p set)| =o |UNIV :: 'p set|"
    using card_of_Plus_infinite[OF infinite_UNIV
          ordLeq_reflexive[OF card_of_Well_order]] by blast
  hence "|UNIV :: ('p + 'p) set| ≤o |UNIV :: 'p set|"
    by (metis UNIV_Plus_UNIV ordIso_imp_ordLeq)
  then obtain j :: "'p + 'p ⇒ 'p" where injj: "inj j"
    by (meson card_of_ordLeq)
  define h where "h = (λp. j (Inl p))"
  have injh: "inj h" using injj by (auto simp: h_def inj_on_def)
  have sub: "(λq. j (Inr q)) ` UNIV ⊆ - range h"
    using injD[OF injj] by (auto simp: h_def)
  have inj1: "inj_on (λq :: 'p. j (Inr q)) UNIV" using injj by (auto simp: inj_on_def)
  have "|UNIV :: 'p set| ≤o |- range h|"
    by (rule card_of_ordLeq[THEN iffD1]) (use sub inj1 in blast)
  thus ?thesis using injh by blast
qed

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

text ‹We enumerate the sentences along a well-order of the term type 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"

text ‹The enumeration order: a well-order of the term type of @{emph ‹minimal›} order type,
  the cardinal ‹|UNIV|› of ‹'p tm› as provided by the library.  Strictly below any stage lie
  @{emph ‹fewer›} terms than there are terms in total (@{thm [source] card_of_underS}).›

definition tmord :: "('p tm × 'p tm) set" where
  "tmord = |UNIV :: 'p tm set|"

lemma tmord_wo: "wo_rel (tmord :: ('p tm × 'p tm) set)"
  by (simp add: wo_rel_def tmord_def card_of_Well_order)

lemma tmord_wf: "wf (tmord - Id :: ('p tm × 'p tm) set)"
  using card_of_well_order_on[of "UNIV :: 'p tm set"]
  unfolding well_order_on_def tmord_def by blast

lemma tmord_lin: "linear_order_on UNIV (tmord :: ('p tm × 'p tm) set)"
  using card_of_well_order_on[of "UNIV :: 'p tm set"]
  unfolding well_order_on_def tmord_def by blast

lemma tmord_total: "a ≠ b ⟹ (a, b) ∈ tmord ∨ (b, a) ∈ tmord"
  using tmord_lin unfolding linear_order_on_def total_on_def by blast

lemma tmord_trans: "(a, b) ∈ tmord ⟹ (b, c) ∈ tmord ⟹ (a, c) ∈ tmord"
  using tmord_lin
  unfolding linear_order_on_def partial_order_on_def preorder_on_def
  by (blast dest: transD)

lemma tmord_refl: "(a, a) ∈ tmord"
  using tmord_lin
  unfolding linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by blast

lemma tmord_induct [case_names below]:
  assumes "⋀a. (⋀b. b ∈ underS tmord a ⟹ P b) ⟹ P a"
  shows "P (a :: 'p tm)"
proof (rule wf_induct_rule[OF tmord_wf])
  fix a :: "'p tm" assume IH: "⋀b. (b, a) ∈ tmord - Id ⟹ P b"
  show "P a"
  proof (rule assms)
    fix b assume "b ∈ underS tmord a"
    hence "(b, a) ∈ tmord - Id" by (auto simp: underS_def)
    thus "P b" by (rule IH)
  qed
qed

lemma tmord_underS_small: "|underS tmord (a :: 'p tm)| <o |UNIV :: 'p tm set|"
proof -
  have co: "Card_order (tmord :: ('p tm × 'p tm) set)"
    unfolding tmord_def by (rule card_of_Card_order)
  have fld: "(a :: 'p tm) ∈ Field tmord"
    by (simp add: tmord_def Field_card_of)
  from card_of_underS[OF co fld] show ?thesis
    by (simp add: tmord_def)
qed

lemma tmord_under: "under tmord a = insert a (underS tmord a)"
  by (auto simp: under_def underS_def tmord_refl)

text ‹The extension, by well-order recursion: at stage ‹a› the term ‹a› itself is decided
  over the union of all earlier stages (a no-op unless ‹a› is a sentence) --- each term is
  its own index, so no enumeration function is needed.›

definition ext :: "'p tm set ⇒ 'p tm ⇒ 'p tm set" where
  "ext Φ = wo_rel.worec tmord (λf a. step (Φ ∪ (⋃b ∈ underS tmord a. f b)) a)"

lemma ext_unfold:
  fixes Φ :: "'p tm set"
  shows "ext Φ a = step (Φ ∪ (⋃b ∈ underS tmord a. ext Φ b)) a"
proof -
  have adm: "wo_rel.adm_wo tmord (λf a. step (Φ ∪ (⋃b ∈ underS tmord a. f b)) a)"
  proof -
    { fix f g :: "'p tm ⇒ 'p tm set" and x :: "'p tm"
      assume "∀y ∈ underS tmord x. f y = g y"
      hence "(⋃b ∈ underS tmord x. f b) = (⋃b ∈ underS tmord x. g b)" by auto
      hence "step (Φ ∪ (⋃b ∈ underS tmord x. f b)) x
           = step (Φ ∪ (⋃b ∈ underS tmord x. g b)) x" by simp }
    thus ?thesis unfolding wo_rel.adm_wo_def[OF tmord_wo] by blast
  qed
  show ?thesis
    using fun_cong[OF wo_rel.worec_fixpoint[OF tmord_wo adm], of a]
    unfolding ext_def by simp
qed

definition Hset :: "'p tm set ⇒ 'p tm set" where
  "Hset Φ = (⋃a. ext Φ a)"

text ‹The chain is directed, each stage extends ‹Φ›, and each stage stays ‹freep› and consistent.›

lemma step_expand: "S ⊆ step S A"
  by (auto simp: step_def)

text ‹The next lemma, ‹freep_step›, keeps its statement from the initial release of this
  entry (August 2026) (compatibility export); the transfinite chain below tracks parameter usage by
  counting instead.›

lemma freep_step: "freep S ⟹ freep (step S A)"
  by (simp add: finite_wit freep_add freep_un_finite step_def)

lemma ext_stage_sub: "Φ ∪ (⋃b ∈ underS tmord a. ext Φ b) ⊆ ext Φ a"
  by (subst ext_unfold) (rule step_expand)

lemma Phi_sub_ext: "Φ ⊆ ext Φ a"
  using ext_stage_sub by blast

lemma ext_mono: "b ∈ underS tmord a ⟹ ext Φ b ⊆ ext Φ a"
  using ext_stage_sub by blast

lemma ext_finite_ub:
  assumes "finite B" and "B ≠ {}"
  shows "∃b ∈ B. ∀c ∈ B. ext Φ c ⊆ ext Φ b"
  using assms
proof (induction B rule: finite_ne_induct)
  case (singleton x) show ?case by blast
next
  case (insert x B)
  then obtain b where b: "b ∈ B" "∀c∈B. ext Φ c ⊆ ext Φ b" by blast
  consider "x = b" | "x ∈ underS tmord b" | "b ∈ underS tmord x"
    using tmord_total by (auto simp: underS_def)
  thus ?case
  proof cases
    case 1 thus ?thesis using b by blast
  next
    case 2 thus ?thesis using b ext_mono by blast
  next
    case 3
    hence bx: "ext Φ b ⊆ ext Φ x" by (rule ext_mono)
    thus ?thesis using b by blast
  qed
qed

lemma ext_directed: "∃c. ext Φ a ⊆ ext Φ c ∧ ext Φ b ⊆ ext Φ c"
proof -
  have "∃d ∈ {a, b}. ∀c ∈ {a, b}. ext Φ c ⊆ ext Φ d"
    by (rule ext_finite_ub) auto
  thus ?thesis by blast
qed
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
text ‹Bookkeeping for freshness: each stage consumes only finitely many parameters (the
  sentence decided, plus at most one witness), and below any stage there are fewer stages
  than terms --- while the ‹richp› reserve holds at least ‹|'p tm|›-many parameters
  (@{thm [source] richp_reserve}).  So every stage stays ‹freep› --- which is all
  that ‹con_step› asks for.›

definition stagep :: "'p tm set ⇒ 'p tm ⇒ 'p set" where
  "stagep Φ b = pars b ∪ usedp (wit (Φ ∪ (⋃c ∈ underS tmord b. ext Φ c)) b)"

lemma finite_stagep: "finite (stagep Φ b)"
  by (simp add: stagep_def finite_wit usedp_def)

lemma usedp_step_sub: "usedp (step S A) ⊆ usedp S ∪ pars A ∪ usedp (wit S A)"
  by (auto simp: step_def usedp_def)

lemma usedp_ext_bound:
  "usedp (ext Φ a) ⊆ usedp Φ ∪ (⋃b ∈ under tmord a. stagep Φ b)"
proof (induction a rule: tmord_induct)
  case (below a)
  have su: "c ∈ under tmord a" if "b ∈ underS tmord a" "c ∈ under tmord b" for b c
    using that by (auto simp: under_def underS_def intro: tmord_trans)
  have "usedp (ext Φ a)
        ⊆ usedp (Φ ∪ (⋃b ∈ underS tmord a. ext Φ b)) ∪ stagep Φ a"
    using usedp_step_sub[of "Φ ∪ (⋃b ∈ underS tmord a. ext Φ b)" a]
    by (subst ext_unfold) (auto simp: stagep_def)
  moreover have "usedp (Φ ∪ (⋃b ∈ underS tmord a. ext Φ b))
        = usedp Φ ∪ (⋃b ∈ underS tmord a. usedp (ext Φ b))"
    by (auto simp: usedp_def)
  moreover have "usedp (ext Φ b) ⊆ usedp Φ ∪ (⋃c ∈ under tmord a. stagep Φ c)"
    if b: "b ∈ underS tmord a" for b
    using below.IH[OF b] su[OF b] by blast
  moreover have "a ∈ under tmord a" by (simp add: tmord_under)
  ultimately show ?case by blast
qed

lemma ext_reserve:
  assumes rp: "richp (Φ :: 'p::infinite tm set)"
  shows "freep (Φ ∪ (⋃b ∈ underS tmord a. ext Φ b))" and "freep (ext Φ a)"
proof -
  define X where "X = (⋃b ∈ under tmord a. stagep Φ b)"
  have "under tmord (a :: 'p tm) = {a} ∪ underS tmord a"
    by (auto simp: tmord_under)
  hence "|under tmord (a :: 'p tm)| <o |UNIV :: 'p tm set|"
    using card_of_Un_ordLess_infinite[OF infinite_tm_UNIV
          card_of_finite_infinite[OF _ infinite_tm_UNIV] tmord_underS_small,
          of "{a}"] by simp
  hence Xsmall: "|X| <o |UNIV :: 'p tm set|"
    unfolding X_def
    by (rule card_of_UNION_finite_small[OF _ infinite_tm_UNIV]) (rule finite_stagep)
  have su: "c ∈ under tmord a" if "b ∈ underS tmord a" "c ∈ under tmord b" for b c
    using that by (auto simp: under_def underS_def intro: tmord_trans)
  have bound': "usedp (ext Φ b) ⊆ usedp Φ ∪ X" if b: "b ∈ under tmord a" for b
  proof (cases "b = a")
    case True
    thus ?thesis using usedp_ext_bound[of Φ b] unfolding X_def by simp
  next
    case False
    hence bS: "b ∈ underS tmord a" using b by (auto simp: under_def underS_def)
    have "(⋃c ∈ under tmord b. stagep Φ c) ⊆ X"
      unfolding X_def using su[OF bS] by blast
    thus ?thesis using usedp_ext_bound[of Φ b] by blast
  qed
  have bound: "usedp (Φ ∪ (⋃b ∈ underS tmord a. ext Φ b)) ⊆ usedp Φ ∪ X"
  proof -
    have "usedp (Φ ∪ (⋃b ∈ underS tmord a. ext Φ b))
        = usedp Φ ∪ (⋃b ∈ underS tmord a. usedp (ext Φ b))"
      by (auto simp: usedp_def)
    moreover have "usedp (ext Φ b) ⊆ usedp Φ ∪ X" if "b ∈ underS tmord a" for b
      using bound' that by (auto simp: under_def underS_def)
    ultimately show ?thesis by blast
  qed
  have inf: "infinite (- (usedp Φ ∪ X))"
  proof
    assume fin: "finite (- (usedp Φ ∪ X))"
    have "- usedp Φ ⊆ X ∪ (- (usedp Φ ∪ X))" by blast
    hence "|- usedp Φ| ≤o |X ∪ (- (usedp Φ ∪ X))|" by (rule card_of_mono1)
    moreover have "|X ∪ (- (usedp Φ ∪ X))| <o |UNIV :: 'p tm set|"
      by (rule card_of_Un_ordLess_infinite[OF infinite_tm_UNIV Xsmall
            card_of_finite_infinite[OF fin infinite_tm_UNIV]])
    ultimately have "|UNIV :: 'p tm set| <o |UNIV :: 'p tm set|"
      using richp_reserve[OF rp] by (meson ordLeq_ordLess_trans ordLeq_transitive)
    thus False using ordLess_irreflexive by blast
  qed
  show "freep (Φ ∪ (⋃b ∈ underS tmord a. ext Φ b))"
    unfolding freep_def by (rule infinite_super[OF _ inf]) (use bound in blast)
  have aa: "a ∈ under tmord a" by (simp add: under_def tmord_refl)
  show "freep (ext Φ a)"
    unfolding freep_def
    by (rule infinite_super[OF _ inf]) (use bound'[OF aa] in blast)
qed

lemma con_ext:
  assumes conΦ: "con Φ" and rp: "richp (Φ :: 'p::infinite tm set)"
  shows "con (ext Φ a)"
proof (induction a rule: tmord_induct)
  case (below a)
  let ?S = "Φ ∪ (⋃b ∈ underS tmord a. ext Φ b)"
  have conS: "con ?S"
  proof (rule con_compact)
    fix F :: "'p tm set" assume finF: "finite F" and subF: "F ⊆ ?S"
    show "con F"
    proof (cases "F ⊆ Φ")
      case True
      show ?thesis by (rule con_mono[OF conΦ True richp_freep[OF rp]])
    next
      case False
      have "∀x ∈ F - Φ. ∃b. b ∈ underS tmord a ∧ x ∈ ext Φ b"
        using subF by blast
      then obtain f where f: "⋀x. x ∈ F - Φ ⟹ f x ∈ underS tmord a ∧ x ∈ ext Φ (f x)"
        by (metis bchoice)
      have finB: "finite (f ` (F - Φ))" and neB: "f ` (F - Φ) ≠ {}"
        and subB: "f ` (F - Φ) ⊆ underS tmord a"
        using finF False f by auto
      obtain b where b: "b ∈ f ` (F - Φ)" "⋀c. c ∈ f ` (F - Φ) ⟹ ext Φ c ⊆ ext Φ b"
        using ext_finite_ub[where Φ = Φ, OF finB neB] by blast
      have FbF: "F ⊆ ext Φ b"
      proof
        fix x assume x: "x ∈ F"
        show "x ∈ ext Φ b"
        proof (cases "x ∈ Φ")
          case True thus ?thesis using Phi_sub_ext by blast
        next
          case False
          hence "x ∈ ext Φ (f x)" and "f x ∈ f ` (F - Φ)" using f x by auto
          thus ?thesis using b(2) by blast
        qed
      qed
      have conb: "con (ext Φ b)" using below.IH b(1) subB by blast
      show ?thesis by (rule con_mono[OF conb FbF ext_reserve(2)[OF rp]])
    qed
  qed
  show ?case by (subst ext_unfold) (rule con_step[OF conS ext_reserve(1)[OF rp]])
qed

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

lemma Phi_sub_Hset: "Φ ⊆ Hset Φ"
  unfolding Hset_def using Phi_sub_ext by blast

lemma finite_sub_ext: "finite F ⟹ F ⊆ Hset Φ ⟹ ∃a. F ⊆ ext Φ a"
proof (induction F rule: finite_induct)
  case empty thus ?case by blast
next
  case (insert x F)
  then obtain a where a: "F ⊆ ext Φ a" by auto
  from insert.prems obtain b where b: "x ∈ ext Φ b" by (auto simp: Hset_def)
  obtain c where "ext Φ a ⊆ ext Φ c" and "ext Φ b ⊆ ext Φ c"
    using ext_directed by blast
  thus ?case using a b by blast
qed

lemma con_Hset: fixes Φ :: "'p::infinite tm set"
  assumes "con Φ" and "richp Φ"
  shows "con (Hset Φ)"
  by (meson assms con_compact con_ext con_mono ext_reserve(2) finite_sub_ext)

text ‹‹freep (Hset Φ)› fails: a maximal set uses every parameter, since for each parameter
  ‹c› it contains ‹c ❙= c› or its negation.  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::infinite tm set"
  assumes "con Φ" and "richp Φ" and "finite F" and "F ⊆ Hset Φ"
  shows "con F"
  by (meson assms con_ext con_mono ext_reserve(2) finite_sub_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:
  assumes c: "cwff 𝗈 A" shows "A ∈ Hset Φ ∨ ❙¬ A ∈ Hset Φ"
proof -
  have "A ∈ ext Φ A ∨ ❙¬ A ∈ ext Φ A"
    using c by (subst (1 2) ext_unfold) (simp add: step_def)
  thus ?thesis unfolding Hset_def by blast
qed

text ‹The maximal set uses every parameter, so it is not ‹freep› (cf.\ the remark before
  ‹Hset_finite_con›).›

lemma Hset_not_freep: fixes Φ :: "'p tm set" shows "¬ freep (Hset Φ)"
proof -
  have "p ∈ usedp (Hset Φ)" for p
  proof -
    let ?e = "(p⇧p⇘ι⇙) ❙=⇘ι⇙ (p⇧p⇘ι⇙) :: 'p tm"
    have "cwff 𝗈 ?e" by (simp add: cwff_def wff_PEq wff_Par)
    hence "?e ∈ Hset Φ ∨ ❙¬ ?e ∈ Hset Φ" by (rule Hset_maximal)
    thus ?thesis
    proof (elim disjE)
      assume "?e ∈ Hset Φ" thus ?thesis unfolding usedp_def by (intro UN_I[of ?e]) simp_all
    next
      assume "❙¬ ?e ∈ Hset Φ" thus ?thesis unfolding usedp_def
        by (intro UN_I[of "❙¬ ?e"]) simp_all
    qed
  qed
  hence "usedp (Hset Φ) = UNIV" by blast
  thus ?thesis by (simp add: freep_def)
qed

lemma Hset_saturated: fixes Φ :: "'p::infinite tm set"
  assumes conΦ: "con Φ" and fp: "richp Φ"
  and cA: "cwff 𝗈 (❙¬ ((Pi α) ❙⋅ G))" and inH: "❙¬ ((Pi α) ❙⋅ G) ∈ Hset Φ"
shows "∃c. ❙¬ (G ❙⋅ (c⇧p⇘α⇙)) ∈ Hset Φ"
proof -
  note wA = cwff_wff[OF cA]
  let ?A = "❙¬ ((Pi α) ❙⋅ G)"
  let ?S = "Φ ∪ (⋃b ∈ underS tmord ?A. ext Φ b)"
  have step: "ext Φ ?A = step ?S ?A"
    by (rule ext_unfold)
  have "con (insert ?A ?S)"
  proof (rule ccontr)
    assume "¬ con (insert ?A ?S)"
    hence "❙¬ ?A ∈ ext Φ ?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 Φ ?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 ‹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::infinite tm set"
  assumes conΦ: "con Φ" and fpΦ: "richp Φ"
      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

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::infinite tm set"
  assumes conΦ: "con Φ" and fpΦ: "richp Φ"
begin

text ‹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, congruence and truth-transfer follow, all by @{thm [source] Hset_deduct}
  over the corresponding derived rules of the calculus.›

lemma Hset_leib_refl: assumes ca: "cwff α A" shows "(A ❙≐⇘α⇙ A) ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ, of "{}"])
  show "finite {}" by simp
  show "{} ⊆ Hset Φ" by simp
  show "{} ⊢ A ❙≐⇘α⇙ A" by (rule leib_refl[OF cwff_wff[OF ca]])
  show "cwff 𝗈 (A ❙≐⇘α⇙ A)" by (rule cwff_LeibE[OF ca ca])
qed

lemma Hset_leib_sym:
  assumes 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 wb = cwff_wff[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 cwff_LeibE[OF cb ca])
qed

lemma Hset_leib_trans:
  assumes 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 wc = cwff_wff[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 cwff_LeibE[OF ca cc])
qed

lemma Hset_leib_cong:
  assumes 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 wC' = cwff_wff[OF cc'] and
       wA = cwff_wff[OF ca] and wA' = cwff_wff[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 cwff_LeibE[OF cwff_App[OF cc ca] cwff_App[OF cc' ca']])
qed

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

lemma Hset_leib_mp:
  assumes 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 wB = cwff_wff[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)
  show "?F ⊢ B"
    by (rule leib_transport[OF s1 fp wA wB wP PA PB]) (auto intro: bprov.Hyp)
qed

text ‹The ‹∼›-equivalence classes of closed well-formed terms (@{const cwff} from
  theory ‹Syntax›): ‹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 by (auto simp: cls_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 cwff_wff
      Hset_leib_sym Hset_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 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)

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}.›

text ‹The one step behind functionality and description: if every instance of an abstracted
  body lies in ‹H›, the ‹Π›-sentence lies in ‹H› by saturation (@{thm [source] Hset_pi_iff}),
  and anything derivable from it is in ‹H› by @{thm [source] Hset_deduct}.›

lemma Hset_forall_intro:
  assumes wB: "cwff (σ❙⇒𝗈) (❙Λ⇘σ⇙ body)"
      and inst: "⋀a. cwff σ a ⟹ (❙Λ⇘σ⇙ body) ❙⋅ a ∈ Hset Φ"
      and drv: "{❙Π⇘σ⇙ body} ⊢ S"
      and cS: "cwff 𝗈 S"
    shows "S ∈ Hset Φ"
proof (rule Hset_deduct[OF conΦ fpΦ, of "{❙Π⇘σ⇙ body}"])
  show "finite {❙Π⇘σ⇙ body}" by simp
  show "{❙Π⇘σ⇙ body} ⊆ Hset Φ"
    unfolding Forall_def using Hset_pi_iff[OF wB] inst by blast
  show "{❙Π⇘σ⇙ body} ⊢ S" by (rule drv)
  show "cwff 𝗈 S" by (rule cS)
qed

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›.›

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 "(g ❙≐⇘σ❙⇒τ⇙ h) ∈ Hset Φ"
  proof (rule Hset_forall_intro[OF wB inst])
    have "{❙Π⇘σ⇙ ?body} ⊢ ❙Π⇘σ⇙ ?body" by (auto intro: bprov.Hyp)
    thus "{❙Π⇘σ⇙ ?body} ⊢ g ❙≐⇘σ❙⇒τ⇙ h"
      using FuncE cwff_wff wg wh by blast
    show "cwff 𝗈 (g ❙≐⇘σ❙⇒τ⇙ h)" by (rule cwff_LeibE[OF wg wh])
  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)
  ― ‹‹NK(f)› reduces to the literal singleton, ‹NK(ι)› describes it›
  have "(((Iota σ) ❙⋅ f) ❙≐⇘σ⇙ a) ∈ Hset Φ"
  proof (rule Hset_forall_intro[OF wB inst])
    let ?F = "{❙Π⇘σ⇙ ?body}"
    have fpF: "freep ?F" by (rule freep_finite) simp
    have PiD: "?F ⊢ ❙Π⇘σ⇙ ?body"
      by (auto intro: bprov.Hyp)
    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)" by (rule cwff_LeibE[OF wa wb])
  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
    show "{a ❙≐⇘σ⇙ b} ⊢ a ❙=⇘σ⇙ b"
      by (rule leib_to_peq[OF _ _ cwff_wff[OF wa] cwff_wff[OF wb]])
         (auto intro: bprov.Hyp freep_finite)
    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 Theorem 7.6)›

text ‹The maximal saturated extension ‹Hset Φ› --- BKK's Hintikka set; we use the two names
  interchangeably from here on --- 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 theory ‹Semantics›, 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).  A sentence denotes its own class --- under @{emph ‹any›}
  assignment, since a closed formula ignores it.  It denotes the truth value ‹cls ❙⊤› of the
  term model exactly when it belongs to ‹H›.›

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

end

subsubsection ‹Model existence, packaged: the term model›

text ‹A set that injects into the term type of a countable signature is countable.›

lemma countable_of_inj_on_tm:
  fixes rep :: "'a ⇒ 'p::countable tm"
  assumes "inj_on rep D" shows "countable D"
proof -
  have "inj_on (to_nat ∘ rep) D"
    by (rule comp_inj_on[OF assms]) (rule inj_on_subset[OF inj_to_nat subset_UNIV])
  thus ?thesis unfolding countable_def by blast
qed

text ‹The construction, packaged once: every consistent parameter-rich set ‹Φ› of sentences
  has a ‹Σ›-Henkin model --- the Hintikka term model, whose domains are ‹∼›-classes of
  closed wffs --- satisfying every member of ‹Φ› (the model-existence theorem, BKK
  Theorem 7.6).  The total domain injects into the term type, so over a countable signature
  it is countable (@{thm [source] countable_of_inj_on_tm}).  The refuting countermodel, the
  completeness theorem and the single-sentence model-existence form are all instances.›

theorem term_model_sat:
  fixes Φ :: "'p::infinite tm set"
  assumes con: "con Φ" and fp: "richp Φ" and sen: "⋀B. B ∈ Φ ⟹ cwff 𝗈 B"
  obtains Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set"
    and vl ξ and rep :: "'p tm set ⇒ 'p tm"
  where "bkk_model Dm Ap Ee vl" "inj_on rep {x. ∃τ. Dm τ x}"
        "app_struct.asg Dm ξ" "∀B∈Φ. vl (Ee ξ B)"
proof -
  interpret H: hintikka_model Φ 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.Eval (λa. a = H.cls ❙⊤)"
    by intro_locales
  ― ‹the term model satisfies every member of ‹Φ› by the truth lemma›
  have sat: "∀B∈Φ. H.V.Eval ξ B = H.cls ❙⊤"
    using H.truth_lemma sen Phi_sub_Hset[of Φ]
    by (auto simp: cwff_def)
  ― ‹the total domain injects into the term type: choose a representative of each class›
  have "{x. ∃τ. H.Dm τ x} ⊆ H.cls ` UNIV" by (auto simp: H.Dm_def)
  hence inj: "inj_on (inv_into UNIV H.cls) {x. ∃τ. H.Dm τ x}"
    by (rule inj_on_inv_into)
  show ?thesis by (rule that[OF bm inj ra]) (use sat in auto)
qed

text ‹The refuting instance: if ‹A› is not derivable @{emph ‹from›} a parameter-rich set ‹Φ›
  of closed sentences, the term model of ‹{❙¬A} ∪ Φ› satisfies every hypothesis yet refutes ‹A› ---
  the abstract negation law @{thm [source] sigma_model.sat_Neg} turns satisfaction of
  ‹❙¬A› into refutation of ‹A›.›

lemma refuting_term_model_hyps:
  fixes Φ :: "'p::infinite tm set" and A :: "'p tm"
  assumes c: "cwff 𝗈 A" and fp: "richp Φ" and sen: "⋀B. B ∈ Φ ⟹ cwff 𝗈 B"
      and nd: "¬ Φ ⊢ A"
  obtains Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set"
    and vl ξ and rep :: "'p tm set ⇒ 'p tm"
  where "bkk_model Dm Ap Ee vl" "inj_on rep {x. ∃τ. Dm τ x}"
        "app_struct.asg Dm ξ" "∀B∈Φ. vl (Ee ξ B)" "¬ vl (Ee ξ A)"
proof -
  note wA = cwff_wff[OF c]
  let ?Ψ = "insert (❙¬ A) Φ"
  have conΨ: "con ?Ψ" using bprov.simps con_def nd wA by fastforce
  have fpΨ: "richp ?Ψ" by (rule richp_add[OF fp])
  have cN: "cwff 𝗈 (❙¬ A)" using c by (auto simp: cwff_def intro!: wff_Not)
  have senΨ: "⋀B. B ∈ ?Ψ ⟹ cwff 𝗈 B" using sen cN by auto
  obtain Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set"
    and vl ξ and rep :: "'p tm set ⇒ 'p tm"
    where bm: "bkk_model Dm Ap Ee vl" and inj: "inj_on rep {x. ∃τ. Dm τ x}"
      and xi: "app_struct.asg Dm ξ" and sat: "∀B∈?Ψ. vl (Ee ξ B)"
    using term_model_sat[OF conΨ fpΨ senΨ] .
  interpret M: bkk_model Dm Ap Ee vl by (rule bm)
  have ref: "¬ vl (Ee ξ A)" using sat M.sat_Neg[OF wA xi] by auto
  show ?thesis by (rule that[OF bm inj xi]) (use sat ref in auto)
qed

text ‹The positive counterpart: the model-existence half of Henkin completeness.  From the
  @{emph ‹consistency›} of a single sentence ‹A› one obtains a ‹Σ›-Henkin model with
  @{emph ‹countable›} total domain (the term model) that @{emph ‹satisfies›} ‹A›.  This
  holds for @{emph ‹any›} consistent sentence --- an axiom of infinity included --- and
  stays entirely within plain HOL: the carrier is the type \<^typ>‹'p tm set›, the domains
  are the ‹∼›-classes of closed wffs, so the total domain is countable, and no
  set-theoretic universe is involved.  A stronger meta-theory can thus be needed only to establish the consistency
  premise (for an axiom without finite models), never for the model construction.›

theorem countable_henkin_sat:
  fixes A :: "'p::{countable,infinite} tm"
  assumes cA: "cwff 𝗈 A" and con: "con {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 -
  have fp: "richp {A}"
    unfolding richp_iff_freep by (intro freep_finite) simp
  obtain Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set"
    and vl ξ and rep :: "'p tm set ⇒ 'p tm"
    where M: "bkk_model Dm Ap Ee vl" and inj: "inj_on rep {x. ∃τ. Dm τ x}"
      and xi: "app_struct.asg Dm ξ" and sat: "∀B∈{A}. vl (Ee ξ B)"
    by (rule term_model_sat[OF con fp]) (use cA in auto)
  have cnt: "countable {x. ∃τ. Dm τ x}" by (rule countable_of_inj_on_tm[OF inj])
  show ?thesis by (rule that[OF M cnt xi]) (use sat in auto)
qed

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 ‹ℳ⇘βfb⇙›, cf.\ Andrews 1972): a sentence that is
  valid in every such model of a sufficiently ‹Σ›-pure set of
  sentences ‹Φ› (it suffices to assume validity over the models carried by ‹'p tm set› --- in
  particular the term model) is derivable from ‹Φ›.  Like BKK, who allow signatures of any
  infinite cardinality ‹ℵ⇩s› (BKK Remark 3.16), we admit an arbitrary infinite type of
  parameter names; purity is then the parameter-rich ‹richp›, which over a countable
  signature is the familiar ‹freep› (BKK Definition 6.3).  The proof
  is by contraposition, BKK's argument: if ‹Φ ⊢ A› fails, the refuting term model
  satisfies ‹Φ› but refutes ‹A›, contradicting validity.›

text ‹The theorem is stated after its generalisation to arbitrary carriers below, of which it
  is the instance at the term carrier.  Its statement follows the initial release of this
  entry (August 2026), except for the three changes listed in the document's compatibility
  paragraph: the hypothesis-relative premise, ‹richp› in place of ‹freep›, and no
  countability constraint on the signature.›

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 a satisfaction-equivalent copy on ‹'u›.  The
  term model's total domain injects into the term
  type, and ‹|'p tm| ≤ |'p|› over an infinite signature, so the term model embeds into
  every carrier at least as large as the signature --- over a countable signature, into
  every infinite carrier --- and validity there suffices for derivability.  Completeness is then
  extended further, to open formulas, to signatures with infinitely many parameters, and to
  derivation from hypotheses, and the development closes with the main theorems stated in
  self-contained notation.›

subsubsection ‹Model embedding: satisfaction is carrier-independent›

text ‹A ‹Σ›-model over a carrier ‹'v› whose total domain maps injectively into a
  carrier ‹'u› has a satisfaction-equivalent copy over ‹'u›.  The lemma is stated in the
  form used below, for a refuted formula ‹A›; the copy itself does not depend on ‹A›.
  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)"
        "⋀B. wff⇘𝗈⇙(B) ⟹ vl' (Ee' ξ' B) = vl (Ee ξ B)"
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 agrees with the original on every formula, so satisfaction
     (and the refutation of ‹A›) transfers›
  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 push: "Ee' ξ' B = i (Ee ξ B)" for B by (simp add: Ee'_def ξ'_def pull_push)
  have agree: "vl' (Ee' ξ' B) = vl (Ee ξ B)" if "wff⇘𝗈⇙(B)" for B
    by (simp add: push vl'I[OF DmD[OF M.ev_type[OF that xi]]])
  have nA': "¬ vl' (Ee' ξ' A)" using nA agree[OF wA] by simp
  show ?thesis by (rule that[OF BM asg' nA' agree])
qed

subsubsection ‹Completeness at every infinite carrier›

text ‹The strengthened form of BKK Corollary 7.7: consequence over the models of
  ‹ℳ⇘βfb⇙› at a value carrier @{emph ‹at least as large as the signature›} implies
  derivability.  The term carrier plays no special role: it only needs to embed into the
  given carrier --- its total domain injects into ‹'p tm›, and ‹|'p tm| ≤ |'p| ≤ |'u|› ---
  and the embedding preserves the satisfaction of ‹Φ› and the refutation of ‹A›.  The
  cardinality link is stated as an injection ‹emb :: 'p ⇒ 'u›; over a countable signature
  every infinite carrier qualifies, which recovers the every-carrier form below.›

theorem completeness_hyps_rich:
  fixes Φ :: "'p::infinite tm set" and A :: "'p tm" and emb :: "'p ⇒ 'u"
  assumes emb: "inj emb" and c: "cwff 𝗈 A" and fp: "richp Φ"
      and sen: "⋀B. B ∈ Φ ⟹ cwff 𝗈 B"
      and valid: "Φ ⊨('u) 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 ξ and rep :: "'p tm set ⇒ 'p tm"
    where M: "bkk_model Dm Ap Ee vl" and injr: "inj_on rep {x. ∃τ. Dm τ x}"
      and xi: "app_struct.asg Dm ξ" and sat: "∀B∈Φ. vl (Ee ξ B)"
      and nA: "¬ vl (Ee ξ A)"
    by (rule refuting_term_model_hyps[OF c fp sen nd])
  ― ‹embed the total domain into the carrier ‹'u›, via ‹|'p tm| ≤ |'p| ≤ |'u|››
  have "|UNIV :: 'p set| ≤o |UNIV :: 'u set|"
    using card_of_ordLeq emb by auto
  hence "|UNIV :: 'p tm set| ≤o |UNIV :: 'u set|"
    using card_of_tm ordLeq_transitive by blast
  then obtain g :: "'p tm ⇒ 'u" where g: "inj g"
    by (meson card_of_ordLeq)
  have inj: "inj_on (g ∘ rep) {x. ∃τ. Dm τ x}"
    using injr 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 M': "bkk_model Dm' Ap' Ee' vl'" and asg': "app_struct.asg Dm' ξ'"
      and nA': "¬ vl' (Ee' ξ' A)"
      and agree: "⋀B. wff⇘𝗈⇙(B) ⟹ vl' (Ee' ξ' B) = vl (Ee ξ B)"
    by (rule bkk_model_embed[OF M inj cwff_wff[OF c] xi nA]) (rule that)
  ― ‹the image model still satisfies every hypothesis›
  have satw': "∀B∈Φ. wff 𝗈 B ∧ vl' (Ee' ξ' B)"
  proof
    fix B assume B: "B ∈ Φ"
    have wB: "wff 𝗈 B" using cwff_wff[OF sen[OF B]] .
    have "vl' (Ee' ξ' B) = vl (Ee ξ B)" by (rule agree[OF wB])
    moreover have "vl (Ee ξ B)" using sat B by blast
    ultimately show "wff 𝗈 B ∧ vl' (Ee' ξ' B)" using wB by simp
  qed
  ― ‹so validity of ‹A› forces it to hold, contradicting the refutation›
  have "vl' (Ee' ξ' A)"
    using valid M' asg' satw'
    unfolding bkk_consequence_def rel_truth_def by blast
  thus False using nA' by simp
qed

subsubsection ‹Signature transport›

text ‹On the syntactic side, transport is by @{emph ‹retraction›}: any finite parameter
  support relocates injectively into ‹ℕ› and back, ‹g ∘ h› being the identity on the
  support, so ‹prn g ∘ prn h› fixes the terms and contexts concerned.  Two retractions are
  used: into a copy of ‹ℕ› (‹nat_retract›, for finite contexts) and, along an arbitrary
  injection of the signature into itself, within the signature (‹inj_finite_retract›, for
  ‹completeness_fprov›).›

lemma nat_retract:
  fixes P :: "'p::infinite set"
  assumes fin: "finite P"
  shows "∃(g :: nat ⇒ 'p) h. inj g ∧ (∀p ∈ P. g (h p) = p)"
proof -
  obtain g0 :: "nat ⇒ 'p" where g0: "inj g0"
    using infinite_UNIV infinite_countable_subset by blast
  define S where "S = P ∪ 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 cS: "countable S" and iS: "infinite S"
    unfolding S_def using rc ri fin by (auto intro: countable_finite)
  define g where "g = from_nat_into S"
  have g: "inj g" and cover: "P ⊆ range g"
    using bij_betw_from_nat_into[OF cS iS]
    unfolding g_def bij_betw_def S_def by auto
  define h :: "'p ⇒ nat" where "h = (λp. SOME n. g n = p)"
  have gh: "g (h p) = p" if "p ∈ P" 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
  show ?thesis using g gh by blast
qed

lemma prn_retract:
  assumes "⋀p. p ∈ pars A ⟹ g (h p) = p"
  shows "prn g (prn h A) = A"
  by (simp add: assms prn_cong prn_prn)

lemma prn_retract_set:
  assumes "⋀p. p ∈ usedp Φ ⟹ g (h p) = p"
  shows "prn g ` prn h ` Φ = Φ"
proof -
  have "prn g (prn h B) = B" if "B ∈ Φ" for B
    by (rule prn_retract) (use assms that in ‹auto simp: usedp_def›)
  thus ?thesis by (force simp: image_image)
qed

text ‹Retraction along an @{emph ‹arbitrary›} injection into the same signature: an
  injective renaming ‹g› that undoes a given injection ‹h› on any finite support.  On the
  support, ‹g› inverts ‹h›; away from it, the two cofinite remainders have full
  cardinality, so they inject into each other without touching the support's values.›

lemma inj_finite_retract:
  fixes h :: "'p::infinite ⇒ 'p"
  assumes injh: "inj h" and fin: "finite P"
  shows "∃g :: 'p ⇒ 'p. inj g ∧ (∀p ∈ P. g (h p) = p)"
proof -
  define Q where "Q = h ` P"
  have finQ: "finite Q" using fin by (simp add: Q_def)
  have "|UNIV :: 'p set| ≤o |UNIV :: 'p set|"
    by (rule ordLeq_reflexive[OF card_of_Well_order])
  hence "|UNIV :: 'p set| ≤o |UNIV - P :: 'p set|"
    using card_of_diff_finite[OF _ fin] by fastforce
  hence "|UNIV - Q :: 'p set| ≤o |UNIV - P :: 'p set|"
    using card_of_mono1[of "UNIV - Q" UNIV] ordLeq_transitive by blast
  then obtain k :: "'p ⇒ 'p"
    where k: "inj_on k (UNIV - Q)" and rk: "k ` (UNIV - Q) ⊆ UNIV - P"
    using card_of_ordLeq[THEN iffD2] by blast
  define g where "g = (λx. if x ∈ Q then inv_into P h x else k x)"
  have gh: "g (h p) = p" if "p ∈ P" for p
    using that inv_into_f_f[OF inj_on_subset[OF injh subset_UNIV]]
    by (auto simp: g_def Q_def)
  have "inj g"
  proof (rule injI)
    fix x y assume e: "g x = g y"
    have inP: "g z ∈ P" if "z ∈ Q" for z
      using that inv_into_into[of z h P] by (auto simp: g_def Q_def)
    have notP: "g z ∉ P" if "z ∉ Q" for z
      using that rk by (auto simp: g_def)
    consider "x ∈ Q" "y ∈ Q" | "x ∉ Q" "y ∉ Q" | "x ∈ Q" "y ∉ Q" | "x ∉ Q" "y ∈ Q"
      by blast
    thus "x = y"
    proof cases
      case 1 thus ?thesis
        using e inj_on_inv_into[of Q h P] by (auto simp: g_def Q_def inj_on_def)
    next
      case 2 thus ?thesis using e k by (auto simp: g_def inj_on_def)
    next
      case 3 thus ?thesis using e inP notP by metis
    next
      case 4 thus ?thesis using e inP notP by metis
    qed
  qed
  thus ?thesis using gh by blast
qed

subsubsection ‹Arbitrary parameter-rich contexts: discharging the free-variable stock›

text ‹Finally the restriction to a @{emph ‹finite›} context is lifted: an arbitrary
  parameter-rich context of open formulas is admissible.  With infinitely many typed free
  variables there is no finite measure for an induction over single variables, so all free
  variables are replaced by parameters at once, by the closure ‹vpar S π› of theory
  ‹Syntax› (the parameter-valued instance of the simultaneous substitution
  @{const msub}).  The proof has four steps.  (1) An injective ‹π› assigning pairwise
  distinct fresh parameters to the countably many typed variables exists because
  ‹richp Φ› provides unused parameters as numerous as the signature: an injection of
  ‹'p + ℕ› into them is split, its ‹ℕ›-part defines ‹π›, and its ‹'p›-part remains
  unused and keeps the closed image parameter-rich.  (2) The substitution-value law
  @{thm [source] sigma_eval.ev_vpar} of theory ‹Semantics› transports the semantic
  consequence to the closed image, where @{thm [source] completeness_hyps_rich} yields a
  derivation.  (3) That derivation is finite (@{thm [source] bprov_finite}), so it uses
  only finitely many of the new parameters, and @{thm [source] bprov_pvar} turns them back
  into variables one at a time (@{thm [source] pvar_vpar}).  (4) Weakening restores the
  full context.›

text ‹Syntactic inversion: a derivation of the closed image over a @{emph ‹finite›} stock of
  substituted variables is undone by @{thm [source] bprov_pvar}, one parameter at a time.›

lemma bprov_vpar_invert:
  assumes inj: "⋀n τ x σ. π n τ = π x σ ⟹ n = x ∧ τ = σ"
      and fr: "⋀B n σ. B ∈ insert A Ψ ⟹ π n σ ∉ pars B"
  shows "finite W ⟹ vpar W π ` Ψ ⊢ vpar W π A ⟹ Ψ ⊢ A"
proof (induction rule: finite_induct)
  case empty
  have e: "vpar {} π t = t" for t by (simp add: vpar_id)
  show ?case using empty.prems unfolding e by (simp add: image_ident)
next
  case (insert p W)
  obtain x σ where p: "p = (x, σ)" by (cases p) auto
  have injx: "⋀n τ. π n τ = π x σ ⟹ n = x ∧ τ = σ" using inj by blast
  have inv: "pvar (π x σ) σ x (vpar (insert p W) π B) = vpar W π B"
    if B: "B ∈ insert A Ψ" for B
  proof -
    have W: "insert p W - {(x, σ)} = W" using insert.hyps(2) p by auto
    have "pvar (π x σ) σ x (vpar (insert p W) π B) = vpar (insert p W - {(x, σ)}) π B"
      by (rule pvar_vpar[OF injx fr[OF B]])
    thus ?thesis unfolding W .
  qed
  have "pvar (π x σ) σ x ` (vpar (insert p W) π ` Ψ)
      ⊢ pvar (π x σ) σ x (vpar (insert p W) π A)"
    by (rule bprov_pvar[OF insert.prems])
  moreover have "pvar (π x σ) σ x ` (vpar (insert p W) π ` Ψ) = vpar W π ` Ψ"
    unfolding image_image by (rule image_cong[OF HOL.refl]) (rule inv, blast)
  moreover have "pvar (π x σ) σ x (vpar (insert p W) π A) = vpar W π A"
    by (rule inv) blast
  ultimately have "vpar W π ` Ψ ⊢ vpar W π A" by simp
  thus ?case by (rule insert.IH)
qed

text ‹Hypothesis-relative completeness in full generality: an arbitrary parameter-rich
  context of open formulas, with no finiteness condition of any kind, at @{emph ‹any›}
  infinite signature --- the carrier need only be at least as large as the signature.  The reserve
  is split in two by an injection ‹j› of ‹'p + ℕ› into it: the ‹ℕ›-half supplies the
  pairwise distinct fresh parameters that close the free variables, the ‹'p›-half is
  untouched by the closure and keeps the closed image parameter-rich.›

theorem completeness_hyps_open_rich:
  fixes Φ :: "'p::infinite tm set" and A :: "'p tm" and emb :: "'p ⇒ 'u"
  assumes emb: "inj emb" and wA: "wff⇘𝗈⇙(A)" and fp: "richp Φ"
      and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
      and valid: "Φ ⊨('u) A"
    shows "Φ ⊢ A"
proof -
  ― ‹the reserve stays full-size after removing the parameters of ‹A››
  have rA: "|UNIV :: 'p set| ≤o |- usedp Φ - pars A|"
    by (rule card_of_diff_finite[OF fp[unfolded richp_def] finite_pars])
  ― ‹split it: an injection of ‹'p + ℕ› into the reserve›
  have "|(UNIV :: 'p set) <+> (UNIV :: nat set)| =o |UNIV :: 'p set|"
    using card_of_Plus_infinite[OF infinite_UNIV]
          infinite_iff_card_of_nat[of "UNIV :: 'p set"] infinite_UNIV by blast
  hence "|UNIV :: ('p + nat) set| ≤o |- usedp Φ - pars A|"
    using rA unfolding UNIV_Plus_UNIV
    by (meson ordIso_imp_ordLeq ordLeq_transitive)
  from card_of_ordLeq[THEN iffD2, OF this]
  obtain j :: "'p + nat ⇒ 'p" where injj: "inj j"
      and rj: "range j ⊆ - usedp Φ - pars A"
    by blast
  define f :: "nat ⇒ 'p" where "f = (λn. j (Inr n))"
  have injf: "inj f" using injj by (auto simp: f_def inj_on_def)
  have rf: "range f ⊆ - usedp Φ - pars A" using rj by (auto simp: f_def)
  define π :: "nat ⇒ ty ⇒ 'p" where "π = (λn σ. f (to_nat (n, σ)))"
  have injπ: "n = x ∧ τ = σ" if "π n τ = π x σ" for n τ x σ
    using injD[OF injf that[unfolded π_def]] by simp
  have freshΦ: "π n σ ∉ usedp Φ" and freshA: "π n σ ∉ pars A" for n σ
    using rf unfolding π_def by auto
  ― ‹the closed image is a parameter-rich context of sentences›
  define Φc where "Φc = vpar UNIV π ` Φ"
  have cA: "cwff 𝗈 (vpar UNIV π A)" by (rule cwff_vpar[OF wA])
  have cB: "cwff 𝗈 B'" if B': "B' ∈ Φc" for B'
  proof -
    obtain B where B: "B ∈ Φ" and eq: "B' = vpar UNIV π B"
      using B' unfolding Φc_def by auto
    show ?thesis unfolding eq by (rule cwff_vpar[OF wΦ[OF B]])
  qed
  have fpc: "richp Φc"
  proof -
    have sub: "range (λp. j (Inl p)) ⊆ - usedp Φc"
    proof
      fix q assume "q ∈ range (λp. j (Inl p))"
      then obtain p where q: "q = j (Inl p)" by auto
      have "q ∉ pars B'" if B': "B' ∈ Φc" for B'
      proof
        assume qp: "q ∈ pars B'"
        obtain B where B: "B ∈ Φ" and B'B: "B' = vpar UNIV π B"
          using B' unfolding Φc_def by auto
        have dis: "q ∈ pars B ∨ (∃n σ'. q = π n σ')"
          using qp unfolding B'B by (rule pars_vpar)
        have nB: "q ∉ pars B" using rj q B by (auto simp: usedp_def)
        have nπ: "q ≠ π n σ'" for n σ'
          using injD[OF injj] q by (auto simp: π_def f_def)
        show False using dis nB nπ by blast
      qed
      thus "q ∈ - usedp Φc" by (auto simp: usedp_def)
    qed
    have inj1: "inj (λp. j (Inl p))" using injj by (auto simp: inj_on_def)
    have "|UNIV :: 'p set| ≤o |- usedp Φc|"
      by (rule card_of_ordLeq[THEN iffD1]) (use sub inj1 in blast)
    thus ?thesis by (simp add: richp_def)
  qed
  ― ‹transport the consequence and apply the closed parameter-rich completeness›
  have vc: "Φc ⊨('u) vpar UNIV π A"
    unfolding Φc_def by (rule bkk_consequence_vpar[OF valid wΦ wA])
  have dc: "Φc ⊢ vpar UNIV π A"
    by (rule completeness_hyps_rich[OF emb cA fpc cB vc])
  ― ‹the derivation is finite, so it lives over a finite subcontext›
  obtain Φ⇩0 where fin0: "finite Φ⇩0" and sub0: "Φ⇩0 ⊆ Φc" and d0: "Φ⇩0 ⊢ vpar UNIV π A"
    using bprov_finite[OF dc] by blast
  obtain Ψ where subΨ: "Ψ ⊆ Φ" and finΨ: "finite Ψ" and im: "Φ⇩0 = vpar UNIV π ` Ψ"
    using finite_subset_image[OF fin0 sub0[unfolded Φc_def]] by blast
  ― ‹restrict the closure to the finitely many occurring variables and invert them›
  define W where "W = occ A ∪ (⋃B∈Ψ. occ B)"
  have finW: "finite W" unfolding W_def using finΨ finite_occ by auto
  have "occ A ⊆ W" unfolding W_def by blast
  hence eqA: "vpar UNIV π A = vpar W π A" by (rule vpar_cong[symmetric])
  have eqB: "vpar UNIV π B = vpar W π B" if B: "B ∈ Ψ" for B
  proof -
    have "occ B ⊆ W" unfolding W_def using B by blast
    thus ?thesis by (rule vpar_cong[symmetric])
  qed
  have imΨ: "vpar UNIV π ` Ψ = vpar W π ` Ψ" by (rule image_cong[OF HOL.refl eqB])
  have dW: "vpar W π ` Ψ ⊢ vpar W π A" using d0 unfolding im imΨ eqA .
  have fr: "π n σ ∉ pars B" if "B ∈ insert A Ψ" for B n σ
    using freshΦ freshA subΨ that by (auto simp: usedp_def)
  have "Ψ ⊢ A" by (rule bprov_vpar_invert[OF injπ fr finW dW])
  thus ?thesis by (rule bprov_weaken[OF _ subΨ richp_freep[OF fp]])
qed

text ‹Over a countable signature every infinite carrier is admissible and ‹richp› is
  ‹freep›, so the classical statement follows; its closed, empty-context and
  finite-context forms are the corollary ladder below.›

theorem completeness_hyps_open_full:
  fixes Φ :: "'p::{countable,infinite} tm set" and A :: "'p tm"
  assumes wA: "wff⇘𝗈⇙(A)" and fp: "freep Φ"
      and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
      and valid: "Φ ⊨('u::infinite) A"
    shows "Φ ⊢ A"
proof -
  obtain g :: "nat ⇒ 'u" where g: "inj g"
    using infinite_UNIV infinite_countable_subset by blast
  have emb: "inj (λp :: 'p. g (to_nat p))"
    by (auto simp: inj_on_def dest!: injD[OF g])
  show ?thesis
    by (rule completeness_hyps_open_rich[OF emb wA iffD2[OF richp_iff_freep fp] wΦ valid])
qed

subsubsection ‹Hypothesis-relative completeness without purity›

text ‹For the hypothesis relation ‹⊩› even the parameter reserve disappears: an
  @{emph ‹arbitrary›} context of open formulas is admitted, over any carrier at least as
  large as the signature.  The reserve is created rather than assumed --- the signature
  folds injectively into one half of itself (‹|'p + 'p| = |'p|›), the untouched half makes
  the image context parameter-rich, and @{thm [source] completeness_hyps_open_rich}
  applies.  The resulting derivation is finite, so it retracts along the fold
  (@{thm [source] inj_finite_retract}) to a derivation from a finite part of the original
  context --- which is exactly ‹Φ ⊩ A›.  Semantic compactness of the Henkin consequence
  thus needs no ultraproducts: it falls out of this theorem together with soundness
  (‹Main_Results›).›

theorem completeness_fprov:
  fixes Φ :: "'p::infinite tm set" and A :: "'p tm" and emb :: "'p ⇒ 'u"
  assumes emb: "inj emb" and wA: "wff⇘𝗈⇙(A)"
      and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
      and valid: "Φ ⊨('u) A"
    shows "Φ ⊩ A"
proof -
  ― ‹fold the signature into one half of itself; the other half is an untouched reserve›
  obtain h :: "'p ⇒ 'p" where injh: "inj h" and res: "|UNIV :: 'p set| ≤o |- range h|"
    using signature_fold by blast
  define Φ' where "Φ' = prn h ` Φ"
  have rich': "richp Φ'"
  proof -
    have "usedp Φ' ⊆ range h" by (auto simp: Φ'_def usedp_def tm.set_map)
    hence "|- range h| ≤o |- usedp Φ'|" by (intro card_of_mono1) auto
    thus ?thesis unfolding richp_def using res ordLeq_transitive by blast
  qed
  ― ‹transport validity and well-formedness along the fold›
  have valid': "Φ' ⊨('u) prn h A"
    unfolding Φ'_def by (rule bkk_consequence_map[OF valid wΦ])
  have wA': "wff⇘𝗈⇙(prn h A)" by (rule wff_prn[OF wA])
  have wΦ': "⋀B'. B' ∈ Φ' ⟹ wff⇘𝗈⇙(B')"
    by (auto simp: Φ'_def intro: wff_prn wΦ)
  ― ‹complete over the image and extract the finite kernel of the derivation›
  have "Φ' ⊢ prn h A"
    by (rule completeness_hyps_open_rich[OF emb wA' rich' wΦ' valid'])
  then obtain Ψ0 where finΨ: "finite Ψ0" and subΨ: "Ψ0 ⊆ Φ'"
      and dΨ: "Ψ0 ⊢ prn h A"
    using bprov_finite by blast
  obtain Φ⇩0 where subΦ: "Φ⇩0 ⊆ Φ" and finΦ: "finite Φ⇩0" and im: "Ψ0 = prn h ` Φ⇩0"
    using finite_subset_image[OF finΨ subΨ[unfolded Φ'_def]] by blast
  ― ‹retract the finite derivation back along the fold›
  define P where "P = pars A ∪ usedp Φ⇩0"
  have finP: "finite P"
    unfolding P_def usedp_def using finΦ finite_pars by auto
  obtain g :: "'p ⇒ 'p" where injg: "inj g" and gh: "∀p ∈ P. g (h p) = p"
    using inj_finite_retract[OF injh finP] by blast
  have "prn g ` Ψ0 ⊢ prn g (prn h A)" by (rule bprov_rename[OF injg dΨ])
  moreover have "prn g (prn h A) = A"
    by (rule prn_retract) (use gh in ‹auto simp: P_def›)
  moreover have "prn g ` Ψ0 = Φ⇩0"
    unfolding im by (rule prn_retract_set) (use gh in ‹auto simp: P_def›)
  ultimately have "Φ⇩0 ⊢ A" by simp
  thus ?thesis using finΦ subΦ by (rule fprovI[rotated 2])
qed

subsubsection ‹The exported corollary ladder›

text ‹First the finite-context forms at every infinite signature, then the completeness forms
  of the initial release of this entry (August 2026) as their instances: over a countable signature
  every infinite carrier is admissible, open formulas need no closure, and a finite context
  is automatically pure.›

theorem completeness_hyps_open_finite_countable:
  fixes Φ :: "'p::{countable,infinite} tm set" and A :: "'p tm"
  assumes fin: "finite Φ"
      and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
      and wA: "wff⇘𝗈⇙(A)"
      and valid: "Φ ⊨('u::infinite) A"
    shows "Φ ⊢ A"
  by (rule completeness_hyps_open_full[OF wA freep_finite[OF fin] wΦ valid])

text ‹The same at every infinite signature.  A finite context and its conclusion mention
  only finitely many parameters, so the problem relocates into a copy of ‹ℕ› inside ‹'p›
  and ‹bprov_rename› transports the derivation back.  Countability of ‹'p› thus drops out,
  and only ‹'p› infinite remains.›

theorem completeness_hyps_open_finite:
  fixes Φ :: "'p::infinite tm set" and A :: "'p tm"
  assumes fin: "finite Φ"
      and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
      and wA: "wff⇘𝗈⇙(A)"
      and v: "Φ ⊨('u::infinite) A"
    shows "Φ ⊢ A"
proof -
  have finP: "finite (pars A ∪ usedp Φ)" using fin by (simp add: usedp_def)
  obtain g :: "nat ⇒ 'p" and h where g: "inj g"
      and gh: "∀p ∈ pars A ∪ usedp Φ. g (h p) = p"
    using nat_retract[OF finP] by blast
  ― ‹into the countable subsignature›
  have finN: "finite (prn h ` Φ)" using fin by simp
  have wNΦ: "wff⇘𝗈⇙(B')" if "B' ∈ prn h ` Φ" for B' :: "nat tm"
    using that wΦ by (auto intro: wff_prn)
  have wN: "wff⇘𝗈⇙(prn h A)" by (rule wff_prn[OF wA])
  have vN: "prn h ` Φ ⊨('u) (prn h A :: nat tm)"
    by (rule bkk_consequence_map[OF v wΦ])
  have dN: "prn h ` Φ ⊢ (prn h A :: nat tm)"
    by (rule completeness_hyps_open_finite_countable[OF finN wNΦ wN vN])
  ― ‹and back along ‹g››
  have "prn g ` (prn h ` Φ) ⊢ prn g (prn h A)"
    by (rule bprov_rename[OF g dN])
  moreover have "prn g (prn h A) = A"
    by (rule prn_retract) (use gh in auto)
  moreover have "prn g ` prn h ` Φ = Φ"
    by (rule prn_retract_set) (use gh in auto)
  ultimately show ?thesis by simp
qed

text ‹The empty-context instance: completeness for every signature with infinitely many
  parameters.  (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 -
  have v0: "{} ⊨('u) A" using v by (simp add: bkk_valid_def bkk_consequence_def)
  show ?thesis
    by (rule completeness_hyps_open_finite[OF _ _ wA v0]) auto
qed

text ‹The forms of the initial release.  ‹completeness› is BKK's Corollary 7.7 proper --- consequence over
  the term carrier, for a parameter-rich context of sentences --- and the instance of
  ‹completeness_hyps_rich› at the injection ‹p ↦ {p⇧p⇘ι⇙}› of the signature into the term
  carrier.›

lemma inj_par_singleton: "inj (λp :: 'p. {p⇧p⇘ι⇙} :: 'p tm set)"
  by (simp add: inj_on_def)

theorem completeness:
  fixes Φ :: "'p::infinite tm set" and A :: "'p tm"
  assumes c: "cwff 𝗈 A" and fp: "richp Φ"
      and valid: "Φ ⊨('p tm set) A"
      and sen: "⋀B. B ∈ Φ ⟹ cwff 𝗈 B"
  shows "Φ ⊢ A"
  by (rule completeness_hyps_rich[OF inj_par_singleton c fp sen valid])

theorem completeness_open_at_any_carrier:
  fixes A :: "'p::{countable,infinite} tm"
  assumes wA: "wff⇘𝗈⇙(A)" and valid: "⊨('u::infinite) A"
  shows "⊢ A"
  by (rule completeness_at_any_signature[OF wA valid])

theorem completeness_open:
  fixes A :: "'p::{countable,infinite} tm"
  assumes wA: "wff⇘𝗈⇙(A)" and valid: "⊨('p tm set) A"
  shows "⊢ A"
proof -
  have v0: "{} ⊨('p tm set) A"
    using valid by (simp add: bkk_valid_def bkk_consequence_def)
  have rp: "richp ({} :: 'p tm set)" by (simp add: richp_iff_freep freep_finite)
  show ?thesis by (rule completeness_hyps_open_rich[OF inj_par_singleton wA rp _ v0]) simp
qed

text ‹The closed-formula equivalence of the initial release, its statement verbatim; the open-formula
  strengthening is ‹completeness_open› above together with ‹soundness_valid›.›

theorem derivable_iff_valid:
  fixes A :: "'p::{countable,infinite} tm"
  assumes "cwff 𝗈 A"
  shows "⊢ A ⟷ ⊨('p tm set) A"
  using completeness_open[OF cwff_wff[OF assms]] soundness_valid by blast

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 -
  have fp: "richp ({} :: 'p tm set)"
    by (simp add: richp_iff_freep freep_finite)
  obtain Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set"
      and vl ξ and rep :: "'p tm set ⇒ 'p tm"
    where M: "bkk_model Dm Ap Ee vl" and inj: "inj_on rep {x. ∃τ. Dm τ x}"
      and xi: "app_struct.asg Dm ξ" and "∀B∈({} :: 'p tm set). vl (Ee ξ B)"
      and nA: "¬ vl (Ee ξ A)"
    by (rule refuting_term_model_hyps[OF c fp _ nd]) simp_all
  have cnt: "countable {x. ∃τ. Dm τ x}" by (rule countable_of_inj_on_tm[OF inj])
  show ?thesis by (rule that[OF M cnt xi nA])
qed

theorem completeness_at_any_carrier:
  fixes A :: "'p::{countable,infinite} tm"
  assumes c: "cwff 𝗈 A" and valid: "⊨('u::infinite) A"
  shows "⊢ A"
  by (rule completeness_at_any_signature[OF cwff_wff[OF c] valid])

text ‹The cardinality link between signature and carrier in the hypothesis forms is needed;
  the argument is informal and not formalised here.  Let the signature ‹'p› be strictly
  larger than the carrier ‹'u›, and let ‹Φ› consist of the inequations ‹{c⇩a ≠ c⇩b}›
  between ‹|'p|›-many parameter constants, indexed so that a reserve of ‹|'p|›-many
  parameters stays unused; then ‹Φ› is parameter-rich.  ‹Φ› is consistent, since every
  finite part has a finite model and derivability is finitary (the countable analogue is
  ‹con_Ineq› in ‹NK_Infinity›); in particular ‹Φ ⊢ ❙⊥› and ‹Φ ⊩ ❙⊥› both fail.  But
  no model over ‹'u› satisfies ‹Φ›, because its domains are subsets of ‹'u› and cannot
  keep ‹|'p|›-many constants apart; so ‹Φ ⊨('u) ❙⊥› holds vacuously.  Completeness at
  the carrier ‹'u› therefore fails for both hypothesis relations.

  Consequently the every-carrier form of completeness holds for finite contexts
  (@{thm [source] completeness_hyps_open_finite}) but not for contexts of unbounded size:
  there the carrier has to be at least as large as the signature, which is the premise
  ‹inj emb› of @{thm [source] completeness_fprov} and
  @{thm [source] completeness_hyps_open_rich}.  Over a countable signature every infinite
  carrier qualifies, and the every-carrier statement
  @{thm [source] completeness_hyps_open_full} is recovered.

  Whether the parameter-rich reserve of the ‹⊢›-level forms could be weakened to the
  merely infinite reserve ‹freep› is not settled here; the two coincide over countable
  signatures, and for the hypothesis relation ‹⊩› the question does not arise, since
  @{thm [source] completeness_fprov} assumes no purity at all.›

end