# Theory Deduction2

chapter ‹Deduction with Two Provability Relations›
(*<*)
theory Deduction2 imports "Syntax_Independent_Logic.Deduction"
begin
(*>*)

text ‹We work with two provability relations:
provability @{term prv} and basic provability @{term bprv}.›

section ‹From Deduction with One Provability Relation to Two›

locale Deduct2 =
Deduct
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv
+
B: Deduct
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
bprv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
+
assumes bprv_prv: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv φ ⟹ prv φ"
begin

(* Removing the sentence (empty Fvars) hypothesis from bprv_prv *)
lemma bprv_prv':
assumes φ: "φ ∈ fmla" and b: "bprv φ"
shows "prv φ"
proof-
obtain V where V: "Fvars φ = V" by blast
have VV: "V ⊆ var" using Fvars V φ by blast
have f: "finite V" using V finite_Fvars[OF φ] by auto
thus ?thesis using φ b V VV
proof(induction V arbitrary: φ rule: finite.induct)
case (emptyI φ)
then show ?case by (simp add: bprv_prv)
next
case (insertI W v φ)
show ?case proof(cases "v ∈ W")
case True
thus ?thesis
using insertI.IH[OF ‹φ ∈ fmla›] insertI.prems
by (simp add: insert_absorb)
next
case False
hence 1: "Fvars (all v φ) = W"
using insertI.prems by auto
moreover have "bprv (all v φ)"
using B.prv_all_gen insertI.prems by auto
ultimately have "prv (all v φ)" using insertI by auto
thus ?thesis using allE_id insertI.prems by blast
qed
qed
qed

end ― ‹context @{locale Deduct2}›

locale Deduct2_with_False =
Deduct_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv
+
B: Deduct_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
bprv
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 num
and prv bprv
+
assumes bprv_prv: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv φ ⟹ prv φ"

sublocale Deduct2_with_False < d_dwf: Deduct2
by standard (fact bprv_prv)

context Deduct2_with_False begin

lemma consistent_B_consistent: "consistent ⟹ B.consistent"
using B.consistent_def bprv_prv consistent_def by blast

end ― ‹context @{locale Deduct2_with_False}›

locale Deduct2_with_False_Disj =
Deduct_with_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv
+
B: Deduct_with_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
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 bprv
+
assumes bprv_prv: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv φ ⟹ prv φ"

sublocale Deduct2_with_False_Disj < dwf_dwfd: Deduct2_with_False
by standard (fact bprv_prv)

