Theory Tarski

chapter ‹Abstract Formulation of Tarski's Theorems›

text ‹We prove Tarski's proof-theoretic and semantic theorems about the
non-definability and respectively non-expressiveness (in the standard model) of truth›

theory Tarski
  imports Goedel_Formula Standard_Model_More

section ‹Non-Definability of Truth›

context Goedel_Form

  fixes T :: 'fmla
  assumes T[simp,intro!]: "T  fmla"
  and Fvars_T[simp]: "Fvars T = {xx}"
  and prv_T: "φ. φ  fmla  Fvars φ = {}  prv (eqv (subst T φ xx) φ)"

definition φT :: 'fmla where "φT  diag (neg T)"

lemma φT[simp,intro!]: "φT  fmla" and
Fvars_φT[simp]: "Fvars φT = {}"
  unfolding φT_def PP_def by auto

lemma bprv_φT_eqv:
"bprv (eqv φT (neg (subst T φT xx)))"
  unfolding φT_def using bprv_diag_eqv[of "neg T"] by simp

lemma prv_φT_eqv:
"prv (eqv φT (neg (subst T φT xx)))"
  using d_dwf.bprv_prv'[OF _ bprv_φT_eqv, simplified] .

lemma φT_prv_fls: "prv fls"
using prv_eqv_eqv_neg_prv_fls2[OF _ _ prv_T[OF φT Fvars_φT] prv_φT_eqv] by auto

end ― ‹context›

theorem Tarski_proof_theoretic:
assumes "T  fmla" "Fvars T = {xx}"
and "φ. φ  fmla  Fvars φ = {}  prv (eqv (subst T φ xx) φ)"
shows "¬ consistent"
using φT_prv_fls[OF assms] consistent_def by auto

end ― ‹context @{locale Goedel_Form}

section ‹Non-Expressiveness of Truth›

text ‹This follows as a corollary of the syntactic version, after taking prv
to be isTrue on sentences.Indeed, this is a virtue of our abstract treatment
of provability: We don't work with a particular predicate, but with any predicate
that is closed under some rules --- which could as well be a semantic notion of truth (for sentences).›

locale Goedel_Form_prv_eq_isTrue =
  var trm fmla Var num FvarsT substT Fvars subst
  eql cnj imp all exi
  prv bprv
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var num FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and prv bprv
and enc ("_")
and S
and P
fixes isTrue :: "'fmla  bool"
assumes prv_eq_isTrue: " φ. φ  fmla  Fvars φ = {}  prv φ = isTrue φ"

theorem Tarski_semantic:
assumes 0: "T  fmla" "Fvars T = {xx}"
and 1: "φ. φ  fmla  Fvars φ = {}  isTrue (eqv (subst T φ xx) φ)"
shows "¬ consistent"
using assms prv_eq_isTrue[of "eqv (subst T _ xx) _"]
  by (intro Tarski_proof_theoretic[OF 0]) auto

text ‹NB: To instantiate the semantic version of Tarski's theorem for a truth predicate
isTruth on sentences, one needs to extend it to a predicate "prv" on formulas and verify
that "prv" satisfies the rules of intuitionistic logic.›

end ― ‹context @{locale Goedel_Form_prv_eq_isTrue}