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