Theory Main_Results

theory Main_Results
  imports Completeness Cantor NK_Infinity
begin

section ‹Main results›

text ‹The central results of this entry, restated in one place.  Soundness
  and completeness of ‹NK› for the class ‹ℳ⇘_βfb⇙› (BKK Theorem 7.3 and a
  strengthening of BKK Corollary 7.7): for well-formed (open) formulas over
  every signature with infinitely many parameters ‹'p›, derivability coincides
  with validity at @{emph ‹every›} infinite value carrier ‹'u› --- no cardinality
  link between the parameter type ‹'p› and the carrier ‹'u› is needed.  Consistency holds
  for arbitrary signatures, by the concrete standard model --- note the asymmetry:
  consistency needs @{emph ‹no›} constraint on ‹'p› at all, whereas completeness
  requires ‹'p› infinite, since the rule ‹NK(ΠI)› consumes fresh
  eigen-parameters.  Cantor's theorem, surjective and injective, is derived inside ‹NK›
  at every type.›

text ‹Completeness comes without hypotheses (‹NK_completeness›) and relative to hypotheses.
  For the latter the primary relation is ‹Φ ⊩ A› --- some finite part of ‹Φ› derives
  ‹A› (theory ‹Calculus›) --- which is monotone and of finite character by construction
  and coincides with ‹Φ ⊢ A› whenever the context leaves enough parameters unused.  For
  ‹⊩›, completeness holds with @{emph ‹no›} condition on the context beyond
  well-formedness: any set of @{emph ‹open›} formulas --- context and conclusion may
  together carry infinitely many free variables --- at any infinite signature, over any
  carrier at least as large as the signature (‹NK_completeness_hyps›); the instance for a closed
  context and conclusion over a countable signature is BKK Corollary 7.7 proper.  At the
  level of the calculus ‹⊢› itself --- deriving from the @{emph ‹whole›} context rather
  than from a finite part --- a proviso on the context is needed, since an impure infinite
  context can exhaust the eigen-parameters of ‹NK(ΠI)›; that family of theorems lives in
  theory ‹Completeness› (‹completeness_hyps_open_full›, ‹completeness_hyps_open_rich›).
  Restated here is only its @{emph ‹finite›}-context form, which needs no side condition
  at all (‹NK_completeness_hyps_fin›), as unrestricted as ‹NK_completeness› itself.›

theorem NK_soundness:
  "Φ ⊢ C ⟹ Φ ⊨('u) C"
  by (rule soundness_sat)

theorem NK_completeness:
  assumes "wff⇘𝗈⇙(A::'p::infinite tm)" and "⊨('u::infinite) A"
  shows "⊢ A"
  by (rule completeness_at_any_signature[OF assms])

text ‹Derivability from hypotheses, in final form.  The premise ‹inj emb› --- the carrier
  is at least as large as the signature --- cannot be dropped for contexts of unbounded
  size; the argument, which is informal, is the closing remark of theory
  ‹Completeness›.  Nothing else is assumed about the context.  Semantic compactness of
  the Henkin consequence follows as a corollary: consequence at one sufficiently large
  carrier reduces to a finite sub-context, which by soundness has ‹A› as a consequence at
  @{emph ‹every›} carrier ‹'v› --- no ultraproducts are involved.›

theorem NK_soundness_hyps: "Φ ⊩ C ⟹ Φ ⊨('u) C"
  by (rule soundness_fprov)

theorem NK_completeness_hyps:
  fixes Φ :: "'p::infinite tm set" and emb :: "'p ⇒ 'u"
  assumes "inj emb" and "wff⇘𝗈⇙(A)" and "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
      and "Φ ⊨('u) A"
  shows "Φ ⊩ A"
  by (rule completeness_fprov[OF assms])

