Theory HOL_Universe
theory HOL_Universe
imports "HOL_in_HOL_Deep.Completeness" "HOL_in_HOL_Deep.NK_Infinity"
begin
section ‹Full classical HOL, abstractly: the choice scheme, the axioms' satisfaction, and ‹hol_universe››
text ‹This theory is the @{emph ‹set-theory-free›} half of the companion development: it
imports only the main entry @{session HOL_in_HOL_Deep} and never mentions a set-theoretic
universe. The Dedekind axiom of infinity ‹DInf›, its satisfaction conditions and its
separation from the infinity scheme are inherited from the main entry (theory
‹NK_Infinity›); here the relational choice scheme
‹ACrel› is added as an object formula with its satisfaction condition in an
@{emph ‹arbitrary›}
‹Σ›-standard model, the abstract relative-consistency theorem is derived --- full
classical
‹HOL› is consistent as soon as @{emph ‹some›} standard model has Dedekind-infinite
individuals --- and the universe interfaces are isolated from which the required standard
model is @{emph ‹constructed›}: the locale ‹hol_universe›, and beneath it an at most as
strong Harrison-style locale ‹harrison_universe›.
Completeness for the extension by ‹DInf› is likewise established here, in plain HOL.
That the assumptions of these locales are satisfiable is a separate question --- no
@{emph ‹plain-HOL›} type answers it: Cantor's tower outgrows every type plain HOL can
construct, and G\"odel's second theorem bars every other plain-HOL route (see the document
introduction) --- and is deferred to this entry's final theory, ‹HOL_in_HOL_Deep_Infinity_ZFC›,
which instantiates both locales with Paulson's axiomatic set-theoretic universe ∗‹V›. The split makes the
dependency structure machine-visible: nothing in this theory rests on ‹ZFC_in_HOL›.›
section ‹Consistency of full classical HOL: infinity and choice›
text ‹‹NK› already carries extensionality (property f) and typed description. Adding the
Dedekind axiom of infinity ‹DInf› and the axiom of ∗‹choice› makes the object logic full
classical higher-order logic in the sense of Church. The consistency of the whole package
is reduced, in one carrier-generic argument, to the existence of a standard frame with
Dedekind-infinite individuals.›
subsection ‹The axiom of choice as a relational scheme›
text ‹Choice is stated, without any new primitive, as the relational scheme
‹AC⇘σ,τ⇙ = ❙ΠR. (❙ΠX. ❙∃Y. R⋅X⋅Y) ❙⊃ (❙∃F. ❙ΠX. R⋅X⋅(F⋅X))› at every pair of types.›
definition rR where "rR = (5::nat)"
definition rX where "rX = (6::nat)"
definition rY where "rY = (7::nat)"
definition rF where "rF = (8::nat)"
definition ACatom1 :: "ty ⇒ ty ⇒ 'p tm" where
"ACatom1 σ τ = (((rR⇧f⇘σ ❙⇒ τ ❙⇒ 𝗈⇙) ❙⋅ (rX⇧f⇘σ⇙)) ❙⋅ (rY⇧f⇘τ⇙))"
definition ACatom2 :: "ty ⇒ ty ⇒ 'p tm" where
"ACatom2 σ τ = (((rR⇧f⇘σ ❙⇒ τ ❙⇒ 𝗈⇙) ❙⋅ (rX⇧f⇘σ⇙)) ❙⋅ ((rF⇧f⇘σ ❙⇒ τ⇙) ❙⋅ (rX⇧f⇘σ⇙)))"
definition ACprem :: "ty ⇒ ty ⇒ 'p tm" where
"ACprem σ τ = ❙ΠrX⇘σ⇙. ❙∃rY⇘τ⇙. ACatom1 σ τ"
definition ACconcl :: "ty ⇒ ty ⇒ 'p tm" where
"ACconcl σ τ = ❙∃rF⇘σ ❙⇒ τ⇙. ❙ΠrX⇘σ⇙. ACatom2 σ τ"
definition ACrel :: "ty ⇒ ty ⇒ 'p tm" where
"ACrel σ τ = ❙ΠrR⇘σ ❙⇒ τ ❙⇒ 𝗈⇙. (ACprem σ τ ❙⊃ ACconcl σ τ)"
lemma wff_ACatom1 [intro]: "wff⇘𝗈⇙(ACatom1 σ τ :: 'p tm)"
unfolding ACatom1_def by (rule wff_App[OF wff_App[OF wff_Fre wff_Fre] wff_Fre])
lemma wff_ACatom2 [intro]: "wff⇘𝗈⇙(ACatom2 σ τ :: 'p tm)"
unfolding ACatom2_def
by (rule wff_App[OF wff_App[OF wff_Fre wff_Fre] wff_App[OF wff_Fre wff_Fre]])
lemma wff_ACprem: "wff⇘𝗈⇙(ACprem σ τ :: 'p tm)"
unfolding ACprem_def by (rule wff_AllN[OF wff_ExN[OF wff_ACatom1]])
lemma wff_ACconcl: "wff⇘𝗈⇙(ACconcl σ τ :: 'p tm)"
unfolding ACconcl_def by (rule wff_ExN[OF wff_AllN[OF wff_ACatom2]])
lemma wff_ACrel: "wff⇘𝗈⇙(ACrel σ τ :: 'p tm)"
unfolding ACrel_def by (rule wff_AllN[OF wff_ImpB[OF wff_ACprem wff_ACconcl]])
lemmas rdefs = rR_def rX_def rY_def rF_def
lemma fvs_ACrel: "fvs (ACrel σ τ :: 'p tm) = {}"
by (simp add: ACrel_def ACprem_def ACconcl_def ACatom1_def ACatom2_def
ExN_def AllN_def Forall_def ImpB_def rdefs)
lemma cwff_ACrel: "cwff 𝗈 (ACrel σ τ :: 'p tm)"
by (rule cwffI[OF wff_ACrel fvs_ACrel])
text ‹The scheme in full, as for ‹DInf›: assembled by definitional unfolding, and in its
locally-nameless normal form:›
lemma ACrel_unfolded:
"(ACrel σ τ :: 'p tm)
= (❙ΠrR⇘σ ❙⇒ τ ❙⇒ 𝗈⇙.
((❙ΠrX⇘σ⇙. ❙∃rY⇘τ⇙. (((rR⇧f⇘σ ❙⇒ τ ❙⇒ 𝗈⇙) ❙⋅ (rX⇧f⇘σ⇙)) ❙⋅ (rY⇧f⇘τ⇙)))
❙⊃ (❙∃rF⇘σ ❙⇒ τ⇙. ❙ΠrX⇘σ⇙.
(((rR⇧f⇘σ ❙⇒ τ ❙⇒ 𝗈⇙) ❙⋅ (rX⇧f⇘σ⇙)) ❙⋅ ((rF⇧f⇘σ ❙⇒ τ⇙) ❙⋅ (rX⇧f⇘σ⇙))))))"
by (simp only: ACrel_def ACprem_def ACconcl_def ACatom1_def ACatom2_def)
lemma ACrel_norm:
"(ACrel σ τ :: 'p tm)
= ❙Π⇘σ ❙⇒ τ ❙⇒ 𝗈⇙
((❙Π⇘σ⇙ (❙∃⇘τ⇙ ((Bnd (Suc (Suc 0)) ❙⋅ Bnd (Suc 0)) ❙⋅ Bnd 0)))
❙⊃ (❙∃⇘σ ❙⇒ τ⇙ (❙Π⇘σ⇙ ((Bnd (Suc (Suc 0)) ❙⋅ Bnd 0) ❙⋅ (Bnd (Suc 0) ❙⋅ Bnd 0)))))"
by (simp add: ACrel_def ACprem_def ACconcl_def ACatom1_def ACatom2_def
ExN_def AllN_def Forall_def ImpB_def rdefs)
subsection ‹Satisfaction of the choice scheme in an arbitrary standard model›
text ‹Every instance of the scheme holds in ∗‹any› ‹Σ›-standard model: the full function
space supplies the choice function as the ‹λ›-abstraction of a meta-level Hilbert
choice. (The corresponding satisfaction analysis for ‹DInf› --- ‹DInf_sat› and its
relatives --- lives in the main entry's ‹NK_Infinity› and is used below unchanged.)›
context standard_model
begin
lemma ACrel_sat:
assumes xi: "bkkA.asg ξ"
shows "den (ACrel σ τ) ξ = Tv"
proof -
have body: "den (ACprem σ τ ❙⊃ ACconcl σ τ) (ξ(rR⇘σ ❙⇒ τ ❙⇒ 𝗈⇙ := d)) = Tv"
if d: "Dm (σ ❙⇒ τ ❙⇒ 𝗈) d" for d
proof -
define η where "η = ξ(rR⇘σ ❙⇒ τ ❙⇒ 𝗈⇙ := d)"
have ea: "bkkA.asg η" unfolding η_def using xi d by (rule bkkA.asg_upd)
have prem: "(den (ACprem σ τ) η = Tv)
= (∀a. Dm σ a ⟶ (∃b. Dm τ b ∧ (d ❙@ a) ❙@ b = Tv))"
proof -
have inner: "(den (ACatom1 σ τ) ((η(rX⇘σ⇙ := a))(rY⇘τ⇙ := b)) = Tv) = ((d ❙@ a) ❙@ b = Tv)"
if a: "Dm σ a" and b: "Dm τ b" for a b
proof -
define ρ where "ρ = (η(rX⇘σ⇙ := a))(rY⇘τ⇙ := b)"
have "den (ACatom1 σ τ) ρ = (d ❙@ a) ❙@ b"
unfolding ACatom1_def by (simp add: den.simps(8) ρ_def η_def upd_def rdefs)
thus ?thesis by (simp add: ρ_def)
qed
have step: "(den (❙∃rY⇘τ⇙. ACatom1 σ τ) (η(rX⇘σ⇙ := a)) = Tv)
= (∃b. Dm τ b ∧ (d ❙@ a) ❙@ b = Tv)" if a: "Dm σ a" for a
proof -
have "(den (❙∃rY⇘τ⇙. ACatom1 σ τ) (η(rX⇘σ⇙ := a)) = Tv)
= (∃b. Dm τ b ∧ den (ACatom1 σ τ) ((η(rX⇘σ⇙ := a))(rY⇘τ⇙ := b)) = Tv)"
by (rule sat_ExN[OF wff_ACatom1 bkkA.asg_upd[OF ea a]])
thus ?thesis using inner[OF a] by (simp cong: conj_cong)
qed
have "(den (ACprem σ τ) η = Tv)
= (∀a. Dm σ a ⟶ den (❙∃rY⇘τ⇙. ACatom1 σ τ) (η(rX⇘σ⇙ := a)) = Tv)"
unfolding ACprem_def by (rule sat_AllN[OF wff_ExN[OF wff_ACatom1] ea])
thus ?thesis using step by simp
qed
have concl: "den (ACconcl σ τ) η = Tv"
if P: "∀a. Dm σ a ⟶ (∃b. Dm τ b ∧ (d ❙@ a) ❙@ b = Tv)"
proof -
define g where "g = Lm σ (λx. SOME y. Dm τ y ∧ (d ❙@ x) ❙@ y = Tv)"
have resp: "Dm τ (SOME y. Dm τ y ∧ (d ❙@ x) ❙@ y = Tv)" if x: "Dm σ x" for x
proof -
from P x have "∃y. Dm τ y ∧ (d ❙@ x) ❙@ y = Tv" by blast
from someI_ex[OF this] show ?thesis by simp
qed
have gdom: "Dm (σ ❙⇒ τ) g"
unfolding g_def by (rule Lm_dom) (rule resp)
have gapp: "(d ❙@ a) ❙@ (g ❙@ a) = Tv" if a: "Dm σ a" for a
proof -
have e: "g ❙@ a = (SOME y. Dm τ y ∧ (d ❙@ a) ❙@ y = Tv)"
unfolding g_def by (rule beta_Lm[OF resp a])
from P a have ex: "∃y. Dm τ y ∧ (d ❙@ a) ❙@ y = Tv" by blast
from someI_ex[OF ex] show ?thesis by (simp add: e)
qed
have inner2: "(den (ACatom2 σ τ) ((η(rF⇘σ ❙⇒ τ⇙ := g))(rX⇘σ⇙ := a)) = Tv)
= ((d ❙@ a) ❙@ (g ❙@ a) = Tv)" if a: "Dm σ a" for a
proof -
define ρ where "ρ = (η(rF⇘σ ❙⇒ τ⇙ := g))(rX⇘σ⇙ := a)"
have "den (ACatom2 σ τ) ρ = (d ❙@ a) ❙@ (g ❙@ a)"
unfolding ACatom2_def by (simp add: den.simps(8) ρ_def η_def upd_def rdefs)
thus ?thesis by (simp add: ρ_def)
qed
have step2: "(den (❙ΠrX⇘σ⇙. ACatom2 σ τ) (η(rF⇘σ ❙⇒ τ⇙ := g)) = Tv)
= (∀a. Dm σ a ⟶ (d ❙@ a) ❙@ (g ❙@ a) = Tv)"
proof -
have "(den (❙ΠrX⇘σ⇙. ACatom2 σ τ) (η(rF⇘σ ❙⇒ τ⇙ := g)) = Tv)
= (∀a. Dm σ a ⟶ den (ACatom2 σ τ) ((η(rF⇘σ ❙⇒ τ⇙ := g))(rX⇘σ⇙ := a)) = Tv)"
by (rule sat_AllN[OF wff_ACatom2 bkkA.asg_upd[OF ea gdom]])
thus ?thesis using inner2 by simp
qed
have "(den (ACconcl σ τ) η = Tv)
= (∃k. Dm (σ ❙⇒ τ) k ∧ den (❙ΠrX⇘σ⇙. ACatom2 σ τ) (η(rF⇘σ ❙⇒ τ⇙ := k)) = Tv)"
unfolding ACconcl_def by (rule sat_ExN[OF wff_AllN[OF wff_ACatom2] ea])
thus ?thesis using gdom step2 gapp by auto
qed
have imp: "(den (ACprem σ τ ❙⊃ ACconcl σ τ) η = Tv)
= ((den (ACprem σ τ) η = Tv) ⟶ (den (ACconcl σ τ) η = Tv))"
by (rule sat_ImpBB[OF wff_ACprem wff_ACconcl ea])
have "den (ACprem σ τ ❙⊃ ACconcl σ τ) η = Tv"
unfolding imp using prem concl by blast
thus ?thesis by (simp add: η_def)
qed
have "(den (ACrel σ τ) ξ = Tv)
= (∀d. Dm (σ ❙⇒ τ ❙⇒ 𝗈) d
⟶ den (ACprem σ τ ❙⊃ ACconcl σ τ) (ξ(rR⇘σ ❙⇒ τ ❙⇒ 𝗈⇙ := d)) = Tv)"
unfolding ACrel_def by (rule sat_AllN[OF wff_ImpB[OF wff_ACprem wff_ACconcl] xi])
thus "den (ACrel σ τ) ξ = Tv" using body by simp
qed
end
text ‹❙‹The relative-consistency theorem, abstractly.› Suppose ∗‹some› ∗‹standard›
‹Σ›-model has an injective but not surjective self-map of its individuals --- that is,
Dedekind-infinitely many individuals. Then full classical ‹HOL› is consistent.
Consistency is the predicate ‹con› of the main entry, defined by
‹con Φ ⟷ ¬ (Φ ⊢ ❙⊥)›: the conclusion below states that ‹NK› cannot derive falsity
from ‹DInf› together with all instances of ‹ACrel›. The eigen-parameter starvation that
makes ‹con› a weak reading for impure infinite contexts (main entry, ‹NK_Infinity›)
cannot arise here: the axioms use no parameters at all, so the context is pure, and over
an infinite signature ‹con Φ› and ‹¬ (Φ ⊩ ❙⊥)› provably coincide
(@{thm [source] fprov_eq_bprov}). The proof
works for an ∗‹arbitrary› such model, whatever type its elements come from, and uses no
set theory. The one thing plain HOL cannot supply is the premise --- a model with
infinitely many individuals; producing one is the central task of the set-theoretic theory
that concludes this entry.⁋‹Why not? Plain HOL has infinite @{emph ‹types›}, and every
single level ‹nat›, ‹nat ⇒ bool›, ‹…› of the full tower exists as a type. What it lacks
is @{emph ‹one carrier›} for the whole tower at once. In BKK's sense ``standard'' means
only that the function domains are @{emph ‹full›}; but a model formalised inside plain HOL
necessarily has one further feature: the object types are values of the datatype ‹ty›, so
any formalised model --- the locale @{locale standard_model} included --- interprets all
domains inside a single carrier type ‹'u› (simple types cannot assign each object type its
own meta-type). Over infinite individuals with full function spaces that one carrier must
outgrow every level of the tower. No plain-HOL type reaches that far: every type plain HOL can construct is bounded
in cardinality by some finite tower of function spaces over its one primitive infinite
type ‹ind› (of which ‹nat› is the familiar copy). One might hope to escape with a @{emph ‹Henkin›} model, whose function domains
need not be full and which therefore fits into a small carrier. But a sparse function
domain need not provide what the axiom asks for. ‹DInf› says: @{emph ‹there exists›} an injective,
non-surjective self-map of the individuals. In a Henkin model that map has to be an
element of the (now sparse) function domain ‹D⇘ι ❙⇒ ι⇙› --- and it may simply not be
there, even when the individuals are infinite. This is not a hypothetical: the main
entry's ‹henkin_scheme_refutes_DInf› constructs a Henkin model with infinitely many
individuals in which ‹DInf› is nevertheless @{emph ‹false›}. And the canonical way to build
a Henkin model that does contain the witness --- the term-model construction --- takes the
consistency of ‹DInf› as its @{emph ‹premise›}, and so cannot be the way to prove it
(that @{emph ‹every›} other route fails as well is G\"odel's second theorem, see the
introduction).››
theorem con_full_HOL_rel:
fixes Dm :: "ty ⇒ 'u ⇒ bool" and Ap :: "'u ⇒ 'u ⇒ 'u"
and Lm :: "ty ⇒ ('u ⇒ 'u) ⇒ 'u" and Tv Fv Ngv Dsv :: 'u
and Iv Ev Piv :: "ty ⇒ 'u" and Jv :: "'p ⇒ ty ⇒ 'u"
assumes M: "standard_model Dm Ap Lm Tv Fv Ngv Dsv Iv Ev Piv Jv"
and inf: "∃d. Dm (ι ❙⇒ ι) d
∧ (∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (Ap d a = Ap d b ⟶ a = b)))
∧ (∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ Ap d z ≠ c))"
shows "con (insert (DInf :: 'p tm) (range (λ(σ,τ). ACrel σ τ)))"
proof -
interpret standard_model Dm Ap Lm Tv Fv Ngv Dsv Iv Ev Piv Jv by (rule M)
define ξ :: "nat ⇒ ty ⇒ 'u" where "ξ = (λn ρ. Jv undefined ρ)"
have xi: "bkkA.asg ξ" by (simp add: ξ_def bkkA.asg_def Jv_dom)
from inf obtain d where d: "Dm (ι ❙⇒ ι) d"
and dinj: "∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (Ap d a = Ap d b ⟶ a = b))"
and dns: "∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ Ap d z ≠ c)" by blast
have satD: "den (DInf :: 'p tm) ξ = Tv" by (rule DInf_sat[OF xi d dinj dns])
have satAC: "den (ACrel σ τ :: 'p tm) ξ = Tv" for σ τ by (rule ACrel_sat[OF xi])
show ?thesis
by (rule model_con[OF xi]) (use wff_DInf wff_ACrel satD satAC in auto)
qed
text ‹Completeness carries over to the axiomatic extension, in its strongest form: ‹{DInf}› is
a finite context, so @{thm [source] completeness_hyps_open_finite} applies ---
free variables are allowed in the conclusion, the carrier and the signature are any infinite
types, and purity is automatic. Any formula true in every infinite-carrier model of ‹DInf›
is thus already derivable from ‹DInf› in ‹NK›, and with soundness the two coincide ---
established by the plain-HOL completeness of the main entry, with no set universe.›
theorem NK_completeness_DInf:
fixes A :: "'p::infinite tm"
assumes "wff⇘𝗈⇙(A)" and "{DInf} ⊨('u::infinite) A"
shows "{DInf} ⊢ A"
proof (rule completeness_hyps_open_finite[OF _ _ assms(1) assms(2)])
show "finite {DInf :: 'p tm}" by simp
next
fix B :: "'p tm" assume "B ∈ {DInf}"
thus "wff⇘𝗈⇙(B)" by (simp add: wff_DInf)
qed
theorem sound_and_complete_DInf:
fixes A :: "'p::infinite tm"
assumes "wff⇘𝗈⇙(A)"
shows "{DInf} ⊢ A ⟷ {DInf} ⊨('u::infinite) A"
using assms NK_completeness_DInf soundness_sat by blast
section ‹Minimising the meta-theory: a weaker universe suffices›
text ‹We weaken the premise of @{thm [source] con_full_HOL_rel} once more. Instead of
∗‹assuming› the logical constants (as ‹standard_model› does), the locale ‹hol_universe›
adds Dedekind-infinite individuals to the constants-construction interface
@{locale lambda_universe} of the main entry: a universe with full function spaces,
booleans, extensionality and a domain-respecting parameter interpretation, over which
the constants are @{emph ‹constructed›}. Any model of these weaker assumptions ---
the final theory provides one over ‹V› --- thus yields the relative consistency of full ‹HOL›.›
locale hol_universe = lambda_universe Dm Ap Lm Tv Fv Jv
for Dm :: "ty ⇒ 'u ⇒ bool" and Ap :: "'u ⇒ 'u ⇒ 'u"
and Lm :: "ty ⇒ ('u ⇒ 'u) ⇒ 'u" and Tv Fv :: 'u and Jv :: "'p ⇒ ty ⇒ 'u" +
assumes ind_inf: "∃d. Dm (ι ❙⇒ ι) d
∧ (∀a. Dm ι a ⟶ (∀b. Dm ι b ⟶ (Ap d a = Ap d b ⟶ a = b)))
∧ (∃c. Dm ι c ∧ (∀z. Dm ι z ⟶ Ap d z ≠ c))"
begin
theorem con_full_HOL_universe:
"con (insert (DInf :: 'p tm) (range (λ(σ,τ). ACrel σ τ)))"
by (rule con_full_HOL_rel[OF is_standard_model ind_inf])
end
section ‹Minimising further: a Harrison-style universe axiom›
text ‹Harrison's self-verification of HOL Light \<^cite>‹Harrison06› proves the soundness of
HOL-with-infinity in a meta-logic strengthened by a single ∗‹universe axiom›: an infinite
type closed under the set-forming operations that full function spaces require. The
locale ‹harrison_universe› is our rendering of that axiom, one level below
‹hol_universe›: it mentions neither types, domains, application nor abstraction. Fixed
are an injective pairing ‹pr›, an injective coding ‹enc› of the ∗‹small› collections
‹Sm›, and a small Dedekind-infinite collection ‹D0› of individuals; smallness is closed
downwards, under products and --- the strong-limit core of Harrison's axiom --- under
∗‹coded power collections› (‹Sm_pow›).⁋‹In effect this axiom postulates a fresh base
type ‹v› that gathers the domains of the whole type hierarchy over ‹ι› and ‹𝗈›, so that
every finite-type domain embeds into it. The subtlety is that ‹v› is closed only under the
operations those finite types require --- pairing and ∗‹small› (coded) power collections ---
and ∗‹not› under its own full function space ‹v ❙⇒ 𝗈›, which by Cantor would be strictly
larger. This restricted closure, rather than a full powerset, is exactly what keeps the
axiom consistent and of merely strong-limit strength.› From these data alone the whole
‹hol_universe› structure is @{emph ‹constructed›}: domains as collections of coded functional
graphs, abstraction by coding, application by decoding.›
locale harrison_universe =
fixes pr :: "'u ⇒ 'u ⇒ 'u" and enc :: "('u ⇒ bool) ⇒ 'u"
and Sm :: "('u ⇒ bool) ⇒ bool" and D0 :: "'u ⇒ bool"
assumes pr_inj: "pr a b = pr c d ⟹ a = c ∧ b = d"
and enc_inj: "⟦Sm X; Sm Y; enc X = enc Y⟧ ⟹ X = Y"
and Sm_sub: "⟦Sm X; Y ≤ X⟧ ⟹ Sm Y"
and Sm_prod: "⟦Sm X; Sm Y⟧ ⟹ Sm (λz. ∃a b. X a ∧ Y b ∧ z = pr a b)"
and Sm_pow: "Sm X ⟹ Sm (λz. ∃Y. Y ≤ X ∧ Sm Y ∧ z = enc Y)"
and Sm_D0: "Sm D0"
and D0_inf: "∃f c. (∀a. D0 a ⟶ D0 (f a))
∧ (∀a b. D0 a ⟶ D0 b ⟶ f a = f b ⟶ a = b)
∧ D0 c ∧ (∀a. D0 a ⟶ f a ≠ c)"
begin
text ‹Smallness of the empty collection need not be assumed: it is a sub-collection of the
small ‹D0›.›
lemma Sm_empty: "Sm (λ_. False)"
by (rule Sm_sub[OF Sm_D0]) (simp add: le_fun_def)
subsection ‹Truth values, domains, abstraction, application›
text ‹The truth values are the first stages of the cumulative hierarchy in miniature: ‹HTv›
codes the empty collection, ‹HFv› its singleton. Both collections are small --- the empty
one by ‹Sm_empty›, its singleton as the coded power collection of the empty one
(‹Sm_pow›) --- and ‹enc_inj› keeps the two codes apart. A function domain consists of the codes of the
functional graphs over the argument domain; application decodes, abstraction codes.›
definition HTv :: 'u where "HTv = enc (λ_. False)"
definition HFv :: 'u where "HFv = enc (λz. z = HTv)"
primrec HD :: "ty ⇒ 'u ⇒ bool" where
"HD ι = D0"
| "HD 𝗈 = (λx. x = HTv ∨ x = HFv)"
| "HD (σ ❙⇒ τ) = (λx. ∃g. (∀a. HD σ a ⟶ HD τ (g a))
∧ x = enc (λz. ∃a. HD σ a ∧ z = pr a (g a)))"
definition Hgr :: "ty ⇒ ('u ⇒ 'u) ⇒ 'u ⇒ bool" where
"Hgr σ g = (λz. ∃a. HD σ a ∧ z = pr a (g a))"
definition HLm :: "ty ⇒ ('u ⇒ 'u) ⇒ 'u" where "HLm σ g = enc (Hgr σ g)"
text ‹The ‹THE› below is Isabelle's @{emph ‹definite description›} at the meta-level ---
unique choice, not a choice principle; decoding is well-defined by ‹enc_inj›. (The
‹SOME› in ‹HJv› is meta-level Hilbert choice of Isabelle/HOL. Neither adds an axiom to
the embedded object logic.)›
definition Hdec :: "'u ⇒ 'u ⇒ bool" where "Hdec x = (THE X. Sm X ∧ enc X = x)"
definition HAp :: "'u ⇒ 'u ⇒ 'u" where "HAp f a = (THE b. Hdec f (pr a b))"
definition HJv :: "'p ⇒ ty ⇒ 'u" where "HJv p σ = (SOME d. HD σ d)"
lemma HD_Fun: "HD (σ ❙⇒ τ) x ⟷ (∃g. (∀a. HD σ a ⟶ HD τ (g a)) ∧ x = HLm σ g)"
by (simp add: HLm_def Hgr_def)
subsection ‹Every domain is small and inhabited›
lemma Sm_singleton_HTv: "Sm (λz. z = HTv)"
proof -
have "(λz. ∃Y. Y ≤ (λ_. False) ∧ Sm Y ∧ z = enc Y) = (λz. z = HTv)"
proof (rule ext)
fix z show "(∃Y. Y ≤ (λ_. False) ∧ Sm Y ∧ z = enc Y) = (z = HTv)"
proof
assume "∃Y. Y ≤ (λ_. False) ∧ Sm Y ∧ z = enc Y"
then obtain Y where "Y ≤ (λ_. False)" and z: "z = enc Y" by blast
from this(1) have "Y = (λ_. False)" by (auto simp: le_fun_def fun_eq_iff)
with z show "z = HTv" by (simp add: HTv_def)
next
assume "z = HTv"
hence "(λ_. False) ≤ (λ_. False) ∧ Sm (λ_. False) ∧ z = enc (λ_. False)"
using Sm_empty by (simp add: HTv_def)
thus "∃Y. Y ≤ (λ_. False) ∧ Sm Y ∧ z = enc Y" by blast
qed
qed
with Sm_pow[OF Sm_empty] show ?thesis by simp
qed
lemma HTv_neq_HFv: "HTv ≠ HFv"
proof
assume "HTv = HFv"
hence "(λ_. False) = (λz. z = HTv)"
using enc_inj[OF Sm_empty Sm_singleton_HTv] HTv_def HFv_def by metis
from fun_cong[OF this, of HTv] show False by simp
qed
lemma Sm_bool: "Sm (HD 𝗈)"
proof -
have sub: "Y = (λ_. False) ∨ Y = (λz. z = HTv)" if le: "Y ≤ (λz. z = HTv)" for Y
proof -
have imp: "Y w ⟹ w = HTv" for w using le_funD[OF le, of w] by simp
show ?thesis
proof (cases "Y HTv")
case True
have "Y = (λz. z = HTv)" by (rule ext) (use imp True in blast)
thus ?thesis ..
next
case False
have "Y = (λ_. False)" by (rule ext) (use imp False in blast)
thus ?thesis ..
qed
qed
have "(λz. ∃Y. Y ≤ (λz. z = HTv) ∧ Sm Y ∧ z = enc Y) = HD 𝗈"
proof (rule ext)
fix z show "(∃Y. Y ≤ (λz. z = HTv) ∧ Sm Y ∧ z = enc Y) = HD 𝗈 z"
proof
assume "∃Y. Y ≤ (λz. z = HTv) ∧ Sm Y ∧ z = enc Y"
then obtain Y where "Y ≤ (λz. z = HTv)" and z: "z = enc Y" by blast
from sub[OF this(1)] z show "HD 𝗈 z" by (auto simp: HTv_def HFv_def)
next
assume "HD 𝗈 z"
then consider "z = HTv" | "z = HFv" by auto
thus "∃Y. Y ≤ (λz. z = HTv) ∧ Sm Y ∧ z = enc Y"
proof cases
case 1
hence "(λ_. False) ≤ (λz. z = HTv) ∧ Sm (λ_. False) ∧ z = enc (λ_. False)"
using Sm_empty by (simp add: le_fun_def HTv_def)
thus ?thesis by blast
next
case 2
hence "(λz. z = HTv) ≤ (λz. z = HTv) ∧ Sm (λz. z = HTv) ∧ z = enc (λz. z = HTv)"
using Sm_singleton_HTv by (simp add: HFv_def)
thus ?thesis by blast
qed
qed
qed
with Sm_pow[OF Sm_singleton_HTv] show ?thesis by simp
qed
text ‹The function-space case is the Harrison core: every coded graph is a small
subcollection of the product of the two domains, so the domain of codes sits inside the
coded power collection of that product.›
lemma Sm_HD: "Sm (HD σ)"
proof (induction σ)
case Ind show ?case by (simp add: Sm_D0)
next
case Bool show ?case by (rule Sm_bool)
next
case (Fun σ τ)
let ?P = "λz. ∃a b. HD σ a ∧ HD τ b ∧ z = pr a b"
have "HD (σ ❙⇒ τ) ≤ (λz. ∃Y. Y ≤ ?P ∧ Sm Y ∧ z = enc Y)"
proof (intro le_funI le_boolI)
fix x assume "HD (σ ❙⇒ τ) x"
hence "∃g. (∀a. HD σ a ⟶ HD τ (g a)) ∧ x = HLm σ g"
by (simp add: HLm_def Hgr_def)
then obtain g where g: "∀a. HD σ a ⟶ HD τ (g a)" and x: "x = HLm σ g" by blast
have le: "Hgr σ g ≤ ?P" using g by (auto simp: Hgr_def le_fun_def)
have "Sm (Hgr σ g)" by (rule Sm_sub[OF Sm_prod[OF Fun.IH] le])
with le x show "∃Y. Y ≤ ?P ∧ Sm Y ∧ x = enc Y" by (auto simp: HLm_def)
qed
from Sm_sub[OF Sm_pow[OF Sm_prod[OF Fun.IH]] this] show ?case .
qed
lemma HLm_dom: assumes "⋀d. HD σ d ⟹ HD τ (h d)" shows "HD (σ ❙⇒ τ) (HLm σ h)"
unfolding HD_Fun using assms by blast
lemma HD_ne: "∃x. HD σ x"
proof (induction σ)
case Ind show ?case using D0_inf by auto
next
case Bool show ?case by auto
next
case (Fun σ τ)
from Fun.IH(2) obtain w where w: "HD τ w" by blast
have "HD (σ ❙⇒ τ) (HLm σ (λ_. w))" by (rule HLm_dom) (rule w)
thus ?case by blast
qed
subsection ‹Decoding is inverse to coding, and the frame conditions follow›
lemma Hdec_enc: assumes "Sm X" shows "Hdec (enc X) = X"
unfolding Hdec_def by (rule the_equality) (use assms enc_inj in ‹blast+›)
lemma Hgr_pr: assumes "HD σ a" shows "Hgr σ h (pr a b) ⟷ b = h a"
using assms by (auto simp: Hgr_def dest: pr_inj)
lemma Sm_Hgr: assumes "⋀d. HD σ d ⟹ HD τ (h d)" shows "Sm (Hgr σ h)"
proof (rule Sm_sub[OF Sm_prod[OF Sm_HD Sm_HD]])
show "Hgr σ h ≤ (λz. ∃a b. HD σ a ∧ HD τ b ∧ z = pr a b)"
using assms by (auto simp: Hgr_def le_fun_def)
qed
lemma HAp_HLm: assumes sm: "Sm (Hgr σ h)" and a: "HD σ a" shows "HAp (HLm σ h) a = h a"
unfolding HAp_def HLm_def Hdec_enc[OF sm]
by (rule the_equality) (simp_all add: Hgr_pr[OF a])
lemma HD_FunE:
assumes f: "HD (σ ❙⇒ τ) f"
shows "∃g. (∀a. HD σ a ⟶ HD τ (g a)) ∧ f = HLm σ g ∧ (∀a. HD σ a ⟶ HAp f a = g a)"
proof -
from f have "∃g. (∀a. HD σ a ⟶ HD τ (g a)) ∧ f = HLm σ g"
by (simp add: HLm_def Hgr_def)
then obtain g where g: "∀a. HD σ a ⟶ HD τ (g a)" and fe: "f = HLm σ g" by blast
have sm: "Sm (Hgr σ g)" by (rule Sm_Hgr) (use g in blast)
have "∀a. HD σ a ⟶ HAp f a = g a" unfolding fe using HAp_HLm[OF sm] by blast
with g fe show ?thesis by blast
qed
lemma HAp_dom: assumes f: "HD (σ ❙⇒ τ) f" and a: "HD σ a" shows "HD τ (HAp f a)"
proof -
from HD_FunE[OF f] obtain g where g: "∀a. HD σ a ⟶ HD τ (g a)"
and app: "∀a. HD σ a ⟶ HAp f a = g a" by blast
from g app a show ?thesis by auto
qed
lemma HAp_ext:
assumes g: "HD (σ ❙⇒ τ) g" and k: "HD (σ ❙⇒ τ) k"
and e: "⋀a. HD σ a ⟹ HAp g a = HAp k a"
shows "g = k"
proof -
from HD_FunE[OF g] obtain g0 where g0: "g = HLm σ g0"
and appg: "∀a. HD σ a ⟶ HAp g a = g0 a" by blast
from HD_FunE[OF k] obtain k0 where k0: "k = HLm σ k0"
and appk: "∀a. HD σ a ⟶ HAp k a = k0 a" by blast
have gk: "g0 a = k0 a" if "HD σ a" for a
using appg appk e[OF that] that by simp
have "Hgr σ g0 = Hgr σ k0" by (rule ext) (auto simp: Hgr_def gk)
thus ?thesis by (simp add: g0 k0 HLm_def)
qed
lemma HJv_dom: "HD σ (HJv p σ)"
unfolding HJv_def by (rule someI_ex[OF HD_ne])
text ‹Dedekind infinity transfers from the meta-level self-map ‹f› of ‹D0› to the object
level: the witness in ‹HD (ι ❙⇒ ι)› is its coded graph ‹HLm ι f›.›
lemma HD_inf:
"∃d. HD (ι ❙⇒ ι) d
∧ (∀a. HD ι a ⟶ (∀b. HD ι b ⟶ (HAp d a = HAp d b ⟶ a = b)))
∧ (∃c. HD ι c ∧ (∀z. HD ι z ⟶ HAp d z ≠ c))"
proof -
from D0_inf obtain f c where f: "∀a. D0 a ⟶ D0 (f a)"
and inj: "∀a b. D0 a ⟶ D0 b ⟶ f a = f b ⟶ a = b"
and c: "D0 c" and ns: "∀a. D0 a ⟶ f a ≠ c" by blast
have sm: "Sm (Hgr ι f)" by (rule Sm_Hgr[where τ = ι]) (use f in simp)
have dty: "HD (ι ❙⇒ ι) (HLm ι f)" by (rule HLm_dom) (use f in simp)
have dapp: "⋀a. HD ι a ⟹ HAp (HLm ι f) a = f a" by (rule HAp_HLm[OF sm])
have "∀a. HD ι a ⟶ (∀b. HD ι b ⟶ (HAp (HLm ι f) a = HAp (HLm ι f) b ⟶ a = b))"
using inj by (simp add: dapp)
moreover have "∃c'. HD ι c' ∧ (∀z. HD ι z ⟶ HAp (HLm ι f) z ≠ c')"
using c ns by (auto simp: dapp intro!: exI[of _ c])
ultimately show ?thesis using dty by blast
qed
subsection ‹Every Harrison universe is a ‹hol_universe››
theorem harrison_hol_universe: "hol_universe HD HAp HLm HTv HFv (HJv :: 'p ⇒ ty ⇒ 'u)"
proof unfold_locales
show "⋀σ τ g k. HD (σ ❙⇒ τ) g ⟹ HD (σ ❙⇒ τ) k ⟹
(⋀a. HD σ a ⟹ HAp g a = HAp k a) ⟹ g = k" by (rule HAp_ext)
show "⋀a. HD 𝗈 a ⟷ a = HTv ∨ a = HFv" by simp
qed(safe intro!: HD_inf HJv_dom HTv_neq_HFv HAp_dom HLm_dom HAp_HLm[OF Sm_Hgr])
lemmas harrison_standard_model =
lambda_universe.is_standard_model[OF hol_universe.axioms(1)[OF harrison_hol_universe]]
theorem con_full_HOL_harrison:
"con (insert (DInf :: 'p tm) (range (λ(σ,τ). ACrel σ τ)))"
by (rule hol_universe.con_full_HOL_universe[OF harrison_hol_universe])
end
end