Theory Calculus

theory Calculus
  imports Semantics "HOL-Library.Infinite_Typeclass"
begin

section ‹The natural-deduction calculus NK›

text ‹We formalise the calculus ‹NK⇩β⇩f⇩b› 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(ι)›, a premise-free axiom scheme describing
  Leibniz singletons (beyond BKK, following Andrews 1972, their reference [3]).  BKK prove
  ‹NK⇩β⇩f⇩b› sound and complete for the class of ‹Σ›-Henkin models ‹ℳ⇩β⇩f⇩b› (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, Section 2).  The provability judgement ‹Φ ⊢ A› relates a set
      of sentences
  ‹Φ› to a sentence ‹A›.  Eigenvariables are @{emph ‹parameters›} (BKK's ‹w⇘α⇙›), which --- unlike
  the free variables used only during evaluation --- never occur bound.›

subsection ‹The inference rules of ‹NK⇩β⇩f⇩b› (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(∨I⇩L)››
  | DisIR: "Φ ⊢ B ⟹ wff⇘𝗈⇙(A) ⟹ Φ ⊢ A ❙∨ B"  ― ‹BKK ‹NK(∨I⇩R)››
  | DisE:  "Φ ⊢ A ❙∨ B ⟹ Φ ∪ {A} ⊢ C ⟹ Φ ∪ {B} ⊢ C
            ⟹ wff⇘𝗈⇙(A) ⟹ wff⇘𝗈⇙(B) ⟹ Φ ⊢ C"  ― ‹BKK ‹NK(∨E)››
  | PiI:   "Φ ⊢ G ❙⋅ (w⇧p⇘α⇙) ⟹ 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)"
proof (induct rule: bprov.induct)
  case PiI thus ?case by (meson wff_App wff_Pi)
next
  case Desc thus ?case by (metis wff_Leib wff_App wff_Iota)
qed(auto simp: beq_wff wff_App)


text ‹Derivability is stable under injective parameter renaming --- injectivity keeps the
  eigen-parameter side-conditions of ‹NK(ΠI)›.  This lets us move eigen-parameters out of the
  way, 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 DisE thus ?case using DisE bprov.DisE by auto
next
  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 genuine lemma, proved
      by transposing the 
  eigen-parameter out of the way of the enlarged context.›

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)
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 ‹The parameters used by a context, and the property of leaving infinitely many free.
  ‹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,
      for each type, a witness
   reservoir of the cardinality of the (countable) language.›

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 pars_prn)
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_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 ❙⋅ (w⇧p⇘α⇙)"
    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
  genuine lemma.›

text ‹When the parameter type is infinite, every finite context leaves infinitely many
  parameters free, and every derivation uses only a finite part of its context.›

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)

end