Theory Calculus

theory Calculus
  imports Syntax "HOL-Library.Infinite_Typeclass" "HOL-Eisbach.Eisbach"
begin

section ‹The natural-deduction calculus NK›

text ‹We formalise the calculus ‹NKβfb› of BKK (BKK Definition 7.1, Figures 6 and 7) --- the base
  system ‹NKβ› together with the extensional rules ‹NK(f)› and ‹NK(b)› --- extended by BKK's
  rules ‹NK(=r)› and ‹NK(=l)› for the primitive equality of our signature (BKK Figure 9,
  Remark 7.9) and by the description rule ‹NK(ι)›, an axiom scheme whose only premise is
  well-formedness, describing Leibniz singletons (beyond BKK, following Andrews 1972, their reference [3]).  BKK prove
  ‹NKβfb› sound and complete for the class of ‹Σ›-Henkin models ‹ℳβfb› (BKK Theorem 7.3,
  Theorem 7.6, Corollary 7.7), and sketch the extension by primitive equality in Remark 7.9; we
  prove the fully extended calculus sound and complete for the correspondingly enriched class (with
  primitive equality and description, theory ‹Semantics›).  The provability judgement ‹Φ ⊢ A› relates a set
  ‹Φ› of formulas to a formula ‹A›; the rules impose well-formedness where they need it, and
  closedness is nowhere required.  The eigenvariables of ‹NK(ΠI)› are @{emph ‹parameters›}
  (BKK's ‹wα›), called eigen-parameters below; unlike the free variables used only
  during evaluation, they never occur bound.›

subsection ‹Discharging well-formedness side conditions›

text ‹Nearly every derived rule and every derivation inside the calculus carries ‹wff›
  side conditions.  The Eisbach method ‹wffs› discharges the routine ones: the composite
  introduction rules are tried first --- the applied connectives ahead of raw application,
  so that ‹¬ A› is decomposed by ‹wff_Not› rather than mistyped as a bare application ---
  and the atoms close the leaves.›

method wffs =
  ((intro wff_Not wff_ImpB wff_AndB wff_AllN wff_ExN wff_Forall wff_PEq wff_LeibE
          wff_Leib wff_Eq wff_TrueB wff_FalseB wff_Iota wff_App)?;
   (rule wff_Fre wff_Par)?)

subsection ‹The inference rules of ‹NKβfb› (BKK Figures 6, 7 and 9)›

text ‹Following BKK we work with the primitive constants ‹¬›, ‹∨›, ‹Πα›, ‹=α› and ‹ια›;
  the remaining operators (‹⊃›, ‹⊥›, Leibniz equality ‹≐›) are defined.  The rule ‹NK(ΠI)›
  discharges an eigen-parameter ‹w› that must not occur in the context ‹Φ› or in the
  quantified predicate.›

inductive bprov :: "'p tm set ⇒ 'p tm ⇒ bool" (infix ‹⊢› 40) where
    Hyp:   "A ∈ Φ ⟹ Φ ⊢ A"  ― ‹BKK ‹NK(Hyp)››
  | Beta:  "A ≈⇘𝗈⇙ B ⟹ Φ ⊢ A ⟹ Φ ⊢ B"  ― ‹BKK ‹NK(β)››
  | NegI:  "Φ ∪ {A} ⊢ ⊥ ⟹ wff⇘𝗈⇙(A) ⟹ Φ ⊢ ¬ A"  ― ‹BKK ‹NK(¬I)››
  | NegE:  "Φ ⊢ ¬ A ⟹ Φ ⊢ A ⟹ wff⇘𝗈⇙(C) ⟹ Φ ⊢ C"  ― ‹BKK ‹NK(¬E)››
  | DisIL: "Φ ⊢ A ⟹ wff⇘𝗈⇙(B) ⟹ Φ ⊢ A ∨ B"  ― ‹BKK ‹NK(∨IL)››
  | DisIR: "Φ ⊢ B ⟹ wff⇘𝗈⇙(A) ⟹ Φ ⊢ A ∨ B"  ― ‹BKK ‹NK(∨IR)››
  | DisE:  "Φ ⊢ A ∨ B ⟹ Φ ∪ {A} ⊢ C ⟹ Φ ∪ {B} ⊢ C
            ⟹ wff⇘𝗈⇙(A) ⟹ wff⇘𝗈⇙(B) ⟹ Φ ⊢ C"  ― ‹BKK ‹NK(∨E)››
  | PiI:   "Φ ⊢ G ⋅ (wp⇘α⇙) ⟹ wff⇘α⇒𝗈⇙(G) ⟹ w ∉ pars G
            ⟹ (∀D ∈ Φ. w ∉ pars D)
            ⟹ Φ ⊢ (Pi α) ⋅ G"  ― ‹BKK ‹NK(ΠI)››
  | PiE:   "Φ ⊢ (Pi α) ⋅ G ⟹ wff⇘α⇙(A) ⟹ Φ ⊢ G ⋅ A"  ― ‹BKK ‹NK(ΠE)››
  | Contr: "Φ ∪ {¬ A} ⊢ ⊥ ⟹ wff⇘𝗈⇙(A) ⟹ Φ ⊢ A"  ― ‹BKK ‹NK(Contr)››
  | FuncE: "Φ ⊢ Π⇘α⇙ (G ⋅ (Bnd 0) ≐⇘β⇙ H ⋅ (Bnd 0))
            ⟹ wff⇘α⇒β⇙(G) ⟹ wff⇘α⇒β⇙(H)
            ⟹ Φ ⊢ G ≐⇘α⇒β⇙ H"  ― ‹BKK ‹NK(f)››
  | BoolE: "Φ ∪ {A} ⊢ B ⟹ Φ ∪ {B} ⊢ A ⟹ wff⇘𝗈⇙(A) ⟹ wff⇘𝗈⇙(B)
            ⟹ Φ ⊢ A ≐⇘𝗈⇙ B"  ― ‹BKK ‹NK(b)››
  | Desc:  "wff⇘α⇙(A) ⟹ Φ ⊢ (Iota α) ⋅ ((Leib α) ⋅ A) ≐⇘α⇙ A"
      ― ‹‹NK(ι)›, beyond BKK: Leibniz-singleton description (Andrews 1972)›
  | EqR:   "wff⇘α⇙(A) ⟹ Φ ⊢ A =⇘α⇙ A"  ― ‹BKK ‹NK(=r)›, Figure 9›
  | EqL:   "Φ ⊢ C =⇘α⇙ D ⟹ Φ ⊢ C ≐⇘α⇙ D"  ― ‹BKK ‹NK(=l)›, Figure 9›

text ‹Provability from the empty hypothesis set, with its own turnstile.›

abbreviation provable :: "'p tm ⇒ bool"  (‹⊢ _› [61] 60) where
  "provable A ≡ {} ⊢ A"

text ‹Everything derivable from a set of propositions is a proposition.›

lemma bprov_wff: "Φ ⊢ C ⟹ (⋀ A . A ∈ Φ ⟹ wff⇘𝗈⇙(A)) ⟹ wff⇘𝗈⇙(C)"
  by (induct rule: bprov.induct) (auto intro: wff_Pi wff_App wff_Iota simp: beq_wffR)

text ‹Derivability is stable under injective parameter renaming --- injectivity keeps the
  eigen-parameter side-conditions of ‹NK(ΠI)›.  This lets us rename eigen-parameters apart,
  which is what makes weakening (and later, extension of consistent sets) admissible.›

lemma bprov_rename: assumes π: "inj π" shows "Φ ⊢ C ⟹ prn π ` Φ ⊢ prn π C"
proof (induction rule: bprov.induct)
  case PiI thus ?case
    by auto (smt (verit) assms bprov.PiI image_iff inj_image_mem_iff tm.set_map wff_prn)
qed(auto intro: bprov.intros)

subsection ‹Weakening›

text ‹Weakening is admissible.  BKK leave this structural property implicit (their contexts
  are sets and the rules mention the context only via membership and extension); in the
  formalisation the eigen-parameter condition of ‹NK(ΠI)› makes it a lemma that has to be proved.›

text ‹Transposing two parameters --- an involutive, injective renaming --- lets us shift an
  eigen-parameter to a fresh one when weakening the context.›

definition swp :: "'p ⇒ 'p ⇒ 'p ⇒ 'p" where
  "swp a b = (λx. if x = a then b else if x = b then a else x)"
lemma swp_inj: "inj (swp a b)" by (auto simp: swp_def inj_def)
lemma swp_swp [simp]: "swp a b (swp a b x) = x" by (auto simp: swp_def)
text ‹The next lemma, ‹swp_apply›, keeps its statement from the initial release of this
  entry (August 2026) (compatibility export).›

lemma swp_apply: "swp a b a = b" by (simp add: swp_def)
lemma prn_swp_swp [simp]: "prn (swp a b) (prn (swp a b) t) = t" by (simp add: prn_prn)
lemma image_prn_swp_swp [simp]: "prn (swp a b) ` (prn (swp a b) ` S) = S"
  by (simp add: image_image)

text ‹‹freep› is our rendering of BKK's @{emph ‹sufficiently ‹Σ›-pure›} (BKK Definition 6.3):
  since a parameter name may be used at every type, infinitely many unused names provide
  fresh witnesses at every type.›

definition usedp :: "'p tm set ⇒ 'p set" where "usedp Φ ≡ (⋃D ∈ Φ. pars D)"
definition freep :: "'p tm set ⇒ bool" where "freep Φ ≡ infinite (- usedp Φ)"
lemma usedp_insert: "usedp (insert A Φ) = pars A ∪ usedp Φ" by (auto simp: usedp_def)
lemma usedp_prn: "usedp (prn π ` Φ) = π ` usedp Φ" by (auto simp: usedp_def tm.set_map)
lemma bij_swp: "bij (swp a b)" by (simp add: involuntory_imp_bij)
lemma infinite_inj_image: "inj f ⟹ infinite A ⟹ infinite (f ` A)"
  by (metis finite_imageD inj_on_subset subset_UNIV)
lemma freep_add: "freep Φ ⟹ freep (insert A Φ)"
  by (simp add: usedp_insert freep_def)
     (metis finite_pars Diff_eq Diff_infinite_finite inf.commute)
lemma freep_un: "freep Φ ⟹ freep (Φ ∪ {A})"
  by (metis freep_add Un_insert_right sup_bot.right_neutral)
lemma freep_un_finite: "freep S ⟹ finite T ⟹ freep (S ∪ T)"
proof -
  assume "freep S" "finite T"
  hence "finite (usedp T)" by (auto simp: usedp_def)
  moreover have "- usedp (S ∪ T) = - usedp S - usedp T"
    by (auto simp: usedp_def)
  ultimately show ?thesis using ‹freep S›
    by (metis freep_def Diff_infinite_finite)
qed
lemma freep_fresh: "freep Φ ⟹ finite F ⟹ ∃w. w ∉ usedp Φ ∧ w ∉ F" 
  by (meson ComplD freep_def rev_finite_subset subsetI)
lemma freep_prn: "freep Φ ⟹ freep (prn (swp a b) ` Φ)" 
  by (metis bij_image_Compl_eq bij_swp freep_def infinite_inj_image
      swp_inj usedp_prn)

lemma bprov_weaken: "Φ ⊢ C ⟹ Φ ⊆ Ψ ⟹ freep Ψ ⟹ Ψ ⊢ C"
proof (induction arbitrary: Ψ rule: bprov.induct)
  case NegI thus ?case
    by (simp add: bprov.NegI freep_add sup.order_iff)
next
  case DisE thus ?case
    by (metis Un_insert_right bprov.DisE freep_add sup.cobounded2
              sup.order_iff sup_bot_right)
next
  case (PiI Φ G w α) 
  then obtain w' where w': "w' ∉ usedp Ψ" "w' ∉ pars G" "w' ≠ w"
    using freep_fresh[of _ "pars G ∪ {w}"] by force
  have wsub: "Φ ⊆ prn (swp w w') ` Ψ"
  proof
    fix D assume D: "D ∈ Φ"
    hence "w ∉ pars D" and "w' ∉ pars D"  
      by (simp add: PiI.hyps(4)) (metis D PiI.prems(1) UN_I subset_iff usedp_def w'(1)) 
    hence "prn (swp w w') D = D" by (auto simp: swp_def intro: prn_cong)
    thus "D ∈ prn (swp w w') ` Ψ" using D PiI.prems(1) by force
  qed
  have "prn (swp w w') ` Ψ ⊢ G ⋅ (wp⇘α⇙)"
    using PiI freep_prn wsub by meson
  hence "Ψ ⊢ (prn (swp w w') G) ⋅ (w'p⇘α⇙)"
     by (metis bprov_rename image_prn_swp_swp swp_inj tm.simps(121,127) swp_def)
  moreover have "prn (swp w w') G = G"
    using PiI.hyps(3) w'(2)
    by (auto simp: swp_def intro: prn_cong)
  ultimately have "Ψ ⊢ G ⋅ (w'p⇘α⇙)" by simp
  moreover have "∀D ∈ Ψ. w' ∉ pars D" using w'(1)
    by (auto simp: usedp_def)
  ultimately show ?case using PiI.hyps(2) w'(2)
    by (auto intro: bprov.PiI)
next case Contr thus ?case 
  by (metis Un_insert_right bprov.Contr freep_add sup.cobounded2
      sup.order_iff sup_bot.right_neutral)
next case BoolE thus ?case by (simp add: bprov.BoolE freep_add sup.absorb_iff2)
qed(auto intro: bprov.intros)

subsection ‹Compactness›

text ‹Every derivation uses only finitely many hypotheses --- BKK: ``since every ‹NK*›-proof is
  finite'' (used in the proof of BKK Corollary 7.8).  With set-based contexts this is again a
  lemma that has to be proved, stated for an infinite parameter type (the sort constraint of
  ‹bprov_finite›, needed for the weakening steps).›

text ‹When the parameter type is infinite, every finite context leaves infinitely many
  parameters free.›

lemma freep_finite: fixes Φ :: "'p::infinite tm set" assumes "finite Φ"
  shows "freep Φ"
by (metis assms freep_def usedp_def finite_pars infinite_UNIV
    finite_Diff2 Compl_eq_Diff_UNIV finite_UN)

lemma bprov_finite: "Φ ⊢ (C :: 'p::infinite tm) ⟹ ∃Φ0. finite Φ0 ∧ Φ0 ⊆ Φ ∧ Φ0 ⊢ C"
proof (induction rule: bprov.induct)
  case (NegI Φ A) thus ?case
    by (smt (verit) Un_infinite Un_insert_right bprov.NegI
        bprov_weaken freep_add freep_finite subset_UnE
        subset_insertI subset_singleton_iff)
next
  case (NegE Φ A C) thus ?case
    by (smt (verit) bprov.NegE bprov_weaken finite_UnI freep_finite le_sup_iff
        sup_ge1 sup_ge2)
next
  case (DisE Φ A B C)
  then obtain Φ1 Φ2 Φ3 where
    Q1: "finite Φ1" "Φ1 ⊆ Φ" "Φ1 ⊢ A ∨ B" and
    Q2: "finite Φ2" "Φ2 ⊆ Φ ∪ {A}" "Φ2 ⊢ C" and
    Q3: "finite Φ3" "Φ3 ⊆ Φ ∪ {B}" "Φ3 ⊢ C"
    by blast
  moreover define Φ0 where "Φ0 = Φ1 ∪ (Φ2 - {A}) ∪ (Φ3 - {B})"
  ultimately have "finite Φ0" and "Φ0 ⊆ Φ" by auto
  moreover {
    have "Φ0 ⊢ A ∨ B"
      by (metis Q1(3) Φ0_def bprov_weaken dual_order.refl calculation(1)
          freep_finite le_sup_iff)
    moreover have "Φ0 ∪ {A} ⊢ C" and "Φ0 ∪ {B} ⊢ C"
      by (auto intro: bprov_weaken[OF Q2(3)] bprov_weaken[OF Q3(3)]
               simp: Φ0_def Q1(1) Q2(1) Q3(1) freep_finite)
    ultimately have "Φ0 ⊢ C" by (auto intro: DisE bprov.DisE)
  }
  ultimately show ?case by blast
next case (Contr Φ A) show ?case by (smt (verit, del_insts) Contr.IH
    Contr.hyps(2) Un_infinite Un_insert_right
          bprov.Contr bprov_weaken freep_add freep_finite subset_UnE
              subset_insertI subset_singleton_iff)
next case (BoolE Φ A B)
  then obtain Φ1 Φ2 where
    Q1: "finite Φ1" "Φ1 ⊆ Φ ∪ {A}" "Φ1 ⊢ B" and
    Q2: "finite Φ2" "Φ2 ⊆ Φ ∪ {B}" "Φ2 ⊢ A" 
    by blast
  moreover define Φ0 where "Φ0 = (Φ1 - {A}) ∪ (Φ2 - {B})"
  ultimately have "finite Φ0" and "Φ0 ⊆ Φ" by auto
  moreover {
    have "Φ0 ∪ {A} ⊢ B" and "Φ0 ∪ {B} ⊢ A"
      by (auto intro: bprov_weaken[OF Q1(3)] bprov_weaken[OF Q2(3)]
               simp: calculation Q1(1,2) Q2(1) Φ0_def freep_finite)
    hence "Φ0 ⊢ A ≐⇘𝗈⇙ B" using BoolE by (auto intro: bprov.intros)
  }
  ultimately show ?case by blast
qed(auto intro: bprov.intros)

subsection ‹Derivability from hypotheses›

text ‹The calculus ‹⊢› manipulates its context as a set, and ‹NK(ΠI)› consumes fresh
  eigen-parameters; over a context that uses @{emph ‹every›} parameter, generalisation ---
  and with it weakening --- becomes unavailable (hence the proviso ‹freep Ψ› in
  @{thm [source] bprov_weaken}).  Derivability from a set of @{emph ‹hypotheses›} is
  therefore defined through finite sub-contexts, in the style of Andrews (2002): ‹Φ ⊩ A›
  holds when some finite part of ‹Φ› derives ‹A›.  This relation is monotone without any
  proviso and of finite character by construction, and over an infinite parameter type it
  coincides with ‹⊢› on ‹freep› contexts, in particular on all finite ones.›

definition fprov :: "'p tm set ⇒ 'p tm ⇒ bool"  (infix ‹⊩› 40) where
  "Φ ⊩ A ⟷ (∃Φ0. finite Φ0 ∧ Φ0 ⊆ Φ ∧ Φ0 ⊢ A)"

lemma fprovI: "finite Φ0 ⟹ Φ0 ⊆ Φ ⟹ Φ0 ⊢ A ⟹ Φ ⊩ A"
  by (auto simp: fprov_def)

lemma bprov_fprov: "Φ ⊢ (A :: 'p::infinite tm) ⟹ Φ ⊩ A"
  using bprov_finite by (auto simp: fprov_def)

lemma fprov_bprov: "Φ ⊩ A ⟹ freep Φ ⟹ Φ ⊢ A"
  using bprov_weaken by (auto simp: fprov_def)

lemma fprov_eq_bprov: "freep Φ ⟹ (Φ ⊩ (A :: 'p::infinite tm)) ⟷ (Φ ⊢ A)"
  using bprov_fprov fprov_bprov by blast

lemma fprov_finite_eq_bprov:
  "finite Φ ⟹ (Φ ⊩ (A :: 'p::infinite tm)) ⟷ (Φ ⊢ A)"
  by (simp add: fprov_eq_bprov freep_finite)

lemma fprov_mono: "Φ ⊩ A ⟹ Φ ⊆ Ψ ⟹ Ψ ⊩ A"
  by (auto simp: fprov_def)

lemma fprov_compact: "Φ ⊩ A ⟷ (∃Φ0. finite Φ0 ∧ Φ0 ⊆ Φ ∧ Φ0 ⊩ A)"
  by (auto simp: fprov_def)

subsection ‹Consistency›

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

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

text ‹Subsets of a consistent set are consistent, provided the superset leaves infinitely many
  parameters unused (by weakening).›

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

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

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

text ‹For the hypothesis relation, consistency of finite character is a definitional
  unfolding.›

lemma fprov_con:
  "(¬ (Φ ⊩ (⊥ :: 'p tm))) ⟷ (∀Φ0. finite Φ0 ⟶ Φ0 ⊆ Φ ⟶ con Φ0)"
  by (auto simp: fprov_def con_def)

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

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

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

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

subsection ‹Admissible rules›

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

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

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

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

subsection ‹Derived rules for the defined quantifiers›

text ‹‹NK(ΠE)› and ‹NK(ΠI)› for the folded quantifier ‹Πσ›.›

lemma PiE_Forall: "Φ ⊢ Π⇘α⇙ b ⟹ wff⇘α⇙(A) ⟹ Φ ⊢ (Λ⇘α⇙ b) ⋅ A"
  unfolding Forall_def by (rule bprov.PiE)
lemma PiI_Forall: "Φ ⊢ (Λ⇘α⇙ b) ⋅ (wp⇘α⇙) ⟹ wff⇘α ⇒ 𝗈⇙(Λ⇘α⇙ b) ⟹ w ∉ pars (Λ⇘α⇙ b)
                   ⟹ (∀D ∈ Φ. w ∉ pars D)  ⟹ Φ ⊢ Π⇘α⇙ b"
  unfolding Forall_def by (rule bprov.PiI)

text ‹Existential elimination at a fresh eigen-parameter, for the defined quantifier
  ‹∃ = ¬Π¬›: the derived counterpart of the paper-style step ``obtain a witness''.›

lemma ExE: assumes ex: "Φ ⊢ ∃⇘σ⇙ b" and step: "Φ ∪ {b⟨wp⇘σ⇙⟩} ⊢ C"
    and wb: "wff⇘σ ⇒ 𝗈⇙(Λ⇘σ⇙ b)"
  and wC: "wff⇘𝗈⇙(C)" and wpb: "w ∉ pars b" and wpC: "w ∉ pars C"
      and wpΦ: "∀D ∈ Φ. w ∉ pars D" and fp: "freep Φ"
  shows "Φ ⊢ C"
proof -
  have wNb: "wff⇘σ ⇒ 𝗈⇙(Λ⇘σ⇙ (¬ b))"
    by (auto intro!: wff_opn[OF wb] wff_Fre wff_AbsI)
  have fp1: "freep (Φ ∪ {¬ C})" using freep_add[OF fp] by simp
  have fp2: "freep (Φ ∪ {¬ C} ∪ {b⟨wp⇘σ⇙⟩})"
      using freep_add[OF freep_add[OF fp]] by simp
  have s1: "Φ ∪ {¬ C} ∪ {b⟨wp⇘σ⇙⟩} ⊢ C"
    by (rule bprov_weaken[OF step _ fp2]) auto
  have s2: "Φ ∪ {¬ C} ∪ {b⟨wp⇘σ⇙⟩} ⊢ ¬ C" by (auto intro: bprov.Hyp)
  have bq: "(Λ⇘σ⇙ (¬ b)) ⋅ (wp⇘σ⇙) ≈⇘𝗈⇙ ¬ (b⟨wp⇘σ⇙⟩)"
    using beq.beta[OF wNb wff_Par] by simp
  have s5: "Φ ∪ {¬ C} ⊢ Π⇘σ⇙ (¬ b)"
    using wpb wpC wpΦ
    by (safe intro!:
        PiI_Forall[OF bprov.Beta[OF beq.sym[OF bq] bprov.NegI[OF
              bprov.NegE[OF s2 s1 wff_FalseB] wff_opn[OF wb wff_Par]]] wNb]) auto
  have s6: "Φ ∪ {¬ C} ⊢ ¬ (Π⇘σ⇙ (¬ b))" by (rule bprov_weaken[OF ex _ fp1]) auto
  show ?thesis by (rule bprov.Contr[OF bprov.NegE[OF s6 s5 wff_FalseB] wC])
qed

text ‹Universal instantiation directly at the ‹β›-reduced instance.›

lemma PiE_open: "Φ ⊢ Π⇘α⇙ b ⟹ wff⇘α ⇒ 𝗈⇙(Λ⇘α⇙ b) ⟹ wff⇘α⇙(A) ⟹ Φ ⊢ b⟨A⟩"
  by (metis PiE_Forall beq.beta bprov.Beta)

text ‹The same rules for the named binders ‹Πxσ.› and ‹∃xσ.›: instantiation and
  elimination substitute for the named variable (instances of ‹PiE_open› and ‹ExE› via
  ‹opn_clos_sub›), and introduction of ‹∃› comes from an instance.›

lemma AllN_E:
  assumes h: "Φ ⊢ Πx⇘σ⇙. b" and wb: "wff⇘𝗈⇙(b)" and wA: "wff⇘σ⇙(A)"
  shows "Φ ⊢ fsub x σ A b"
proof -
  have "Φ ⊢ (clos 0 x σ b)⟨A⟩"
    using h unfolding AllN_def by (rule PiE_open[OF _ wff_LamN_clos[OF wb] wA])
  thus ?thesis by (simp only: opn_clos_sub[OF opn_lc[OF wff_lc[OF wb]]])
qed

lemma ExN_I:
  assumes h: "Φ ⊢ fsub x σ A b" and wb: "wff⇘𝗈⇙(b)" and wA: "wff⇘σ⇙(A)" and fp: "freep Φ"
  shows "Φ ⊢ ∃x⇘σ⇙. b"
proof -
  let ?P = "Π⇘σ⇙ (¬ (clos 0 x σ b))"
  have e: "(∃x⇘σ⇙. b) = ¬ ?P" by (simp add: ExN_def)
  have wL: "wff⇘σ ⇒ 𝗈⇙(Λ⇘σ⇙ (¬ (clos 0 x σ b)))"
    using wff_LamN_clos[OF wff_Not[OF wb]] by simp
  have wP: "wff⇘𝗈⇙(?P)" unfolding Forall_def by (rule wff_App[OF wff_Pi wL])
  have "Φ ∪ {?P} ⊢ ⊥"
  proof (rule bprov.NegE[OF _ _ wff_FalseB])
    have "Φ ∪ {?P} ⊢ (¬ (clos 0 x σ b))⟨A⟩"
      by (rule PiE_open[OF _ wL wA]) (auto intro: bprov.Hyp)
    thus "Φ ∪ {?P} ⊢ ¬ (fsub x σ A b)"
      by (simp add: opn_clos_sub[OF opn_lc[OF wff_lc[OF wb]]])
    show "Φ ∪ {?P} ⊢ fsub x σ A b"
      by (rule bprov_weaken[OF h]) (auto simp: freep_add fp)
  qed
  thus ?thesis unfolding e by (rule bprov.NegI[OF _ wP])
qed

lemma ExN_E:
  assumes ex: "Φ ⊢ ∃x⇘σ⇙. b" and step: "Φ ∪ {fsub x σ (wp⇘σ⇙) b} ⊢ C"
    and wb: "wff⇘𝗈⇙(b)" and wC: "wff⇘𝗈⇙(C)" and wpb: "w ∉ pars b" and wpC: "w ∉ pars C"
    and wpΦ: "∀D ∈ Φ. w ∉ pars D" and fp: "freep Φ"
  shows "Φ ⊢ C"
proof (rule ExE[OF _ _ wff_LamN_clos[OF wb] wC _ wpC wpΦ fp])
  show "Φ ⊢ ∃⇘σ⇙ (clos 0 x σ b)" using ex by (simp add: ExN_def)
  show "Φ ∪ {(clos 0 x σ b)⟨wp⇘σ⇙⟩} ⊢ C"
    using step by (simp add: opn_clos_sub[OF opn_lc[OF wff_lc[OF wb]]])
  show "w ∉ pars (clos 0 x σ b)" using wpb by simp
qed

text ‹Cut: a hypothesis that is itself derivable can be discharged; iterated over a finite
  set of derivable hypotheses.›

lemma bprov_cut:
  assumes AC: "Φ ∪ {A} ⊢ C" and A: "Φ ⊢ A" and wA: "wff⇘𝗈⇙(A)" and wC: "wff⇘𝗈⇙(C)"
    and fp: "freep Φ"
  shows "Φ ⊢ C"
proof (rule bprov.Contr[OF _ wC])
  have 1: "Φ ∪ {¬ C} ∪ {A} ⊢ ⊥"
  proof (rule bprov.NegE[OF _ _ wff_FalseB])
    show "Φ ∪ {¬ C} ∪ {A} ⊢ ¬ C" by (auto intro: bprov.Hyp)
    show "Φ ∪ {¬ C} ∪ {A} ⊢ C" by (rule bprov_weaken[OF AC]) (auto simp: freep_add fp)
  qed
  have n: "Φ ∪ {¬ C} ⊢ ¬ A" by (rule bprov.NegI[OF 1 wA])
  have p: "Φ ∪ {¬ C} ⊢ A" by (rule bprov_weaken[OF A]) (auto simp: freep_add fp)
  show "Φ ∪ {¬ C} ⊢ ⊥" by (rule bprov.NegE[OF n p wff_FalseB])
qed

lemma bprov_cut_set:
  assumes fin: "finite Λ"
  shows "Φ ∪ Λ ⊢ C ⟹ (⋀B. B ∈ Λ ⟹ Φ ⊢ B) ⟹ (⋀B. B ∈ Λ ⟹ wff⇘𝗈⇙(B))
         ⟹ wff⇘𝗈⇙(C) ⟹ freep Φ ⟹ Φ ⊢ C"
  using fin
proof (induction Λ)
  case empty thus ?case by simp
next
  case (insert B Λ)
  have fp': "freep (Φ ∪ Λ)" by (rule freep_un_finite[OF insert.prems(5) insert.hyps(1)])
  have wB: "wff⇘𝗈⇙(B)" by (rule insert.prems(3)) simp
  have dB: "Φ ⊢ B" by (rule insert.prems(2)) simp
  have AC: "Φ ∪ Λ ∪ {B} ⊢ C" using insert.prems(1) by simp
  have "Φ ∪ Λ ⊢ B" by (rule bprov_weaken[OF dB _ fp']) auto
  hence "Φ ∪ Λ ⊢ C" by (rule bprov_cut[OF AC _ wB insert.prems(4) fp'])
  thus ?case using insert.prems by (intro insert.IH) auto
qed

text ‹Introduction and elimination for the defined conjunction ‹∧›.›

lemma AndI:
  assumes A: "Φ ⊢ A" and B: "Φ ⊢ B" and wA: "wff⇘𝗈⇙(A)" and wB: "wff⇘𝗈⇙(B)"
    and fp: "freep Φ"
  shows "Φ ⊢ A ∧ B"
proof -
  let ?D = "¬ A ∨ ¬ B"
  have wD: "wff⇘𝗈⇙(?D)" by (rule wff_Or[OF wff_Not[OF wA] wff_Not[OF wB]])
  have 1: "Φ ∪ {?D} ∪ {¬ A} ⊢ ⊥"
  proof (rule bprov.NegE[OF _ _ wff_FalseB])
    show "Φ ∪ {?D} ∪ {¬ A} ⊢ ¬ A" by (auto intro: bprov.Hyp)
    show "Φ ∪ {?D} ∪ {¬ A} ⊢ A" by (rule bprov_weaken[OF A]) (auto simp: freep_add fp)
  qed
  have 2: "Φ ∪ {?D} ∪ {¬ B} ⊢ ⊥"
  proof (rule bprov.NegE[OF _ _ wff_FalseB])
    show "Φ ∪ {?D} ∪ {¬ B} ⊢ ¬ B" by (auto intro: bprov.Hyp)
    show "Φ ∪ {?D} ∪ {¬ B} ⊢ B" by (rule bprov_weaken[OF B]) (auto simp: freep_add fp)
  qed
  have "Φ ∪ {?D} ⊢ ⊥"
    by (rule bprov.DisE[OF _ 1 2 wff_Not[OF wA] wff_Not[OF wB]]) (auto intro: bprov.Hyp)
  thus ?thesis unfolding AndB_def by (rule bprov.NegI[OF _ wD])
qed

lemma AndE1:
  assumes AB: "Φ ⊢ A ∧ B" and wA: "wff⇘𝗈⇙(A)" and wB: "wff⇘𝗈⇙(B)" and fp: "freep Φ"
  shows "Φ ⊢ A"
proof (rule bprov.Contr[OF _ wA])
  have p: "Φ ∪ {¬ A} ⊢ ¬ A ∨ ¬ B"
    by (rule bprov.DisIL[OF _ wff_Not[OF wB]]) (auto intro: bprov.Hyp)
  have n: "Φ ∪ {¬ A} ⊢ ¬ (¬ A ∨ ¬ B)"
    using AB unfolding AndB_def by (rule bprov_weaken) (auto simp: freep_add fp)
  show "Φ ∪ {¬ A} ⊢ ⊥" by (rule bprov.NegE[OF n p wff_FalseB])
qed

lemma AndE2:
  assumes AB: "Φ ⊢ A ∧ B" and wA: "wff⇘𝗈⇙(A)" and wB: "wff⇘𝗈⇙(B)" and fp: "freep Φ"
  shows "Φ ⊢ B"
proof (rule bprov.Contr[OF _ wB])
  have p: "Φ ∪ {¬ B} ⊢ ¬ A ∨ ¬ B"
    by (rule bprov.DisIR[OF _ wff_Not[OF wA]]) (auto intro: bprov.Hyp)
  have n: "Φ ∪ {¬ B} ⊢ ¬ (¬ A ∨ ¬ B)"
    using AB unfolding AndB_def by (rule bprov_weaken) (auto simp: freep_add fp)
  show "Φ ∪ {¬ B} ⊢ ⊥" by (rule bprov.NegE[OF n p wff_FalseB])
qed

text ‹Syntactic generalisation: a fresh parameter substituted for a free variable can
  be quantified away and re-instantiated, recovering the open formula (the rule chain
  ‹NK(β)›--‹NK(ΠI)›--‹NK(ΠE)›--‹NK(β)›).  Statement preserved verbatim from the
  initial release of this entry, August 2026 (compatibility export, relocated from ‹Completeness›);
  the completeness proof now uses the simultaneous variable-for-parameter substitution of
  ‹Completeness› instead.›

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

subsection ‹Parameter-to-variable substitution in derivations›

text ‹Derivability is stable under replacing a parameter by a @{emph ‹free variable›}, as it
  is under injective renamings (@{thm [source] bprov_rename}).  No eigen-parameter need be
  renamed: the substitution only ever removes parameters, so the side conditions of ‹NK(ΠI)›
  survive; and where the eigen-parameter @{emph ‹is›} the substituted one, ‹pvar› is the
  identity on context and quantified predicate, so the original rule instance already applies.›

lemma bprov_pvar: "Φ ⊢ C ⟹ pvar w σ x ` Φ ⊢ pvar w σ x C"
proof (induction rule: bprov.induct)
  case Beta thus ?case by (meson beq_pvar bprov.Beta)
next
  case DisE thus ?case by (simp add: bprov.DisE wff_pvar)
next
  case (PiI Φ G v α)
  show ?case
  proof (cases "v = w ∧ α = σ")
    case True
    have "pvar w σ x G = G" using PiI.hyps(3) True by simp
    moreover have "pvar w σ x ` Φ = Φ"
      using PiI.hyps(4) True by (simp add: pvar_image_id)
    ultimately show ?thesis
      using bprov.PiI[OF PiI.hyps(1) PiI.hyps(2) PiI.hyps(3) PiI.hyps(4)] by simp
  next
    case False
    hence pv: "pvar w σ x (vp⇘α⇙) = vp⇘α⇙" by simp
    have h1: "pvar w σ x ` Φ ⊢ (pvar w σ x G) ⋅ (vp⇘α⇙)" using PiI.IH pv by simp
    have h2: "wff⇘α⇒𝗈⇙(pvar w σ x G)" by (rule wff_pvar[OF PiI.hyps(2)])
    have h3: "v ∉ pars (pvar w σ x G)"
      using PiI.hyps(3) pars_pvar[of w σ x G] by blast
    have h4: "∀D ∈ pvar w σ x ` Φ. v ∉ pars D"
    proof
      fix D' assume "D' ∈ pvar w σ x ` Φ"
      then obtain D where D: "D ∈ Φ" "D' = pvar w σ x D" by auto
      have "v ∉ pars D" using PiI.hyps(4) D(1) by blast
      thus "v ∉ pars D'" using D(2) pars_pvar[of w σ x D] by blast
    qed
    show ?thesis using bprov.PiI[OF h1 h2 h3 h4] by simp
  qed
next
  case Contr thus ?case by (simp add: bprov.Contr wff_pvar)
next
  case NegE thus ?case by (metis bprov.NegE pvar.simps(4) pvar.simps(9) wff_pvar)
next
  case PiE thus ?case by (metis bprov.PiE pvar.simps(6) pvar.simps(9) wff_pvar)
qed(auto simp: bprov.EqL bprov.EqR bprov.Desc bprov.FuncE bprov.DisIL bprov.DisIR bprov.Hyp
               bprov.BoolE bprov.NegI wff_pvar)

subsection ‹Leibniz equality in the calculus›

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

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

lemma leib_subst:
  assumes AB: "Φ ⊢ A ≐⇘α⇙ B" and fp: "freep Φ" and wa: "wff⇘α⇙(A)" and wb: "wff⇘α⇙(B)"
      and wP: "wff⇘α⇒𝗈⇙(P)" and PA: "Φ ⊢ P ⋅ A"
    shows "Φ ⊢ P ⋅ B"
proof -
  let ?body = "(Bnd 0) ⋅ A ⊃ (Bnd 0) ⋅ B"
  have "Φ ⊢ Π⇘α⇒𝗈⇙ ?body"
    using Leib_beq[OF wa wb] AB by (rule bprov.Beta)
  hence "Φ ⊢ (Pi (α ⇒ 𝗈)) ⋅ (Λ⇘α ⇒ 𝗈⇙ ?body)" by (simp add: Forall_def)
  hence P: "Φ ⊢ (Λ⇘α ⇒ 𝗈⇙ ?body) ⋅ P" using wP by (rule bprov.PiE)
  have wAbs: "wff⇘(α⇒𝗈)⇒𝗈⇙(Λ⇘α ⇒ 𝗈⇙ ?body)"
    by (auto simp: opn_lc[OF wff_lc[OF wa]] opn_lc[OF wff_lc[OF wb]]
             intro!: wff_App wff_Fre wa wb wff_AbsI)
  have "(Λ⇘α ⇒ 𝗈⇙ ?body) ⋅ P ≈⇘𝗈⇙ P ⋅ A ⊃ P ⋅ B"
  proof -
    have "(Λ⇘α ⇒ 𝗈⇙ ?body) ⋅ P ≈⇘𝗈⇙ ?body⟨P⟩"
      by (rule beq.beta[OF wAbs wP])
    thus ?thesis
      by (simp add: opn_lc[OF wff_lc[OF wa]] opn_lc[OF wff_lc[OF wb]])
  qed
  from bprov.Beta[OF this P] have "Φ ⊢ P ⋅ A ⊃ P ⋅ B".
  moreover have "wff⇘𝗈⇙(P ⋅ A)" by (rule wff_App[OF wP wa])
  moreover have "wff⇘𝗈⇙(P ⋅ B)" by (rule wff_App[OF wP wb])
  ultimately show ?thesis using PA fp by (metis bprov_ImpE)
qed

text ‹The one transport step behind symmetry, transitivity, congruence and modus ponens:
  a proven ‹β›-reduct ‹X› of ‹P ⋅ A› transports along ‹Φ ⊢ A ≐ B› to the ‹β›-reduct
  ‹Y› of ‹P ⋅ B›.  Each rule below just picks its predicate ‹P› and its base fact.›

lemma leib_transport:
  assumes AB: "Φ ⊢ A ≐⇘α⇙ B" and fp: "freep Φ"
      and wa: "wff⇘α⇙(A)" and wb: "wff⇘α⇙(B)" and wP: "wff⇘α⇒𝗈⇙(P)"
      and bX: "P ⋅ A ≈⇘𝗈⇙ X" and bY: "P ⋅ B ≈⇘𝗈⇙ Y"
      and X: "Φ ⊢ X"
    shows "Φ ⊢ Y"
proof -
  have "Φ ⊢ P ⋅ A" by (rule bprov.Beta[OF beq.sym[OF bX] X])
  hence "Φ ⊢ P ⋅ B" by (rule leib_subst[OF AB fp wa wb wP])
  thus ?thesis by (rule bprov.Beta[OF bY])
qed

lemma leib_sym:
  assumes AB: "Φ ⊢ A ≐⇘α⇙ B" and fp: "freep Φ" and wa: "wff⇘α⇙(A)" and wb: "wff⇘α⇙(B)"
  shows "Φ ⊢ B ≐⇘α⇙ A"
proof -
  have lcA: "lc A" using wa by (rule wff_lc)
  let ?P = "Λ⇘α⇙ (((Leib α) ⋅ (Bnd 0)) ⋅ A)" ― ‹the predicate ‹λx. x ≐ A››
  have wP: "wff⇘α⇒𝗈⇙(?P)" by (auto simp: opn_lc[OF lcA] intro!: wff_Fre wa wff_AbsI)
  have PbA: "?P ⋅ A ≈⇘𝗈⇙ (A ≐⇘α⇙ A)"
    using beq.beta[OF wP wa] by (simp add: opn_lc[OF lcA])
  have PbB: "?P ⋅ B ≈⇘𝗈⇙ (B ≐⇘α⇙ A)"
    using beq.beta[OF wP wb] by (simp add: opn_lc[OF lcA])
  show ?thesis
    by (rule leib_transport[OF AB fp wa wb wP PbA PbB leib_refl[OF wa]])
qed
lemma leib_trans:
  assumes AB: "Φ ⊢ A ≐⇘α⇙ B" and BC: "Φ ⊢ B ≐⇘α⇙ C" and fp: "freep Φ"
      and wa: "wff⇘α⇙(A)" and wb: "wff⇘α⇙(B)" and wc: "wff⇘α⇙(C)"
    shows "Φ ⊢ A ≐⇘α⇙ C"
proof -
  have lcA: "lc A" using wa by (rule wff_lc)
  let ?P = "Λ⇘α⇙ (((Leib α) ⋅ A) ⋅ (Bnd 0))" ― ‹the predicate ‹λx. A ≐ x››
  have wP: "wff⇘α⇒𝗈⇙(?P)"
    by (auto simp: opn_lc[OF lcA] intro!: wff_Fre wa wff_AbsI)
  have PbB: "?P ⋅ B ≈⇘𝗈⇙ (A ≐⇘α⇙ B)"
    using beq.beta[OF wP wb] by (simp add: opn_lc[OF lcA])
  have PbC: "?P ⋅ C ≈⇘𝗈⇙ (A ≐⇘α⇙ C)"
    using beq.beta[OF wP wc] by (simp add: opn_lc[OF lcA])
  show ?thesis by (rule leib_transport[OF BC fp wb wc wP PbB PbC AB])
qed
lemma leib_cong2:
  assumes AA: "Φ ⊢ A ≐⇘α⇙ A'" and fp: "freep Φ"
  and wa: "wff⇘α⇙(A)" and wa': "wff⇘α⇙(A')" and wC: "wff⇘α⇒β⇙(C)"
  shows "Φ ⊢ (C ⋅ A) ≐⇘β⇙ (C ⋅ A')"
proof -
  have lcC: "lc C" using wC by (rule wff_lc)
  have lcA: "lc A" using wa by (rule wff_lc)
  let ?P = "Λ⇘α⇙ (C ⋅ A ≐⇘β⇙ C ⋅ (Bnd 0))"   ― ‹‹λx. (C A) ≐ (C x)››
  have wP: "wff⇘α⇒𝗈⇙(?P)"
    by (auto simp: opn_lc[OF lcC] opn_lc[OF lcA]
             intro!: wff_AbsI wff_App wff_Fre wC wa wff_App[OF wC wa])
  have PbA: "?P ⋅ A ≈⇘𝗈⇙ (C ⋅ A ≐⇘β⇙ C ⋅ A)"
    using beq.beta[OF wP wa] by (simp add: opn_lc[OF lcC] opn_lc[OF lcA])
  have PbA': "?P ⋅ A' ≈⇘𝗈⇙ (C ⋅ A ≐⇘β⇙ C ⋅ A')"
    using beq.beta[OF wP wa'] by (simp add: opn_lc[OF lcC] opn_lc[OF lcA])
  show ?thesis
    by (rule leib_transport[OF AA fp wa wa' wP PbA PbA' leib_refl[OF wff_App[OF wC wa]]])
qed
lemma leib_cong1:
  assumes CC: "Φ ⊢ C ≐⇘α⇒β⇙ C'" and fp: "freep Φ"
      and wC: "wff⇘α⇒β⇙(C)" and wC': "wff⇘α⇒β⇙(C')" and wa: "wff⇘α⇙(A)"
    shows "Φ ⊢ (C ⋅ A) ≐⇘β⇙ (C' ⋅ A)"
proof -
  have lcC: "lc C" using wC by (rule wff_lc)
  have lcA: "lc A" using wa by (rule wff_lc)
  let ?P = "Λ⇘α ⇒ β⇙ (C ⋅ A ≐⇘β⇙ (Bnd 0) ⋅ A)"   ― ‹‹λf. (C A) ≐ (f A)››
  have wP: "wff⇘(α⇒β)⇒𝗈⇙(?P)"
    by (auto simp: opn_lc[OF lcC] opn_lc[OF lcA]
             intro!: wff_AbsI wff_App wff_Fre wC wa wff_App[OF wC wa])
  have PbC: "?P ⋅ C ≈⇘𝗈⇙ (C ⋅ A ≐⇘β⇙ C ⋅ A)"
    using beq.beta[OF wP wC] by (simp add: opn_lc[OF lcC] opn_lc[OF lcA])
  have PbC': "?P ⋅ C' ≈⇘𝗈⇙ (C ⋅ A ≐⇘β⇙ C' ⋅ A)"
    using beq.beta[OF wP wC'] by (simp add: opn_lc[OF lcC] opn_lc[OF lcA])
  show ?thesis
    by (rule leib_transport[OF CC fp wC wC' wP PbC PbC' leib_refl[OF wff_App[OF wC wa]]])
qed

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

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

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

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

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

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

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

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

text ‹For @{emph ‹primitive›} equality the same facts are available through the translation
  (‹NK(=l)› in, ‹leib_to_peq› out); symmetry, and symmetry of a negated equation, are
  the two instances used in ‹NK_Infinity›.›

lemma peq_sym:
  assumes AB: "Φ ⊢ A =⇘α⇙ B" and fp: "freep Φ" and wA: "wff⇘α⇙(A)" and wB: "wff⇘α⇙(B)"
  shows "Φ ⊢ B =⇘α⇙ A"
  by (rule leib_to_peq[OF leib_sym[OF bprov.EqL[OF AB] fp wA wB] fp wB wA])

lemma peq_neg_sym:
  assumes nAB: "Φ ⊢ ¬ (A =⇘α⇙ B)" and fp: "freep Φ" and wA: "wff⇘α⇙(A)" and wB: "wff⇘α⇙(B)"
  shows "Φ ⊢ ¬ (B =⇘α⇙ A)"
proof (rule bprov.NegI[OF _ wff_PEq[OF wB wA]])
  have fp': "freep (Φ ∪ {B =⇘α⇙ A})" by (rule freep_un[OF fp])
  have p: "Φ ∪ {B =⇘α⇙ A} ⊢ A =⇘α⇙ B"
    by (rule peq_sym[OF _ fp' wB wA]) (auto intro: bprov.Hyp)
  have n: "Φ ∪ {B =⇘α⇙ A} ⊢ ¬ (A =⇘α⇙ B)"
    by (rule bprov_weaken[OF nAB]) (auto simp: freep_add fp)
  show "Φ ∪ {B =⇘α⇙ A} ⊢ ⊥" by (rule bprov.NegE[OF n p wff_FalseB])
qed

end