theorem sound_and_complete_hyps:
  fixes Φ :: "'p::infinite tm set" and emb :: "'p ⇒ 'u"
  assumes emb: "inj emb" and A: "wff⇘𝗈⇙(A)" and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
  shows "Φ ⊩ A ⟷ Φ ⊨('u) A"
  using NK_completeness_hyps[OF emb A wΦ] NK_soundness_hyps by blast

corollary NK_consequence_compact:
  fixes Φ :: "'p::infinite tm set" and emb :: "'p ⇒ 'u"
  assumes "inj emb" and "wff⇘𝗈⇙(A)" and "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
      and "Φ ⊨('u) A"
  shows "∃Φ⇩₀. finite Φ⇩₀ ∧ Φ⇩₀ ⊆ Φ ∧ Φ⇩₀ ⊨('v) A"
  using NK_completeness_hyps[OF assms] soundness_sat by (auto simp: fprov_def)

text ‹For a ∗‹finite› context nothing beyond well-formedness is required: free variables
  may occur in the hypotheses ∗‹and› in the conclusion, and neither purity nor
  countability of ‹'p› is assumed.  The hypotheses are discharged into implications.›

theorem NK_completeness_hyps_fin:
  fixes Φ :: "'p::infinite tm set"
  assumes "finite Φ" and "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)" and "wff⇘𝗈⇙(A)"
      and "Φ ⊨('u::infinite) A"
  shows "Φ ⊢ A"
  by (rule completeness_hyps_open_finite[OF assms(1) assms(2) assms(3) assms(4)])

theorem sound_and_complete_hyps_fin:
  fixes Φ :: "'p::infinite tm set"
  assumes fin: "finite Φ" and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)" and A: "wff⇘𝗈⇙(A)"
  shows "Φ ⊢ A ⟷ Φ ⊨('u::infinite) A"
proof
  assume "Φ ⊢ A" thus "Φ ⊨('u) A" by (rule NK_soundness)
next
  assume h: "Φ ⊨('u) A"
  show "Φ ⊢ A" by (rule NK_completeness_hyps_fin[OF fin wΦ A h])
qed

theorem sound_and_complete:
  assumes "wff⇘𝗈⇙(A::'p::infinite tm)"
  shows "⊢ A ⟷ ⊨('u::infinite) A"
  using assms completeness_at_any_signature soundness_valid by blast

text ‹The constraint ‹'u::infinite› is not an artefact of the proof; the following argument
  is not formalised.  Soundness needs no constraint on ‹'u›.  Completeness does: over a @{emph ‹finite›} carrier no model
  of the class ‹ℳ⇘_βfb⇙› exists at all --- with negation and disjunction in the signature
  every boolean function is ‹λ›-definable, so the domains at the types ‹𝗈⇧ⁿ ❙⇒ 𝗈› grow
  beyond any bound --- and validity at a finite carrier would hold vacuously for every
  formula, making the direction ‹⊨ ⟹ ⊢› false.›

theorem consistency: "¬ ⊢ ❙⊥"
  by (rule nk_consistent)

corollary no_contradiction: "⊢ A ⟹ ¬ ⊢ ❙¬ A"
  by (rule nk_not_both)

text ‹Cantor's theorem is derived @{emph ‹inside›} ‹NK›, in surjective and injective form
  and at every type: @{thm [source] nk_surjective_cantor} and
  @{thm [source] nk_injective_cantor} in theory ‹Cantor›.  The two facts keep the names
  under which the initial release of this entry (August 2026) exported them:›

lemmas cantor_surjective = nk_surjective_cantor
lemmas cantor_injective = nk_injective_cantor

text ‹Consistency with the inequation scheme over new constants, for every injective family of
  individual constants, obtained by compactness from arbitrarily large finite
  models:›

corollary consistency_with_inequation_scheme:
  "inj (f :: nat ⇒ 'p::infinite) ⟹ con (Ineq f)"
  by (rule con_Ineq)