(* Factoring in a strict-order-like relation (not actually required to be an order): *)
locale Deduct2_with_PseudoOrder =
Deduct2_with_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
+
Syntax_PseudoOrder
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
Lq
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 bprv
and Lq
+
assumes
(* We do not assume any ordering properties, but only these two axioms, Lq_num and Lq_num2,
which (interestingly) would be satisfied by both ≤ and < within a sufficiently strong
arithmetic such as Robinson's Q *)
(* For each formula φ(z) and numeral q, if φ(p) is provable for all p
then ∀ z ≤ q. φ(z) is provable.
(Note that a more natural property would assume φ(p) is provable for all p≤q,
but we can get away with the stronger assumption (on the left of the implication). )
*)
Lq_num:
"let LLq = (λ t1 t2. psubst Lq [(t1,zz), (t2,yy)]) in
∀ φ ∈ fmla. ∀ q ∈ num. Fvars φ = {zz} ∧ (∀ p ∈ num. bprv (subst φ p zz))
⟶ prv (all zz (imp (LLq (Var zz) q) φ))"
and
(* For each numeral p, there exists a finite set P such that it is provable that
∀ y. (⋁p∈P. x = p) ∨ y ≤ p
(where we write ≤ instead of Lq, but could also think of <):
*)
Lq_num2:
"let LLq = (λ t1 t2. psubst Lq [(t1,zz), (t2,yy)]) in
∀ p ∈ num. ∃ P ⊆ num. finite P ∧ prv (dsj (sdsj {eql (Var yy) r | r. r ∈ P}) (LLq p (Var yy)))"
begin

lemma LLq_num:
assumes "φ ∈ fmla" "q ∈ num" "Fvars φ = {zz}" "∀ p ∈ num. bprv (subst φ p zz)"
shows "prv (all zz (imp (LLq (Var zz) q) φ))"
using assms Lq_num unfolding LLq_def by auto

lemma LLq_num2:
assumes "p ∈ num"
shows "∃ P ⊆ num. finite P ∧ prv (dsj (sdsj {eql (Var yy) r | r. r ∈ P}) (LLq p (Var yy)))"
using assms Lq_num2 unfolding LLq_def by auto

end ― ‹context @{locale Deduct2_with_PseudoOrder}›

section ‹Factoring In Explicit Proofs›

locale Deduct_with_Proofs =
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
+
fixes
"proof" :: "'proof set"
and
prfOf :: "'proof ⇒ 'fmla ⇒ bool"
assumes
― ‹Provability means there exists a proof (only needed for sentences):›
prv_prfOf: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟷ (∃ prf ∈ proof. prfOf prf φ)"

(* We consider proof structure only for prv, not for bprv *)
locale Deduct2_with_Proofs =
Deduct2_with_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
+
Deduct_with_Proofs
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv
"proof" prfOf
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 bprv
and "proof" :: "'proof set" and prfOf

locale Deduct2_with_Proofs_PseudoOrder =
Deduct2_with_Proofs
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
"proof" prfOf
+
Deduct2_with_PseudoOrder
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
Lq
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 bprv
and "proof" :: "'proof set" and prfOf
and Lq

(*<*)
end
(*>*)

# Theory Abstract_Encoding

chapter ‹Abstract Encoding›

(*<*)
theory Abstract_Encoding imports Deduction2
begin
(*>*)

text ‹Here we simply fix some unspecified encoding functions: encoding formulas
and proofs as numerals.›

locale Encode =
Syntax_with_Numerals
var trm fmla Var FvarsT substT Fvars subst
num
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
+
fixes enc :: "'fmla ⇒ 'trm" ("⟨_⟩")
assumes
enc[simp,intro!]: "⋀ φ. φ ∈ fmla ⟹ enc φ ∈ num"
begin

end ― ‹context @{locale Encode}›

text ‹Explicit proofs (encoded as numbers), needed only for the harder half of
Goedel's first, and for both half's of Rosser's version; not needed in Goedel's
second.›

locale Encode_Proofs =
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
+
Deduct2_with_Proofs
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
"proof" prfOf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("⟨_⟩")
and fls dsj
and "proof" :: "'proof set" and prfOf
+
fixes encPf :: "'proof ⇒ 'trm"
assumes
encPf[simp,intro!]: "⋀ pf. pf ∈ proof ⟹ encPf pf ∈ num"

(*<*)
end
(*>*)

# Theory Abstract_Representability

chapter ‹Representability Assumptions›

(*<*)
theory Abstract_Representability imports Abstract_Encoding
begin
(*>*)

text ‹Here we make assumptions about various functions or relations being
representable.›

section ‹Representability of Negation›

text ‹The negation function neg is assumed to be representable by a
two-variable formula N.›

locale Repr_Neg =
Deduct2_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv bprv
+
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
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 num
and prv bprv
and enc ("⟨_⟩")
+
fixes N :: 'fmla
assumes
N[simp,intro!]: "N ∈ fmla"
and
Fvars_N[simp]: "Fvars N = {xx,yy}"
and
neg_implies_prv_N:
"⋀ φ.
let NN = (λ t1 t2. psubst N [(t1,xx), (t2,yy)]) in
φ ∈ fmla ⟶ Fvars φ = {} ⟶ bprv (NN ⟨φ⟩ ⟨neg φ⟩)"
and
N_unique:
"⋀ φ.
let NN = (λ t1 t2. psubst N [(t1,xx), (t2,yy)]) in
φ ∈ fmla ⟶ Fvars φ = {} ⟶
bprv (all yy (all yy'
(imp (cnj (NN ⟨φ⟩ (Var yy)) (NN ⟨φ⟩ (Var yy')))
(eql (Var yy) (Var yy')))))"
begin

text ‹NN is a notation for the predicate that takes terms and returns corresponding instances
of N, obtained by substituting its free variables with these terms. This is very convenient
for reasoning, and will be done for all the representing formulas we will consider.›

definition NN where "NN ≡ λ t1 t2. psubst N [(t1,xx), (t2,yy)]"

lemma NN_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
NN t1 t2 = subst (subst N t1 xx) t2 yy"
unfolding NN_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma NN_neg:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (NN ⟨φ⟩ ⟨neg φ⟩)"
using neg_implies_prv_N unfolding Let_def NN_def by meson

lemma NN_unique:
assumes "φ ∈ fmla" "Fvars φ = {}"
shows "bprv (all yy (all yy'
(imp (cnj (NN ⟨φ⟩ (Var yy)) (NN ⟨φ⟩ (Var yy')))
(eql (Var yy) (Var yy')))))"
using assms N_unique unfolding Let_def NN_def by meson

lemma NN[simp,intro]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ NN t1 t2 ∈ fmla"
unfolding NN_def by auto

lemma Fvars_NN[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
Fvars (NN t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: NN_def2 subst2_fresh_switch)

(* Here and elsewhere: hard to make into one or two uniform statements,
given that we don't assume sufficiently powerful properties for trm substitution.
So such lists would need to be maintained on an ad hoc basis, keeping adding instances
when needed. *)
lemma [simp]:
"m ∈ num ⟹ n ∈ num ⟹ subst (NN m (Var yy)) n yy = NN m n"
"m ∈ num ⟹ n ∈ num ⟹ subst (NN m (Var yy')) n yy = NN m (Var yy')"
"m ∈ num ⟹ subst (NN m (Var yy')) (Var yy) yy' = NN m (Var yy)"
"n ∈ num ⟹ subst (NN (Var xx) (Var yy)) n xx = NN n (Var yy)"
"n ∈ num ⟹ subst (NN (Var xx) (Var xx')) n xx = NN n (Var xx')"
"m ∈ num ⟹ n ∈ num ⟹ subst (NN m (Var xx')) n zz = NN m (Var xx')"
"n ∈ num ⟹ subst (NN n (Var yy)) (Var xx') yy = NN n (Var xx')"
"m ∈ num ⟹ n ∈ num ⟹ subst (NN m (Var xx')) n xx' = NN m n"
by (auto simp add: NN_def2 subst2_fresh_switch)

lemma NN_unique2:
assumes [simp]:"φ ∈ fmla" "Fvars φ = {}"
shows
"bprv (all yy
(imp (NN ⟨φ⟩ (Var yy))
(eql ⟨neg φ⟩ (Var yy))))"
proof-
have 1: "bprv (NN ⟨φ⟩ ⟨neg φ⟩)"
using NN_neg[OF assms] .
have 2: "bprv (all yy' (
imp (cnj (NN ⟨φ⟩ ⟨neg φ⟩)
(NN ⟨φ⟩ (Var yy')))
(eql ⟨neg φ⟩ (Var yy'))))"
using B.prv_allE[of yy, OF _ _ _ NN_unique, of "φ" "⟨neg φ⟩"]
by fastforce
have 31: "bprv (all yy' (
imp (NN ⟨φ⟩ ⟨neg φ⟩)
(imp (NN ⟨φ⟩ (Var yy'))
(eql ⟨neg φ⟩ (Var yy')))))"
using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
have 32: "bprv (imp (NN ⟨φ⟩ ⟨neg φ⟩)
(all yy' (imp (NN ⟨φ⟩ (Var yy'))
(eql ⟨neg φ⟩ (Var yy')))))"
by (rule B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: NN_def2)
have 33: "bprv (all yy' (imp (NN ⟨φ⟩ (Var yy'))
(eql ⟨neg φ⟩ (Var yy'))))"
by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
thus ?thesis using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy] by simp
qed

lemma NN_neg_unique:
assumes [simp]:"φ ∈ fmla" "Fvars φ = {}"
shows
"bprv (imp (NN ⟨φ⟩ (Var yy))
(eql ⟨neg φ⟩ (Var yy)))" (is "bprv ?A")
proof-
have 0: "bprv (all yy ?A)"
using NN_unique2[of "φ"] by simp
show ?thesis by (rule B.allE_id[OF _ _ 0]) auto
qed

lemma NN_exi_cnj:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and χ[simp]: "χ ∈ fmla"
assumes f: "Fvars χ = {yy}"
shows "bprv (eqv (subst χ ⟨neg φ⟩ yy)
(exi yy (cnj χ (NN ⟨φ⟩ (Var yy)))))"
(is "bprv (eqv ?A ?B)")
proof(intro B.prv_eqvI)
have yy: "yy ∈ var" by simp
let ?N = "NN ⟨φ⟩ (Var yy)"
have "bprv (imp (subst χ ⟨neg φ⟩ yy) ((subst (cnj χ ?N) ⟨neg φ⟩ yy)))" using NN_neg[OF φ]
by (simp add: B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv)
thus "bprv (imp ?A ?B)"
by (elim B.prv_prv_imp_trans[rotated 3], intro B.prv_exi_inst) auto
next
have 00: "bprv (imp (eql ⟨neg φ⟩ (Var yy)) (imp χ (subst χ ⟨neg φ⟩ yy)))"
by (rule B.prv_eql_subst_trm_id_rev) auto
have 11: "bprv (imp (NN ⟨φ⟩ (Var yy)) (imp χ (subst χ ⟨neg φ⟩ yy)))"
using 00 NN_neg_unique[OF φ]
using NN num Var Variable φ χ eql imp subst B.prv_prv_imp_trans
by (metis (no_types, lifting) enc in_num neg)
hence "bprv (imp (cnj χ (NN ⟨φ⟩ (Var yy))) (subst χ ⟨neg φ⟩ yy))"
by (simp add: 11 B.prv_cnj_imp_monoR2 B.prv_imp_com)
hence 1: "bprv (all yy (imp (cnj χ (NN ⟨φ⟩ (Var yy))) (subst χ ⟨neg φ⟩ yy)))"
by (simp add: B.prv_all_gen)
have 2: "Fvars (subst χ ⟨neg φ⟩ yy) = {}" using f by simp
show "bprv (imp ?B ?A)" using 1 2
by (simp add: B.prv_exi_imp)
qed auto

end ― ‹context @{locale Repr_Neg}›

section ‹Representability of Self-Substitution›

text ‹Self-substitution is the function that takes a formula @{term φ}
and returns $\phi[\langle\phi\rangle/\mathit{xx}]$ (for the fixed variable @{term xx}). This is all that
will be needed for the diagonalization lemma.›

locale Repr_SelfSubst =
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
+
Deduct2
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("⟨_⟩")
+
fixes S :: 'fmla
assumes
S[simp,intro!]: "S ∈ fmla"
and
Fvars_S[simp]: "Fvars S = {xx,yy}"
and
subst_implies_prv_S:
"⋀ φ.
let SS = (λ t1 t2. psubst S [(t1,xx), (t2,yy)]) in
φ ∈ fmla ⟶ Fvars φ = {xx} ⟶
bprv (SS ⟨φ⟩ ⟨subst φ ⟨φ⟩ xx⟩)"
and
S_unique:
"⋀ φ.
let SS = (λ t1 t2. psubst S [(t1,xx), (t2,yy)]) in
φ ∈ fmla ⟶ Fvars φ = {xx} ⟶
bprv (all yy (all yy'
(imp (cnj (SS ⟨φ⟩ (Var yy)) (SS ⟨φ⟩ (Var yy')))
(eql (Var yy) (Var yy')))))"
begin

text ‹SS is the instantiation combinator of S:›
definition SS where "SS ≡ λ t1 t2. psubst S [(t1,xx), (t2,yy)]"

lemma SS_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹
yy ∉ FvarsT t1 ⟹
SS t1 t2 = subst (subst S t1 xx) t2 yy"
unfolding SS_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma subst_implies_prv_SS:
"φ ∈ fmla ⟹ Fvars φ = {xx} ⟹ bprv (SS ⟨φ⟩ ⟨subst φ ⟨φ⟩ xx⟩)"
using subst_implies_prv_S unfolding Let_def SS_def by meson

lemma SS_unique:
"φ ∈ fmla ⟹ Fvars φ = {xx} ⟹
bprv (all yy (all yy'
(imp (cnj (SS ⟨φ⟩ (Var yy)) (SS ⟨φ⟩ (Var yy')))
(eql (Var yy) (Var yy')))))"
using S_unique unfolding Let_def SS_def by meson

lemma SS[simp,intro]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ SS t1 t2 ∈ fmla"
unfolding SS_def by auto

lemma Fvars_SS[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
Fvars (SS t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: SS_def2 subst2_fresh_switch)

lemma [simp]:
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy)) p yy = SS m p"
"m ∈ num ⟹ subst (SS m (Var yy')) (Var yy) yy' = SS m (Var yy)"
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy')) p yy' = SS m p"
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy')) p yy = SS m (Var yy')"
"m ∈ num ⟹ subst (SS (Var xx) (Var yy)) m xx = SS m (Var yy)"
by (auto simp add: SS_def2 subst_comp_num Let_def)

end ― ‹context @{locale Repr_SelfSubst}›

section ‹Representability of Self-Soft-Substitution›

text ‹The soft substitution function performs substitution logically instead of
syntactically. In particular, its "self" version sends @{term φ} to
@{term "exi xx (cnj (eql (Var xx) (enc φ)) φ)"}. Representability of self-soft-substitution will be
an alternative assumption in the diagonalization lemma.›

locale Repr_SelfSoftSubst =
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
+
Deduct2
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("⟨_⟩")
+
fixes S :: 'fmla
assumes
S[simp,intro!]: "S ∈ fmla"
and
Fvars_S[simp]: "Fvars S = {xx,yy}"
and
softSubst_implies_prv_S:
"⋀ φ.
let SS = (λ t1 t2. psubst S [(t1,xx), (t2,yy)]) in
φ ∈ fmla ⟶ Fvars φ = {xx} ⟶
bprv (SS ⟨φ⟩ ⟨softSubst φ ⟨φ⟩ xx⟩)"
and
S_unique:
"⋀ φ.
let SS = (λ t1 t2. psubst S [(t1,xx), (t2,yy)]) in
φ ∈ fmla ⟶ Fvars φ = {xx} ⟶
bprv (all yy (all yy'
(imp (cnj (SS ⟨φ⟩ (Var yy)) (SS ⟨φ⟩ (Var yy')))
(eql (Var yy) (Var yy')))))"
begin

text ‹SS is the instantiation combinator of S:›
definition SS where "SS ≡ λ t1 t2. psubst S [(t1,xx), (t2,yy)]"

lemma SS_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹
yy ∉ FvarsT t1 ⟹
SS t1 t2 = subst (subst S t1 xx) t2 yy"
unfolding SS_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma softSubst_implies_prv_SS:
"φ ∈ fmla ⟹ Fvars φ = {xx} ⟹ bprv (SS ⟨φ⟩ ⟨softSubst φ ⟨φ⟩ xx⟩)"
using softSubst_implies_prv_S unfolding Let_def SS_def by meson

lemma SS_unique:
"φ ∈ fmla ⟹ Fvars φ = {xx} ⟹
bprv (all yy (all yy'
(imp (cnj (SS ⟨φ⟩ (Var yy)) (SS ⟨φ⟩ (Var yy')))
(eql (Var yy) (Var yy')))))"
using S_unique unfolding Let_def SS_def by meson

lemma SS[simp,intro]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ SS t1 t2 ∈ fmla"
unfolding SS_def by auto

lemma Fvars_SS[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
Fvars (SS t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: SS_def2 subst2_fresh_switch)

lemma [simp]:
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy)) p yy = SS m p"
"m ∈ num ⟹ subst (SS m (Var yy')) (Var yy) yy' = SS m (Var yy)"
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy')) p yy' = SS m p"
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy')) p yy = SS m (Var yy')"
"m ∈ num ⟹ subst (SS (Var xx) (Var yy)) m xx = SS m (Var yy)"
by (auto simp add: SS_def2 subst_comp_num Let_def)

end ― ‹context @{locale Repr_SelfSoftSubst}›

section ‹Clean Representability of the "Proof-of" Relation›

text‹For the proof-of relation, we must assume a stronger version of
representability, namely clean representability on the first argument, which
is dedicated to encoding the proof component. The property asks that the
representation predicate is provably false on numerals that do not encode
proofs; it would hold trivially for surjective proof encodings.

Cleanness is not a standard concept in the literature -- we have
introduced it in our CADE 2019 paper~\cite{DBLP:conf/cade/0001T19}.›

locale CleanRepr_Proofs =
Encode_Proofs
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
fls
dsj
"proof" prfOf
encPf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("⟨_⟩")
and fls dsj
and "proof" :: "'proof set" and prfOf
and encPf
+
fixes Pf :: 'fmla
assumes
Pf[simp,intro!]: "Pf ∈ fmla"
and
Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
and
prfOf_Pf:
"⋀ prf φ.
let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
(prf ∈ proof ∧ φ ∈ fmla ∧ Fvars φ = {} ⟶
prfOf prf φ
⟶
bprv (PPf (encPf prf) ⟨φ⟩))"
and
not_prfOf_Pf:
"⋀ prf φ.
let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
(prf ∈ proof ∧ φ ∈ fmla ∧ Fvars φ = {} ⟶
¬ prfOf prf φ
⟶
bprv (neg (PPf (encPf prf) ⟨φ⟩)))"
and
Clean_Pf_encPf:
"⋀ p φ. let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
p ∈ num ∧ φ ∈ fmla ∧ Fvars φ = {} ⟶ p ∉ encPf  proof ⟶ bprv (neg (PPf p ⟨φ⟩))"
begin

text ‹PPf is the instantiation combinator of Pf:›
definition PPf where "PPf ≡ λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]"

lemma prfOf_PPf:
assumes "prf ∈ proof" "φ ∈ fmla" "Fvars φ = {}" "prfOf prf φ"
shows "bprv (PPf (encPf prf) ⟨φ⟩)"
using assms prfOf_Pf unfolding PPf_def by auto

lemma not_prfOf_PPf:
assumes "prf ∈ proof" "φ ∈ fmla" "Fvars φ = {}" "¬ prfOf prf φ"
shows "bprv (neg (PPf (encPf prf) ⟨φ⟩))"
using assms not_prfOf_Pf unfolding PPf_def by auto

lemma Clean_PPf_encPf:
assumes "φ ∈ fmla" "Fvars φ = {}" and "p ∈ num" "p ∉ encPf  proof"
shows "bprv (neg (PPf p ⟨φ⟩))"
using assms Clean_Pf_encPf unfolding PPf_def by auto

lemma PPf[simp,intro!]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹ PPf t1 t2 ∈ fmla"
unfolding PPf_def by auto

lemma PPf_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹
PPf t1 t2 = subst (subst Pf t1 yy) t2 xx"
unfolding PPf_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma Fvars_PPf[simp]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹
Fvars (PPf t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: PPf_def2 subst2_fresh_switch)

lemma [simp]:
"n ∈ num ⟹ subst (PPf (Var yy) (Var xx)) n xx = PPf (Var yy) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf (Var yy) m) n yy = PPf n m"
"n ∈ num ⟹ subst (PPf (Var yy) (Var xx)) n yy = PPf n (Var xx)"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf m (Var xx)) n xx = PPf m n"
"m ∈ num ⟹ subst (PPf (Var zz) (Var xx')) m zz = PPf m (Var xx')"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf m (Var xx')) n xx' = PPf m n"
"n ∈ num ⟹ subst (PPf (Var zz) (Var xx')) n xx' = PPf (Var zz) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf (Var zz) n) m zz = PPf m n"
by (auto simp add: PPf_def2 subst2_fresh_switch)

lemma B_consistent_prfOf_iff_PPf:
"B.consistent ⟹ prf ∈ proof ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟶ prfOf prf φ ⟷ bprv (PPf (encPf prf) ⟨φ⟩)"
unfolding B.consistent_def3 using not_prfOf_PPf[of "prf" φ] prfOf_PPf[of "prf" φ] by force

lemma consistent_prfOf_iff_PPf:
"consistent ⟹ prf ∈ proof ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟶ prfOf prf φ ⟷ bprv (PPf (encPf prf) ⟨φ⟩)"
using B_consistent_prfOf_iff_PPf[OF dwf_dwfd.consistent_B_consistent] .

end ― ‹context @{locale CleanRepr_Proofs}›

(*<*)
end
(*>*)


# Theory Diagonalization

chapter ‹Diagonalization›

text ‹This theory proves abstract versions of the diagonalization lemma,
with both hard and soft substitution.›

section ‹Alternative Diagonalization via Self-Substitution›

(*<*)
theory Diagonalization imports Abstract_Representability
begin
(*>*)

text ‹
Assuming representability of the diagonal instance of the substitution function,
we prove the standard diagonalization lemma. More precisely, we show that it applies
to any logic that
-- embeds intuitionistic first-order logic over numerals
-- has a countable number of formulas
-- has formula self-substitution representable
›

context Repr_SelfSubst
begin

theorem diagonalization:
assumes φ[simp,intro!]: "φ ∈ fmla" "Fvars φ = {xx}"
shows "∃ ψ. ψ ∈ fmla ∧ Fvars ψ = {} ∧ bprv (eqv ψ (subst φ ⟨ψ⟩ xx))"
proof-
let ?phi = "λ t. subst φ t xx"
define χ where "χ ≡ exi yy (cnj (?phi (Var yy)) (SS (Var xx) (Var yy)))"
have χ[simp,intro!]: "χ ∈ fmla" unfolding χ_def by auto
let ?chi = "λ t. subst χ t xx"
define ψ where "ψ ≡ ?chi ⟨χ⟩"
have ψ[simp,intro!]: "ψ ∈ fmla" unfolding ψ_def by auto
have fχ[simp]: "Fvars χ = {xx}" unfolding χ_def by auto
hence Fvars_ψ: "Fvars ψ = {}" unfolding ψ_def by auto
have 1: "bprv (SS ⟨χ⟩ ⟨ψ⟩)"
using subst_implies_prv_SS[OF χ] unfolding ψ_def by simp
have 2: "bprv (all yy' (
imp (cnj (SS ⟨χ⟩ ⟨ψ⟩)
(SS ⟨χ⟩ (Var yy')))
(eql ⟨ψ⟩ (Var yy'))))"
using Fvars_ψ B.prv_allE[OF _ _ _ SS_unique, of χ "⟨ψ⟩"]
by fastforce
have 31: "bprv (all yy'
(imp (SS ⟨χ⟩ ⟨ψ⟩)
(imp (SS ⟨χ⟩ (Var yy'))
(eql ⟨ψ⟩ (Var yy')))))"
using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
have 32: "bprv (imp (SS ⟨χ⟩ ⟨ψ⟩)
(all yy' (imp (SS ⟨χ⟩ (Var yy'))
(eql ⟨ψ⟩ (Var yy')))))"
by (intro B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: SS_def2)
have 33: "bprv (all yy' (imp (SS ⟨χ⟩ (Var yy'))
(eql ⟨ψ⟩ (Var yy'))))"
by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
have 3: "bprv (all yy (imp (SS ⟨χ⟩ (Var yy))
(eql ⟨ψ⟩ (Var yy))))"
using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy]
by fastforce
have 41: "bprv (imp (?phi ⟨ψ⟩)
(cnj (?phi ⟨ψ⟩)
(SS ⟨χ⟩ ⟨ψ⟩)))"
by (auto intro: in_num B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv[OF _ _ 1])
have [simp]: "subst (subst φ ⟨ψ⟩ xx) ⟨ψ⟩ yy = subst φ ⟨ψ⟩ xx"
by (intro subst_notIn) auto
have [simp]: "subst (subst φ (Var yy) xx) ⟨ψ⟩ yy = subst φ ⟨ψ⟩ xx"
by (intro subst_subst) auto
have 42: "bprv (exi yy (imp (?phi ⟨ψ⟩)
(cnj (?phi (Var yy))
(SS ⟨χ⟩ (Var yy)))))"
using 41 by (intro B.prv_exiI[of _ _ "⟨ψ⟩"]) auto
have 4: "bprv (imp (?phi ⟨ψ⟩) (?chi ⟨χ⟩))"
using B.prv_imp_exi[OF _ _ _ _ 42,simplified]
by (subst χ_def) (auto simp add: subst_comp_num)
have 50: "bprv (all yy (
(imp (eql ⟨ψ⟩ (Var yy))
(imp (?phi (Var yy))
(?phi ⟨ψ⟩)))))"
using B.prv_all_eql[of yy xx φ "⟨ψ⟩" "Var yy"] by simp
have 51: "bprv (all yy (
(imp (SS ⟨χ⟩ (Var yy))
(imp (?phi (Var yy))
(?phi ⟨ψ⟩)))))" using B.prv_all_imp_trans[OF _ _ _ _ 3 50] by simp
have 52: "bprv (all yy (
(imp (cnj (?phi (Var yy))
(SS ⟨χ⟩ (Var yy)))
(?phi ⟨ψ⟩))))" using B.prv_all_imp_cnj[OF _ _ _ _ 51] by simp
have 5: "bprv (imp (?chi ⟨χ⟩) (?phi ⟨ψ⟩))"
using B.prv_exi_imp[OF _ _ _ _ 52,simplified]
by (subst χ_def) (simp add: subst_comp_num)
have 6: "bprv (eqv (?chi ⟨χ⟩) (?phi ⟨ψ⟩))"
using B.prv_cnjI[OF _ _ 5 4] unfolding eqv_def by simp
have 7: "bprv (eqv ψ (?phi ⟨ψ⟩))" using 6 unfolding ψ_def .
show ?thesis using ψ 7 Fvars_ψ by blast
qed

text ‹Making this existential into a function.›

definition diag :: "'fmla ⇒ 'fmla" where
"diag φ ≡ SOME ψ. ψ ∈ fmla ∧ Fvars ψ = {} ∧ bprv (eqv ψ (subst φ ⟨ψ⟩ xx))"

theorem diag_everything:
assumes "φ ∈ fmla" and "Fvars φ = {xx}"
shows "diag φ ∈ fmla ∧ Fvars (diag φ) = {} ∧ bprv (eqv (diag φ) (subst φ ⟨diag φ⟩ xx))"
unfolding diag_def using someI_ex[OF diagonalization[OF assms]] .

lemmas diag[simp] = diag_everything[THEN conjunct1]
lemmas Fvars_diag[simp] = diag_everything[THEN conjunct2, THEN conjunct1]
lemmas bprv_diag_eqv = diag_everything[THEN conjunct2, THEN conjunct2]

end ― ‹context @{locale Repr_SelfSubst}›

section ‹Alternative Diagonalization via Soft Self-Substitution›

context Repr_SelfSoftSubst
begin

theorem diagonalization:
assumes φ[simp,intro!]: "φ ∈ fmla" "Fvars φ = {xx}"
shows "∃ ψ. ψ ∈ fmla ∧ Fvars ψ = {} ∧ bprv (eqv ψ (subst φ ⟨ψ⟩ xx))"
proof-
let ?phi = "λ t. subst φ t xx"
define χ where "χ ≡ exi yy (cnj (?phi (Var yy)) (SS (Var xx) (Var yy)))"
have χ[simp,intro!]: "χ ∈ fmla" unfolding χ_def by auto
let ?chi = "λ t. softSubst χ t xx"
define ψ where "ψ ≡ ?chi ⟨χ⟩"
have ψ[simp,intro!]: "ψ ∈ fmla" unfolding ψ_def by auto
have fχ[simp]: "Fvars χ = {xx}" unfolding χ_def by auto
hence Fvars_ψ: "Fvars ψ = {}" unfolding ψ_def by auto
have 1: "bprv (SS ⟨χ⟩ ⟨ψ⟩)"
using softSubst_implies_prv_SS[OF χ] unfolding ψ_def by simp
have 2: "bprv (all yy' (
imp (cnj (SS ⟨χ⟩ ⟨ψ⟩)
(SS ⟨χ⟩ (Var yy')))
(eql ⟨ψ⟩ (Var yy'))))"
using Fvars_ψ B.prv_allE[OF _ _ _ SS_unique, of χ "⟨ψ⟩"]
by fastforce
have 31: "bprv (all yy'
(imp (SS ⟨χ⟩ ⟨ψ⟩)
(imp (SS ⟨χ⟩ (Var yy'))
(eql ⟨ψ⟩ (Var yy')))))"
using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
have 32: "bprv (imp (SS ⟨χ⟩ ⟨ψ⟩)
(all yy' (imp (SS ⟨χ⟩ (Var yy'))
(eql ⟨ψ⟩ (Var yy')))))"
by (intro B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: SS_def2)
have 33: "bprv (all yy' (imp (SS ⟨χ⟩ (Var yy'))
(eql ⟨ψ⟩ (Var yy'))))"
by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
have 3: "bprv (all yy (imp (SS ⟨χ⟩ (Var yy))
(eql ⟨ψ⟩ (Var yy))))"
using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy]
by fastforce
have 41: "bprv (imp (?phi ⟨ψ⟩)
(cnj (?phi ⟨ψ⟩)
(SS ⟨χ⟩ ⟨ψ⟩)))"
by (auto intro: in_num B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv[OF _ _ 1])
have [simp]: "subst (subst φ ⟨ψ⟩ xx) ⟨ψ⟩ yy = subst φ ⟨ψ⟩ xx"
by (intro subst_notIn) auto
have [simp]: "subst (subst φ (Var yy) xx) ⟨ψ⟩ yy = subst φ ⟨ψ⟩ xx"
by (intro subst_subst) auto
have 42: "bprv (exi yy (imp (?phi ⟨ψ⟩)
(cnj (?phi (Var yy))
(SS ⟨χ⟩ (Var yy)))))"
using 41 by (intro B.prv_exiI[of _ _ "⟨ψ⟩"]) auto
have 4: "bprv (imp (?phi ⟨ψ⟩) (subst χ ⟨χ⟩ xx))"
using B.prv_imp_exi[OF _ _ _ _ 42,simplified]
by (subst χ_def) (auto simp add: subst_comp_num)
moreover have "bprv (imp (subst χ ⟨χ⟩ xx) (?chi ⟨χ⟩))" by (rule B.prv_subst_imp_softSubst) auto
ultimately have 4: "bprv (imp (?phi ⟨ψ⟩) (?chi ⟨χ⟩))"
by (rule B.prv_prv_imp_trans[rotated -2]) auto
have 50: "bprv (all yy (
(imp (eql ⟨ψ⟩ (Var yy))
(imp (?phi (Var yy))
(?phi ⟨ψ⟩)))))"
using B.prv_all_eql[of yy xx φ "⟨ψ⟩" "Var yy"] by simp
have 51: "bprv (all yy (
(imp (SS ⟨χ⟩ (Var yy))
(imp (?phi (Var yy))
(?phi ⟨ψ⟩)))))" using B.prv_all_imp_trans[OF _ _ _ _ 3 50] by simp
have 52: "bprv (all yy (
(imp (cnj (?phi (Var yy))
(SS ⟨χ⟩ (Var yy)))
(?phi ⟨ψ⟩))))" using B.prv_all_imp_cnj[OF _ _ _ _ 51] by simp
have "bprv (imp (?chi ⟨χ⟩) (subst χ ⟨χ⟩ xx))" by (rule B.prv_softSubst_imp_subst) auto
moreover have "bprv (imp (subst χ ⟨χ⟩ xx) (?phi ⟨ψ⟩))"
using B.prv_exi_imp[OF _ _ _ _ 52,simplified]
by (subst χ_def) (simp add: subst_comp_num)
ultimately have 5: "bprv (imp (?chi ⟨χ⟩) (?phi ⟨ψ⟩))"
by (rule B.prv_prv_imp_trans[rotated -2]) auto
have 6: "bprv (eqv (?chi ⟨χ⟩) (?phi ⟨ψ⟩))"
using B.prv_cnjI[OF _ _ 5 4] unfolding eqv_def by simp
have 7: "bprv (eqv ψ (?phi ⟨ψ⟩))" using 6 unfolding ψ_def .
show ?thesis using ψ 7 Fvars_ψ by blast
qed

text ‹Making this existential into a function.›

definition diag :: "'fmla ⇒ 'fmla" where
"diag φ ≡ SOME ψ. ψ ∈ fmla ∧ Fvars ψ = {} ∧ bprv (eqv ψ (subst φ ⟨ψ⟩ xx))"

theorem diag_everything:
assumes "φ ∈ fmla" and "Fvars φ = {xx}"
shows "diag φ ∈ fmla ∧ Fvars (diag φ) = {} ∧ bprv (eqv (diag φ) (subst φ ⟨diag φ⟩ xx))"
unfolding diag_def using someI_ex[OF diagonalization[OF assms]] .

lemmas diag[simp] = diag_everything[THEN conjunct1]
lemmas Fvars_diag[simp] = diag_everything[THEN conjunct2, THEN conjunct1]
lemmas prv_diag_eqv = diag_everything[THEN conjunct2, THEN conjunct2]

end ― ‹context @{locale Repr_SelfSoftSubst}›

(*<*)
end
(*>*)


# Theory Derivability_Conditions

chapter ‹The Hilbert-Bernays-Löb (HBL) Derivability Conditions›

(*<*)
theory Derivability_Conditions imports Abstract_Representability
begin
(*>*)

section ‹First Derivability Condition›

(* Assume the provability predicate is "very-weakly" representable,
in that one implication of the weak representability condition holds.   *)
locale HBL1 =
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
+
Deduct2
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("⟨_⟩")
+
(* Very-weak represenatbility of provability, as a one-variable formula P, usually called the provability predicate: *)
fixes P :: 'fmla
assumes
P[intro!,simp]: "P ∈ fmla"
and
Fvars_P[simp]: "Fvars P = {xx}"
and
HBL1: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ bprv (subst P ⟨φ⟩ xx)"
begin

(* For all our (very-weak) representability assumptions, in addition to
the representing formulas,
here, P, we define a corresponding instantiation combinator, here the
predicate PP.
If we think of P as P(xx), then PP t is the instance PP(t)  *)
definition PP where "PP ≡ λt. subst P t xx"

lemma PP[simp]: "⋀t. t ∈ trm ⟹ PP t ∈ fmla"
unfolding PP_def by auto

lemma Fvars_PP[simp]: "⋀t. t ∈ trm ⟹ Fvars (PP t) = FvarsT t"
unfolding PP_def by auto

lemma [simp]:
"n ∈ num ⟹ subst (PP (Var yy)) n yy = PP n"
"n ∈ num ⟹ subst (PP (Var xx)) n xx = PP n"
unfolding PP_def by auto

lemma HBL1_PP:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ bprv (PP ⟨φ⟩)"
using HBL1 unfolding PP_def by auto

end ― ‹context @{locale HBL1}›

section ‹Connections between Proof Representability,
First Derivability Condition, and Its Converse›

context CleanRepr_Proofs
begin

text ‹Defining @{term P}, the internal notion of provability,
from @{term Pf} (in its predicate form @{term PPf}), the internal notion of "proof-of".
NB: In the technical sense of the term "represents", we have that
@{term Pf} represents @{term pprv}, whereas @{term P} will not represent @{term prv}, but satisfy a weaker
condition (weaker than weak representability), namely HBL1.›

subsection ‹HBL1 from "proof-of" representability›

definition P :: "'fmla" where "P ≡ exi yy (PPf (Var yy) (Var xx))"

lemma P[simp,intro!]: "P ∈ fmla" and Fvars_P[simp]: "Fvars P = {xx}"
unfolding P_def by (auto simp: PPf_def2)

text ‹We infer HBL1 from Pf representing prv:›
lemma HBL1:
assumes φ: "φ ∈ fmla" "Fvars φ = {}" and pφ: "prv φ"
shows "bprv (subst P ⟨φ⟩ xx)"
proof-
obtain "prf" where pf: "prf ∈ proof" and "prfOf prf φ" using prv_prfOf assms by auto
hence 0: "bprv (PPf (encPf prf) (enc φ))"
using prfOf_PPf φ by auto
have 1: "subst (subst Pf (encPf prf) yy) ⟨φ⟩ xx = subst (subst Pf ⟨φ⟩ xx) (substT (encPf prf) ⟨φ⟩ xx) yy"
using assms pf by (intro subst_compose_diff) auto
show ?thesis using 0 unfolding P_def using assms
by (auto simp: PPf_def2 1 pf intro!: B.prv_exiI[of _ _ "encPf prf"])
qed

text ‹This is used in several places, including for the hard half of
Gödel's First and the truth of Gödel formulas (and also for the Rosser variants
of these).›
lemma not_prv_prv_neg_PPf:
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "¬ prv φ" and n[simp]: "n ∈ num"
shows "bprv (neg (PPf n ⟨φ⟩))"
proof-
have "∀prf∈proof. ¬ prfOf prf φ" using prv_prfOf p by auto
hence "∀prf∈proof. bprv (neg (PPf (encPf prf) ⟨φ⟩))" using not_prfOf_PPf by auto
thus ?thesis using not_prfOf_PPf using Clean_PPf_encPf by (cases "n ∈ encPf  proof") auto
qed

lemma consistent_not_prv_not_prv_PPf:
assumes c: consistent
and 0[simp]: "φ ∈ fmla" "Fvars φ = {}" "¬ prv φ" "n ∈ num"
shows "¬ bprv (PPf n ⟨φ⟩)"
using not_prv_prv_neg_PPf[OF 0] c[THEN dwf_dwfd.consistent_B_consistent] unfolding B.consistent_def3 by auto

end ― ‹context @{locale CleanRepr_Proofs}›

text ‹The inference of HBL1 from "proof-of" representability, in locale form:›
sublocale CleanRepr_Proofs < wrepr: HBL1
where P = P
using HBL1 by unfold_locales auto

subsection ‹Sufficient condition for the converse of HBL1›

context CleanRepr_Proofs
begin

lemma PP_PPf:
assumes "φ ∈ fmla"
shows "wrepr.PP ⟨φ⟩ = exi yy (PPf (Var yy) ⟨φ⟩)"
unfolding wrepr.PP_def using assms
by (auto simp: PPf_def2 P_def)

text ‹The converse of HLB1 condition follows from (the standard notion of)
$\omega$-consistency for @{term bprv} and strong representability of proofs:›
lemma ωconsistentStd1_HBL1_rev:
assumes oc: "B.ωconsistentStd1"
and φ[simp]: "φ ∈ fmla" "Fvars φ = {}"
and iPP: "bprv (wrepr.PP ⟨φ⟩)"
shows "prv φ"
proof-
have 0: "bprv (exi yy (PPf (Var yy) ⟨φ⟩))" using iPP by (simp add: PP_PPf)
{assume "¬ prv φ"
hence "∀n ∈ num. bprv (neg (PPf n ⟨φ⟩))" using not_prv_prv_neg_PPf by auto
hence "¬ bprv (exi yy (PPf (Var yy) ⟨φ⟩))"
using oc unfolding B.ωconsistentStd1_def using φ by auto
hence False using 0 by simp
}
thus ?thesis by auto
qed

end ― ‹context @{locale CleanRepr_Proofs}›

section ‹Second and Third Derivability Conditions›

text ‹These are only needed for Gödel's Second.›

locale HBL1_2_3 =
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
P
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("⟨_⟩")
and P
+
assumes
HBL2: "⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ Fvars φ = {} ⟹ Fvars χ = {} ⟹
bprv (imp (cnj (PP ⟨φ⟩) (PP ⟨imp φ χ⟩))
(PP ⟨χ⟩))"
and
HBL3: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (imp (PP ⟨φ⟩) (PP ⟨PP ⟨φ⟩⟩))"
begin

text ‹The implicational form of HBL2:›
lemma HBL2_imp:
"⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ Fvars φ = {} ⟹ Fvars χ = {} ⟹
bprv (imp (PP ⟨imp φ χ⟩) (imp (PP ⟨φ⟩) (PP ⟨χ⟩)))"
using HBL2 by (simp add: B.prv_cnj_imp B.prv_imp_com)

text ‹... and its weaker, "detached" version:›
lemma HBL2_imp2:
assumes "φ ∈ fmla" and "χ ∈ fmla" "Fvars φ = {}" "Fvars χ = {}"
assumes "bprv (PP ⟨imp φ χ⟩)"
shows "bprv (imp (PP ⟨φ⟩) (PP ⟨χ⟩))"
using assms by (meson HBL2_imp PP enc imp num B.prv_imp_mp subsetCE)

end ― ‹context @{locale HBL1_2_3}›

(*<*)
end
(*>*)



# Theory Goedel_Formula

chapter ‹Gödel Formulas›

(*<*)
theory Goedel_Formula imports Diagonalization Derivability_Conditions
begin
(*>*)

text ‹Gödel formulas are defined by diagonalizing the negation of the provability predicate.›

locale Goedel_Form =
― ‹Assuming the @{term fls} (False) connective gives us negation:›
Deduct2_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv bprv
+
Repr_SelfSubst
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
S
+
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
P
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
begin

text ‹The Gödel formula.
NB, we speak of "the" Gödel formula because the diagonalization function makes a choice.›
definition φG :: 'fmla where "φG ≡ diag (neg P)"

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

lemma bprv_φG_eqv:
"bprv (eqv φG (neg (PP ⟨φG⟩)))"
unfolding φG_def PP_def using bprv_diag_eqv[of "neg P"] by simp

lemma prv_φG_eqv:
"prv (eqv φG (neg (PP ⟨φG⟩)))"
using bprv_prv[OF _ _ bprv_φG_eqv, simplified] .

end ― ‹context @{locale Goedel_Form}›

text ‹Adding cleanly representable proofs to the assumptions
behind Gödel formulas:›

locale Goedel_Form_Proofs =
Repr_SelfSubst
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
S
+
CleanRepr_Proofs
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
fls
dsj
"proof" prfOf
encPf
Pf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst num
and eql cnj imp all exi
and fls
and prv bprv
and enc ("⟨_⟩")
and S
and dsj
and "proof" :: "'proof set" and prfOf encPf
and Pf

text ‹... and extending the sublocale relationship @{locale CleanRepr_Proofs} < @{locale HBL1}:›
sublocale Goedel_Form_Proofs < Goedel_Form where P = P by standard

context Goedel_Form_Proofs
begin

lemma bprv_φG_eqv_not_exi_PPf:
"bprv (eqv φG (neg (exi yy (PPf (Var yy) ⟨φG⟩))))"
proof-
have P: "P = exi yy Pf" using P_def by (simp add: PPf_def2)
hence "subst P ⟨φG⟩ xx = subst (exi yy Pf) ⟨φG⟩ xx" by auto
hence "subst P ⟨φG⟩ xx = exi yy (subst Pf ⟨φG⟩ xx)" by simp
thus ?thesis using bprv_φG_eqv by (simp add: wrepr.PP_def PPf_def2)
qed

lemma prv_φG_eqv_not_exi_PPf:
"prv (eqv φG (neg (exi yy (PPf (Var yy) ⟨φG⟩))))"
using bprv_prv[OF _ _ bprv_φG_eqv_not_exi_PPf, simplified] .

lemma bprv_φG_eqv_all_not_PPf:
"bprv (eqv φG (all yy (neg (PPf (Var yy) ⟨φG⟩))))"
by (rule B.prv_eqv_trans[OF _ _ _ bprv_φG_eqv_not_exi_PPf B.prv_neg_exi_eqv_all_neg]) auto

lemma prv_φG_eqv_all_not_PPf:
"prv (eqv φG (all yy (neg (PPf (Var yy) ⟨φG⟩))))"
using bprv_prv[OF _ _ bprv_φG_eqv_all_not_PPf, simplified] .

lemma bprv_eqv_all_not_PPf_imp_φG:
"bprv (imp (all yy (neg (PPf (Var yy) ⟨φG⟩))) φG)"
using bprv_φG_eqv_all_not_PPf by (auto intro: B.prv_imp_eqvER)

lemma prv_eqv_all_not_PPf_imp_φG:
"prv (imp (all yy (neg (PPf (Var yy) ⟨φG⟩))) φG)"
using bprv_prv[OF _ _ bprv_eqv_all_not_PPf_imp_φG, simplified] .

end ― ‹context @{locale Goedel_Form_Proofs}›

(*<*)
end
(*>*)


# Theory Standard_Model_More

chapter ‹Standard Models with Two Provability Relations›

(*<*)
(* Abstract notion of standard model and truth  *)
theory Standard_Model_More
imports Derivability_Conditions "Syntax_Independent_Logic.Standard_Model"
begin
(*>*)

locale Minimal_Truth_Soundness_Proof_Repr =
CleanRepr_Proofs
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
fls
dsj
"proof" prfOf
encPf
Pf
+ ― ‹The label "B" stands for "basic", as a reminder that soundness
refers to the basic provability relation:›
B: Minimal_Truth_Soundness
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
isTrue
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 bprv
and isTrue
and enc ("⟨_⟩")
and "proof" :: "'proof set" and prfOf
and encPf Pf
begin

lemmas prfOf_iff_PPf = B_consistent_prfOf_iff_PPf[OF B.consistent]

text ‹The provability predicate is decided by basic provability on encodings:›
lemma isTrue_prv_PPf_prf_or_neg:
"prf ∈ proof ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
bprv (PPf (encPf prf) ⟨φ⟩) ∨ bprv (neg (PPf (encPf prf) ⟨φ⟩))"
using not_prfOf_PPf prfOf_PPf by blast

text ‹... hence that predicate is complete w.r.t. truth:›
lemma isTrue_PPf_Implies_bprv_PPf:
"prf ∈ proof ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
isTrue (PPf (encPf prf) ⟨φ⟩) ⟹ bprv (PPf (encPf prf) ⟨φ⟩)"
by (metis FvarsT_num Fvars_PPf Fvars_fls PPf
Un_empty empty_iff enc encPf fls in_num isTrue_prv_PPf_prf_or_neg
neg_def B.not_isTrue_fls B.prv_imp_implies_isTrue)

text ‹... and thanks cleanness we can replace encoded proofs
with arbitrary numerals in the completeness property:›
lemma isTrue_implies_bprv_PPf:
assumes [simp]: "n ∈ num" "φ ∈ fmla" "Fvars φ = {}"
and iT: "isTrue (PPf n ⟨φ⟩)"
shows "bprv (PPf n ⟨φ⟩)"
proof(cases "n ∈ encPf  proof")
case True
thus ?thesis
using iT isTrue_PPf_Implies_bprv_PPf by auto
next
case False
hence "bprv (neg (PPf n ⟨φ⟩))" by (simp add: Clean_PPf_encPf)
hence "isTrue (neg (PPf n ⟨φ⟩))" by (intro B.sound_isTrue) auto
hence False using iT by (intro B.isTrue_neg_excl) auto
thus ?thesis by auto
qed

text ‹... in fact, by @{locale Minimal_Truth_Soundness} we even have an iff:›
lemma isTrue_iff_bprv_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹ isTrue (PPf n ⟨φ⟩) ⟷ bprv (PPf n ⟨φ⟩)"
using isTrue_implies_bprv_PPf
using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto

text ‹Truth of the provability representation implies provability (TIP):›
lemma TIP:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}"
and iPP: "isTrue (wrepr.PP ⟨φ⟩)"
shows "prv φ"
proof-
have "isTrue (exi yy (PPf (Var yy) ⟨φ⟩))" using iPP unfolding PP_PPf[OF φ(1)] .
from B.isTrue_exi[OF _ _ _ this]
obtain n where n[simp]: "n ∈ num" and "isTrue (PPf n ⟨φ⟩)" by auto
hence pP: "bprv (PPf n ⟨φ⟩)" using isTrue_implies_bprv_PPf by auto
hence "¬ bprv (neg (PPf n ⟨φ⟩))"
using B.prv_neg_excl[of "PPf n ⟨φ⟩"] by auto
then obtain "prf" where "prf"[simp]: "prf ∈ proof" and nn: "n = encPf prf"
using assms n Clean_PPf_encPf φ(1) by blast
have "prfOf prf φ" using pP unfolding nn using prfOf_iff_PPf by auto
thus ?thesis using prv_prfOf by auto
qed

text ‹The reverse HBL1 -- now without the $\omega$-consistency assumption which holds here
thanks to our truth-in-standard-model assumption:›

lemmas HBL1_rev = ωconsistentStd1_HBL1_rev[OF B.ωconsistentStd1]
text ‹Note that the above would also follow by @{locale Minimal_Truth_Soundness} from TIP:›
lemma TIP_implies_HBL1_rev:
assumes TIP: "∀φ. φ ∈ fmla ∧ Fvars φ = {} ∧ isTrue (wrepr.PP ⟨φ⟩) ⟶ prv φ"
shows "∀φ. φ ∈ fmla ∧ Fvars φ = {} ∧ bprv (wrepr.PP ⟨φ⟩) ⟶ prv φ"
using B.sound_isTrue[of "wrepr.PP ⟨_⟩"] TIP by auto

end ― ‹context @{locale Minimal_Truth_Soundness_Proof_Repr}›

section ‹Proof recovery from $\mathit{HBL1\_iff}$›

locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
P
+
B : Minimal_Truth_Soundness
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
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 enc ("⟨_⟩")
and prv bprv
and P
and isTrue
+
fixes Pf :: 'fmla
assumes
― ‹@{term Pf} is a formula with free variables @{term xx} @{term yy}:›
Pf[simp,intro!]: "Pf ∈ fmla"
and
Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
and
― ‹@{term P} relates to @{term Pf} internally (inside basic provability)
just like a @{term prv} and a @{term prfOf} would relate---via an existential:›
P_Pf:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹
let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
bprv (eqv (subst P ⟨φ⟩ xx) (exi yy (PPf (Var yy) ⟨φ⟩)))"
assumes
― ‹We assume both $\mathit{HBL1}$ and $\mathit{HBL1\_rev}$, i.e., an iff version:›
HBL1_iff: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (PP ⟨φ⟩) ⟷ prv φ"
and
Compl_Pf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
isTrue (PPf n ⟨φ⟩) ⟶ bprv (PPf n ⟨φ⟩)"
begin

definition PPf where "PPf ≡ λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]"

lemma PP_deff: "PP t = subst P t xx" using PP_def by auto

lemma PP_PPf_eqv:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (eqv (PP ⟨φ⟩) (exi yy (PPf (Var yy) ⟨φ⟩)))"
using PP_deff PPf_def P_Pf by auto

(*  *)

lemma PPf[simp,intro!]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹ PPf t1 t2 ∈ fmla"
unfolding PPf_def by auto

lemma PPf_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹
PPf t1 t2 = subst (subst Pf t1 yy) t2 xx"
unfolding PPf_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma Fvars_PPf[simp]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹ Fvars (PPf t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: PPf_def2 subst2_fresh_switch)

lemma [simp]:
"n ∈ num ⟹ subst (PPf (Var yy) (Var xx)) n xx = PPf (Var yy) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf (Var yy) m) n yy = PPf n m"
"n ∈ num ⟹ subst (PPf (Var yy) (Var xx)) n yy = PPf n (Var xx)"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf m (Var xx)) n xx = PPf m n"
"m ∈ num ⟹ subst (PPf (Var zz) (Var xx')) m zz = PPf m (Var xx')"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf m (Var xx')) n xx' = PPf m n"
"n ∈ num ⟹ subst (PPf (Var zz) (Var xx')) n xx' = PPf (Var zz) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf (Var zz) n) m zz = PPf m n"
by (auto simp: PPf_def2 subst2_fresh_switch)

(* *)

lemma PP_PPf:
assumes "φ ∈ fmla" "Fvars φ = {}" shows "bprv (PP ⟨φ⟩) ⟷ bprv (exi yy (PPf (Var yy) ⟨φ⟩))"
using assms PP_PPf_eqv[OF assms] B.prv_eqv_sym[OF _ _ PP_PPf_eqv[OF assms]]
by (auto intro!: B.prv_eqv_prv[of "PP ⟨φ⟩" "exi yy (PPf (Var yy) ⟨φ⟩)"]
B.prv_eqv_prv[of "exi yy (PPf (Var yy) ⟨φ⟩)" "PP ⟨φ⟩"])

lemma isTrue_implies_bprv_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
isTrue (PPf n ⟨φ⟩) ⟹ bprv (PPf n ⟨φ⟩)"
using Compl_Pf by(simp add: PPf_def)

lemma isTrue_iff_bprv_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹ isTrue (PPf n ⟨φ⟩) ⟷ bprv (PPf n ⟨φ⟩)"
using isTrue_implies_bprv_PPf
using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto

text ‹Preparing to instantiate this "proof recovery" alternative into our
mainstream locale hierarchy, which assumes proofs.
We define the "missing" proofs to be numerals, we encode them as the identity,
and we "copy" @{term prfOf} from the corresponding predicate one-level-up, @{term PPf}:›

definition "proof" :: "'trm set" where [simp]: "proof = num"
definition prfOf :: "'trm ⇒ 'fmla ⇒ bool" where
"prfOf n φ ≡ bprv (PPf n ⟨φ⟩)"
definition encPf :: "'trm ⇒ 'trm" where [simp]: "encPf ≡ id"
(*  *)

lemma prv_exi_PPf_iff_isTrue:
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "bprv (exi yy (PPf (Var yy) ⟨φ⟩)) ⟷ isTrue (exi yy (PPf (Var yy) ⟨φ⟩))" (is "?L ⟷ ?R")
proof
assume ?L thus ?R by (intro B.sound_isTrue) auto
next
assume ?R
obtain n where n[simp]: "n ∈ num" and i: "isTrue (PPf n ⟨φ⟩)" using B.isTrue_exi[OF _ _ _ ‹?R›] by auto
hence "bprv (PPf n ⟨φ⟩)" by (auto simp: isTrue_iff_bprv_PPf)
thus ?L by (intro B.prv_exiI[of _ _ n]) auto
qed

lemma isTrue_exi_iff:
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "isTrue (exi yy (PPf (Var yy) ⟨φ⟩)) ⟷ (∃n∈num. isTrue (PPf n ⟨φ⟩))" (is "?L ⟷ ?R")
proof
assume ?L thus ?R using B.isTrue_exi[OF _ _ _ ‹?L›] by auto
next
assume ?R
then obtain n where n[simp]: "n ∈ num" and i: "isTrue (PPf n ⟨φ⟩)" by auto
hence "bprv (PPf n ⟨φ⟩)" by (auto simp: isTrue_iff_bprv_PPf)
hence "bprv (exi yy (PPf (Var yy) ⟨φ⟩))" by (intro B.prv_exiI[of _ _ n]) auto
thus ?L by (intro B.sound_isTrue) auto
qed

lemma prv_prfOf:
assumes "φ ∈ fmla" "Fvars φ = {}"
shows "prv φ ⟷ (∃n∈num. prfOf n φ)"
proof-
have "prv φ ⟷ bprv (PP ⟨φ⟩)" using HBL1_iff[OF assms] by simp
also have "… ⟷ bprv (exi yy (PPf (Var yy) ⟨φ⟩))" unfolding PP_PPf[OF assms] ..
also have "… ⟷ isTrue (exi yy (PPf (Var yy) ⟨φ⟩))" using prv_exi_PPf_iff_isTrue[OF assms] .
also have "… ⟷ (∃n∈num. isTrue (PPf n ⟨φ⟩))" using isTrue_exi_iff[OF assms] .
also have "… ⟷ (∃n∈num. bprv (PPf n ⟨φ⟩))" using isTrue_iff_bprv_PPf[OF _ assms] by auto
also have "… ⟷ (∃n∈num. prfOf n φ)" unfolding prfOf_def ..
finally show ?thesis .
qed

lemma prfOf_prv_Pf:
assumes "n ∈ num" and "φ ∈ fmla" "Fvars φ = {}" and "prfOf n φ"
shows "bprv (psubst Pf [(n, yy), (⟨φ⟩, xx)])"
using assms unfolding prfOf_def by (auto simp: PPf_def2 psubst_eq_rawpsubst2)

lemma isTrue_exi_iff_PP:
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "isTrue (PP ⟨φ⟩) ⟷ (∃n∈num. isTrue (PPf n ⟨φ⟩))"
proof-
have "bprv (eqv (PP ⟨φ⟩) (exi yy (PPf (Var yy) ⟨φ⟩)))"
using PP_PPf_eqv by auto
hence "bprv (imp (PP ⟨φ⟩) (exi yy (PPf (Var yy) ⟨φ⟩)))"
and "bprv (imp (exi yy (PPf (Var yy) ⟨φ⟩)) (PP ⟨φ⟩))"
by (simp_all add: B.prv_imp_eqvEL B.prv_imp_eqvER)
thus ?thesis unfolding isTrue_exi_iff[OF assms, symmetric]
by (intro iffI) (rule B.prv_imp_implies_isTrue; simp)+
qed

lemma bprv_compl_isTrue_PP_enc:
assumes 1: "φ ∈ fmla" "Fvars φ = {}" and 2: "isTrue (PP ⟨φ⟩)"
shows "bprv (PP ⟨φ⟩)"
proof-
obtain n where nn: "n ∈ num" and i: "isTrue (PPf n ⟨φ⟩)"
using 2 unfolding isTrue_exi_iff_PP[OF 1] ..
hence "bprv (PPf n ⟨φ⟩)"
using i using nn assms isTrue_iff_bprv_PPf by blast
hence "bprv (exi yy (PPf (Var yy) ⟨φ⟩))"
using 2 assms isTrue_exi_iff isTrue_exi_iff_PP prv_exi_PPf_iff_isTrue by auto
thus ?thesis using PP_PPf 1 by blast
qed

lemma TIP:
assumes 1: "φ ∈ fmla" "Fvars φ = {}" and 2: "isTrue (PP ⟨φ⟩)"
shows "prv φ"
using bprv_compl_isTrue_PP_enc[OF assms] HBL1_iff assms by blast

end ― ‹context @{locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf}›

locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
Minimal_Truth_Soundness_HBL1iff_Compl_Pf
+
assumes
Compl_NegPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
isTrue (B.neg (PPf n ⟨φ⟩)) ⟶ bprv (B.neg (PPf n ⟨φ⟩))"
begin

lemma isTrue_implies_prv_neg_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
isTrue (B.neg (PPf n ⟨φ⟩)) ⟹ bprv (B.neg (PPf n ⟨φ⟩))"
using Compl_NegPf by(simp add: PPf_def)

lemma isTrue_iff_prv_neg_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹ isTrue (B.neg (PPf n ⟨φ⟩)) ⟷ bprv (B.neg (PPf n ⟨φ⟩))"
using isTrue_implies_prv_neg_PPf
using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto

lemma prv_PPf_decide:
assumes [simp]: "n ∈ num" "φ ∈ fmla" "Fvars φ = {}"
and np: "¬ bprv (PPf n ⟨φ⟩)"
shows "bprv (B.neg (PPf n ⟨φ⟩))"
proof-
have "¬ isTrue (PPf n ⟨φ⟩)" using assms by (auto simp: isTrue_iff_bprv_PPf)
hence "isTrue (B.neg (PPf n ⟨φ⟩))" using B.isTrue_neg[of "PPf n ⟨φ⟩"] by auto
thus ?thesis by (auto simp: isTrue_iff_prv_neg_PPf)
qed

lemma not_prfOf_prv_neg_Pf:
assumes nφ: "n ∈ num" "φ ∈ fmla" "Fvars φ = {}" and "¬ prfOf n φ"
shows "bprv (B.neg (psubst Pf [(n, yy), (⟨φ⟩, xx)]))"
using assms prv_PPf_decide[OF nφ] by (auto simp: prfOf_def PPf_def2 psubst_eq_rawpsubst2)

end ― ‹context @{locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf}›

sublocale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
repr: CleanRepr_Proofs
(* added label to avoid duplicated constant P, which is assumed
in Minimal_Truth_Soundness_HBL1iff_Compl_Pf but defined in CleanRepr_Proofs
(they are of course extensionally equal).
*)
where "proof" = "proof" and prfOf = prfOf and encPf = encPf
by standard (auto simp: bprv_prv prv_prfOf prfOf_prv_Pf not_prfOf_prv_neg_Pf)

(* Lemma 6 ("proof recovery") from the JAR paper: *)
sublocale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
min_truth: Minimal_Truth_Soundness_Proof_Repr
where "proof" = "proof" and prfOf = prfOf and encPf = encPf
by standard

(* FOR THE CLASSICAL REASONING VERSION *)

locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf =
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
P
+
B: Minimal_Truth_Soundness
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
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 enc ("⟨_⟩")
and prv bprv
and P
and isTrue
+
fixes Pf :: 'fmla
assumes
(* Pf is a formula with free variables xx yy  *)
Pf[simp,intro!]: "Pf ∈ fmla"
and
Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
and
(* P relates to Pf internally just like a prv and a proofOf would
relate: via an existential *)
P_Pf:
"φ ∈ fmla ⟹
let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
bprv (eqv (subst P ⟨φ⟩ xx) (exi yy (PPf (Var yy) ⟨φ⟩)))"
assumes
(* We assume, in addition to HBL1, the strong form of HBL1_rev: *)
HBL1_rev_prv: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (PP ⟨φ⟩) ⟹ prv φ"
and
Compl_Pf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
isTrue (PPf n ⟨φ⟩) ⟶ bprv (PPf n ⟨φ⟩)"
begin

lemma HBL1_rev:
assumes f: "φ ∈ fmla" and fv: "Fvars φ = {}" and bp: "bprv (PP ⟨φ⟩)"
shows "prv φ"
using assms by (auto intro!: HBL1_rev_prv bprv_prv[OF _ _ bp])

lemma HBL1_iff: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (PP ⟨φ⟩) ⟷ prv φ"
using HBL1 HBL1_rev unfolding PP_def by auto

lemma HBL1_iff_prv: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (PP ⟨φ⟩) ⟷ prv φ"
by (intro iffI bprv_prv[OF _ _ HBL1_PP], elim HBL1_rev_prv[rotated -1]) auto

end ― ‹context @{locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf}›

sublocale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf <
mts_prv_mts: Minimal_Truth_Soundness_HBL1iff_Compl_Pf where Pf = Pf
using P_Pf HBL1_rev HBL1_PP Compl_Pf
by unfold_locales auto

locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical =
Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf
+
assumes
― ‹NB: we don't really need to assume classical reasoning (double negation) all throughout,
but only for the provability predicate:›
classical_P: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ let PP = (λt. subst P t xx) in
prv (B.neg (B.neg (PP ⟨φ⟩))) ⟹ prv (PP ⟨φ⟩)"
begin

lemma classical_PP: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (B.neg (B.neg (PP ⟨φ⟩))) ⟹ prv (PP ⟨φ⟩)"
using classical_P unfolding PP_def by auto

end ― ‹context @{locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical}›

(*<*)
end
(*>*)


# Theory Abstract_First_Goedel

chapter ‹Abstract Formulations of Gödel's First Incompleteness Theorem›

(*<*)
theory Abstract_First_Goedel imports Goedel_Formula Standard_Model_More
begin
(*>*)

section ‹Proof-Theoretic Versions of Gödel's First›

context Goedel_Form
begin

subsection ‹The easy half›

text ‹First the "direct", positive formulation:›
lemma goedel_first_theEasyHalf_pos:
assumes "prv φG"   shows "prv fls"
proof-
have "prv (neg (PP ⟨φG⟩))" using prv_eqv_prv[OF _ _ assms prv_φG_eqv] by auto
moreover
{have "bprv (PP ⟨φG⟩)" using HBL1[OF φG Fvars_φG assms] unfolding PP_def .
from bprv_prv[OF _ _ this, simplified] have "prv (PP ⟨φG⟩)" .
}
ultimately show ?thesis using PP prv_neg_fls by (meson φG enc in_num)
qed

text ‹... then the more standard contrapositive formulation:›
corollary goedel_first_theEasyHalf:
"consistent ⟹ ¬ prv φG"
using goedel_first_theEasyHalf_pos unfolding consistent_def by auto

end ― ‹context @{locale Goedel_Form}›

subsection ‹The hard half›

text ‹The hard half needs explicit proofs:›
context Goedel_Form_Proofs begin

lemma goedel_first_theHardHalf:
assumes oc: "ωconsistent"
shows "¬ prv (neg φG)"
proof
assume pn: "prv (neg φG)"
hence pnn: "prv (neg (neg (wrepr.PP ⟨φG⟩)))"
using prv_eqv_imp_transi num wrepr.PP φG fls neg neg_def prv_φG_eqv prv_eqv_sym
by (metis (full_types) enc in_num)
note c = ωconsistent_implies_consistent[OF oc]
have np: "¬ prv φG" using pn c unfolding consistent_def3 by blast
have "∀p ∈ num. bprv (neg (PPf p ⟨φG⟩))" using not_prv_prv_neg_PPf[OF _ _ np] by auto
hence 0: "∀p ∈ num. prv (neg (PPf p ⟨φG⟩))" using not_prv_prv_neg_PPf[OF _ _ np]
by (fastforce intro: bprv_prv)
have "¬ prv (neg (neg (exi yy (PPf (Var yy) ⟨φG⟩))))" using 0 oc unfolding ωconsistent_def by auto
hence "¬ prv (neg (neg (wrepr.PP ⟨φG⟩)))"
unfolding wrepr.PP_def by (subst P_def) (simp add:  PPf_def2)
thus False using pnn by auto
qed

theorem goedel_first:
assumes "ωconsistent"
shows "¬ prv φG ∧ ¬ prv (neg φG)"
using assms goedel_first_theEasyHalf goedel_first_theHardHalf ωconsistent_implies_consistent by blast

theorem goedel_first_ex:
assumes "ωconsistent"
shows "∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ)"
using assms goedel_first by (intro exI[of _ φG]) blast

end ― ‹context @{locale Goedel_Form_Proofs}›

section ‹Model-Theoretic Versions of Gödel's First›

text ‹The model-theoretic twist is that of additionally proving
the truth of Gödel sentences.›

subsection ‹First model-theoretic version›

locale Goedel_Form_Proofs_Minimal_Truth =
Goedel_Form_Proofs
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
fls
prv bprv
enc
S
dsj
"proof" prfOf encPf
Pf
+
Minimal_Truth_Soundness
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
isTrue
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 bprv
and enc ("⟨_⟩")
and S
and "proof" :: "'proof set" and prfOf encPf
and Pf
and isTrue
begin

text ‹Recall that "consistent" and "$\omega$-consistent" refer to @{term prv}, not to @{term bprv}.›

theorem isTrue_φG:
assumes "consistent"
shows "isTrue φG"
proof-
have "∀ n ∈ num. bprv (neg (PPf n ⟨φG⟩))"
using not_prv_prv_neg_PPf[OF _ _ goedel_first_theEasyHalf[OF assms]] by auto
hence "∀ n ∈ num. isTrue (neg (PPf n ⟨φG⟩))" by (auto intro: sound_isTrue)
hence "isTrue (all yy (neg (PPf (Var yy) ⟨φG⟩)))" by (auto intro: isTrue_all)
moreover have "isTrue (imp (all yy (neg (PPf (Var yy) ⟨φG⟩))) φG)"
using bprv_eqv_all_not_PPf_imp_φG by (auto intro!: sound_isTrue)
ultimately show ?thesis by (rule isTrue_imp[rotated -2]) auto
qed

text ‹The "strong" form of Gödel's First (also asserting the truth of
the Gödel sentences):›

theorem goedel_first_strong:
"ωconsistent ⟹ ¬ prv φG ∧ ¬ prv (neg φG) ∧ isTrue φG"
using goedel_first isTrue_φG ωconsistent_implies_consistent by blast

theorem goedel_first_strong_ex:
"ωconsistent ⟹ ∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ) ∧ isTrue φ"
using goedel_first_strong by (intro exI[of _ φG]) blast

end ― ‹context @{locale Goedel_Form_Proofs_Minimal_Truth}›

subsection ‹Second model-theoretic version›

locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
Goedel_Form
var trm fmla Var num
FvarsT substT Fvars subst
eql cnj imp all exi
fls
prv bprv
enc
S
P
+
Minimal_Truth_Soundness_HBL1iff_Compl_Pf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
enc
prv bprv
P
isTrue
Pf
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 bprv
and enc ("⟨_⟩")
and S
and isTrue
and P
and Pf

locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
enc
S
isTrue
P
Pf
+
Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
enc
prv bprv
P
isTrue
Pf
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 bprv
and enc ("⟨_⟩")
and S
and isTrue
and P
and Pf
+
assumes prv_ωconsistent: "ωconsistent"

(* Semantic Goedel's first, Goedel-style, second variant
... established as a sublocale statement *)
sublocale
Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
recover_proofs: Goedel_Form_Proofs_Minimal_Truth
where prfOf = prfOf and "proof" = "proof" and encPf = encPf
and prv = prv and bprv = bprv
by standard

(* ... and here is the explicit statement, inside the locale that
provides all the assumptions *)
context Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf begin
thm recover_proofs.goedel_first_strong

end

section ‹Classical-Logic Versions of Gödel's First›

subsection ‹First classical-logic version›

locale Goedel_Form_Classical_HBL1_rev_prv =
Goedel_Form
var trm fmla Var num FvarsT substT Fvars subst
eql cnj imp all exi
fls
prv bprv
enc
S
P
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
+
assumes
― ‹NB: we don't really need to assume classical reasoning (double negation)
for all formulas, but only for the provability predicate:›
classical_P_prv: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ let PP = (λt. subst P t xx) in
prv (neg (neg (PP ⟨φ⟩))) ⟹ prv (PP ⟨φ⟩)"
and
HBL1_rev_prv: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (PP ⟨φ⟩) ⟹ prv φ"
begin

lemma HBL1_rev:
assumes f: "φ ∈ fmla" and fv: "Fvars φ = {}" and bp: "bprv (PP ⟨φ⟩)"
shows "prv φ"
using assms by (auto intro!: HBL1_rev_prv bprv_prv[OF _ _ bp])

lemma classical_PP_prv: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (neg (neg (PP ⟨φ⟩))) ⟹ prv (PP ⟨φ⟩)"
using classical_P_prv unfolding PP_def by auto

lemma HBL1_iff: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (PP ⟨φ⟩) ⟷ prv φ"
using HBL1 HBL1_rev unfolding PP_def by auto

lemma HBL1_iff_prv: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (PP ⟨φ⟩) ⟷ prv φ"
by (meson HBL1_PP HBL1_rev_prv PP d_dwf.bprv_prv' enc in_num)

lemma goedel_first_theHardHalf_pos:
assumes "prv (neg φG)"   shows "prv fls"
proof-
have "prv (neg (neg (PP ⟨φG⟩)))"
using assms neg_def prv_φG_eqv prv_eqv_imp_transi_rev by fastforce
hence "prv (PP ⟨φG⟩)" using classical_PP_prv by auto
hence "prv φG" using Fvars_φG HBL1_rev_prv by blast
thus ?thesis using assms prv_neg_fls by blast
qed

corollary goedel_first_theHardHalf:
"consistent ⟹ ¬ prv (neg φG)"
using goedel_first_theHardHalf_pos unfolding consistent_def by auto

theorem goedel_first_classic:
assumes "consistent"
shows "¬ prv φG ∧ ¬ prv (neg φG)"
using assms goedel_first_theEasyHalf goedel_first_theHardHalf by blast

theorem goedel_first_classic_ex:
assumes "consistent"
shows "∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ)"
using assms goedel_first_classic by (intro exI[of _ φG]) blast

end ― ‹context @{locale Goedel_Form_Classical_HBL1_rev_prv}›

subsection ‹Second classical-logic version›

locale Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP =
Goedel_Form_Classical_HBL1_rev_prv
var trm fmla Var num FvarsT substT Fvars subst
eql cnj imp all exi
fls
prv bprv
enc
S
P
+
Minimal_Truth_Soundness
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
isTrue
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var num FvarsT substT Fvars subst
and eql cnj dsj imp all exi
and fls
and prv bprv
and enc ("⟨_⟩")
and S
and P
and isTrue
+
assumes
―‹Truth of @{term φ} implies provability (TIP) of (the internal representation of) @{term φ}›
TIP: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹
let PP = (λt. subst P t xx) in
isTrue (PP ⟨φ⟩) ⟹ prv φ"
begin

lemma TIP_PP: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ isTrue (PP ⟨φ⟩) ⟹ prv φ"
using TIP unfolding PP_def by auto

theorem isTrue_φG:
assumes consistent
shows "isTrue φG"
proof-
{assume "¬ isTrue φG"
hence 1: "isTrue (neg φG)" using isTrue_neg by fastforce
have "bprv (imp (neg φG) (neg (neg (PP ⟨φG⟩))))"
by (auto simp add: bprv_φG_eqv B.prv_imp_eqvER B.prv_imp_neg_rev)
from prv_imp_implies_isTrue[OF _ _ _ _ this 1, simplified]
have "isTrue (neg (neg (PP ⟨φG⟩)))" .
from isTrue_neg_neg[OF _ _ this, simplified] have "isTrue (PP ⟨φG⟩)" .
hence "prv φG" using assms TIP_PP by auto
hence False using goedel_first_classic assms by auto
}
thus ?thesis by auto
qed

theorem goedel_first_classic_strong: "consistent ⟹ ¬ prv φG ∧ ¬ prv (neg φG) ∧ isTrue φG"
using goedel_first_classic isTrue_φG by simp

theorem goedel_first_classic_strong_ex:
"consistent ⟹ ∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ) ∧ isTrue φ"
using goedel_first_classic_strong by (intro exI[of _ φG]) blast

end ― ‹context @{locale Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP}›

subsection ‹Third classical-logic version›

locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical =
Goedel_Form
var trm fmla Var num FvarsT substT Fvars subst
eql cnj imp all exi
fls
prv bprv
enc
S
P
+
Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
enc
prv bprv
P
isTrue
Pf
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 bprv
and enc ("⟨_⟩")
and S
and isTrue
and P
and Pf

sublocale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical <
recover_proofs: Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP where prv = prv and bprv = bprv
proof (standard, goal_cases classical rev_rpv TIPf)
case (classical φ)
then show ?case using HBL1_iff classical_P by (simp add: mts_prv_mts.PP_deff)
next
case (rev_rpv φ)
then show ?case using HBL1_iff_prv PP_def by simp
next
case (TIPf φ)
then show ?case using classical_P by (simp add: SS_def PP_def mts_prv_mts.TIP)
qed

context Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical begin
thm recover_proofs.goedel_first_classic_strong
end ―‹context @{locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical}›

(*<*)
end
(*>*)


# Theory Rosser_Formula

chapter ‹Rosser Formulas›

text ‹The Rosser formula is a modification of the Gödel formula that
is undecidable assuming consistency only (not $\omega$-consistency).›

(*<*)
theory Rosser_Formula
imports Diagonalization Goedel_Formula
begin
(*>*)

locale Rosser_Form =
Deduct2_with_PseudoOrder
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
Lq
+
Repr_Neg
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv bprv
enc
N
+
Repr_SelfSubst
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
S
+
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
P
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and fls
and prv bprv
and Lq
and dsj
and enc ("⟨_⟩")
and N S P

locale Rosser_Form_Proofs =
Deduct2_with_PseudoOrder
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
Lq
+
Repr_Neg
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv bprv
enc
N
+
Repr_SelfSubst
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
S
+
CleanRepr_Proofs
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
fls
dsj
"proof" prfOf
encPf
Pf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and fls
and prv bprv
and Lq
and dsj and "proof" :: "'proof set" and prfOf
and enc ("⟨_⟩")
and N
and S
and encPf Pf

context Rosser_Form_Proofs
begin

definition R where "R = all zz (imp (LLq (Var zz) (Var yy))
(all xx' (imp (NN (Var xx) (Var xx'))
(neg (PPf (Var zz) (Var xx'))))))"

definition RR where "RR t1 t2 = psubst R [(t1,yy), (t2,xx)]"

lemma R[simp,intro!]: "R ∈ fmla" unfolding R_def by auto

lemma RR_def2:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹ RR t1 t2 = subst (subst R t1 yy) t2 xx"
unfolding RR_def by (rule psubst_eq_rawpsubst2[simplified]) auto

definition P' where "P' = exi yy (cnj (PPf (Var yy) (Var xx)) (RR (Var yy) (Var xx)))"

definition PP' where "PP' t = subst P' t xx"

lemma Fvars_R[simp]: "Fvars R = {xx,yy}" unfolding R_def by auto

lemma [simp]: "Fvars (RR (Var yy) (Var xx)) = {yy,xx}" by (auto simp: RR_def2)

lemma P'[simp,intro!]: "P' ∈ fmla" unfolding P'_def by (auto simp: PPf_def2 RR_def2)

lemma Fvars_P'[simp]: "Fvars P' = {xx}" unfolding P'_def by (auto simp: PPf_def2 RR_def2)

lemma PP'[simp,intro!]: "t ∈ trm ⟹ PP' t ∈ fmla"
unfolding PP'_def by auto

lemma RR[simp,intro]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ RR t1 t2 ∈ fmla"
by (auto simp: RR_def)

lemma RR_simps[simp]:
"n ∈ num ⟹ subst (RR (Var yy) (Var xx)) n xx = RR (Var yy) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (RR (Var yy) m) n yy = RR n m"
by (simp add: RR_def2 subst2_fresh_switch)+

text ‹The Rosser modification of the Gödel formula›
definition φR :: 'fmla where "φR ≡ diag (neg P')"

lemma φR[simp,intro!]: "φR ∈ fmla" and Fvars_φR[simp]: "Fvars φR = {}"
unfolding φR_def wrepr.PP_def by auto

lemma bprv_φR_eqv:
"bprv (eqv φR (neg (PP' ⟨φR⟩)))"
unfolding φR_def PP'_def using bprv_diag_eqv[of "neg P'"] by simp

lemma bprv_imp_φR:
"bprv (imp (neg (PP' ⟨φR⟩)) φR)"
by (rule B.prv_imp_eqvER) (auto intro: bprv_φR_eqv)

lemma prv_φR_eqv:
"prv (eqv φR (neg (PP' ⟨φR⟩)))"
using dwf_dwfd.d_dwf.bprv_prv'[OF _ bprv_φR_eqv, simplified] .

lemma prv_imp_φR:
"prv (imp (neg (PP' ⟨φR⟩)) φR)"
by (rule prv_imp_eqvER) (auto intro: prv_φR_eqv)

end ― ‹context @{locale Rosser_Form}›

sublocale Rosser_Form_Proofs < Rosser_Form where P = P
by standard

sublocale Rosser_Form_Proofs < Goedel_Form where P = P
by standard

(*<*)
end
(*>*)


# Theory Abstract_First_Goedel_Rosser

chapter ‹Abstract Formulations of Gödel-Rosser's First Incompleteness Theorem›

(*<*)
theory Abstract_First_Goedel_Rosser
imports Rosser_Formula Standard_Model_More
begin
(*>*)

text ‹The development here is very similar to that of Gödel First Incompleteness Theorem.
It lacks classical logical variants, since for them Rosser's trick does bring
any extra value.›

section ‹Proof-Theoretic Versions›

context Rosser_Form_Proofs
begin

lemma NN_neg_unique_xx':
assumes [simp]:"φ ∈ fmla" "Fvars φ = {}"
shows
"bprv (imp (NN ⟨φ⟩ (Var xx'))
(eql ⟨neg φ⟩ (Var xx')))"
using B.prv_subst[of yy _ "Var xx'", OF _ _ _ NN_neg_unique[OF assms]] by fastforce

lemma NN_imp_xx':
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}" "χ ∈ fmla"
shows "bprv (imp (subst χ ⟨neg φ⟩ xx')
(all xx' (imp (NN ⟨φ⟩ (Var xx')) χ)))"
proof-
have 2: "bprv (imp (eql ⟨neg φ⟩ (Var xx')) (imp (subst χ ⟨neg φ⟩ xx') χ))"
using B.prv_eql_subst_trm[of xx' χ "⟨neg φ⟩" "Var xx'", simplified] .
have 1: "bprv (imp (subst χ ⟨neg φ⟩ xx') (imp (eql ⟨neg φ⟩ (Var xx')) χ))"
by (simp add: "2" B.prv_imp_com)
have 0: "bprv (imp (subst χ ⟨neg φ⟩ xx') (imp (NN ⟨φ⟩ (Var xx')) χ))"
using 1
by (elim B.prv_prv_imp_trans[rotated 3])
(auto simp add: B.prv_imp_com B.prv_imp_monoR NN_neg_unique_xx')
show ?thesis by (rule B.prv_all_imp_gen) (auto simp: 0)
qed

lemma goedel_rosser_first_theEasyHalf:
assumes c: "consistent"
shows "¬ prv φR"
proof
assume 0: "prv φR"
then obtain "prf" where [simp]: "prf ∈ proof" and "prfOf prf φR" using prv_prfOf by auto
hence 00: "bprv (PPf (encPf prf) ⟨φR⟩)" using prfOf_PPf by auto
from dwf_dwfd.d_dwf.bprv_prv'[OF _ 00, simplified] have b00: "prv (PPf (encPf prf) ⟨φR⟩)" .
have "¬ prv (neg φR)" using 0 c unfolding consistent_def3 by auto
hence "∀ prf ∈ proof.  ¬ prfOf prf (neg φR)" using 00 prv_prfOf by auto
hence "bprv (neg (PPf p ⟨neg φR⟩))" if "p ∈ num" for p using not_prfOf_PPf Clean_PPf_encPf that
by (cases "p ∈ encPf  proof") auto
hence 1: "prv (all zz (imp (LLq (Var zz) (encPf prf)) (neg (PPf (Var zz) ⟨neg φR⟩))))"
(* here use locale assumption about the order-like relation: *)
by (intro LLq_num) auto
have 11: "prv (RR (encPf prf) ⟨φR⟩)"
using NN_imp_xx'[of φR "neg (PPf (Var zz) (Var xx'))", simplified]
by (auto simp add: RR_def2 R_def
intro!: prv_all_congW[OF _ _ _ _ 1] prv_imp_monoL[OF _ _ _ dwf_dwfd.d_dwf.bprv_prv'])
have 3: "prv (cnj (PPf (encPf prf) ⟨φR⟩) (RR (encPf prf) ⟨φR⟩))"
by (rule prv_cnjI[OF _ _ b00 11]) auto
have "prv ((PP' ⟨φR⟩))" unfolding PP'_def P'_def
using 3 by (auto intro: prv_exiI[of _ _ "encPf prf"])
moreover have "prv (neg (PP' ⟨φR⟩))"
using prv_eqv_prv[OF _ _ 0 prv_φR_eqv] by auto
ultimately show False using c unfolding consistent_def3 by auto
qed

lemma goedel_rosser_first_theHardHalf:
assumes c: "consistent"
shows "¬ prv (neg φR)"
proof
assume 0: "prv (neg φR)"
then obtain "prf" where [simp,intro!]: "prf ∈ proof" and pr: "prfOf prf (neg φR)" using prv_prfOf by auto
define p where p: "p = encPf prf"
have [simp,intro!]: "p ∈ num" unfolding p by auto
have 11: "bprv (PPf p ⟨neg φR⟩)" using pr prfOf_PPf unfolding p by auto
have 1: "bprv (NN ⟨φR⟩ ⟨neg φR⟩)" using NN_neg by simp

have "¬ prv φR" using 0 c unfolding consistent_def3 by auto
from not_prv_prv_neg_PPf[OF _ _ this]
have b2: "∀ r ∈ num. bprv (neg (PPf r ⟨φR⟩))" by auto
hence 2: "∀ r ∈ num. prv (neg (PPf r ⟨φR⟩))"
by (auto intro: dwf_dwfd.d_dwf.bprv_prv')

obtain P where P[simp,intro!]: "P ⊆num" "finite P"
and 3: "prv (dsj (sdsj {eql (Var yy) r |r. r ∈ P}) (LLq p (Var yy)))"
(* here use the other locale assumption about the order-like relation: *)
using LLq_num2 by auto

have "prv (imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls)"
proof(rule prv_dsj_cases[OF _ _ _ 3])
{fix r assume r: "r ∈ P" hence rn[simp]: "r ∈ num" using P(1) by blast
have "prv (imp (cnj (PPf r ⟨φR⟩) (RR r ⟨φR⟩)) fls)"
using 2 unfolding neg_def
by (metis FvarsT_num PPf RR rn φR all_not_in_conv cnj enc fls imp in_num prv_imp_cnj3L prv_imp_mp)
hence "prv (imp (eql (Var yy) r)
(imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls))"
using prv_eql_subst_trm_id[of yy "cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)" r,simplified]
unfolding neg_def[symmetric]
by (intro prv_neg_imp_imp_trans) auto
}
thus "prv (imp (sdsj {eql (Var yy) r |r. r ∈ P})
(imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls))"
using Var P(1) eql by (intro prv_sdsj_imp) (auto 0 0 simp: set_rev_mp)
next
let ?φ = "all xx' (imp (NN ⟨φR⟩ (Var xx')) (neg (PPf p (Var xx'))))"
have "bprv (neg ?φ)"
using 1 11 by (intro B.prv_imp_neg_allWI[where t = "⟨neg φR⟩"]) (auto intro: B.prv_prv_neg_imp_neg)
hence "prv (neg ?φ)" by (auto intro: dwf_dwfd.d_dwf.bprv_prv')
hence 00: "prv (imp (LLq p (Var yy))
(imp (imp (LLq p (Var yy)) ?φ) fls))"
unfolding neg_def[symmetric] by (intro prv_imp_neg_imp_neg_imp) auto
have "prv (imp (LLq p (Var yy))
(imp (RR (Var yy) ⟨φR⟩) fls))"
unfolding neg_def[symmetric] using 00[folded neg_def]
by (auto simp add: RR_def2 R_def intro!: prv_imp_neg_allI[where t = p])
thus "prv (imp (LLq p (Var yy))
(imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls))"
unfolding neg_def[symmetric] by (intro prv_imp_neg_imp_cnjR) auto
qed(auto, insert Var P(1) eql, simp_all add: set_rev_mp)
hence "prv (neg (exi yy (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩))))"
unfolding neg_def[symmetric] by (intro prv_neg_neg_exi) auto
hence "prv (neg (PP' ⟨φR⟩))" unfolding PP'_def P'_def by simp
hence "prv φR" using prv_φR_eqv by (meson PP' φR enc in_num neg prv_eqv_prv_rev)
with ‹¬ prv φR› show False using c unfolding consistent_def3 by auto
qed

theorem goedel_rosser_first:
assumes "consistent"
shows "¬ prv φR ∧ ¬ prv (neg φR)"
using assms goedel_rosser_first_theEasyHalf goedel_rosser_first_theHardHalf by blast

theorem goedel_rosser_first_ex:
assumes "consistent"
shows "∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ)"
using assms goedel_rosser_first by (intro exI[of _ φR]) blast

end ― ‹context @{locale Rosser_Form}›

section ‹Model-Theoretic Versions›

subsection ‹First model-theoretic version›

locale Rosser_Form_Proofs_Minimal_Truth =
Rosser_Form_Proofs
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
fls
prv bprv
Lq
dsj
"proof" prfOf
enc
N S
encPf
Pf
+
Minimal_Truth_Soundness
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
isTrue
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 Lq
and prv bprv
and enc ("⟨_⟩")
and N S P
and "proof" :: "'proof set" and prfOf encPf
and Pf
and isTrue
begin

lemma Fvars_PP'[simp]: "Fvars (PP' ⟨φR⟩) = {}" unfolding PP'_def
by (subst Fvars_subst) auto

lemma Fvars_RR'[simp]: "Fvars (RR (Var yy) ⟨φR⟩) = {yy}"
unfolding RR_def
by (subst Fvars_psubst) (fastforce intro!: exI[of _ "{yy}"])+

lemma isTrue_PPf_implies_φR:
assumes "isTrue (all yy (neg (PPf (Var yy) ⟨φR⟩)))"
(is "isTrue ?H")
shows "isTrue φR"
proof-
define F where "F ≡ RR (Var yy) ⟨φR⟩"
have [simp]: "F ∈ fmla" "Fvars F = {yy}"
unfolding F_def by auto
have [simp]: "exi yy (PPf (Var yy) ⟨φR⟩) ∈ fmla"
unfolding PPf_def by auto

have 1: "bprv
(imp (all yy (neg (PPf (Var yy) ⟨φR⟩)))
(neg (exi yy (PPf (Var yy) ⟨φR⟩))))"
(is "bprv (imp (all yy (neg ?G)) (neg (exi yy ?G)))")
using B.prv_all_neg_imp_neg_exi[of yy ?G] by auto
have 2: "bprv (imp (neg (exi yy ?G)) (neg (exi yy (cnj ?G F))))"
by (auto intro!: B.prv_imp_neg_rev B.prv_exi_cong B.prv_imp_cnjL)
have "bprv (imp (all yy (neg ?G)) (neg (exi yy (cnj ?G F))))"
using B.prv_prv_imp_trans[OF _ _ _  1 2] by simp
hence "bprv (imp ?H (neg (PP' ⟨φR⟩)))"
unfolding PP'_def P'_def
by (simp add: F_def)
from B.prv_prv_imp_trans[OF _ _ _  this bprv_imp_φR]
have "bprv (imp ?H φR)" by auto
from prv_imp_implies_isTrue[OF _ _ _ _ this assms, simplified]
show ?thesis .
qed

theorem isTrue_φR:
assumes "consistent"
shows "isTrue φR"
proof-
have "∀ n ∈ num. bprv (neg (PPf n ⟨φR⟩))"
using not_prv_prv_neg_PPf[OF _ _ goedel_rosser_first_theEasyHalf[OF assms]]
by auto
hence "∀ n ∈ num. isTrue (neg (PPf n ⟨φR⟩))" by (auto intro: sound_isTrue)
hence "isTrue (all yy (neg (PPf (Var yy) ⟨φR⟩)))" by (auto intro: isTrue_all)
thus ?thesis using isTrue_PPf_implies_φR by auto
qed

theorem goedel_rosser_first_strong: "consistent ⟹ ¬ prv φR ∧ ¬ prv (neg φR) ∧ isTrue φR"
using isTrue_φR goedel_rosser_first by blast

theorem goedel_rosser_first_strong_ex:
"consistent ⟹ ∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ) ∧ isTrue φ"
using goedel_rosser_first_strong by (intro exI[of _ φR]) blast

end ― ‹context @{locale Rosser_Form_Proofs_Minimal_Truth}›

subsection ‹Second model-theoretic version›

context Rosser_Form
begin
print_context
end

locale Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
Rosser_Form
var trm fmla Var
FvarsT substT Fvars subst
num
eql cnj imp all exi
fls
prv bprv
Lq
dsj
enc
N
S
P
+
Minimal_Truth_Soundness_HBL1iff_Compl_Pf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
enc
prv bprv
P
isTrue
Pf
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 bprv
and Lq
and enc ("⟨_⟩")
and N S
and isTrue
and P Pf

locale Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
Lq
enc
N S
isTrue
P
Pf
+
M : Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
enc
prv bprv
N
isTrue
Pf
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 bprv
and Lq
and enc ("⟨_⟩")
and N S P
and isTrue
and Pf

sublocale
Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
recover_proofs: Rosser_Form_Proofs_Minimal_Truth
where prfOf = prfOf and "proof" = "proof" and encPf = encPf
and prv = prv and bprv = bprv
by standard

context Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
begin
thm recover_proofs.goedel_rosser_first_strong
end

(*<*)
end
(*>*)



# Theory Abstract_Second_Goedel

chapter ‹Abstract Formulation of Gödel's Second Incompleteness Theorem›

(*<*)
theory Abstract_Second_Goedel imports Abstract_First_Goedel Derivability_Conditions
begin
(*>*)

text ‹We assume all three derivability conditions, and assumptions
behind Gödel formulas:›
locale Goedel_Second_Assumptions =
HBL1_2_3
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
P
+
Goedel_Form
var trm fmla Var num FvarsT substT Fvars subst
eql cnj imp all exi
fls
prv bprv
enc
S
P
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("⟨_⟩")
and S
and P
and fls
begin

lemma P_G:
"bprv (imp (PP ⟨φG⟩) (PP ⟨fls⟩))"
proof-
have 0: "prv (imp φG (neg (PP ⟨φG⟩)))"
using prv_φG_eqv by (intro prv_imp_eqvEL) auto
have 1: "bprv (PP ⟨imp φG (neg (PP ⟨φG⟩))⟩)"
using HBL1_PP[OF _ _ 0] by simp
have 2: "bprv (imp (PP ⟨φG⟩) (PP ⟨neg (PP ⟨φG⟩)⟩))"
using HBL2_imp2[OF _ _  _ _ 1] by simp
have 3: "bprv (imp (PP ⟨φG⟩) (PP ⟨PP ⟨φG⟩⟩))"
using HBL3[OF φG] by simp
have 23: "bprv (imp (PP ⟨φG⟩)
(cnj (PP ⟨PP ⟨φG⟩⟩)
(PP ⟨neg (PP ⟨φG⟩)⟩)))"
using B.prv_imp_cnj[OF _ _ _ 3 2] by simp
have 4: "bprv (imp (cnj (PP ⟨PP ⟨φG⟩⟩)
(PP ⟨neg (PP ⟨φG⟩)⟩))
(PP ⟨fls⟩))"
using HBL2[of "PP ⟨φG⟩" fls] unfolding neg_def[symmetric] by simp
show ?thesis using B.prv_prv_imp_trans[OF _ _ _ 23 4] by simp
qed

text ‹First the "direct", positive formulation:›
lemma goedel_second_pos:
assumes "prv (neg (PP ⟨fls⟩))"
shows "prv fls"
proof-
note PG = bprv_prv[OF _ _ P_G, simplified]
have "prv (neg (PP ⟨φG⟩))"
using PG assms unfolding neg_def by (rule prv_prv_imp_trans[rotated 3]) auto
hence "prv φG" using prv_φG_eqv by (rule prv_eqv_prv_rev[rotated 2]) auto
thus ?thesis
―‹The only part of Goedel's first theorem that is needed:›
using goedel_first_theEasyHalf_pos by simp
qed

text ‹Then the more standard, counterpositive formulation:›
theorem goedel_second:
"consistent ⟹ ¬ prv (neg (PP ⟨fls⟩))"
using goedel_second_pos unfolding consistent_def by auto

text ‹It is an immediate consequence of Gödel's Second HLB1, HLB2 that
(assuming consistency)  @{term "prv (neg (PP ⟨φ⟩))"} holds for no sentence, be it
provable or not. The theory is omniscient about what it can prove
(thanks to HLB1), but completely ignorant about what it cannot prove.›

corollary not_prv_neg_PP:
assumes c: "consistent" and [simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "¬ prv (neg (PP ⟨φ⟩))"
proof
assume 0: "prv (neg (PP ⟨φ⟩))"
have "prv (imp fls φ)" by simp
hence "bprv (PP ⟨imp fls φ⟩)" by (intro HBL1_PP) auto
hence "bprv (imp (PP ⟨fls⟩) (PP ⟨φ⟩))" by (intro HBL2_imp2) auto
hence "bprv (imp (neg (PP ⟨φ⟩)) (neg (PP ⟨fls⟩)))" by (intro B.prv_imp_neg_rev) auto
from prv_imp_mp[OF _ _ bprv_prv[OF _ _ this, simplified] 0, simplified]
have "prv (neg (PP ⟨fls⟩))" .
thus False using goedel_second[OF c] by simp
qed

end ― ‹context @{locale Goedel_Second_Assumptions}›

(*<*)
end
(*>*)



# Theory Abstract_Jeroslow_Encoding

chapter ‹Jeroslow's Variant of G\"odel's Second Incompleteness Theorem›

(*<*)
theory Abstract_Jeroslow_Encoding imports
"Syntax_Independent_Logic.Deduction"
begin
(*>*)

section ‹Encodings and Derivability›

text ‹Here we formalize some of the assumptions of Jeroslow's theorem:
encoding, term-encoding and the First Derivability Condition.›

subsection ‹Encoding of formulas›

locale Encode =
Syntax_with_Numerals
var trm fmla Var FvarsT substT Fvars subst
num
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
+
fixes
(*************************************)
(* Numeric formulas are assumed to be encoded as numerals: *)
enc :: "'fmla ⇒ 'trm" ("⟨_⟩")
assumes
enc[simp,intro!]: "⋀ φ. φ ∈ fmla ⟹ enc φ ∈ num"
begin

end ― ‹context @{locale Encode}›

subsection ‹Encoding of computable functions›

text ‹Jeroslow assumes the encodability of an abstract (unspecified) class of
computable functions and the assumption that a particular function, @{term "sub φ"} for each formula
@{term φ}, is in this collection. This is used to prove a different flavor of the diagonalization
lemma (Jeroslow 1973). It turns out that only an encoding of unary computable functions
is needed, so we only assume that.›

locale Encode_UComput =
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and enc ("⟨_⟩")
+
― ‹Abstract (unspeficied) notion of unary "computable" function
between numerals, which are encoded as numerals. They
contain a special substitution-like function @{term "sub φ"} for each formula @{term "φ"}.›
fixes ucfunc :: "('trm ⇒ 'trm) set"
and encF :: "('trm ⇒ 'trm) ⇒ 'trm"
and sub :: "'fmla ⇒ 'trm ⇒ 'trm"
assumes
― ‹NB: Due to the limitations of the type system, we define @{term "ufunc"} as a set of functions
between terms, but we only care about their actions on numerals ...
so we assume they send numerals to numerals:›
ucfunc[simp,intro!]: "⋀ f n. f ∈ ucfunc ⟹ n ∈ num ⟹ f n ∈ num"
and
encF[simp,intro!]: "⋀ f. f ∈ ucfunc ⟹ encF f ∈ num"
and
sub[simp]: "⋀φ. φ ∈ fmla ⟹ sub φ ∈ ucfunc"
and
― ‹The function @{term "sub φ"} takes any encoding of a function @{term "f"} and returns the encoding of
the formula obtained by substituting for @{term "xx"} the value of @{term "f"} applied to its own encoding:›
sub_enc:
"⋀ φ f. φ ∈ fmla ⟹ Fvars φ = {xx} ⟹ f ∈ ucfunc ⟹
sub φ (encF f) = enc (inst φ (f (encF f)))"

subsection ‹Term-encoding of computable functons›

text ‹For handling the notion of term-representation (which we introduce later),
we assume we are given a set @{term "Ops"} of term operators and their encodings as numerals.
We additionally assume that the term operators behave well w.r.t. free variables and
substitution.›

locale TermEncode =
Syntax_with_Numerals
var trm fmla Var FvarsT substT Fvars subst
num
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
+
fixes
Ops ::  "('trm ⇒ 'trm) set"
and
enc :: "('trm ⇒ 'trm) ⇒ 'trm" ("⟨_⟩")
assumes
Ops[simp,intro!]: "⋀f t. f ∈ Ops ⟹ t ∈ trm ⟹ f t ∈ trm"
and
enc[simp,intro!]: "⋀ f. f ∈ Ops ⟹ enc f ∈ num"
and
Ops_FvarsT[simp]: "⋀ f t. f ∈ Ops ⟹ t ∈ trm ⟹ FvarsT (f t) = FvarsT t"
and
Ops_substT[simp]: "⋀ f t. f ∈ Ops ⟹ t ∈ trm ⟹ t1 ∈ trm ⟹ x ∈ var ⟹
substT (f t) t1 x = f (substT t t1 x)"
begin

end ― ‹context @{locale TermEncode}›

subsection ‹The first Hilbert-Bernays-Löb derivability condition›

locale HBL1 =
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
+
Deduct
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("⟨_⟩")
+
fixes P :: 'fmla
assumes
P[intro!,simp]: "P ∈ fmla"
and
Fvars_P[simp]: "Fvars P = {xx}"
and
HBL1: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ prv (subst P ⟨φ⟩ xx)"
begin

text ‹Predicate version of the provability formula›
definition PP where "PP ≡ λt. subst P t xx"

lemma PP[simp]: "⋀t. t ∈ trm ⟹ PP t ∈ fmla"
unfolding PP_def by auto

lemma Fvars_PP[simp]: "⋀t. t ∈ trm ⟹ Fvars (PP t) = FvarsT t"
unfolding PP_def by auto

lemma [simp]:
"n ∈ num ⟹ subst (PP (Var yy)) n yy = PP n"
"n ∈ num ⟹ subst (PP (Var xx)) n xx = PP n"
unfolding PP_def by auto

lemma HBL1_PP:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ prv (PP ⟨φ⟩)"
using HBL1 unfolding PP_def by auto

end ― ‹context @{locale HBL1}›

(*<*)
end
(*>*)

# Theory Jeroslow_Original

section ‹A Formalization of Jeroslow's Original Argument›

(*<*)
theory Jeroslow_Original imports
"Syntax_Independent_Logic.Pseudo_Term"
Abstract_Jeroslow_Encoding
begin
(*>*)

subsection ‹Preliminaries›

text ‹The First Derivability Condition was stated using a formula
with free variable @{term xx}, whereas the pseudo-term theory employs a different variable,
inp. The distinction is of course immaterial, because we can perform
a change of variable in the instantiation:›

context HBL1
begin

text ‹Changing the variable (from @{term xx} to @{term inp}) in the provability predicate:›
definition "Pinp ≡ subst P (Var inp) xx"
lemma PP_Pinp: "t ∈ trm ⟹ PP t = instInp Pinp t"
unfolding PP_def Pinp_def instInp_def by auto

text ‹A version of HBL1 that uses the @{term inp} variable:›
lemma HBL1_inp:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ prv (instInp Pinp ⟨φ⟩)"
unfolding Pinp_def instInp_def by (auto intro: HBL1)

end ― ‹context @{locale HBL1 }›

subsection ‹Jeroslow-style diagonalization›

locale Jeroslow_Diagonalization =
Deduct_with_False_Disj_Rename
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv
+
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
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 enc ("⟨_⟩")
+
fixes F :: "('trm ⇒ 'trm) set"
and encF :: "('trm ⇒ 'trm) ⇒ 'fmla"
and N :: "'trm ⇒ 'trm"
and ssap :: "'fmla ⇒ 'trm ⇒ 'trm"
assumes
― ‹For the members @{term f} of @{term F}, we will only care about their action on numerals,
and we assume that they send numerals to numerals.›
F[simp,intro!]: "⋀ f n. f ∈ F ⟹ n ∈ num ⟹ f n ∈ num"
and
encF[simp,intro!]: "⋀ f. f ∈ F ⟹ encF f ∈ ptrm (Suc 0)"
and
N[simp,intro!]: "N ∈ F"
and
ssap[simp]: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {inp} ⟹ ssap φ ∈ F"
and
ReprF: "⋀f n. f ∈ F ⟹ n ∈ num ⟹ prveqlPT (instInp (encF f) n) (f n)"
and
CapN: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ N ⟨φ⟩ = ⟨neg φ⟩"
and
CapSS: ― ‹We consider formulas @{term ψ} of one variable, called @{term inp}:›
"⋀ ψ f. ψ ∈ fmla ⟹ Fvars ψ = {inp} ⟹ f ∈ F ⟹
ssap ψ ⟨encF f⟩ = ⟨instInpP ψ 0 (instInp (encF f) ⟨encF f⟩)⟩"
begin

lemma encF_fmla[simp,intro!]: "⋀ f. f ∈ F ⟹ encF f ∈ fmla"
by auto

lemma enc_trm: "φ ∈ fmla ⟹ ⟨φ⟩ ∈ trm"
by auto

definition τJ :: "'fmla ⇒ 'fmla" where
"τJ ψ ≡ instInp (encF (ssap ψ)) (⟨encF (ssap ψ)⟩)"

definition φJ :: "'fmla ⇒ 'fmla" where
"φJ ψ ≡ instInpP ψ 0 (τJ ψ)"

lemma τJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {inp}"
shows "τJ ψ ∈ ptrm 0"
unfolding τJ_def apply(rule instInp)
using assms by auto

lemma τJ_fmla[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {inp}"
shows "τJ ψ ∈ fmla"
using τJ[OF assms] unfolding ptrm_def by auto

lemma FvarsT_τJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {inp}"
shows "Fvars (τJ ψ) = {out}"
using τJ[OF assms] unfolding ptrm_def by auto

lemma φJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {inp}"
shows "φJ ψ ∈ fmla"
unfolding φJ_def using assms by (intro instInpP_fmla) auto

lemma Fvars_φJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {inp}"
shows "Fvars (φJ ψ) = {}"
using assms unfolding φJ_def by auto

lemma diagonalization:
assumes ψ[simp]: "ψ ∈ fmla" and [simp]: "Fvars ψ = {inp}"
shows "prveqlPT (τJ ψ) ⟨instInpP ψ 0 (τJ ψ)⟩ ∧
prv (eqv (φJ ψ) (instInp ψ ⟨φJ ψ⟩))"
proof
define f where "f ≡ ssap ψ"
have f[simp]: "f ∈ F" unfolding f_def using assms by auto
have ff: "f ⟨encF f⟩ = ⟨instInpP ψ 0 (τJ ψ)⟩"
using assms unfolding f_def τJ_def by (intro CapSS) auto

show "prveqlPT (τJ ψ) ⟨instInpP ψ 0 (τJ ψ)⟩"
using ReprF[OF f, of "⟨encF f⟩"]
unfolding τJ_def[of ψ, unfolded f_def[symmetric],symmetric] ff[symmetric]
by auto
from prveqlPT_prv_instInp_eqv_instInpP[OF ψ, of "τJ ψ", OF _ _ _ _ this,
unfolded φJ_def[symmetric]]
show "prv (eqv (φJ ψ) (instInp ψ ⟨φJ ψ⟩))"
by auto
qed

end ― ‹context @{locale Jeroslow_Diagonalization}›

subsection ‹Jeroslow's Second Incompleteness Theorem›

text ‹We follow Jeroslow's pseudo-term-based development of the
Second Incompleteness Theorem and point out the location in the proof that
implicitly uses an unstated assumption: the fact that, for certain two provably
equivalent formulas @{term φ} and @{term φ'}, it is provable that
the provability of the encoding of @{term φ'} implies
the provability of the encoding of @{term φ}. ›

locale Jeroslow_Godel_Second =
Jeroslow_Diagonalization
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv
enc
F encF N ssap
+
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv prv
enc
P
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 enc ("⟨_⟩")
and P
and F encF N ssap
+
assumes
SHBL3: "⋀τ. τ ∈ ptrm 0 ⟹ prv (imp (instInpP Pinp 0 τ) (instInp Pinp ⟨instInpP Pinp 0 τ⟩))"
begin

text ‹Consistency formula a la Jeroslow:›
definition jcons :: "'fmla" where
"jcons ≡ all xx (neg (cnj (instInp Pinp (Var xx))
(instInpP Pinp 0 (instInp (encF N) (Var (xx))))))"

lemma prv_eql_subst_trm3:
"x ∈ var ⟹ φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹
prv (eql t1 t2) ⟹ prv (subst φ t1 x) ⟹ prv (subst φ t2 x)"
using prv_eql_subst_trm2
by (meson subst prv_imp_mp)

lemma Pinp[simp,intro!]: "Pinp ∈ fmla"
and Fvars_Pinp[simp]: "Fvars Pinp = {inp}"
unfolding Pinp_def by auto

lemma ReprF_combineWith_CapN:
assumes "φ ∈ fmla" and "Fvars φ = {}"
shows "prveqlPT (instInp (encF N) ⟨φ⟩) ⟨neg φ⟩"
using assms unfolding CapN[symmetric, OF assms] by (intro ReprF) auto

theorem jeroslow_godel_second:
assumes consistent
― ‹Assumption that is not stated by Jeroslow, but seems to be needed:›
assumes unstated:
"let ψ = instInpP Pinp (Suc 0) (encF N);
τ = τJ ψ;
φ = instInpP (instInpP Pinp (Suc 0) (encF N)) 0 τ;
φ' = instInpP Pinp 0 (instInpP (encF N) 0 τ)
in prv (imp (instInp Pinp ⟨φ'⟩) (instInp Pinp ⟨φ⟩))"
shows "¬ prv jcons"
proof
assume *: "prv jcons"

define ψ where "ψ ≡ instInpP Pinp (Suc 0) (encF N)"
define τ where "τ ≡ τJ ψ"
define φ where "φ ≡ φJ ψ"
have ψ[simp,intro]: "ψ ∈ fmla" "Fvars ψ = {inp}"
unfolding ψ_def by auto
have τ[simp,intro]: "τ ∈ ptrm 0" "τ ∈ fmla" "Fvars τ = {out}"
unfolding τ_def by auto
have [simp]: "φ ∈ fmla" "Fvars φ = {}" unfolding φ_def by auto

define eNτ where "eNτ ≡ instInpP (encF N) 0 τ"
have eNτ[simp]: "eNτ ∈ ptrm 0" "eNτ ∈ fmla" "Fvars eNτ = {out}"
unfolding eNτ_def by auto
define φ' where "φ' ≡ instInpP Pinp 0 eNτ"
have [simp]: "φ' ∈ fmla" "Fvars φ' = {}" unfolding φ'_def by auto

have φφ': "prv (imp φ φ')" and φ'φ: "prv (imp φ' φ)" and φeφ': "prv (eqv φ φ')"
unfolding φ_def φJ_def φ'_def eNτ_def τ_def[symmetric] unfolding ψ_def
using prv_instInpP_compose[of Pinp "encF N" τ] by auto

from diagonalization[OF ψ]
have "prveqlPT τ ⟨instInpP ψ 0 τ⟩" and **: "prv (eqv φ (instInp ψ ⟨φ⟩))"
unfolding τ_def[symmetric] φ_def[symmetric] by auto
have "**1": "prv (imp φ (instInp ψ ⟨φ⟩))" "prv (imp (instInp ψ ⟨φ⟩) φ)"
using prv_imp_eqvEL[OF _ _ **] prv_imp_eqvER[OF _ _ **] by auto

from SHBL3[OF eNτ(1)]
have "prv (imp (instInpP Pinp 0 eNτ) (instInp Pinp ⟨instInpP Pinp 0 eNτ⟩))" .
hence "prv (imp φ' (instInp Pinp ⟨φ'⟩))" unfolding φ'_def .
from prv_prv_imp_trans[OF _ _ _ φφ' this]
have 0: "prv (imp φ (instInp Pinp ⟨φ'⟩))" by auto

note unr = unstated[unfolded Let_def
φ_def[unfolded φJ_def τ_def[symmetric], symmetric] ψ_def[symmetric]
τ_def[symmetric] eNτ_def[symmetric] φ'_def[symmetric] φJ_def]

have 1: "prv (imp φ (instInp Pinp ⟨φ⟩))"
apply(nrule r: nprv_prvI)
apply(nrule r: nprv_impI)
apply(nrule r: nprv_addLemmaE[OF unr])
apply(nrule r: nprv_addImpLemmaE[OF 0])
apply(nrule r: nprv_clear3_3)
by (simp add: nprv_clear2_2 prv_nprv1I unr)

have 2: "prv (imp φ (cnj (instInp Pinp ⟨φ⟩)
(instInp ψ ⟨φ⟩)))"
apply(nrule r: nprv_prvI)
apply(nrule r: nprv_impI)
apply(nrule r: nprv_cnjI)
subgoal apply(nrule r: nprv_addImpLemmaE[OF 1]) .
subgoal apply(nrule r: nprv_addImpLemmaE[OF "**1"(1)]) . .

define z where "z ≡ Variable (Suc (Suc 0))"
have z_facts[simp]: "z ∈ var" "z ≠ xx" "z ∉ Fvars Pinp"
"out ≠ z ∧ z ≠ out" "inp ≠ z ∧ z ≠ inp"
unfolding z_def by auto

have 30: "subst (instInpP Pinp 0 (instInp (encF N) (Var xx))) ⟨φ⟩ xx =
instInpP Pinp 0 (instInp (encF N) ⟨φ⟩)"
unfolding z_def[symmetric] instInp_def instInpP_def Let_def
by (variousSubsts4 auto
s1: subst_compose_diff s2: subst_subst
s3: subst_notIn[of _ _ xx] s4: subst_compose_diff)
have 31: "subst (instInp Pinp (Var xx)) ⟨φ⟩ xx =
instInp Pinp ⟨φ⟩" unfolding instInp_def by auto
have [simp]: "instInp (instInpP Pinp (Suc 0) (encF N)) ⟨φ⟩ =
instInpP Pinp 0 (instInp (encF N) ⟨φ⟩)"
by (auto simp: instInp_instInpP ψ_def)

have 3: "prv (neg (cnj (instInp Pinp ⟨φ⟩)
(instInp ψ ⟨φ⟩)))"
apply(nrule r: nprv_prvI)
apply(nrule r: nprv_addLemmaE[OF *, unfolded jcons_def])
apply(rule nprv_allE0[of _ _ _ "⟨φ⟩"], auto)
unfolding 30 31
apply(nrule r: nprv_clear2_2)
apply(nrule r: nprv_negI)
apply(nrule r: nprv_negE0)
apply(nrule r: nprv_clear2_2)
apply(nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear3_3)
apply(nrule r: nprv_cnjI)
apply(nrule r: nprv_clear2_1)
unfolding ψ_def
apply(nrule r: nprv_hyp) .

have ***: "prv (neg φ)"
apply(nrule r: nprv_prvI)
apply(nrule r: nprv_negI)
apply(nrule r: nprv_addImpLemmaE[OF 2])
apply(nrule r: nprv_addLemmaE[OF 3])
apply(nrule r: nprv_negE0) .

have 4: "prv (instInp Pinp ⟨neg φ⟩)" using HBL1_inp[OF _ _ ***] by auto

have 5: "prveqlPT (instInp (encF N) ⟨φ⟩) ⟨neg φ⟩"
using ReprF_combineWith_CapN[of φ] by auto

have [simp]: "instInp (encF N) ⟨φ⟩ ∈ ptrm 0" using instInp by auto

have 6: "prv (instInpP Pinp 0 (instInp (encF N) ⟨φ⟩))"
apply(nrule r: nprv_prvI)
apply(nrule r: nprv_addLemmaE[OF 4])
apply(nrule r: prveqlPT_nprv_instInpP_instInp[OF _ _ _ _ _ 5]) .

note lem = "**1"(2)[unfolded ψ_def]
have "prv φ"
apply(nrule r: nprv_prvI)
apply(nrule r: nprv_addLemmaE[OF 6])
apply(nrule r: nprv_addImpLemmaE[OF lem]) .

from this *** ‹consistent› show False unfolding consistent_def3 by auto
qed

end ― ‹context @{locale Jeroslow_Godel_Second}›

(*<*)
end
(*>*)


# Theory Jeroslow_Simplified

section ‹A Simplification of Jeroslow's Original Argument›

(*<*)
theory Jeroslow_Simplified imports Abstract_Jeroslow_Encoding
begin
(*>*)

text ‹This is the simplified version of Jeroslow's Second Incompleteness Theorem
The simplification consists of replacing pseudo-terms with plain terms
and representability with (what we call in the paper) term-representability.
This simplified version does not incur the complications of the original.›

subsection ‹Jeroslow-style term-based diagonalization›

locale Jeroslow_Diagonalization =
Deduct_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv
+
Encode
var trm fmla Var FvarsT substT Fvars subst
num
enc
+
TermEncode
var trm fmla Var FvarsT substT Fvars subst
num
Ops tenc
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 num
and prv
and enc ("⟨_⟩")
and Ops and tenc
+
fixes F :: "('trm ⇒ 'trm) set"
and encF :: "('trm ⇒ 'trm) ⇒ ('trm ⇒ 'trm)"
and N :: "'trm ⇒ 'trm"
and ssap :: "'fmla ⇒ 'trm ⇒ 'trm"
assumes
F[simp,intro!]: "⋀ f n. f ∈ F ⟹ n ∈ num ⟹ f n ∈ num"
and
encF[simp,intro!]: "⋀ f. f ∈ F ⟹ encF f ∈ Ops"
and
N[simp,intro!]: "N ∈ F"
and
ssap[simp]: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {xx} ⟹ ssap φ ∈ F"
and
ReprF: "⋀f n. f ∈ F ⟹ n ∈ num ⟹ prv (eql (encF f n) (f n))"
and
CapN: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ N ⟨φ⟩ = ⟨neg φ⟩"
and
CapSS:
"⋀ ψ f. ψ ∈ fmla ⟹ Fvars ψ = {xx} ⟹ f ∈ F ⟹
ssap ψ (tenc (encF f)) = ⟨inst ψ (encF f (tenc (encF f)))⟩"
begin

definition tJ :: "'fmla ⇒ 'trm" where
"tJ ψ ≡ encF (ssap ψ) (tenc (encF (ssap ψ)))"

definition φJ :: "'fmla ⇒ 'fmla" where
"φJ ψ ≡ subst ψ (tJ ψ) xx"

lemma tJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "tJ ψ ∈ trm"
using assms tJ_def by auto

lemma FvarsT_tJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "FvarsT (tJ ψ) = {}"
using assms tJ_def by auto

lemma φJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "φJ ψ ∈ fmla"
using assms φJ_def by auto

lemma Fvars_φJ[simp]:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "Fvars (φJ ψ) = {}"
using assms φJ_def by auto

lemma diagonalization:
assumes "ψ ∈ fmla" and "Fvars ψ = {xx}"
shows "prv (eql (tJ ψ) ⟨inst ψ (tJ ψ)⟩) ∧
prv (eqv (φJ ψ) (inst ψ ⟨φJ ψ⟩))"
proof
define fJ where "fJ ≡ ssap ψ"
have fJ[simp]: "fJ ∈ F" unfolding fJ_def using assms by auto
have "fJ (tenc (encF fJ)) = ⟨inst ψ (tJ ψ)⟩"
by (simp add: CapSS assms fJ_def tJ_def)
thus **: "prv (eql (tJ ψ) ⟨inst ψ (tJ ψ)⟩)"
using ReprF fJ fJ_def tJ_def by fastforce
show "prv (eqv (φJ ψ) (inst ψ ⟨φJ ψ⟩))"
using assms prv_eql_subst_trm_eqv[OF xx _  _ _ **, of "ψ"]
by (auto simp: φJ_def inst_def)
qed

end ― ‹context @{locale Jeroslow_Diagonalization}›

subsection ‹Term-based version of Jeroslow's Second Incompleteness Theorem›

locale Jeroslow_Godel_Second =
Jeroslow_Diagonalization
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv
enc
Ops tenc
F encF N ssap
+
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv prv
enc
P
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 num
and prv
and enc ("⟨_⟩")
and Ops and tenc
and P
and F encF N ssap
+
assumes
SHBL3: "⋀t. t ∈ trm ⟹ FvarsT t = {} ⟹ prv (imp (PP t) (PP ⟨PP t⟩))"
begin

text ‹Consistency formula a la Jeroslow:›
definition jcons :: "'fmla" where
"jcons ≡ all xx (neg (cnj (PP (Var xx)) (PP (encF N (Var (xx))))))"

lemma prv_eql_subst_trm3:
"x ∈ var ⟹ φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹
prv (eql t1 t2) ⟹ prv (subst φ t1 x) ⟹ prv (subst φ t2 x)"
using prv_eql_subst_trm2
by (meson subst prv_imp_mp)

lemma prv_eql_neg_encF_N:
assumes "φ ∈ fmla" and "Fvars φ = {}"
shows "prv (eql ⟨neg φ⟩ (encF N ⟨φ⟩))"
unfolding CapN[symmetric, OF assms]
by (rule prv_prv_eql_sym) (auto simp: assms intro: ReprF)

lemma prv_imp_neg_encF_N_aux:
assumes "φ ∈ fmla" and "Fvars φ = {}"
shows "prv (imp (PP ⟨neg φ⟩) (PP (encF N ⟨φ⟩)))"
using assms prv_eql_subst_trm2[OF _ _ _ _ prv_eql_neg_encF_N[OF assms],
of xx "PP (Var xx)"]
unfolding PP_def by auto

lemma prv_cnj_neg_encF_N_aux:
assumes "φ ∈ fmla" and "Fvars φ = {}" "χ ∈ fmla" "Fvars χ = {}"
and "prv (neg (cnj χ (PP ⟨neg φ⟩)))"
shows"prv (neg (cnj χ (PP (encF N ⟨φ⟩))))"
using assms prv_eql_subst_trm3[OF _ _ _ _ prv_eql_neg_encF_N,
of xx "neg (cnj χ (PP (Var xx)))"]
unfolding PP_def by auto

theorem jeroslow_godel_second:
assumes consistent
shows "¬ prv jcons"
proof
assume *: "prv jcons"
define ψ where "ψ ≡ PP (encF N (Var xx))"
define t where "t ≡ tJ ψ"
have ψ[simp,intro]: "ψ ∈ fmla" "Fvars ψ = {xx}"
and t[simp,intro]: "t ∈ trm" "FvarsT t = {}"
unfolding ψ_def t_def by auto

have sPP[simp]: "subst (PP (encF N (Var xx))) ⟨PP (encF N t)⟩ xx =
PP (encF N ⟨PP (encF N t)⟩)"
unfolding PP_def by (subst subst_compose_eq_or) auto
have sPP2[simp]: "subst (PP (encF N (Var xx))) t xx = PP (encF N t)"
unfolding PP_def by (subst subst_compose_eq_or) auto
have 00: "PP (encF N t) = inst ψ t" unfolding ψ_def inst_def PP_def
by (subst subst_compose_eq_or) auto

define φ where "φ ≡ φJ ψ"
have [simp]: "φ ∈ fmla" "Fvars φ = {}" unfolding φ_def by auto
have **: "prv (eql t ⟨φ⟩)"
unfolding 00 φ_def
using φJ_def diagonalization inst_def t_def by auto
have φ: "φ = PP (encF N t)" unfolding φ_def φJ_def t_def ψ_def
using sPP2 ψ_def t_def by blast
have 1: "prv (imp φ (PP ⟨φ⟩))" using SHBL3[of "encF N t"]
using 00 φJ_def φ_def ψ_def inst_def t_def by auto
have eqv_φ: "prv (eqv φ (PP (encF N ⟨φ⟩)))"  using diagonalization
by (metis "00" sPP φJ_def φ_def ψ ψ_def diagonalization inst_def t_def)
have 2: "prv (imp φ (PP (encF N ⟨φ⟩)))"
using prv_cnjEL[OF _ _ eqv_φ[unfolded eqv_def]] by auto
have "prv (imp (PP (encF N ⟨φ⟩)) φ)"
using prv_cnjER[OF _ _ eqv_φ[unfolded eqv_def]] by auto
from  prv_prv_imp_trans[OF _ _ _ prv_imp_neg_encF_N_aux this]
have 22: "prv (imp (PP ⟨neg φ⟩) φ)" by auto
have 3: "prv (imp φ (cnj (PP ⟨φ⟩) (PP (encF N ⟨φ⟩))))"
by (rule prv_imp_cnj[OF _ _ _ 1 2]) (auto simp: φ_def)
have 4: "prv (neg (cnj (PP ⟨φ⟩) (PP (encF N ⟨φ⟩))))"
using prv_allE[OF _ _ _ *[unfolded jcons_def], of "⟨φ⟩"]
by (simp add: φ ψ_def)
have 5: "prv (neg φ)"
unfolding neg_def
by (rule prv_prv_imp_trans[OF _ _ _ 3 4[unfolded neg_def]]) auto
hence "prv (PP ⟨neg φ⟩)" using
HBL1_PP[OF _ _ 5] by auto
hence "prv φ" using prv_imp_mp[OF _ _ 22] by auto
with 5 assms show False unfolding consistent_def3 by auto
qed

subsection ‹A variant of the Second Incompleteness Theorem›

text ‹This variant (also discussed in our CADE 2019 paper~\cite{DBLP:conf/cade/0001T19}) strengthens
the conclusion of the theorem to the standard formulation
of "does not prove its own consistency" at the expense of two
additional derivability-like conditions, HBL4 and WHBL2.›

theorem jeroslow_godel_second_standardCon:
assumes consistent
and HBL4: "⋀φ1 φ2. {φ1,φ2} ⊆ fmla ⟹ Fvars φ1 = {} ⟹ Fvars φ2 = {} ⟹
prv (imp (cnj (PP ⟨φ1⟩) (PP ⟨φ2⟩)) (PP ⟨cnj φ1 φ2⟩))"
and WHBL2: "⋀φ1 φ2. {φ1,φ2} ⊆ fmla ⟹ Fvars φ1 = {} ⟹ Fvars φ2 = {} ⟹
prv (imp φ1 φ2) ⟹ prv (imp (PP ⟨φ1⟩) (PP ⟨φ2⟩))"
shows "¬ prv (neg (PP ⟨fls⟩))"
proof
assume *:  "prv (neg (PP ⟨fls⟩))"
define ψ where "ψ ≡ PP (encF N (Var xx))"
define t where "t ≡ tJ ψ"
have ψ[simp,intro]: "ψ ∈ fmla" "Fvars ψ = {xx}"
and t[simp,intro]: "t ∈ trm" "FvarsT t = {}"
unfolding ψ_def t_def by auto

have [simp]: "subst (PP (encF N (Var xx))) ⟨PP (encF N t)⟩ xx =
PP (encF N ⟨PP (encF N t)⟩)"
unfolding PP_def by (subst subst_compose_eq_or) auto
have [simp]: "subst (PP (encF N (Var xx))) t xx = PP (encF N t)"
unfolding PP_def by (subst subst_compose_eq_or) auto
have 00: "PP (encF N t) = inst ψ t" unfolding ψ_def inst_def PP_def
by (subst subst_compose_eq_or) auto

define φ where "φ = PP (encF N t)"
have [simp]: "φ ∈ fmla" "Fvars φ = {}" unfolding φ_def by auto
have **: "prv (eql t ⟨PP (encF N t)⟩)"
unfolding 00 by (simp add: diagonalization t_def)
have 1: "prv (imp φ (PP ⟨φ⟩))" using SHBL3[of "encF N t"]
by (auto simp: φ_def)
have 2: "prv (imp φ (PP (encF N ⟨φ⟩)))"
using prv_eql_subst_trm2[OF xx _  _ _ **, of "PP (encF N (Var xx))"]
by (auto simp: φ_def)
have "prv (imp (PP (encF N ⟨φ⟩)) φ)"
using prv_eql_subst_trm_rev2[OF xx _  _ _ **, of "PP (encF N (Var xx))"]
by (auto simp: φ_def)
from prv_prv_imp_trans[OF _ _ _ prv_imp_neg_encF_N_aux this]
have 22: "prv (imp (PP ⟨neg φ⟩) φ)" by auto
have 3: "prv (imp φ (cnj (PP ⟨φ⟩) (PP (encF N ⟨φ⟩))))"
by (rule prv_imp_cnj[OF _ _ _ 1 2]) (auto simp: φ_def)

― ‹This is the modification from the proof of @{thm jeroslow_godel_second}:›
have 41: "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)) (PP ⟨cnj φ (neg φ)⟩))"
using HBL4[of φ "neg φ"] by auto
have "prv (imp (cnj φ (neg φ)) (fls))"
by (simp add: prv_cnj_imp_monoR2 prv_imp_neg_fls)
from WHBL2[OF _ _ _ this]
have 42: "prv (imp (PP ⟨cnj φ (neg φ)⟩) (PP ⟨fls⟩))" by auto
from prv_prv_imp_trans[OF _ _ _ 41 42]
have "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)) (PP ⟨fls⟩))" by auto
from prv_prv_imp_trans[OF _ _ _ this *[unfolded neg_def]]
have "prv (neg (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)))"
unfolding neg_def by auto
from prv_cnj_neg_encF_N_aux[OF _ _ _ _ this]
have 4: "prv (neg (cnj (PP ⟨φ⟩) (PP (encF N ⟨φ⟩))))" by auto
― ‹End modification›

have 5: "prv (neg φ)"
unfolding neg_def
by (rule prv_prv_imp_trans[OF _ _ _ 3 4[unfolded neg_def]]) auto
hence "prv (PP ⟨neg φ⟩)" using HBL1_PP[OF _ _ 5] by auto
hence "prv φ" using prv_imp_mp[OF _ _ 22] by auto
with 5 assms show False unfolding consistent_def3 by auto
qed

text ‹Next we perform a formal analysis of some connection between the
above theorems' hypotheses.›

definition noContr :: bool where
"noContr ≡ ∀ φ ∈ fmla. Fvars φ = {} ⟶ prv (neg (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)))"

lemma jcons_noContr:
assumes j: "prv jcons"
shows "noContr"
unfolding noContr_def proof safe
fix φ assume φ[simp]: "φ ∈ fmla" "Fvars φ = {}"
have [simp]: "subst (PP (encF N (Var xx))) ⟨φ⟩ xx =
PP (encF N ⟨φ⟩)"
unfolding PP_def by (simp add: subst_compose_same)
note j = allE_id[OF _ _ j[unfolded jcons_def], simplified]
have 0: "prv (neg (cnj (PP ⟨φ⟩)
(PP (encF N ⟨φ⟩))))"
(is "prv (neg (cnj (PP ⟨φ⟩) ?j))")
using prv_subst[OF _ _ _ j, of xx "⟨φ⟩"] by simp
have 1: "prv (imp (PP ⟨neg φ⟩) ?j)"
using prv_eql_neg_encF_N[of φ, simplified]
using prv_imp_neg_encF_N_aux by auto
have 2: "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩))
(cnj (PP ⟨φ⟩) ?j))"
using 0 1 by (simp add:  prv_cnj_mono prv_imp_refl)

have "prv (imp (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩))
(cnj (PP ⟨φ⟩) ?j))"
by (simp add: 2 prv_cnj_mono prv_imp_refl)
thus "prv (neg (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)))" using 0
unfolding neg_def
by (elim prv_prv_imp_trans[rotated 3]) auto
qed

text ‹@{term noContr} is still stronger than the standard notion of proving own consistency:›

lemma noContr_implies_neg_PP_fls:
assumes "noContr"
shows "prv (neg (PP ⟨fls⟩))"
proof-
have "prv (neg (cnj (PP ⟨fls⟩) (PP ⟨neg fls⟩)))"
using assms unfolding noContr_def by auto
thus ?thesis
using Fvars_tru enc in_num tru_def PP PP_def fls imp HBL1 neg_def
prv_cnj_imp prv_fls prv_imp_com prv_imp_mp
by (metis Encode.enc HBL1_axioms HBL1_def)
qed

corollary jcons_implies_neg_PP_fls:
assumes "prv jcons"
shows "prv (neg (PP ⟨fls⟩))"
by (simp add: assms noContr_implies_neg_PP_fls jcons_noContr)

text ‹However, unlike @{term jcons}, which seems to be quite a bit stronger,
@{term noContr} is equivalent to the standard notion under a slightly
stronger assumption than our WWHBL2, namely, a binary version of that:›

lemma neg_PP_fls_implies_noContr:
assumes WWHBL22:
"⋀φ χ ψ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
Fvars φ = {} ⟹ Fvars χ = {} ⟹ Fvars ψ = {} ⟹
prv (imp φ (imp χ ψ)) ⟹ prv (imp (PP ⟨φ⟩) (imp (PP ⟨χ⟩) (PP ⟨ψ⟩)))"
assumes p: "prv (neg (PP ⟨fls⟩))"
shows "noContr"
unfolding noContr_def proof safe
fix φ assume φ[simp]: "φ ∈ fmla" "Fvars φ = {}"
have 0: "prv (imp φ (imp (neg φ) fls))"
by (simp add: prv_imp_neg_fls)
have 1: "prv (imp (PP ⟨φ⟩) (imp (PP ⟨neg φ⟩) (PP ⟨fls⟩)))"
using WWHBL22[OF _ _ _ _ _ _ 0] by auto
show "prv (neg (cnj (PP ⟨φ⟩) (PP ⟨neg φ⟩)))" using 1 p
unfolding neg_def
by (elim prv_cnj_imp_monoR2[rotated 3, OF prv_prv_imp_trans[rotated 3]])
(auto intro!: prv_imp_monoL)
qed

end ― ‹context @{locale Jeroslow_Godel_Second}›

(*<*)
end
(*>*)


# Theory Loeb_Formula

chapter ‹Löb  Formulas›

(*<*)
theory Loeb_Formula imports Diagonalization Derivability_Conditions
begin
(*>*)

text ‹The Löb formula, parameterized by a sentence @{term φ}, is defined by diagonalizing @{term "imp P φ"}.›

locale Loeb_Form =
Deduct2
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
+
Repr_SelfSubst
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
S
+
HBL1
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
P
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 prv bprv
and enc ("⟨_⟩")
and S
and P
begin

text ‹The Löb formula associated to a formula @{term φ}:›
definition φL :: "'fmla ⇒ 'fmla" where "φL φ ≡ diag (imp P φ)"

lemma φL[simp,intro]: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ φL φ ∈ fmla"
and
Fvars_φL[simp]: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ Fvars (φL φ) = {}"
unfolding φL_def PP_def by auto

lemma bprv_φL_eqv:
"φ ∈ fmla ⟹ Fvars φ  = {} ⟹ bprv (eqv (φL φ) (imp (PP ⟨φL φ⟩) φ))"
unfolding φL_def PP_def using bprv_diag_eqv[of "imp P φ"] by auto

lemma prv_φL_eqv:
"φ ∈ fmla ⟹ Fvars φ  = {} ⟹ prv (eqv (φL φ) (imp (PP ⟨φL φ⟩) φ))"
using bprv_prv[OF _ _ bprv_φL_eqv, simplified] by auto

end ― ‹context @{locale Loeb_Form}›

(*<*)
end
(*>*)


# Theory Loeb

chapter ‹Löb's Theorem›

(*<*)
theory Loeb imports Loeb_Formula Derivability_Conditions
begin
(*>*)

text ‹We have set up the formalization of Gödel's first (easy half) and Gödel's second
so that the following generalizations, leading to Löb's theorem, are trivial
modifications of these, replacing negation with "implies @{term φ}" in all proofs.›

locale Loeb_Assumptions =
HBL1_2_3
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv bprv
enc
P
+
Loeb_Form
var trm fmla Var num FvarsT substT Fvars subst
eql cnj imp all exi
prv bprv
enc
S
P
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 prv bprv
and enc ("⟨_⟩")
and S
and P
begin

text ‹Generalization of $\mathit{goedel\_first\_theEasyHalf\_pos}$, replacing @{term fls} with a sentence @{term φ}:›
lemma loeb_aux_prv:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "prv (φL φ)"
shows "prv φ"
proof-
have "prv (imp (PP ⟨φL φ⟩) φ)" using assms prv_eqv_prv[OF _ _ p prv_φL_eqv] by auto
moreover have "bprv (PP ⟨φL φ⟩)" using HBL1[OF φL[OF φ] _ p] unfolding PP_def by simp
from bprv_prv[OF _ _ this, simplified] have "prv (PP ⟨φL φ⟩)" .
ultimately show ?thesis using PP φL by (meson assms enc in_num prv_imp_mp)
qed

lemma loeb_aux_bprv:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "bprv (φL φ)"
shows "bprv φ"
proof-
note pp = bprv_prv[OF _ _ p, simplified]
have "bprv (imp (PP ⟨φL φ⟩) φ)" using assms B.prv_eqv_prv[OF _ _ p bprv_φL_eqv] by auto
moreover have "bprv (PP ⟨φL φ⟩)" using HBL1[OF φL[OF φ] _ pp] unfolding PP_def by simp
ultimately show ?thesis using PP φL by (meson assms enc in_num B.prv_imp_mp)
qed

text ‹Generalization of $\mathit{P\_G}$, the main lemma used for Gödel's second:›
lemma P_L:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "bprv (imp (PP ⟨φL φ⟩) (PP ⟨φ⟩))"
proof-
have 0: "prv (imp (φL φ) (imp (PP ⟨φL φ⟩) φ))"
using prv_φL_eqv by (intro prv_imp_eqvEL) auto
have 1: "bprv (PP ⟨imp (φL φ) (imp (PP ⟨φL φ⟩) φ)⟩)"
using HBL1_PP[OF _ _ 0] by simp
have 2: "bprv (imp (PP ⟨φL φ⟩) (PP ⟨imp (PP ⟨φL φ⟩) φ⟩))"
using HBL2_imp2[OF _ _ _ _ 1] by simp
have 3: "bprv (imp (PP ⟨φL φ⟩) (PP ⟨PP ⟨φL φ⟩⟩))"
using HBL3[OF φL[OF φ] _] by simp
have 23: "bprv (imp (PP ⟨φL φ⟩)
(cnj (PP ⟨PP ⟨φL φ⟩⟩)
(PP ⟨imp (PP ⟨φL φ⟩) φ⟩)))"
using B.prv_imp_cnj[OF _ _ _ 3 2] by simp
have 4: "bprv (imp (cnj (PP ⟨PP ⟨φL φ⟩⟩)
(PP ⟨imp (PP ⟨φL φ⟩) φ⟩))
(PP ⟨φ⟩))"
using HBL2[of "PP ⟨φL φ⟩" φ] by simp
show ?thesis using B.prv_prv_imp_trans[OF _ _ _ 23 4] by simp
qed

text ‹Löb's theorem generalizes the positive formulation Gödel's Second
($\mathit{goedel\_second}$). In our two-provability-relation framework, we get two variants of Löb's theorem.
A stronger variant, assuming @{term prv} and proving @{term bprv}, seems impossible.›

theorem loeb_bprv:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "bprv (imp (PP ⟨φ⟩) φ)"
shows "bprv φ"
proof-
have "bprv (imp (PP ⟨φL φ⟩) φ)"
by (rule B.prv_prv_imp_trans[OF _ _ _ P_L p]) auto
hence "bprv (φL φ)"
by (rule B.prv_eqv_prv_rev[OF _ _ _ bprv_φL_eqv, rotated 2]) auto
thus ?thesis using loeb_aux_bprv[OF φ] by simp
qed

theorem loeb_prv:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "prv (imp (PP ⟨φ⟩) φ)"
shows "prv φ"
proof-
note PL = bprv_prv[OF _ _ P_L, simplified]
have "prv (imp (PP ⟨φL φ⟩) φ)"
by (rule prv_prv_imp_trans[OF _ _ _ PL p]) auto
hence "prv (φL φ)"
by (rule prv_eqv_prv_rev[OF _ _ _ prv_φL_eqv, rotated 2]) auto
thus ?thesis using loeb_aux_prv[OF φ] by simp
qed

text ‹We could have of course inferred $\mathit{goedel\_first\_theEasyHalf\_pos}$
and $\mathit{goedel\_second}$ from these more general versions, but we leave the original
arguments as they are more instructive.›

end ― ‹context @{locale Loeb_Assumptions}›

(*<*)
end
(*>*)



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


# Theory All_Abstract

(*<*)

text ‹This puts together all the theories of the abstract development›

theory All_Abstract
imports
Abstract_First_Goedel
Abstract_First_Goedel_Rosser
Abstract_Second_Goedel
Jeroslow_Original
Jeroslow_Simplified
Loeb
Tarski
begin

end
(*>*)
`