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
begin
(*>*)

section ‹Non-Definability of Truth›

context Goedel_Form
begin

context
  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) φ)"
begin

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 =
Goedel_Form
  var trm fmla Var num FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  prv bprv
  enc
  P
  S
for
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 φ"
begin

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}›

(*<*)
end
(*>*)