text ‹The same in the finitary form free of eigen-parameter effects, and jointly with the
  negated axiom (see theory ‹NK_Infinity›):›

corollary consistency_with_inequation_scheme_fprov:
  "inj (f :: nat ⇒ 'p::infinite) ⟹ ¬ (Ineq f ⊩ (❙⊥ :: 'p tm))"
  by (rule con_Ineq_fprov)

corollary consistency_with_inequation_scheme_and_negated_axiom:
  "inj (f :: nat ⇒ 'p::infinite) ⟹ con (insert (❙¬ DInf) (Ineq f))"
  by (rule con_Ineq_not_DInf)

text ‹The scheme does not yield the single Dedekind-style axiom of infinity ‹DInf›: no
  finite part of the scheme derives it, and a Henkin model of the whole scheme refutes it
  (@{thm [source] henkin_scheme_refutes_DInf} in theory ‹NK_Infinity›; its total domain
  injects into the term type, so it is countable over a countable signature).  That the
  pure axiom yields no inequation of the scheme is a side remark of the companion
  development.  Both results rest on the
  auxiliary constants of the scheme.  What the axiom does derive is every constant-free
  sentence ``there are at least ‹n› individuals'' (‹ExDistinct n› in theory
  ‹NK_Infinity›), the classical first-order axiomatisation of infinity.›

corollary scheme_does_not_derive_axiom:
  "inj (f :: nat ⇒ 'p::infinite) ⟹ ¬ (Ineq f ⊩ (DInf :: 'p tm))"
  by (rule Ineq_not_derives_DInf)

corollary axiom_derives_every_finite_cardinality:
  "{DInf :: 'p::infinite tm} ⊢ ExDistinct n"
  by (rule DInf_derives_distinct_n)

text ‹The converse fails: the constant-free sentences together do not derive the axiom
  (‹distinct_scheme_not_derives_DInf›; the Henkin model of
  ‹henkin_scheme_refutes_DInf› satisfies all of them and refutes ‹DInf›).  So in ‹NK›
  the first-order axiomatisation of infinity is strictly weaker than the Dedekind axiom;
  over standard models the two are equivalent (the step from an infinite individual
  domain to a Dedekind self-map in the full function space is not formalised).›

corollary finite_cardinalities_do_not_derive_axiom:
  "¬ (range (ExDistinct :: nat ⇒ 'p::infinite tm) ⊩ DInf)"
  by (rule distinct_scheme_not_derives_DInf)

text ‹The constant-free sentences are consistent with ‹NK›: no finite part of them derives
  falsity.  Every finite part holds in a large enough finite model of ‹Consistency›, so, as
  for the scheme, the consistency proof constructs no infinite model.›

corollary finite_cardinalities_consistent:
  "¬ (range (ExDistinct :: nat ⇒ 'p::infinite tm) ⊩ ❙⊥)"
  by (rule con_distinct_scheme)

text ‹Model existence (the positive half of Henkin completeness), restated: every consistent
  sentence over a countable signature has a ‹Σ›-Henkin model with @{emph ‹countable›} total domain, within plain HOL.
  Consistency is the only premise --- so where an axiom (e.g.\ of infinity) has no finite
  models and its consistency has to be established in a stronger meta-theory, that
  meta-theory is used for the consistency premise alone, and the witnessing model still has
  a countable total domain: the ‹∼›-classes of closed wffs, a subset of the carrier
  \<^typ>‹'p tm set›.›

corollary countable_henkin_model:
  fixes A :: "'p::{countable,infinite} tm"
  assumes "cwff 𝗈 A" and "con {A}"
  obtains Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'p tm set) ⇒ 'p tm ⇒ 'p tm set" and vl ξ
  where "bkk_model Dm Ap Ee vl" "countable {x. ∃τ. Dm τ x}"
        "app_struct.asg Dm ξ" "vl (Ee ξ A)"
  by (rule countable_henkin_sat[OF assms])

end