Theory Standard_Model

chapter ‹Truth in a Standard Model›

text ‹Abstract notion of standard model and truth.›

(*<*)
theory Standard_Model imports Deduction
begin
(*>*)

text ‹First some minimal assumptions, involving
implication, negation and (universal and existential) quantification:›

locale Minimal_Truth =
Syntax_with_Numerals_and_Connectives_False_Disj
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
+
― ‹The notion of truth for sentences:›
fixes isTrue :: "'fmla ⇒ bool"
assumes
not_isTrue_fls: "¬ isTrue fls"
and
isTrue_imp:
"⋀φ ψ. φ ∈ fmla ⟹ ψ ∈ fmla ⟹ Fvars φ = {} ⟹ Fvars ψ = {} ⟹
  isTrue φ ⟹ isTrue (imp φ ψ) ⟹ isTrue ψ"
and
isTrue_all:
"⋀x φ. x ∈ var ⟹ φ ∈ fmla ⟹ Fvars φ = {x} ⟹
  (∀ n ∈ num. isTrue (subst φ n x)) ⟹ isTrue (all x φ)"
and
isTrue_exi:
"⋀x φ. x ∈ var ⟹ φ ∈ fmla ⟹ Fvars φ = {x} ⟹
  isTrue (exi x φ) ⟹ (∃ n ∈ num. isTrue (subst φ n x))"
and
isTrue_neg:
"⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹
  isTrue φ ∨ isTrue (neg φ)"
begin

lemma isTrue_neg_excl:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹
 isTrue φ ⟹ isTrue (neg φ) ⟹ False"
  using isTrue_imp not_isTrue_fls unfolding neg_def by auto

lemma isTrue_neg_neg:
assumes "φ ∈ fmla" "Fvars φ = {}"
and "isTrue (neg (neg φ))"
shows "isTrue φ"
using assms isTrue_neg isTrue_neg_excl by fastforce

end ― ‹context @{locale  Minimal_Truth}›


locale Minimal_Truth_Soundness =
Minimal_Truth
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  isTrue
+
Deduct_with_False_Disj
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv
and isTrue
+
assumes
― ‹We assume soundness of the provability for sentences (w.r.t. truth):›
sound_isTrue: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ isTrue φ"
begin

text ‹For sound theories, consistency is a fact rather than a hypothesis:›
lemma consistent: consistent
  unfolding consistent_def using not_isTrue_fls sound_isTrue by blast

lemma prv_neg_excl:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ prv (neg φ) ⟹ False"
using isTrue_neg_excl[of φ] sound_isTrue by auto

lemma prv_imp_implies_isTrue:
assumes [simp]: "φ ∈ fmla" "χ ∈ fmla" "Fvars φ = {}" "Fvars χ = {}"
and p: "prv (imp φ χ)" and i: "isTrue φ"
shows "isTrue χ"
proof-
  have "isTrue (imp φ χ)" using p by (intro sound_isTrue) auto
  thus ?thesis using assms isTrue_imp by blast
qed

text ‹Sound theories are not only consistent, but also $\omega$-consistent
(in the strong, intuitionistic sense):›

lemma ωconsistent: ωconsistent
unfolding ωconsistent_def proof (safe del: notI)
  fix φ x assume 0[simp,intro]: "φ ∈ fmla"  "x ∈ var" and 1: "Fvars φ = {x}"
  and 00: "∀n∈num. prv (neg (subst φ n x))"
  hence "∀n∈num. isTrue (neg (subst φ n x))"
    using 00 1 by (auto intro!: sound_isTrue)
  hence "isTrue (all x (neg φ))" by (simp add: "1" isTrue_all)
  moreover
  {have "prv (imp (all x (neg φ)) (neg (exi x φ)))"
    using prv_all_neg_imp_neg_exi by blast
   hence "isTrue (imp (all x (neg φ)) (neg (exi x φ)))"
    by (simp add: "1" sound_isTrue)
  }
  ultimately have "isTrue (neg (exi x φ))"
    by (metis 0 1 Diff_insert_absorb Fvars_all Fvars_exi Fvars_neg all
      exi insert_absorb insert_not_empty isTrue_imp neg)
  hence "¬ isTrue (neg (neg (exi x φ)))"
    using 1 isTrue_neg_excl by force
  thus "¬ prv (neg (neg (exi x φ)))"
    using "1" sound_isTrue by auto
qed

lemma ωconsistentStd1: ωconsistentStd1
  using ωconsistent ωconsistent_impliesStd1 by blast

lemma ωconsistentStd2: ωconsistentStd2
  using ωconsistent ωconsistent_impliesStd2 by blast

end ― ‹context @{locale Minimal_Truth_Soundness}›

(*<*)
end
(*>*)