Theory Main_Results

theory Main_Results
  imports Cantor
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, derivability coincides
  with validity at @{emph ‹every›} infinite value carrier --- 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.›

theorem NK_soundness:
  "Φ ⊢ C ⟹ Φ ⊨('u) C"
  using soundness_sat.

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

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

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

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

theorem cantor_surjective: fixes σ :: ty shows
  "⊢ (❙¬ (❙∃𝒢⇘σ ❙⇒ σ ❙⇒ 𝗈⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙∃𝒳⇘σ⇙.
     ((𝒢⇧f⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ ❙⋅ 𝒳⇧f⇘σ⇙) ❙=⇘σ ❙⇒ 𝗈⇙ ℱ⇧f⇘σ ❙⇒ 𝗈⇙)) :: 'p::infinite tm)"
  by (rule nk_surjective_cantor)

theorem cantor_injective: fixes σ :: ty shows
  "⊢ (❙¬ (❙∃ℐ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙Πℋ⇘σ ❙⇒ 𝗈⇙.
       (((ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) ❙=⇘σ⇙ (ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))
        ❙⊃ (ℱ⇧f⇘σ ❙⇒ 𝗈⇙ ❙=⇘σ ❙⇒ 𝗈⇙ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))) :: 'p::infinite tm)"
  by (rule nk_injective_cantor)

end