Theory NK_Infinity
theory NK_Infinity
imports Consistency Completeness
begin
section ‹The inequation scheme over new constants›
text ‹The parametric family of finite standard models constructed in ‹Consistency› provides,
for every finite size ‹k > 0›, a standard model with exactly ‹k› individuals whose
parameter interpretation can distinguish any prescribed finite family of parameters. This
is the model-theoretic input to the classical compactness argument of first-order model
theory that a theory with arbitrarily large finite models has an infinite model (Skolem
\<^cite>‹Skolem34›, Mal'cev \<^cite>‹Malcev36›, Henkin \<^cite>‹Henkin49›, Robinson
\<^cite>‹Robinson63›): expand the language by countably many new individual constants
‹c⇩i› and add the inequations ‹Ineq = {c⇩i ≠ c⇩j | i ≠ j}›. In type theory the same
technique appears in Andrews' ‹§55› \<^cite>‹Andrews02› (Theorem 5506), there in the
service of nonstandard models.
Two things should be kept apart. The standard first-order axiomatisation of ``the domain
is infinite'' consists of the constant-free sentences ``there are at least ‹n›
individuals'', one for each ‹n› (‹ExDistinct n› below). The inequation scheme over new
constants is the tool of the compactness argument, not itself an axiomatisation: it
derives each of those sentences (‹Ineq_derives_distinct_n› below); that its
constant-free consequences are no more than theirs is the translation argument, not
formalised here. We keep the short name ‹Ineq› for the scheme. Compactness --- the finite character of derivability,
@{thm [source] con_compact} --- lifts the consistency of each @{emph ‹finite›} part of
the scheme, satisfied in one of the finite models above, to the consistency of the whole
scheme. So consistency of ‹NK› with the scheme is obtained from the finite models
alone: the consistency proof constructs no infinite model, and nothing beyond plain HOL is
used. Neither
the scheme nor the constant-free sentences are to be conflated with a single
Dedekind-style axiom of infinity. The relation is made precise below: the axiom derives
every sentence ‹ExDistinct n›, but neither the scheme nor those sentences derive the
axiom, and some general model of the whole scheme refutes it.›
subsection ‹The scheme as a set of object formulas›
text ‹An arbitrary injective family ‹f› of parameter constants (‹'p› being infinite) and
the sentences ‹f i ≠ f j›; the consistency theorem holds for every such family, so no
canonical choice of constants is needed.›
definition dneq :: "(nat ⇒ 'p) ⇒ nat ⇒ nat ⇒ 'p::infinite tm" where
"dneq f i j = ❙¬ ((f i)⇧p⇘ι⇙ ❙=⇘ι⇙ (f j)⇧p⇘ι⇙)"
lemma wff_dneq: "wff⇘𝗈⇙(dneq f i j :: 'p::infinite tm)"
unfolding dneq_def by (simp add: wff_Not wff_PEq wff_Par)
lemma dneq_inj: "inj f ⟹ dneq f i j = dneq f i' j' ⟹ i = i' ∧ j = j'"
unfolding dneq_def by (auto dest: injD)
inductive_set Ineq :: "(nat ⇒ 'p) ⇒ 'p::infinite tm set" for f where
Ineq_I: "i ≠ j ⟹ dneq f i j ∈ Ineq f"
lemma Ineq_iff: "B ∈ Ineq f ⟷ (∃i j. B = dneq f i j ∧ i ≠ j)"
by (auto simp: Ineq.simps)
text ‹Every finite part of the scheme is satisfied by a large-enough finite model,
hence consistent, and by compactness so is the whole scheme. The finite model is
constructed @{emph ‹once›}, in the separation section below, where the very same model
also refutes the Dedekind axiom; the consistency theorems ‹con_finite_sub›, ‹con_Ineq›
and ‹con_Ineq_fprov› are stated there.›
section ‹The Dedekind axiom of infinity›
text ‹A single axiom of infinity in the sense of Dedekind: some self-map ‹F› of the
individuals is injective but not surjective,
‹DInf = ❙∃F⇘ι ❙⇒ ι⇙. (❙ΠX. ❙ΠY. F⋅X ❙= F⋅Y ❙⊃ X ❙= Y) ❙∧ (❙∃C. ❙ΠZ. ❙¬ F⋅Z ❙= C)›.›
subsection ‹The axiom as an object formula›
definition vF where "vF = (0::nat)"
definition vX where "vX = (1::nat)"
definition vY where "vY = (2::nat)"
definition vC where "vC = (3::nat)"
definition vZ where "vZ = (4::nat)"
lemmas vdefs = vF_def vX_def vY_def vC_def vZ_def
definition EqFXFY :: "'p tm" where
"EqFXFY = (((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vX⇧f⇘ι⇙)) ❙=⇘ι⇙ ((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vY⇧f⇘ι⇙)))"
definition EqXY :: "'p tm" where "EqXY = ((vX⇧f⇘ι⇙) ❙=⇘ι⇙ (vY⇧f⇘ι⇙))"
definition ImpBody :: "'p tm" where "ImpBody = EqFXFY ❙⊃ EqXY"
definition InjBody :: "'p tm" where "InjBody = ❙ΠvX⇘ι⇙. ❙ΠvY⇘ι⇙. ImpBody"
definition NsAtom :: "'p tm" where
"NsAtom = ❙¬ (((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ (vC⇧f⇘ι⇙))"
definition NsBody :: "'p tm" where "NsBody = ❙∃vC⇘ι⇙. ❙ΠvZ⇘ι⇙. NsAtom"
definition DInf :: "'p tm" where "DInf = ❙∃vF⇘ι ❙⇒ ι⇙. (InjBody ❙∧ NsBody)"
lemma wff_EqFXFY [intro]: "wff⇘𝗈⇙(EqFXFY :: 'p tm)"
unfolding EqFXFY_def
by (rule wff_PEq[OF wff_App[OF wff_Fre wff_Fre] wff_App[OF wff_Fre wff_Fre]])
lemma wff_EqXY [intro]: "wff⇘𝗈⇙(EqXY :: 'p tm)"
unfolding EqXY_def by (rule wff_PEq[OF wff_Fre wff_Fre])
lemma wff_ImpBody [intro]: "wff⇘𝗈⇙(ImpBody :: 'p tm)"
unfolding ImpBody_def by (rule wff_ImpB[OF wff_EqFXFY wff_EqXY])
lemma wff_InjBody: "wff⇘𝗈⇙(InjBody :: 'p tm)"
unfolding InjBody_def by (rule wff_AllN[OF wff_AllN[OF wff_ImpBody]])
lemma wff_NsAtom [intro]: "wff⇘𝗈⇙(NsAtom :: 'p tm)"
unfolding NsAtom_def
by (rule wff_Not[OF wff_PEq[OF wff_App[OF wff_Fre wff_Fre] wff_Fre]])
lemma wff_NsBody: "wff⇘𝗈⇙(NsBody :: 'p tm)"
unfolding NsBody_def by (rule wff_ExN[OF wff_AllN[OF wff_NsAtom]])
lemma wff_DInf: "wff⇘𝗈⇙(DInf :: 'p tm)"
unfolding DInf_def by (rule wff_ExN[OF wff_AndB[OF wff_InjBody wff_NsBody]])
lemma fvs_DInf: "fvs (DInf :: 'p tm) = {}"
by (simp add: DInf_def InjBody_def NsBody_def ImpBody_def NsAtom_def EqFXFY_def
EqXY_def AndB_def ExN_def AllN_def Forall_def ImpB_def vdefs)
lemma cwff_DInf: "cwff 𝗈 (DInf :: 'p tm)"
by (rule cwffI[OF wff_DInf fvs_DInf])
lemma pars_DInf: "pars (DInf :: 'p tm) = {}"
by (simp add: DInf_def InjBody_def NsBody_def ImpBody_def NsAtom_def EqFXFY_def
EqXY_def AndB_def ExN_def AllN_def Forall_def ImpB_def vdefs)
text ‹Assembled, the axiom in full --- first by pure definitional unfolding, then, following
the presentation of the Cantor sentences in ‹Cantor›, in its machine-level
locally-nameless normal form (de Bruijn indices ‹Bnd 0›, ‹Bnd (Suc 0)› and so on),
recovered by computation:›
lemma DInf_unfolded:
"(DInf :: 'p tm)
= (❙∃vF⇘ι ❙⇒ ι⇙.
((❙ΠvX⇘ι⇙. ❙ΠvY⇘ι⇙.
((((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vX⇧f⇘ι⇙)) ❙=⇘ι⇙ ((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vY⇧f⇘ι⇙)))
❙⊃ ((vX⇧f⇘ι⇙) ❙=⇘ι⇙ (vY⇧f⇘ι⇙))))
❙∧ (❙∃vC⇘ι⇙. ❙ΠvZ⇘ι⇙. ❙¬ (((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ (vC⇧f⇘ι⇙)))))"
by (simp only: DInf_def InjBody_def NsBody_def ImpBody_def NsAtom_def EqFXFY_def
EqXY_def)
lemma DInf_norm:
"(DInf :: 'p tm)
= ❙∃⇘ι ❙⇒ ι⇙
((❙Π⇘ι⇙ (❙Π⇘ι⇙
(((Bnd (Suc (Suc 0)) ❙⋅ Bnd (Suc 0)) ❙=⇘ι⇙ (Bnd (Suc (Suc 0)) ❙⋅ Bnd 0))
❙⊃ (Bnd (Suc 0) ❙=⇘ι⇙ Bnd 0))))
❙∧ (❙∃⇘ι⇙ (❙Π⇘ι⇙ (❙¬ ((Bnd (Suc (Suc 0)) ❙⋅ Bnd 0) ❙=⇘ι⇙ Bnd (Suc 0))))))"
by (simp add: DInf_def InjBody_def NsBody_def ImpBody_def NsAtom_def EqFXFY_def
EqXY_def AndB_def ExN_def AllN_def Forall_def ImpB_def vdefs)
subsection ‹The axiom derives every finite cardinality›
text ‹The constant-free first-order sentences ``there are at least ‹n› individuals'',
‹❙∃x⇩1 … ❙∃x⇩n. ⋀⇩i⇩<⇩j ❙¬ (x⇩i ❙= x⇩j)›, are derivable from ‹DInf› inside ‹NK›: the
witnesses are ‹C, F C, F (F C), …› for the self-map ‹F› and the point ‹C› outside its
range, and their pairwise distinctness follows from injectivity by induction. The
derivation is built by meta-level recursion on ‹n›, one ‹NK›-derivation for each ‹n›.
These sentences are the standard first-order axiomatisation of infinity; the inequation
scheme derives them too (‹Ineq_derives_distinct_n›, below), and so does the axiom.›
text ‹The sentences. ‹AllNeq t ss› says that ‹t› differs from every member of ‹ss›,
‹Distinct ts› that the members of ‹ts› are pairwise distinct, and ‹ExD ts vs› binds the
variables ‹vs› existentially in front of ‹Distinct (ts @ vs)›. The variable names
‹vD i› are kept apart from the names ‹vF, …, vZ› used in ‹DInf›.›
primrec AllNeq :: "'p tm ⇒ 'p tm list ⇒ 'p tm" where
"AllNeq t [] = ❙⊤"
| "AllNeq t (s # ss) = (❙¬ (t ❙=⇘ι⇙ s)) ❙∧ AllNeq t ss"
primrec Distinct :: "'p tm list ⇒ 'p tm" where
"Distinct [] = ❙⊤"
| "Distinct (t # ts) = AllNeq t ts ❙∧ Distinct ts"
primrec ExD :: "'p tm list ⇒ nat list ⇒ 'p tm" where
"ExD ts [] = Distinct ts"
| "ExD ts (v # vs) = ❙∃v⇘ι⇙. ExD (ts @ [v⇧f⇘ι⇙]) vs"
definition vD :: "nat ⇒ nat" where "vD i = 10 + i"
definition ExDistinct :: "nat ⇒ 'p tm" where
"ExDistinct n = ExD [] (map vD [0..<n])"
lemma wff_AllNeq: "wff⇘ι⇙(t) ⟹ ∀s ∈ set ss. wff⇘ι⇙(s) ⟹ wff⇘𝗈⇙(AllNeq t ss)"
by (induction ss) (auto intro: wff_AndB wff_Not wff_PEq)
lemma wff_Distinct: "∀t ∈ set ts. wff⇘ι⇙(t) ⟹ wff⇘𝗈⇙(Distinct ts)"
by (induction ts) (auto intro: wff_AndB wff_AllNeq)
lemma wff_ExD: "∀t ∈ set ts. wff⇘ι⇙(t) ⟹ wff⇘𝗈⇙(ExD ts vs)"
proof (induction vs arbitrary: ts)
case Nil thus ?case by (simp add: wff_Distinct)
next
case (Cons v vs)
have "wff⇘𝗈⇙(ExD (ts @ [v⇧f⇘ι⇙]) vs)"
by (rule Cons.IH) (use Cons.prems in ‹auto intro: wff_Fre›)
thus ?case by (simp add: wff_ExN)
qed
lemma wff_ExDistinct: "wff⇘𝗈⇙(ExDistinct n)"
unfolding ExDistinct_def by (rule wff_ExD) simp
lemma fsub_AllNeq: "fsub x σ u (AllNeq t ss) = AllNeq (fsub x σ u t) (map (fsub x σ u) ss)"
by (induction ss) auto
lemma fsub_Distinct: "fsub x σ u (Distinct ts) = Distinct (map (fsub x σ u) ts)"
by (induction ts) (auto simp: fsub_AllNeq)
lemma fsub_ExD:
"x ∉ set vs ⟹ fvs u = {} ⟹ fsub x ι u (ExD ts vs) = ExD (map (fsub x ι u) ts) vs"
by (induction vs arbitrary: ts) (auto simp: fsub_Distinct fsub_ExN)
lemma pars_AllNeq: "pars (AllNeq t ss) ⊆ pars t ∪ (⋃s ∈ set ss. pars s)"
by (induction ss) (auto simp: AndB_def)
lemma pars_Distinct: "pars (Distinct ts) ⊆ (⋃t ∈ set ts. pars t)"
by (induction ts) (auto simp: AndB_def dest: subsetD[OF pars_AllNeq])
lemma pars_ExD: "pars (ExD ts vs) ⊆ (⋃t ∈ set ts. pars t)"
proof (induction vs arbitrary: ts)
case Nil thus ?case by (simp add: pars_Distinct)
next
case (Cons v vs)
have "pars (ExD ts (v # vs)) = pars (ExD (ts @ [v⇧f⇘ι⇙]) vs)" by (simp add: ExN_def)
also have "… ⊆ (⋃t ∈ set (ts @ [v⇧f⇘ι⇙]). pars t)" by (rule Cons.IH)
also have "… = (⋃t ∈ set ts. pars t)" by simp
finally show ?case .
qed
lemma pars_ExDistinct: "pars (ExDistinct n) = {}"
using pars_ExD[of "[]" "map vD [0..<n]"] by (simp add: ExDistinct_def)
text ‹The witnesses ‹F⇧k C›, as closed object terms over two parameters.›
primrec itF :: "'p ⇒ 'p ⇒ nat ⇒ 'p tm" where
"itF F C 0 = C⇧p⇘ι⇙"
| "itF F C (Suc k) = (F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ itF F C k"
lemma wff_itF [simp, intro]: "wff⇘ι⇙(itF F C k)"
by (induction k) (auto intro: wff_Par wff_App)
lemma fvs_itF [simp]: "fvs (itF F C k) = {}"
by (induction k) auto
lemma fsub_itF [simp]: "fsub x σ u (itF F C k) = itF F C k"
by (rule fsub_notin) simp
text ‹Pairwise distinctness assembled into the sentence ‹Distinct›, for any family of
closed witnesses whose members below a bound ‹N› are provably distinct.›
lemma AllNeq_family:
assumes fp: "freep Φ" and wt: "⋀k. wff⇘ι⇙(t k)"
and neq: "⋀i j. i < j ⟹ j < N ⟹ Φ ⊢ ❙¬ (t i ❙=⇘ι⇙ t j)"
shows "∀j ∈ set js. i < j ∧ j < N ⟹ Φ ⊢ AllNeq (t i) (map t js)"
proof (induction js)
case Nil show ?case by (simp add: bprov_TrueB)
next
case (Cons j js)
have ij: "i < j" "j < N" and rest: "∀j ∈ set js. i < j ∧ j < N" using Cons.prems by auto
show ?case unfolding list.map AllNeq.simps
by (rule AndI[OF neq[OF ij] Cons.IH[OF rest] _ _ fp])
(auto del: wff_Not wff_PEq intro!: wff_AllNeq wff_Not wff_PEq wff_Eq wff_App wff_Par wt)
qed
lemma Distinct_family:
assumes fp: "freep Φ" and wt: "⋀k. wff⇘ι⇙(t k)"
and neq: "⋀i j. i < j ⟹ j < N ⟹ Φ ⊢ ❙¬ (t i ❙=⇘ι⇙ t j)"
shows "i + m ≤ N ⟹ Φ ⊢ Distinct (map t [i..<i + m])"
proof (induction m arbitrary: i)
case 0 show ?case by (simp add: bprov_TrueB)
next
case (Suc m)
have e: "[i..<i + Suc m] = i # [Suc i..<Suc i + m]"
using upt_conv_Cons[of i "i + Suc m"] by simp
show ?case unfolding e list.map Distinct.simps
by (rule AndI[OF AllNeq_family[OF fp wt neq] Suc.IH _ _ fp])
(use Suc.prems in ‹auto intro!: wff_AllNeq wff_Distinct wt›)
qed
text ‹The derivation, from the two witnessed halves of ‹DInf›: injectivity of ‹F› and the
point ‹C› outside its range.›
context
fixes F C :: "'p::infinite" and Φ :: "'p tm set"
assumes fp: "freep Φ"
and inj: "Φ ⊢ ❙ΠvX⇘ι⇙. ❙ΠvY⇘ι⇙.
((((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ (vX⇧f⇘ι⇙)) ❙=⇘ι⇙ ((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ (vY⇧f⇘ι⇙)))
❙⊃ ((vX⇧f⇘ι⇙) ❙=⇘ι⇙ (vY⇧f⇘ι⇙)))"
and ns: "Φ ⊢ ❙ΠvZ⇘ι⇙. ❙¬ (((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ (C⇧p⇘ι⇙))"
begin
lemma inj_inst:
"Φ ⊢ (itF F C (Suc i) ❙=⇘ι⇙ itF F C (Suc j)) ❙⊃ (itF F C i ❙=⇘ι⇙ itF F C j)"
proof -
have 1: "Φ ⊢ fsub vX ι (itF F C i) (❙ΠvY⇘ι⇙.
((((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ (vX⇧f⇘ι⇙)) ❙=⇘ι⇙ ((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ (vY⇧f⇘ι⇙)))
❙⊃ ((vX⇧f⇘ι⇙) ❙=⇘ι⇙ (vY⇧f⇘ι⇙))))"
by (rule AllN_E[OF inj _ wff_itF])
(auto del: wff_ImpB wff_PEq
intro!: wff_AllN wff_ImpB wff_PEq wff_Eq wff_App wff_Par wff_Fre)
have 2: "Φ ⊢ ❙ΠvY⇘ι⇙.
((((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ itF F C i) ❙=⇘ι⇙ ((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ (vY⇧f⇘ι⇙)))
❙⊃ (itF F C i ❙=⇘ι⇙ (vY⇧f⇘ι⇙)))"
using 1 by (simp add: fsub_AllN vdefs)
have 3: "Φ ⊢ fsub vY ι (itF F C j)
((((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ itF F C i) ❙=⇘ι⇙ ((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ (vY⇧f⇘ι⇙)))
❙⊃ (itF F C i ❙=⇘ι⇙ (vY⇧f⇘ι⇙)))"
by (rule AllN_E[OF 2 _ wff_itF])
(auto del: wff_ImpB wff_PEq intro!: wff_ImpB wff_PEq wff_Eq wff_App wff_Par wff_Fre)
thus ?thesis by (simp add: vdefs)
qed
lemma ns_inst: "Φ ⊢ ❙¬ (itF F C (Suc k) ❙=⇘ι⇙ itF F C 0)"
proof -
have "Φ ⊢ fsub vZ ι (itF F C k) (❙¬ (((F⇧p⇘ι ❙⇒ ι⇙) ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ (C⇧p⇘ι⇙)))"
by (rule AllN_E[OF ns _ wff_itF])
(auto del: wff_Not wff_PEq intro!: wff_Not wff_PEq wff_Eq wff_App wff_Par wff_Fre)
thus ?thesis by (simp add: vdefs)
qed
lemma neq_itF: "i < j ⟹ Φ ⊢ ❙¬ (itF F C i ❙=⇘ι⇙ itF F C j)"
proof (induction i arbitrary: j)
case 0
then obtain k where j: "j = Suc k" by (cases j) auto
show ?case unfolding j by (rule peq_neg_sym[OF ns_inst fp wff_itF wff_itF])
next
case (Suc i)
then obtain k where j: "j = Suc k" and ik: "i < k" by (cases j) auto
let ?E = "itF F C (Suc i) ❙=⇘ι⇙ itF F C (Suc k)"
have fp': "freep (Φ ∪ {?E})" by (rule freep_un[OF fp])
have imp: "Φ ∪ {?E} ⊢ ?E ❙⊃ (itF F C i ❙=⇘ι⇙ itF F C k)"
by (rule bprov_weaken[OF inj_inst]) (auto simp: freep_add fp)
have hyp: "Φ ∪ {?E} ⊢ ?E" by (auto intro: bprov.Hyp)
have p: "Φ ∪ {?E} ⊢ itF F C i ❙=⇘ι⇙ itF F C k"
by (rule bprov_ImpE[OF imp hyp fp'])
(auto del: wff_PEq intro!: wff_PEq wff_Eq wff_App wff_Par)
have n: "Φ ∪ {?E} ⊢ ❙¬ (itF F C i ❙=⇘ι⇙ itF F C k)"
by (rule bprov_weaken[OF Suc.IH[OF ik]]) (auto simp: freep_add fp)
have "Φ ∪ {?E} ⊢ ❙⊥" by (rule bprov.NegE[OF n p wff_FalseB])
thus ?case unfolding j by (rule bprov.NegI[OF _ wff_PEq[OF wff_itF wff_itF]])
qed
lemma Distinct_itF: "Φ ⊢ Distinct (map (itF F C) [0..<n])"
proof -
have neq: "⋀i j. i < j ⟹ j < n ⟹ Φ ⊢ ❙¬ (itF F C i ❙=⇘ι⇙ itF F C j)"
by (rule neq_itF)
show ?thesis using Distinct_family[OF fp wff_itF neq, where i = 0 and m = n] by simp
qed
end
text ‹Existential closure: from the distinctness of closed witnesses to the sentence.›
lemma ExD_I:
assumes d: "Φ ⊢ Distinct (ts @ us)" and fp: "freep Φ"
and cts: "∀t ∈ set ts. wff⇘ι⇙(t) ∧ fvs t = {}"
and cus: "∀u ∈ set us. wff⇘ι⇙(u) ∧ fvs u = {}"
and len: "length us = length vs" and dv: "distinct vs"
shows "Φ ⊢ ExD ts vs"
using d cts cus len dv
proof (induction vs arbitrary: ts us)
case Nil thus ?case by simp
next
case (Cons v vs)
obtain u us' where us: "us = u # us'" using Cons.prems(4) by (cases us) auto
have IH: "Φ ⊢ ExD (ts @ [u]) vs"
by (rule Cons.IH) (use Cons.prems us in auto)
have wb: "wff⇘𝗈⇙(ExD (ts @ [v⇧f⇘ι⇙]) vs)"
by (rule wff_ExD) (use Cons.prems(2) in ‹auto intro: wff_Fre›)
have m: "map (fsub v ι u) ts = ts"
using Cons.prems(2) by (auto intro!: map_idI simp: fsub_notin)
have sub: "fsub v ι u (ExD (ts @ [v⇧f⇘ι⇙]) vs) = ExD (ts @ [u]) vs"
using Cons.prems(3,5) us by (simp add: fsub_ExD m)
show ?case unfolding ExD.simps
by (rule ExN_I[OF IH[folded sub] wb _ fp]) (use Cons.prems(3) us in auto)
qed
theorem DInf_derives_distinct_n: "{DInf :: 'p::infinite tm} ⊢ ExDistinct n"
proof -
obtain F C :: 'p where FC: "F ≠ C"
by (metis (full_types) ex_new_if_finite finite.emptyI
finite.insertI infinite_UNIV insert_iff)
note CF = FC[symmetric]
let ?FP = "F⇧p⇘ι ❙⇒ ι⇙ :: 'p tm" and ?CP = "C⇧p⇘ι⇙ :: 'p tm"
define InjF :: "'p tm" where
"InjF = ❙ΠvX⇘ι⇙. ❙ΠvY⇘ι⇙. (((?FP ❙⋅ (vX⇧f⇘ι⇙)) ❙=⇘ι⇙ (?FP ❙⋅ (vY⇧f⇘ι⇙)))
❙⊃ ((vX⇧f⇘ι⇙) ❙=⇘ι⇙ (vY⇧f⇘ι⇙)))"
define NsB :: "'p tm" where "NsB = ❙ΠvZ⇘ι⇙. ❙¬ ((?FP ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ (vC⇧f⇘ι⇙))"
define NsC :: "'p tm" where "NsC = ❙ΠvZ⇘ι⇙. ❙¬ ((?FP ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ ?CP)"
have subF: "fsub vF (ι ❙⇒ ι) ?FP (InjBody ❙∧ NsBody) = InjF ❙∧ (❙∃vC⇘ι⇙. NsB)"
by (simp add: InjF_def NsB_def InjBody_def NsBody_def ImpBody_def NsAtom_def
EqFXFY_def EqXY_def fsub_AllN fsub_ExN vdefs)
have subC: "fsub vC ι ?CP NsB = NsC"
by (simp add: NsB_def NsC_def fsub_AllN vdefs)
have wInjF: "wff⇘𝗈⇙(InjF)" unfolding InjF_def
by (auto del: wff_ImpB wff_PEq
intro!: wff_AllN wff_ImpB wff_PEq wff_Eq wff_App wff_Par wff_Fre)
have wNsB: "wff⇘𝗈⇙(NsB)" unfolding NsB_def
by (auto del: wff_Not wff_PEq
intro!: wff_AllN wff_Not wff_PEq wff_Eq wff_App wff_Par wff_Fre)
have wExNsB: "wff⇘𝗈⇙(❙∃vC⇘ι⇙. NsB)" by (rule wff_ExN[OF wNsB])
have wBody: "wff⇘𝗈⇙(InjBody ❙∧ NsBody :: 'p tm)" by (rule wff_AndB[OF wff_InjBody wff_NsBody])
have pBody: "pars (InjBody ❙∧ NsBody :: 'p tm) = {}"
by (simp add: InjBody_def NsBody_def ImpBody_def NsAtom_def EqFXFY_def EqXY_def
AndB_def ExN_def AllN_def)
have pInjF: "pars InjF = {F}" by (simp add: InjF_def AllN_def)
have pNsB: "pars NsB = {F}" by (simp add: NsB_def AllN_def)
let ?Φ1 = "{DInf :: 'p tm} ∪ {InjF ❙∧ (❙∃vC⇘ι⇙. NsB)}"
let ?Φ2 = "?Φ1 ∪ {NsC}"
have fp0: "freep {DInf :: 'p tm}" and fp1: "freep ?Φ1" and fp2: "freep ?Φ2"
by (intro freep_finite; simp)+
have and2: "?Φ2 ⊢ InjF ❙∧ (❙∃vC⇘ι⇙. NsB)" by (auto intro: bprov.Hyp)
have inj2: "?Φ2 ⊢ InjF" by (rule AndE1[OF and2 wInjF wExNsB fp2])
have ns2: "?Φ2 ⊢ NsC" by (auto intro: bprov.Hyp)
have inj2': "?Φ2 ⊢ ❙ΠvX⇘ι⇙. ❙ΠvY⇘ι⇙. (((?FP ❙⋅ (vX⇧f⇘ι⇙)) ❙=⇘ι⇙ (?FP ❙⋅ (vY⇧f⇘ι⇙)))
❙⊃ ((vX⇧f⇘ι⇙) ❙=⇘ι⇙ (vY⇧f⇘ι⇙)))"
using inj2 by (simp add: InjF_def)
have ns2': "?Φ2 ⊢ ❙ΠvZ⇘ι⇙. ❙¬ ((?FP ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ ?CP)"
using ns2 by (simp add: NsC_def)
have d: "?Φ2 ⊢ Distinct (map (itF F C) [0..<n])"
by (rule Distinct_itF[OF fp2 inj2' ns2'])
have main: "?Φ2 ⊢ ExDistinct n"
unfolding ExDistinct_def
proof (rule ExD_I[OF _ fp2])
show "?Φ2 ⊢ Distinct ([] @ map (itF F C) [0..<n])" using d by simp
show "distinct (map vD [0..<n])" by (simp add: distinct_map inj_on_def vD_def)
qed simp_all
have ex1: "?Φ1 ⊢ ❙∃vC⇘ι⇙. NsB"
by (rule AndE2[OF _ wInjF wExNsB fp1]) (auto intro: bprov.Hyp)
have h1: "?Φ1 ⊢ ExDistinct n"
by (rule ExN_E[OF ex1 main[folded subC] wNsB wff_ExDistinct _ _ _ fp1])
(simp_all add: pNsB pInjF pars_DInf pars_ExDistinct AndB_def ExN_def CF)
have ex0: "{DInf :: 'p tm} ⊢ ❙∃vF⇘ι ❙⇒ ι⇙. (InjBody ❙∧ NsBody)"
using bprov.Hyp[of "DInf :: 'p tm" "{DInf}"] unfolding DInf_def by simp
show ?thesis
by (rule ExN_E[OF ex0 h1[folded subF] wBody wff_ExDistinct _ _ _ fp0])
(simp_all add: pBody pars_DInf pars_ExDistinct)
qed
subsection ‹Injectivity and non-surjectivity in an arbitrary general model›
text ‹These facts hold in ∗‹any› ‹Σ›-Henkin general model --- fullness of the function
domains is never used: they peel ‹InjBody› / ‹NsBody› down
to injectivity and non-surjectivity of a self-map ‹d› on the individuals. Only the
witness for such a ‹d› is model-specific, so ‹DInf_sat› takes that data as hypotheses,
and the consistency arguments about ‹DInf›, here and in the companion development,
share this carrier-generic core. Conversely, ‹DInf_sat_Dedekind_infinite› extracts
from satisfaction of ‹DInf› an injective, non-surjective self-map of the individual
domain: even in a Henkin model, the axiom forces Dedekind infinitude of ‹𝒟⇘ι⇙›.›
context general_model
begin
lemma InjSat:
assumes xi: "bkkA.asg ξ" and d: "Dm (ι ❙⇒ ι) d"
shows "(den InjBody (ξ(vF⇘ι ❙⇒ ι⇙ := d)) = Tv)
= (∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (d ❙@ a = d ❙@ b ⟶ a = b)))"
proof -
define η where "η = ξ(vF⇘ι ❙⇒ ι⇙ := d)"
have ea: "bkkA.asg η" unfolding η_def using xi d by (rule bkkA.asg_upd)
have inner: "(den ImpBody ((η(vX⇘ι⇙ := a))(vY⇘ι⇙ := b)) = Tv)
= (d ❙@ a = d ❙@ b ⟶ a = b)" if a: "Dm ι a" and b: "Dm ι b" for a b
proof -
define ρ where "ρ = (η(vX⇘ι⇙ := a))(vY⇘ι⇙ := b)"
have er: "bkkA.asg ρ" unfolding ρ_def using ea a b by (auto intro: bkkA.asg_upd)
have fx: "den ((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vX⇧f⇘ι⇙)) ρ = d ❙@ a"
by (simp add: den.simps(8) ρ_def η_def upd_def vdefs)
have fy: "den ((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vY⇧f⇘ι⇙)) ρ = d ❙@ b"
by (simp add: den.simps(8) ρ_def η_def upd_def vdefs)
have ex: "den (vX⇧f⇘ι⇙) ρ = a" by (simp add: ρ_def upd_def vdefs)
have ey: "den (vY⇧f⇘ι⇙) ρ = b" by (simp add: ρ_def upd_def vdefs)
have peq1: "(den EqFXFY ρ = Tv) = (d ❙@ a = d ❙@ b)"
unfolding EqFXFY_def
using sat_PEqB[OF wff_App[OF wff_Fre wff_Fre] wff_App[OF wff_Fre wff_Fre] er] fx fy
by simp
have peq2: "(den EqXY ρ = Tv) = (a = b)"
unfolding EqXY_def using sat_PEqB[OF wff_Fre wff_Fre er] ex ey by simp
have "(den ImpBody ρ = Tv)
= ((den EqFXFY ρ = Tv) ⟶ (den EqXY ρ = Tv))"
unfolding ImpBody_def by (rule sat_ImpBB[OF wff_EqFXFY wff_EqXY er])
also have "… = (d ❙@ a = d ❙@ b ⟶ a = b)" using peq1 peq2 by simp
finally show ?thesis by (simp add: ρ_def)
qed
have step2: "(den (❙ΠvY⇘ι⇙. ImpBody) (η(vX⇘ι⇙ := a)) = Tv)
= (∀b. Dm ι b ⟶ (d ❙@ a = d ❙@ b ⟶ a = b))" if a: "Dm ι a" for a
proof -
have "(den (❙ΠvY⇘ι⇙. ImpBody) (η(vX⇘ι⇙ := a)) = Tv)
= (∀b. Dm ι b ⟶ den ImpBody ((η(vX⇘ι⇙ := a))(vY⇘ι⇙ := b)) = Tv)"
by (rule sat_AllN[OF wff_ImpBody bkkA.asg_upd[OF ea a]])
thus ?thesis using inner[OF a] by simp
qed
have "(den InjBody η = Tv)
= (∀a. Dm ι a ⟶ den (❙ΠvY⇘ι⇙. ImpBody) (η(vX⇘ι⇙ := a)) = Tv)"
unfolding InjBody_def by (rule sat_AllN[OF wff_AllN[OF wff_ImpBody] ea])
thus ?thesis using step2 by (simp add: η_def)
qed
lemma NsSat:
assumes xi: "bkkA.asg ξ" and d: "Dm (ι ❙⇒ ι) d"
shows "(den NsBody (ξ(vF⇘ι ❙⇒ ι⇙ := d)) = Tv)
= (∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ d ❙@ z ≠ c))"
proof -
define η where "η = ξ(vF⇘ι ❙⇒ ι⇙ := d)"
have ea: "bkkA.asg η" unfolding η_def using xi d by (rule bkkA.asg_upd)
have inner: "(den NsAtom ((η(vC⇘ι⇙ := c))(vZ⇘ι⇙ := z)) = Tv)
= (d ❙@ z ≠ c)" if c: "Dm ι c" and z: "Dm ι z" for c z
proof -
define ρ where "ρ = (η(vC⇘ι⇙ := c))(vZ⇘ι⇙ := z)"
have er: "bkkA.asg ρ" unfolding ρ_def using ea c z by (auto intro: bkkA.asg_upd)
have fz: "den ((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vZ⇧f⇘ι⇙)) ρ = d ❙@ z"
by (simp add: den.simps(8) ρ_def η_def upd_def vdefs)
have ec: "den (vC⇧f⇘ι⇙) ρ = c" by (simp add: ρ_def upd_def vdefs)
have peq: "(den (((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ (vC⇧f⇘ι⇙)) ρ = Tv) = (d ❙@ z = c)"
using sat_PEqB[OF wff_App[OF wff_Fre wff_Fre] wff_Fre er] fz ec by simp
have "(den NsAtom ρ = Tv)
= (¬ (den (((vF⇧f⇘ι ❙⇒ ι⇙) ❙⋅ (vZ⇧f⇘ι⇙)) ❙=⇘ι⇙ (vC⇧f⇘ι⇙)) ρ = Tv))"
unfolding NsAtom_def
by (rule sat_NegB[OF wff_PEq[OF wff_App[OF wff_Fre wff_Fre] wff_Fre] er])
also have "… = (d ❙@ z ≠ c)" using peq by simp
finally show ?thesis by (simp add: ρ_def)
qed
have step2: "(den (❙ΠvZ⇘ι⇙. NsAtom) (η(vC⇘ι⇙ := c)) = Tv)
= (∀z. Dm ι z ⟶ d ❙@ z ≠ c)" if c: "Dm ι c" for c
proof -
have "(den (❙ΠvZ⇘ι⇙. NsAtom) (η(vC⇘ι⇙ := c)) = Tv)
= (∀z. Dm ι z ⟶ den NsAtom ((η(vC⇘ι⇙ := c))(vZ⇘ι⇙ := z)) = Tv)"
by (rule sat_AllN[OF wff_NsAtom bkkA.asg_upd[OF ea c]])
thus ?thesis using inner[OF c] by simp
qed
have hall: "(den NsBody η = Tv)
= (∃c. Dm ι c ∧ den (❙ΠvZ⇘ι⇙. NsAtom) (η(vC⇘ι⇙ := c)) = Tv)"
unfolding NsBody_def by (rule sat_ExN[OF wff_AllN[OF wff_NsAtom] ea])
have "(den NsBody η = Tv) = (∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ d ❙@ z ≠ c))"
using hall by (simp add: step2 cong: conj_cong)
thus ?thesis by (simp add: η_def)
qed
lemma DInf_sat:
assumes xi: "bkkA.asg ξ" and d: "Dm (ι ❙⇒ ι) d"
and inj: "∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (d ❙@ a = d ❙@ b ⟶ a = b))"
and ns: "∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ d ❙@ z ≠ c)"
shows "den DInf ξ = Tv"
proof -
have conj: "den (InjBody ❙∧ NsBody) (ξ(vF⇘ι ❙⇒ ι⇙ := d)) = Tv"
using sat_AndB[OF wff_InjBody wff_NsBody bkkA.asg_upd[OF xi d]]
InjSat[OF xi d] NsSat[OF xi d] inj ns by simp
have "(den DInf ξ = Tv)
= (∃e. Dm (ι ❙⇒ ι) e ∧ den (InjBody ❙∧ NsBody) (ξ(vF⇘ι ❙⇒ ι⇙ := e)) = Tv)"
unfolding DInf_def by (rule sat_ExN[OF wff_AndB[OF wff_InjBody wff_NsBody] xi])
thus ?thesis using d conj by auto
qed
lemma DInf_sat_Dedekind_infinite:
assumes xi: "bkkA.asg ξ" and sat: "den DInf ξ = Tv"
shows "∃d. Dm (ι ❙⇒ ι) d
∧ (∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (d ❙@ a = d ❙@ b ⟶ a = b)))
∧ (∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ d ❙@ z ≠ c))"
proof -
have unf: "(den DInf ξ = Tv)
= (∃e. Dm (ι ❙⇒ ι) e ∧ den (InjBody ❙∧ NsBody) (ξ(vF⇘ι ❙⇒ ι⇙ := e)) = Tv)"
unfolding DInf_def by (rule sat_ExN[OF wff_AndB[OF wff_InjBody wff_NsBody] xi])
from sat unf obtain e where e: "Dm (ι ❙⇒ ι) e"
and cj: "den (InjBody ❙∧ NsBody) (ξ(vF⇘ι ❙⇒ ι⇙ := e)) = Tv" by auto
have inj: "∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (e ❙@ a = e ❙@ b ⟶ a = b))"
and ns: "∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ e ❙@ z ≠ c)"
using cj sat_AndB[OF wff_InjBody wff_NsBody bkkA.asg_upd[OF xi e]]
InjSat[OF xi e] NsSat[OF xi e] by simp_all
show ?thesis using e inj ns by blast
qed
end
section ‹Consistency of the scheme, and its separation from the axiom›
text ‹The scheme does not yield the axiom. Every general model with @{emph ‹finitely›} many individuals refutes ‹DInf›
--- an injective self-map of a finite set is surjective --- while a large enough finite
standard model satisfies any finite part of the scheme. Hence the scheme together with ‹❙¬ DInf› is consistent,
no finite part of ‹Ineq f› derives ‹DInf› (‹¬ (Ineq f ⊩ DInf)›), and a Henkin
model of the whole scheme, countable over a countable signature, refutes the axiom,
making the separation model-theoretic. All of this stays
in plain HOL: the refuting models are the finite ones from ‹Consistency›, and the Henkin
model is the term model of ‹Completeness›. Conversely, ‹DInf› mentions no constants, so
once a model of it exists, one in which all constants coincide refutes every inequation;
the companion notes this in passing. This separation rests on the auxiliary constants of the scheme: ‹DInf› derives,
for every ‹n›, the existence of ‹n› pairwise distinct individuals
(@{thm [source] DInf_derives_distinct_n}), so every constant-free consequence of a finite
part of the scheme is a consequence of ‹DInf› (the remaining step, replacing the
constants of a derivation by terms, is not formalised here); and
over standard models the whole scheme entails ‹DInf›, since an infinite individual domain
with full function spaces has an injective, non-surjective self-map (not formalised here
either). What the scheme cannot supply is that self-map as an element of ‹𝒟⇘ι ❙⇒ ι⇙›,
and that is where its Henkin models refute the axiom.›
context general_model
begin
text ‹The two directions combined: in any general model, ‹DInf› holds exactly when the
function domain ‹𝒟⇘ι ❙⇒ ι⇙› contains an injective, non-surjective self-map of the
individuals. In a standard model, where that domain is full, this is Dedekind
infinitude of ‹𝒟⇘ι⇙›; in a Henkin model the domain may lack the self-map.›
lemma DInf_sat_iff:
assumes xi: "bkkA.asg ξ"
shows "(den DInf ξ = Tv)
= (∃d. Dm (ι ❙⇒ ι) d
∧ (∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (d ❙@ a = d ❙@ b ⟶ a = b)))
∧ (∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ d ❙@ z ≠ c)))"
using DInf_sat[OF xi] DInf_sat_Dedekind_infinite[OF xi] by blast
lemma DInf_refuted_finite:
assumes xi: "bkkA.asg ξ" and fin: "finite {x. Dm ι x}"
shows "den (❙¬ DInf) ξ = Tv"
proof -
have "¬ (den DInf ξ = Tv)"
proof
assume "den DInf ξ = Tv"
then obtain d where d: "Dm (ι ❙⇒ ι) d"
and dinj: "∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (d ❙@ a = d ❙@ b ⟶ a = b))"
and dns: "∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ d ❙@ z ≠ c)"
using DInf_sat_iff[OF xi] by blast
have eq: "(λa. d ❙@ a) ` {x. Dm ι x} = {x. Dm ι x}"
proof (rule endo_inj_surj[OF fin])
show "(λa. d ❙@ a) ` {x. Dm ι x} ⊆ {x. Dm ι x}"
using gm_appTy[OF d] by auto
show "inj_on (λa. d ❙@ a) {x. Dm ι x}"
using dinj by (auto simp: inj_on_def)
qed
obtain c where c: "Dm ι c" and nc: "∀z. Dm ι z ⟶ d ❙@ z ≠ c"
using dns by blast
have "c ∈ (λa. d ❙@ a) ` {x. Dm ι x}" using c eq by auto
then obtain z where "Dm ι z" and "d ❙@ z = c" by auto
thus False using nc by blast
qed
thus ?thesis using sat_NegB[OF wff_DInf xi] by simp
qed
end
text ‹The refuting finite models: the size-‹k› family of ‹Consistency›, with the parameter
interpretation distinguishing the finitely many constants of the scheme at hand. The
construction happens @{emph ‹once›}: the same model satisfies the fragment and refutes
the axiom, and the plain consistency of the scheme falls out by monotonicity below.›
lemma con_DInf_neg_finite_sub:
assumes injf: "inj (f :: nat ⇒ 'p::infinite)"
and finF: "finite F" and FI: "F ⊆ Ineq f"
shows "con (insert (❙¬ DInf) F)"
proof -
have finP: "finite {(i,j). dneq f i j ∈ F}"
proof -
have "{(i,j). dneq f i j ∈ F} = (λ(i,j). dneq f i j) -` F"
by (auto simp: vimage_def)
moreover have "inj (λ(i,j). dneq f i j :: 'p tm)"
by (auto simp: inj_on_def dneq_inj[OF injf])
ultimately show ?thesis using finite_vimageI[OF finF] by simp
qed
define idxs where "idxs = (⋃(i,j)∈{(i,j). dneq f i j ∈ F}. {i,j})"
have finI: "finite idxs" unfolding idxs_def using finP by auto
define m where "m = Max (insert 0 idxs)"
define k where "k = Suc m"
define ix where "ix = (λp::'p. min m (inv f p))"
have kpos: "0 < k" by (simp add: k_def)
have ix_le: "ix p ≤ m" for p by (simp add: ix_def)
have ix_bound: "ix p < k" for p using ix_le[of p] by (simp add: k_def)
have ix_f: "ix (f i) = i" if "i ≤ m" for i
using that by (simp add: ix_def inv_f_f[OF injf] min.absorb2)
have idx_le: "i ≤ m" if "dneq f i j ∈ F" for i j
unfolding m_def
proof (rule Max_ge)
show "finite (insert 0 idxs)" using finI by simp
show "i ∈ insert 0 idxs" using that unfolding idxs_def by auto
qed
have jdx_le: "j ≤ m" if "dneq f i j ∈ F" for i j
unfolding m_def
proof (rule Max_ge)
show "finite (insert 0 idxs)" using finI by simp
show "j ∈ insert 0 idxs" using that unfolding idxs_def by auto
qed
interpret U: lambda_universe "cD k" cAp "cLm k" "VB True" "VB False"
"cJv k ix :: 'p ⇒ ty ⇒ ival"
by (rule concrete_lambda_universe[OF kpos ix_bound])
interpret standard_model "cD k" cAp "cLm k" "VB True" "VB False"
U.Ngv U.Dsv U.Iv U.Ev U.Piv "cJv k ix :: 'p ⇒ ty ⇒ ival"
by (rule U.is_standard_model)
have asgX: "bkkA.asg (cXi k)" by (simp add: bkkA.asg_def cXi_def hd_en_dom[OF kpos])
have vEq: "cAp (cAp (U.Ev ι) (VI a)) (VI b) = VB (a = b)" if "a < k" "b < k" for a b
using U.Ev_app[of ι "VI a" "VI b"] that by (simp add: cD_def)
have vNg: "cAp U.Ngv (VB c) = VB (¬ c)" for c
using U.Ngv_app[of "VB c"] by (cases c) (auto simp: cD_def)
have den_dneq: "den (dneq f i j) (cXi k) = VB (ix (f i) ≠ ix (f j))"
if hi: "ix (f i) < k" and hj: "ix (f j) < k" for i j
proof -
have "den (dneq f i j) (cXi k)
= cAp U.Ngv (cAp (cAp (U.Ev ι) (VI (ix (f i)))) (VI (ix (f j))))"
unfolding dneq_def by (simp add: den.simps(8) cJv_def)
also have "… = cAp U.Ngv (VB (ix (f i) = ix (f j)))"
using vEq[OF hi hj] by simp
also have "… = VB (ix (f i) ≠ ix (f j))" using vNg by simp
finally show ?thesis .
qed
have Fsat: "∀B∈F. wff⇘𝗈⇙(B) ∧ den B (cXi k) = VB True"
proof
fix B assume "B ∈ F"
then have "B ∈ Ineq f" using FI by blast
then obtain i j where B: "B = dneq f i j" and ne: "i ≠ j"
by (auto simp: Ineq_iff)
have im: "i ≤ m" and jm: "j ≤ m"
using ‹B ∈ F› B by (auto intro: idx_le jdx_le)
have "den B (cXi k) = VB (ix (f i) ≠ ix (f j))"
unfolding B by (rule den_dneq[OF ix_bound ix_bound])
also have "… = VB (i ≠ j)" by (simp add: ix_f[OF im] ix_f[OF jm])
also have "… = VB True" using ne by simp
finally show "wff⇘𝗈⇙(B) ∧ den B (cXi k) = VB True"
using B by (simp add: wff_dneq)
qed
have finD: "finite {x. cD k ι x}" by (simp add: cD_def)
have nDsat: "den (❙¬ DInf :: 'p tm) (cXi k) = VB True"
by (rule DInf_refuted_finite[OF asgX finD])
show ?thesis
by (rule model_con[OF asgX])
(use Fsat nDsat wff_DInf in ‹auto intro!: wff_Not›)
qed
text ‹Discarding the refuted axiom, monotonicity gives the finite consistency of the
finite parts of the scheme --- the compactness argument announced above --- and
compactness the consistency of the whole scheme.›
lemma con_finite_sub:
assumes injf: "inj (f :: nat ⇒ 'p::infinite)"
and finF: "finite F" and FI: "F ⊆ Ineq f"
shows "con F"
proof -
have "con (insert (❙¬ DInf) F)" by (rule con_DInf_neg_finite_sub[OF assms])
moreover have "F ⊆ insert (❙¬ DInf) F" by auto
moreover have "freep (insert (❙¬ DInf) F)"
by (rule freep_finite) (simp add: finF)
ultimately show ?thesis by (rule con_mono)
qed
theorem con_Ineq:
assumes "inj (f :: nat ⇒ 'p::infinite)"
shows "con (Ineq f)"
by (rule con_compact) (rule con_finite_sub[OF assms])
text ‹A caveat on ‹con› for an impure infinite context. ‹⊢› derives from the whole
context, and ‹NK(ΠI)› needs an eigen-parameter that occurs nowhere in it. If ‹f› uses
every parameter (‹'p = ℕ›, ‹f› surjective), no such parameter exists, and
‹con (Ineq f)› then holds partly because generalisation is blocked. The proviso that
infinitely many parameters remain unused is BKK's ``sufficiently ‹Σ›-pure'' (BKK
Definition 6.3). The statement free of this effect is the one for Andrews' finitary
consequence ‹⊩›: no finite part of the scheme derives falsity, which is
@{thm [source] con_finite_sub} restated through @{thm [source] fprov_con}.›
theorem con_Ineq_fprov:
assumes "inj (f :: nat ⇒ 'p::infinite)"
shows "¬ (Ineq f ⊩ (❙⊥ :: 'p tm))"
unfolding fprov_con by (blast intro: con_finite_sub[OF assms])
text ‹Thus ‹NK› is consistent with the inequation scheme, for every
injective constant family ‹f›. The scheme ‹Ineq f› forces ‹𝒟⇩ι› to be infinite in
every model of the whole scheme, since it makes the denotations of the constants ‹f i›
pairwise distinct (an immediate consequence, not stated as a lemma).›
theorem con_Ineq_not_DInf:
assumes injf: "inj (f :: nat ⇒ 'p::infinite)"
shows "con (insert (❙¬ DInf) (Ineq f))"
proof (rule con_compact)
fix F' :: "'p tm set"
assume finF': "finite F'" and sub': "F' ⊆ insert (❙¬ DInf) (Ineq f)"
have "con (insert (❙¬ DInf) (F' - {❙¬ DInf}))"
by (rule con_DInf_neg_finite_sub[OF injf]) (use finF' sub' in auto)
moreover have "F' ⊆ insert (❙¬ DInf) (F' - {❙¬ DInf})" by auto
moreover have "freep (insert (❙¬ DInf) (F' - {❙¬ DInf}))"
by (rule freep_finite) (simp add: finF')
ultimately show "con F'" by (rule con_mono)
qed
theorem Ineq_not_derives_DInf:
assumes injf: "inj (f :: nat ⇒ 'p::infinite)"
shows "¬ (Ineq f ⊩ (DInf :: 'p tm))"
proof
assume "Ineq f ⊩ (DInf :: 'p tm)"
then obtain F where finF: "finite F" and FI: "F ⊆ Ineq f"
and FD: "F ⊢ (DInf :: 'p tm)"
by (auto simp: fprov_def)
have D: "insert (❙¬ DInf) F ⊢ (DInf :: 'p tm)"
by (rule bprov_weaken[OF FD]) (auto simp: freep_finite finF)
have N: "insert (❙¬ DInf) F ⊢ (❙¬ DInf :: 'p tm)" by (auto intro: bprov.Hyp)
have "insert (❙¬ DInf) F ⊢ (❙⊥ :: 'p tm)"
by (rule bprov.NegE[OF N D wff_FalseB])
moreover have "con (insert (❙¬ DInf) F)"
by (rule con_DInf_neg_finite_sub[OF injf finF FI])
ultimately show False by (simp add: con_def)
qed
subsection ‹The constant-free sentences and the scheme›
text ‹The scheme derives every constant-free sentence ‹ExDistinct n›: the first ‹n›
constants are the witnesses, and their inequations are hypotheses.›
theorem Ineq_derives_distinct_n:
fixes f :: "nat ⇒ 'p::infinite"
shows "Ineq f ⊩ ExDistinct n"
proof -
let ?c = "λi. (f i)⇧p⇘ι⇙ :: 'p tm"
define F where "F = (λ(i, j). dneq f i j) ` {(i, j). i < j ∧ j < n}"
have "{(i, j). i < j ∧ j < n} ⊆ {0..<n} × {0..<n}" by auto
hence finF: "finite F" unfolding F_def by (blast intro: finite_imageI finite_subset)
have FI: "F ⊆ Ineq f" unfolding F_def by (auto intro: Ineq_I)
have fpF: "freep F" by (rule freep_finite[OF finF])
have neq: "⋀i j. i < j ⟹ j < n ⟹ F ⊢ ❙¬ (?c i ❙=⇘ι⇙ ?c j)"
by (rule bprov.Hyp) (force simp: F_def dneq_def)
have wc: "⋀k. wff⇘ι⇙(?c k)" by (simp add: wff_Par)
have d: "F ⊢ Distinct (map ?c [0..<n])"
using Distinct_family[OF fpF wc neq, where i = 0 and m = n] by simp
have "F ⊢ ExDistinct n"
unfolding ExDistinct_def
proof (rule ExD_I[OF _ fpF])
show "F ⊢ Distinct ([] @ map ?c [0..<n])" using d by simp
show "distinct (map vD [0..<n])" by (simp add: distinct_map inj_on_def vD_def)
qed (simp_all add: wff_Par)
thus ?thesis by (rule fprovI[OF finF FI])
qed
text ‹Hence the constant-free sentences do not derive the axiom either: a derivation
from finitely many of them would, by cut, be a derivation from a finite part of the
scheme. As a first-order axiomatisation of infinity, ‹{ExDistinct n | n}› is thus
strictly weaker than ‹DInf› in ‹NK› (the converse derivations are
@{thm [source] DInf_derives_distinct_n}). Over standard models the two are
equivalent, since an infinite individual domain with a full function space has an
injective, non-surjective self-map; this last step is not formalised. The Henkin
countermodel of the next subsection satisfies all ‹ExDistinct n› and refutes ‹DInf›.›
lemma distinct_scheme_fprov_Ineq:
fixes f :: "nat ⇒ 'p::infinite"
assumes A: "range ExDistinct ⊩ (A :: 'p tm)" and wA: "wff⇘𝗈⇙(A)"
shows "Ineq f ⊩ A"
proof -
from A obtain Λ where finΛ: "finite Λ" and ΛI: "Λ ⊆ range ExDistinct"
and ΛA: "Λ ⊢ A"
by (auto simp: fprov_def)
have "∀B ∈ Λ. ∃G. finite G ∧ G ⊆ Ineq f ∧ G ⊢ B"
using ΛI Ineq_derives_distinct_n[where f = f] by (auto simp: fprov_def)
then obtain G where G: "⋀B. B ∈ Λ ⟹ finite (G B) ∧ G B ⊆ Ineq f ∧ G B ⊢ B"
by metis
define F where "F = (⋃B ∈ Λ. G B)"
have finF: "finite F" unfolding F_def using finΛ G by auto
have FI: "F ⊆ Ineq f" unfolding F_def using G by auto
have fpF: "freep F" by (rule freep_finite[OF finF])
have wΛ: "⋀B. B ∈ Λ ⟹ wff⇘𝗈⇙(B)" using ΛI wff_ExDistinct by auto
have FA: "F ∪ Λ ⊢ A"
by (rule bprov_weaken[OF ΛA]) (auto simp: freep_finite finF finΛ)
have FB: "F ⊢ B" if B: "B ∈ Λ" for B
proof -
have "G B ⊢ B" and "G B ⊆ F" using G[OF B] B by (auto simp: F_def)
thus ?thesis by (rule bprov_weaken[OF _ _ fpF])
qed
have "F ⊢ A" by (rule bprov_cut_set[OF finΛ FA FB wΛ wA fpF])
thus ?thesis by (rule fprovI[OF finF FI])
qed
theorem distinct_scheme_not_derives_DInf:
"¬ (range (ExDistinct :: nat ⇒ 'p::infinite tm) ⊩ DInf)"
proof
assume h: "range (ExDistinct :: nat ⇒ 'p tm) ⊩ DInf"
obtain f :: "nat ⇒ 'p" where injf: "inj f"
using infinite_UNIV infinite_countable_subset by blast
have "Ineq f ⊩ (DInf :: 'p tm)"
by (rule distinct_scheme_fprov_Ineq[OF h wff_DInf])
thus False using Ineq_not_derives_DInf[OF injf] by simp
qed
text ‹Consistency of the constant-free sentences themselves, by the same reduction: no finite
part of ‹{ExDistinct n | n}› derives falsity. The finite models of ‹Consistency› of size
‹k› satisfy ‹ExDistinct n› for every ‹n ≤ k›, so the sentences need no auxiliary
constants at all; the route through the scheme is a convenience of the formalisation.›
theorem con_distinct_scheme:
"¬ (range (ExDistinct :: nat ⇒ 'p::infinite tm) ⊩ ❙⊥)"
proof
assume h: "range (ExDistinct :: nat ⇒ 'p tm) ⊩ ❙⊥"
obtain f :: "nat ⇒ 'p" where injf: "inj f"
using infinite_UNIV infinite_countable_subset by blast
have "Ineq f ⊩ (❙⊥ :: 'p tm)"
by (rule distinct_scheme_fprov_Ineq[OF h wff_FalseB])
thus False using con_Ineq_fprov[OF injf] by simp
qed
subsection ‹The Henkin countermodel›
text ‹The model-theoretic side of the separation: a general model of the @{emph ‹whole›}
scheme in which ‹DInf› fails --- the refuting term model of ‹Completeness›, applied to
‹Ineq f› and ‹DInf›. The term-model construction needs the context to be parameter-rich
(‹richp›, BKK Definition 6.3 scaled to the size of the signature), which here means that the parameters left unused by the
family ‹f› are as numerous as the signature. This is a condition of the construction only,
and it is discharged below: any injective family is renamed into one with such a reserve
(@{thm [source] signature_fold}), and the model obtained there is pulled back along the
renaming (@{thm [source] bkk_model_reduct}), which fixes the pure sentence ‹DInf›.›
lemma henkin_scheme_refutes_DInf_reserve:
fixes f :: "nat ⇒ 'p::infinite"
assumes injf: "inj f" and res: "|UNIV :: 'p set| ≤o |- range f|"
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∈Ineq f. vl (Ee ξ B)" "¬ vl (Ee ξ (DInf :: 'p tm))"
proof -
have nd: "¬ (Ineq f ⊢ (DInf :: 'p tm))"
using Ineq_not_derives_DInf[OF injf] bprov_fprov by blast
have "usedp (Ineq f) ⊆ range f"
by (auto simp: usedp_def Ineq_iff dneq_def)
hence "- range f ⊆ - usedp (Ineq f)" by auto
hence "|- range f| ≤o |- usedp (Ineq f)|" by (rule card_of_mono1)
hence fp: "richp (Ineq f)" unfolding richp_def using res ordLeq_transitive by blast
have sen: "cwff 𝗈 B" if "B ∈ Ineq f" for B :: "'p tm"
proof -
have "∃i j. B = dneq f i j ∧ i ≠ j" using that by (simp add: Ineq_iff)
then obtain i j where B: "B = dneq f i j" by blast
show ?thesis unfolding B dneq_def cwff_def
by (auto intro!: wff_Not wff_PEq wff_Par)
qed
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 "bkk_model Dm Ap Ee vl" and "inj_on rep {x. ∃τ. Dm τ x}"
and "app_struct.asg Dm ξ" and "∀B∈Ineq f. vl (Ee ξ B)"
and "¬ vl (Ee ξ (DInf :: 'p tm))"
using refuting_term_model_hyps[OF cwff_DInf fp sen nd] .
thus ?thesis by (rule that)
qed
text ‹Renaming commutes with the inequations of the scheme and fixes the pure axiom.›
lemma prn_dneq: "prn h (dneq f i j) = dneq (h ∘ f) i j"
by (simp add: dneq_def)
lemma prn_DInf: fixes h :: "'p ⇒ 'p" shows "prn h (DInf :: 'p tm) = DInf"
using prn_cong[of "DInf :: 'p tm" h] by (simp add: pars_DInf)
text ‹The separation theorem, for @{emph ‹every›} injective family over an infinite signature:
the signature is folded injectively into one half of itself, the renamed family satisfies
the reserve condition, and the reduct of its refuting model along the fold is a model of
the original scheme. The model satisfies every ‹ExDistinct n› as well --- its individual
domain is infinite --- and refutes ‹DInf›. Its total domain injects into the term type,
so over a countable signature it is countable (@{thm [source] countable_of_inj_on_tm}).›
theorem henkin_scheme_refutes_DInf:
fixes f :: "nat ⇒ 'p::infinite"
assumes injf: "inj f"
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∈Ineq f. vl (Ee ξ B)" "∀n. vl (Ee ξ (ExDistinct n :: 'p tm))"
"¬ vl (Ee ξ (DInf :: 'p tm))"
proof -
obtain h :: "'p ⇒ 'p" where injh: "inj h" and res_h: "|UNIV :: 'p set| ≤o |- range h|"
using signature_fold by blast
define f' where "f' = h ∘ f"
have injf': "inj f'" unfolding f'_def using injh injf by (rule inj_compose)
have res': "|UNIV :: 'p set| ≤o |- range f'|"
proof -
have "- range h ⊆ - range f'" by (auto simp: f'_def)
hence "|- range h| ≤o |- range f'|" by (rule card_of_mono1)
thus ?thesis using res_h ordLeq_transitive by blast
qed
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∈Ineq f'. vl (Ee ξ B)"
and nD: "¬ vl (Ee ξ (DInf :: 'p tm))"
using henkin_scheme_refutes_DInf_reserve[OF injf' res'] .
define Ee' where "Ee' = (λξ t. Ee ξ (prn h t))"
have M': "bkk_model Dm Ap Ee' vl" unfolding Ee'_def by (rule bkk_model_reduct[OF M])
have sat': "∀B∈Ineq f. vl (Ee' ξ B)"
proof
fix B assume "B ∈ Ineq f"
then obtain i j' where B: "B = dneq f i j'" and ne: "i ≠ j'" by (auto simp: Ineq_iff)
have "dneq f' i j' ∈ Ineq f'" using ne by (rule Ineq_I)
thus "vl (Ee' ξ B)" using sat by (simp add: Ee'_def B prn_dneq f'_def)
qed
have nD': "¬ vl (Ee' ξ (DInf :: 'p tm))" using nD by (simp add: Ee'_def prn_DInf)
have satn: "vl (Ee' ξ (ExDistinct n :: 'p tm))" for n
proof -
obtain G where GI: "G ⊆ Ineq f" and GD: "G ⊢ (ExDistinct n :: 'p tm)"
using Ineq_derives_distinct_n[where f = f and n = n] by (auto simp: fprov_def)
have wG: "∀A∈G. wff⇘𝗈⇙(A)" using GI by (auto simp: Ineq_iff wff_dneq dest!: subsetD)
have sG: "∀A∈G. vl (Ee' ξ A)" using GI sat' by blast
show ?thesis by (rule soundness_bkk[OF GD M' xi wG sG])
qed
hence all: "∀n. vl (Ee' ξ (ExDistinct n :: 'p tm))" by blast
show ?thesis by (rule that[OF M' inj xi sat' all nD'])
qed
end