Theory Incompleteness.Goedel_I
chapter ‹Section 6 Material and Gödel's First Incompleteness Theorem›
theory Goedel_I
imports Pf_Predicates Functions
begin
section‹The Function W and Lemma 6.1›
subsection‹Predicate form, defined on sequences›
definition SeqWR :: "hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqWR s k y ≡ LstSeq s k y ∧ app s 0 = 0 ∧
(∀l ❙∈ k. app s (succ l) = q_Eats (app s l) (app s l))"
nominal_function SeqWRP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,k,sl); atom sl ♯ (s)⟧ ⟹
SeqWRP s k y = LstSeqP s k y AND
HPair Zero Zero IN s AND
All2 l k (Ex sl (HPair (Var l) (Var sl) IN s AND
HPair (SUCC (Var l)) (Q_Succ (Var sl)) IN s))"
by (auto simp: eqvt_def SeqWRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma
shows SeqWRP_fresh_iff [simp]: "a ♯ SeqWRP s k y ⟷ a ♯ s ∧ a ♯ k ∧ a ♯ y" (is ?thesis1)
and eval_fm_SeqWRP [simp]: "eval_fm e (SeqWRP s k y) ⟷ SeqWR ⟦s⟧e ⟦k⟧e ⟦y⟧e" (is ?thesis2)
and SeqWRP_sf [iff]: "Sigma_fm (SeqWRP s k y)" (is ?thsf)
proof -
obtain l::name and sl::name where "atom l ♯ (s,k,sl)" "atom sl ♯ (s)"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: SeqWR_def q_defs LstSeq_imp_Ord
Seq_iff_app [of "⟦s⟧e", OF LstSeq_imp_Seq_succ]
Ord_trans [of _ _ "succ ⟦k⟧e"])
qed
lemma SeqWRP_subst [simp]:
"(SeqWRP s k y)(i::=t) = SeqWRP (subst i t s) (subst i t k) (subst i t y)"
proof -
obtain l::name and sl::name
where "atom l ♯ (s,k,sl,t,i)" "atom sl ♯ (s,k,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqWRP.simps [where l=l and sl=sl])
qed
lemma SeqWRP_cong:
assumes "H ⊢ s EQ s'" and "H ⊢ k EQ k'" and "H ⊢ y EQ y'"
shows "H ⊢ SeqWRP s k y IFF SeqWRP s' k' y'"
by (rule P3_cong [OF _ assms], auto)
declare SeqWRP.simps [simp del]
subsection‹Predicate form of W›
definition WR :: "hf ⇒ hf ⇒ bool"
where "WR x y ≡ (∃s. SeqWR s x y)"
nominal_function WRP :: "tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (x,y)⟧ ⟹
WRP x y = Ex s (SeqWRP (Var s) x y)"
by (auto simp: eqvt_def WRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma
shows WRP_fresh_iff [simp]: "a ♯ WRP x y ⟷ a ♯ x ∧ a ♯ y" (is ?thesis1)
and eval_fm_WRP [simp]: "eval_fm e (WRP x y) ⟷ WR ⟦x⟧e ⟦y⟧e" (is ?thesis2)
and sigma_fm_WRP [simp]: "Sigma_fm (WRP x y)" (is ?thsf)
proof -
obtain s::name where "atom s ♯ (x,y)"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: WR_def)
qed
lemma WRP_subst [simp]: "(WRP x y)(i::=t) = WRP (subst i t x) (subst i t y)"
proof -
obtain s::name where "atom s ♯ (x,y,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: WRP.simps [of s])
qed
lemma WRP_cong: "H ⊢ t EQ t' ⟹ H ⊢ u EQ u' ⟹ H ⊢ WRP t u IFF WRP t' u'"
by (rule P2_cong) auto
declare WRP.simps [simp del]
lemma WR0_iff: "WR 0 y ⟷ y=0"
by (simp add: WR_def SeqWR_def) (metis LstSeq_1 LstSeq_app)
lemma WR0: "WR 0 0"
by (simp add: WR0_iff)
lemma WR_succ_iff: assumes i: "Ord i" shows "WR (succ i) z = (∃y. z = q_Eats y y ∧ WR i y)"
proof
assume "WR (succ i) z"
then obtain s where s: "SeqWR s (succ i) z"
by (auto simp: WR_def i)
moreover then have "app s (succ i) = z"
by (auto simp: SeqWR_def)
ultimately show "∃y. z = q_Eats y y ∧ WR i y" using i
by (auto simp: WR_def SeqWR_def) (metis LstSeq_trunc hmem_succ_self)
next
assume "∃y. z = q_Eats y y ∧ WR i y"
then obtain y where z: "z = q_Eats y y" and y: "WR i y"
by blast
thus "WR (succ i) z" using i
apply (auto simp: WR_def SeqWR_def)
apply (rule_tac x="insf s (succ i) (q_Eats y y)" in exI)
apply (auto simp: LstSeq_imp_Seq_succ app_insf_Seq_if LstSeq_insf succ_notin_self)
done
qed
lemma WR_succ: "Ord i ⟹ WR (succ i) (q_Eats y y) = WR i y"
by (metis WR_succ_iff q_Eats_iff)
lemma WR_ord_of: "WR (ord_of i) ⟦«ORD_OF i»⟧e"
by (induct i) (auto simp: WR0_iff WR_succ_iff quot_Succ q_defs)
text‹Lemma 6.1›
lemma WR_quot_Var: "WR ⟦«Var x»⟧e ⟦««Var x»»⟧e"
by (auto simp: quot_Var quot_Succ)
(metis One_nat_def Ord_ord_of WR_ord_of WR_succ htuple.simps q_Eats_def)
lemma ground_WRP [simp]: "ground_fm (WRP x y) ⟷ ground x ∧ ground y"
by (auto simp: ground_aux_def ground_fm_aux_def supp_conv_fresh)
lemma prove_WRP: "{} ⊢ WRP «Var x» ««Var x»»"
by (auto simp: WR_quot_Var ground_aux_def supp_conv_fresh intro: Sigma_fm_imp_thm)
subsection‹Proving that these relations are functions›
lemma SeqWRP_Zero_E:
assumes "insert (y EQ Zero) H ⊢ A" "H ⊢ k EQ Zero"
shows "insert (SeqWRP s k y) H ⊢ A"
proof -
obtain l::name and sl::name
where "atom l ♯ (s,k,sl)" "atom sl ♯ (s)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: SeqWRP.simps [where s=s and l=l and sl=sl])
apply (rule cut_same [where A = "LstSeqP s Zero y"])
apply (blast intro: thin1 assms LstSeqP_cong [OF Refl _ Refl, THEN Iff_MP_same])
apply (rule cut_same [where A = "y EQ Zero"])
apply (blast intro: LstSeqP_EQ)
apply (metis rotate2 assms(1) thin1)
done
qed
lemma SeqWRP_SUCC_lemma:
assumes y': "atom y' ♯ (s,k,y)"
shows "{SeqWRP s (SUCC k) y} ⊢ Ex y' (SeqWRP s k (Var y') AND y EQ Q_Succ (Var y'))"
proof -
obtain l::name and sl::name
where atoms: "atom l ♯ (s,k,y,y',sl)" "atom sl ♯ (s,k,y,y')"
by (metis obtain_fresh)
thus ?thesis using y'
apply (auto simp: SeqWRP.simps [where s=s and l=l and sl=sl])
apply (rule All2_SUCC_E' [where t=k, THEN rotate2], auto)
apply (rule Ex_I [where x = "Var sl"], auto)
apply (blast intro: LstSeqP_SUCC)
apply (blast intro: ContraProve LstSeqP_EQ)
done
qed
lemma SeqWRP_SUCC_E:
assumes y': "atom y' ♯ (s,k,y)" and k': "H ⊢ k' EQ (SUCC k)"
shows "insert (SeqWRP s k' y) H ⊢ Ex y' (SeqWRP s k (Var y') AND y EQ Q_Succ (Var y'))"
using SeqWRP_cong [OF Refl k' Refl] cut1 [OF SeqWRP_SUCC_lemma [of y' s k y]]
by (metis Assume Iff_MP_left Iff_sym y')
lemma SeqWRP_unique: "{OrdP x, SeqWRP s x y, SeqWRP s' x y'} ⊢ y' EQ y"
proof -
obtain i::name and j::name and j'::name and k::name and sl::name and sl'::name and l::name and pi::name
where i: "atom i ♯ (s,s',y,y')" and j: "atom j ♯ (s,s',i,x,y,y')" and j': "atom j' ♯ (s,s',i,j,x,y,y')"
and atoms: "atom k ♯ (s,s',i,j,j')" "atom sl ♯ (s,s',i,j,j',k)" "atom sl' ♯ (s,s',i,j,j',k,sl)"
"atom pi ♯ (s,s',i,j,j',k,sl,sl')"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ All j (All j' (SeqWRP s (Var i) (Var j) IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ Var j)))"
apply (rule OrdIndH [where j=k])
using i j j' atoms apply auto
apply (rule rotate4)
apply (rule OrdP_cases_E [where k=pi], simp_all)
apply (rule SeqWRP_Zero_E [THEN rotate3])
prefer 2 apply blast
apply (rule SeqWRP_Zero_E [THEN rotate4])
prefer 2 apply blast
apply (blast intro: ContraProve [THEN rotate4] Sym Trans)
apply (rule Ex_I [where x = "Var pi"], auto)
apply (metis ContraProve EQ_imp_SUBS2 Mem_SUCC_I2 Refl Subset_D)
apply (rule cut_same)
apply (rule SeqWRP_SUCC_E [of sl' s' "Var pi", THEN rotate4], auto)
apply (rule cut_same)
apply (rule SeqWRP_SUCC_E [of sl s "Var pi", THEN rotate7], auto)
apply (rule All_E [where x = "Var sl", THEN rotate5], simp)
apply (rule All_E [where x = "Var sl'"], simp)
apply (rule Imp_E, blast)+
apply (rule cut_same [OF Q_Succ_cong [OF Assume]])
apply (blast intro: Trans [OF Hyp Sym] HPair_cong)
done
hence "{OrdP (Var i)} ⊢ (All j' (SeqWRP s (Var i) (Var j) IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ Var j)))(j::=y)"
by (metis All_D)
hence "{OrdP (Var i)} ⊢ (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ y))(j'::=y')"
using j j'
by simp (drule All_D [where x=y'], simp)
hence "{} ⊢ OrdP (Var i) IMP (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) y' IMP y' EQ y))"
using j j'
by simp (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) y' IMP y' EQ y)))(i::=x)"
by (metis Subst emptyE)
thus ?thesis using i
by simp (metis anti_deduction insert_commute)
qed
theorem WRP_unique: "{OrdP x, WRP x y, WRP x y'} ⊢ y' EQ y"
proof -
obtain s::name and s'::name
where "atom s ♯ (x,y,y')" "atom s' ♯ (x,y,y',s)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqWRP_unique [THEN rotate3] WRP.simps [of s _ y] WRP.simps [of s' _ y'])
qed
subsection‹The equivalent function›
definition W :: "hf ⇒ tm"
where "W ≡ hmemrec (λf z. if z=0 then Zero else Q_Eats (f (pred z)) (f (pred z)))"
lemma W0 [simp]: "W 0 = Zero"
by (rule trans [OF def_hmemrec [OF W_def]]) auto
lemma W_succ [simp]: "Ord i ⟹ W (succ i) = Q_Eats (W i) (W i)"
by (rule trans [OF def_hmemrec [OF W_def]]) (auto simp: ecut_apply SUCC_def W_def)
lemma W_ord_of [simp]: "W (ord_of i) = «ORD_OF i»"
by (induct i, auto simp: SUCC_def quot_simps)
lemma WR_iff_eq_W: "Ord x ⟹ WR x y ⟷ y = ⟦W x⟧e"
proof (induct x arbitrary: y rule: Ord_induct2)
case 0 thus ?case
by (metis W0 WR0_iff eval_tm.simps(1))
next
case (succ k) thus ?case
by (auto simp: WR_succ_iff q_Eats_def)
qed
section‹The Function HF and Lemma 6.2›
definition SeqHR :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqHR x x' s k ≡
BuildSeq2 (λy y'. Ord y ∧ WR y y')
(λu u' v v' w w'. u = ⟨v,w⟩ ∧ u' = q_HPair v' w') s k x x'"
subsection ‹Defining the syntax: quantified body›
nominal_function SeqHRP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,k,sl,sl',m,n,sm,sm',sn,sn');
atom sl ♯ (s,sl',m,n,sm,sm',sn,sn');
atom sl' ♯ (s,m,n,sm,sm',sn,sn');
atom m ♯ (s,n,sm,sm',sn,sn');
atom n ♯ (s,sm,sm',sn,sn');
atom sm ♯ (s,sm',sn,sn');
atom sm' ♯ (s,sn,sn');
atom sn ♯ (s,sn');
atom sn' ♯ (s)⟧ ⟹
SeqHRP x x' s k =
LstSeqP s k (HPair x x') AND
All2 l (SUCC k) (Ex sl (Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND
((OrdP (Var sl) AND WRP (Var sl) (Var sl')) OR
Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN Var l AND Var n IN Var l AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND
Var sl EQ HPair (Var sm) (Var sn) AND
Var sl' EQ Q_HPair (Var sm') (Var sn')))))))))))"
by (auto simp: eqvt_def SeqHRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma
shows SeqHRP_fresh_iff [simp]:
"a ♯ SeqHRP x x' s k ⟷ a ♯ x ∧ a ♯ x' ∧ a ♯ s ∧ a ♯ k" (is ?thesis1)
and eval_fm_SeqHRP [simp]:
"eval_fm e (SeqHRP x x' s k) ⟷ SeqHR ⟦x⟧e ⟦x'⟧e ⟦s⟧e ⟦k⟧e" (is ?thesis2)
and SeqHRP_sf [iff]: "Sigma_fm (SeqHRP x x' s k)" (is ?thsf)
and SeqHRP_imp_OrdP: "{ SeqHRP x y s k } ⊢ OrdP k" (is ?thord)
proof -
obtain l::name and sl::name and sl'::name and m::name and n::name and
sm::name and sm'::name and sn::name and sn'::name
where atoms:
"atom l ♯ (s,k,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (s,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,n,sm,sm',sn,sn')" "atom n ♯ (s,sm,sm',sn,sn')"
"atom sm ♯ (s,sm',sn,sn')" "atom sm' ♯ (s,sn,sn')"
"atom sn ♯ (s,sn')" "atom sn' ♯ (s)"
by (metis obtain_fresh)
thus ?thesis1 ?thsf ?thord
by (auto intro: LstSeqP_OrdP)
show ?thesis2 using atoms
by (fastforce simp: LstSeq_imp_Ord SeqHR_def
BuildSeq2_def BuildSeq_def Builds_def
HBall_def q_HPair_def q_Eats_def
Seq_iff_app [of "⟦s⟧e", OF LstSeq_imp_Seq_succ]
Ord_trans [of _ _ "succ ⟦k⟧e"]
cong: conj_cong)
qed
lemma SeqHRP_subst [simp]:
"(SeqHRP x x' s k)(i::=t) = SeqHRP (subst i t x) (subst i t x') (subst i t s) (subst i t k)"
proof -
obtain l::name and sl::name and sl'::name and m::name and n::name and
sm::name and sm'::name and sn::name and sn'::name
where "atom l ♯ (s,k,t,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s,t,i,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (s,t,i,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,t,i,n,sm,sm',sn,sn')" "atom n ♯ (s,t,i,sm,sm',sn,sn')"
"atom sm ♯ (s,t,i,sm',sn,sn')" "atom sm' ♯ (s,t,i,sn,sn')"
"atom sn ♯ (s,t,i,sn')" "atom sn' ♯ (s,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqHRP.simps [of l _ _ sl sl' m n sm sm' sn sn'])
qed
lemma SeqHRP_cong:
assumes "H ⊢ x EQ x'" and "H ⊢ y EQ y'" "H ⊢ s EQ s'" and "H ⊢ k EQ k'"
shows "H ⊢ SeqHRP x y s k IFF SeqHRP x' y' s' k'"
by (rule P4_cong [OF _ assms], auto)
subsection ‹Defining the syntax: main predicate›
definition HR :: "hf ⇒ hf ⇒ bool"
where "HR x x' ≡ ∃s k. SeqHR x x' s k"
nominal_function HRP :: "tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (x,x',k); atom k ♯ (x,x')⟧ ⟹
HRP x x' = Ex s (Ex k (SeqHRP x x' (Var s) (Var k)))"
by (auto simp: eqvt_def HRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma
shows HRP_fresh_iff [simp]: "a ♯ HRP x x' ⟷ a ♯ x ∧ a ♯ x'" (is ?thesis1)
and eval_fm_HRP [simp]: "eval_fm e (HRP x x') ⟷ HR ⟦x⟧e ⟦x'⟧e" (is ?thesis2)
and HRP_sf [iff]: "Sigma_fm (HRP x x')" (is ?thsf)
proof -
obtain s::name and k::name where "atom s ♯ (x,x',k)" "atom k ♯ (x,x')"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: HR_def q_defs)
qed
lemma HRP_subst [simp]: "(HRP x x')(i::=t) = HRP (subst i t x) (subst i t x')"
proof -
obtain s::name and k::name where "atom s ♯ (x,x',t,i,k)" "atom k ♯ (x,x',t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: HRP.simps [of s _ _ k])
qed
subsection‹Proving that these relations are functions›
lemma SeqHRP_lemma:
assumes "atom m ♯ (x,x',s,k,n,sm,sm',sn,sn')" "atom n ♯ (x,x',s,k,sm,sm',sn,sn')"
"atom sm ♯ (x,x',s,k,sm',sn,sn')" "atom sm' ♯ (x,x',s,k,sn,sn')"
"atom sn ♯ (x,x',s,k,sn')" "atom sn' ♯ (x,x',s,k)"
shows "{ SeqHRP x x' s k }
⊢ (OrdP x AND WRP x x') OR
Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN k AND Var n IN k AND
SeqHRP (Var sm) (Var sm') s (Var m) AND
SeqHRP (Var sn) (Var sn') s (Var n) AND
x EQ HPair (Var sm) (Var sn) AND
x' EQ Q_HPair (Var sm') (Var sn')))))))"
proof -
obtain l::name and sl::name and sl'::name
where atoms:
"atom l ♯ (x,x',s,k,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (x,x',s,k,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (x,x',s,k,m,n,sm,sm',sn,sn')"
by (metis obtain_fresh)
thus ?thesis using atoms assms
apply (simp add: SeqHRP.simps [of l s k sl sl' m n sm sm' sn sn'])
apply (rule Conj_E)
apply (rule All2_SUCC_E' [where t=k, THEN rotate2], simp_all)
apply (rule rotate2)
apply (rule Ex_E Conj_E)+
apply (rule cut_same [where A = "HPair x x' EQ HPair (Var sl) (Var sl')"])
apply (metis Assume LstSeqP_EQ rotate4, simp_all, clarify)
apply (rule Disj_E [THEN rotate4])
apply (rule Disj_I1)
apply (metis Assume AssumeH(3) Sym thin1 Iff_MP_same [OF Conj_cong [OF OrdP_cong WRP_cong] Assume])
apply (rule Disj_I2)
apply (rule Ex_E Conj_EH)+
apply simp_all
apply (rule Ex_I [where x = "Var m"], simp)
apply (rule Ex_I [where x = "Var n"], simp)
apply (rule Ex_I [where x = "Var sm"], simp)
apply (rule Ex_I [where x = "Var sm'"], simp)
apply (rule Ex_I [where x = "Var sn"], simp)
apply (rule Ex_I [where x = "Var sn'"], simp)
apply (simp add: SeqHRP.simps [of l _ _ sl sl' m n sm sm' sn sn'])
apply (rule Conj_I, blast)+
apply (rule Conj_I)+
apply (blast intro: LstSeqP_Mem)
apply (rule All2_Subset [OF Hyp], blast)
apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
apply (rule Conj_I)+
apply (blast intro: LstSeqP_Mem)
apply (rule All2_Subset [OF Hyp], blast)
apply (auto intro!: SUCC_Subset_Ord LstSeqP_OrdP)
apply (blast intro: Trans)+
done
qed
lemma SeqHRP_unique: "{SeqHRP x y s u, SeqHRP x y' s' u'} ⊢ y' EQ y"
proof -
obtain i::name and j::name and j'::name and k::name and k'::name and l::name
and m::name and n::name and sm::name and sn::name and sm'::name and sn'::name
and m2::name and n2::name and sm2::name and sn2::name and sm2'::name and sn2'::name
where atoms: "atom i ♯ (s,s',y,y')" "atom j ♯ (s,s',i,x,y,y')" "atom j' ♯ (s,s',i,j,x,y,y')"
"atom k ♯ (s,s',x,y,y',u',i,j,j')" "atom k' ♯ (s,s',x,y,y',k,i,j,j')" "atom l ♯ (s,s',i,j,j',k,k')"
"atom m ♯ (s,s',i,j,j',k,k',l)" "atom n ♯ (s,s',i,j,j',k,k',l,m)"
"atom sm ♯ (s,s',i,j,j',k,k',l,m,n)" "atom sn ♯ (s,s',i,j,j',k,k',l,m,n,sm)"
"atom sm' ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn)" "atom sn' ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm')"
"atom m2 ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn')" "atom n2 ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2)"
"atom sm2 ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2)" "atom sn2 ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2)"
"atom sm2' ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2)" "atom sn2' ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2,sm2')"
by (metis obtain_fresh)
have "{OrdP (Var k)}
⊢ All i (All j (All j' (All k' (SeqHRP (Var i) (Var j) s (Var k) IMP (SeqHRP (Var i) (Var j') s' (Var k') IMP Var j' EQ Var j)))))"
apply (rule OrdIndH [where j=l])
using atoms apply auto
apply (rule Swap)
apply (rule cut_same)
apply (rule cut1 [OF SeqHRP_lemma [of m "Var i" "Var j" s "Var k" n sm sm' sn sn']], simp_all, blast)
apply (rule cut_same)
apply (rule cut1 [OF SeqHRP_lemma [of m2 "Var i" "Var j'" s' "Var k'" n2 sm2 sm2' sn2 sn2']], simp_all, blast)
apply (rule Disj_EH Conj_EH)+
apply (blast intro: cut3 [OF WRP_unique])
apply (rule Conj_EH Ex_EH)+
apply simp_all
apply (rule cut_same [where A = "OrdP (HPair (Var sm) (Var sn))"])
apply (blast intro: OrdP_cong [OF Hyp, THEN Iff_MP_same], blast)
apply (rule Ex_E Disj_EH Conj_EH)+
apply (rule cut_same [where A = "OrdP (HPair (Var sm2) (Var sn2))"])
apply (blast intro: OrdP_cong [OF Hyp, THEN Iff_MP_same], blast)
apply (rule Ex_E Disj_EH Conj_EH)+
apply (rule All_E' [OF Hyp, where x="Var m"], blast)
apply (rule All_E' [OF Hyp, where x="Var n"], blast, simp_all)
apply (rule Disj_EH, blast intro: thin1 ContraProve)+
apply (rule All_E [where x="Var sm"], simp)
apply (rule All_E [where x="Var sm'"], simp)
apply (rule All_E [where x="Var sm2'"], simp)
apply (rule All_E [where x="Var m2"], simp)
apply (rule All_E [where x="Var sn", THEN rotate2], simp)
apply (rule All_E [where x="Var sn'"], simp)
apply (rule All_E [where x="Var sn2'"], simp)
apply (rule All_E [where x="Var n2"], simp)
apply (rule cut_same [where A = "HPair (Var sm) (Var sn) EQ HPair (Var sm2) (Var sn2)"])
apply (blast intro: Sym Trans)
apply (rule cut_same [where A = "SeqHRP (Var sn) (Var sn2') s' (Var n2)"])
apply (blast intro: SeqHRP_cong [OF Hyp Refl Refl, THEN Iff_MP2_same])
apply (rule cut_same [where A = "SeqHRP (Var sm) (Var sm2') s' (Var m2)"])
apply (blast intro: SeqHRP_cong [OF Hyp Refl Refl, THEN Iff_MP2_same])
apply (rule Disj_EH, blast intro: thin1 ContraProve)+
apply (blast intro: Trans [OF Hyp Sym] intro!: HPair_cong)
done
hence "{OrdP (Var k)}
⊢ All j (All j' (All k' (SeqHRP x (Var j) s (Var k)
IMP (SeqHRP x (Var j') s' (Var k') IMP Var j' EQ Var j))))"
apply (rule All_D [where x = x, THEN cut_same])
using atoms by auto
hence "{OrdP (Var k)}
⊢ All j' (All k' (SeqHRP x y s (Var k) IMP (SeqHRP x (Var j') s' (Var k') IMP Var j' EQ y)))"
apply (rule All_D [where x = y, THEN cut_same])
using atoms by auto
hence "{OrdP (Var k)}
⊢ All k' (SeqHRP x y s (Var k) IMP (SeqHRP x y' s' (Var k') IMP y' EQ y))"
apply (rule All_D [where x = y', THEN cut_same])
using atoms by auto
hence "{OrdP (Var k)} ⊢ SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)"
apply (rule All_D [where x = u', THEN cut_same])
using atoms by auto
hence "{SeqHRP x y s (Var k)} ⊢ SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)"
by (metis SeqHRP_imp_OrdP cut1)
hence "{} ⊢ ((SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)))(k::=u)"
by (metis Subst emptyE Assume MP_same Imp_I)
hence "{} ⊢ SeqHRP x y s u IMP (SeqHRP x y' s' u' IMP y' EQ y)"
using atoms by simp
thus ?thesis
by (metis anti_deduction insert_commute)
qed
theorem HRP_unique: "{HRP x y, HRP x y'} ⊢ y' EQ y"
proof -
obtain s::name and s'::name and k::name and k'::name
where "atom s ♯ (x,y,y')" "atom s' ♯ (x,y,y',s)"
"atom k ♯ (x,y,y',s,s')" "atom k' ♯ (x,y,y',s,s',k)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqHRP_unique HRP.simps [of s x y k] HRP.simps [of s' x y' k'])
qed
subsection ‹Finally The Function HF Itself›
definition HF :: "hf ⇒ tm"
where "HF ≡ hmemrec (λf z. if Ord z then W z else Q_HPair (f (hfst z)) (f (hsnd z)))"
lemma HF_Ord [simp]: "Ord i ⟹ HF i = W i"
by (rule trans [OF def_hmemrec [OF HF_def]]) auto
lemma HF_pair [simp]: "HF (hpair x y) = Q_HPair (HF x) (HF y)"
by (rule trans [OF def_hmemrec [OF HF_def]]) (auto simp: ecut_apply HF_def)
lemma SeqHR_hpair: "SeqHR x1 x3 s1 k1 ⟹ SeqHR x2 x4 s2 k2 ⟹ ∃s k. SeqHR ⟨x1,x2⟩ (q_HPair x3 x4) s k"
by (auto simp: SeqHR_def intro: BuildSeq2_combine)
lemma HR_H: "coding_hf x ⟹ HR x ⟦HF x⟧e"
proof (induct x rule: hmem_rel_induct)
case (step x) show ?case
proof (cases "Ord x")
case True thus ?thesis
by (auto simp: HR_def SeqHR_def Ord_not_hpair WR_iff_eq_W [where e=e] intro!: BuildSeq2_exI)
next
case False
then obtain x1 x2 where x: "x = ⟨x1,x2⟩"
by (metis Ord_ord_of coding_hf.simps step.prems)
then have x12: "(x1, x) ∈ hmem_rel" "(x2, x) ∈ hmem_rel"
by (auto simp: hmem_rel_iff_hmem_eclose)
have co12: "coding_hf x1" "coding_hf x2" using False step x
by (metis Ord_ord_of coding_hf_hpair)+
hence "HR x1 ⟦HF x1⟧e" "HR x2 ⟦HF x2⟧e"
by (auto simp: x12 step)
thus ?thesis using x SeqHR_hpair
by (auto simp: HR_def q_defs)
qed
qed
text‹Lemma 6.2›
lemma HF_quot_coding_tm: "coding_tm t ⟹ HF ⟦t⟧e = «t»"
by (induct t rule: coding_tm.induct) (auto, simp add: HPair_def quot_Eats)
lemma HR_quot_fm: fixes A::fm shows "HR ⟦«A»⟧e ⟦««A»»⟧e"
by (metis HR_H HF_quot_coding_tm coding_tm_hf quot_fm_coding)
lemma prove_HRP: fixes A::fm shows "{} ⊢ HRP «A» ««A»»"
by (auto simp: supp_conv_fresh Sigma_fm_imp_thm ground_aux_def ground_fm_aux_def HR_quot_fm)
section‹The Function K and Lemma 6.3›
nominal_function KRP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "atom y ♯ (v,x,x') ⟹
KRP v x x' = Ex y (HRP x (Var y) AND SubstFormP v (Var y) x x')"
by (auto simp: eqvt_def KRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma KRP_fresh_iff [simp]: "a ♯ KRP v x x' ⟷ a ♯ v ∧ a ♯ x ∧ a ♯ x'"
proof -
obtain y::name where "atom y ♯ (v,x,x')"
by (metis obtain_fresh)
thus ?thesis
by auto
qed
lemma KRP_subst [simp]: "(KRP v x x')(i::=t) = KRP (subst i t v) (subst i t x) (subst i t x')"
proof -
obtain y::name where "atom y ♯ (v,x,x',t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: KRP.simps [of y])
qed
declare KRP.simps [simp del]
lemma prove_SubstFormP: "{} ⊢ SubstFormP «Var i» ««A»» «A» «A(i::=«A»)»"
by (auto simp: supp_conv_fresh Sigma_fm_imp_thm ground_aux_def SubstForm_quot)
lemma prove_KRP: "{} ⊢ KRP «Var i» «A» «A(i::=«A»)»"
by (auto simp: KRP.simps [of y]
intro!: Ex_I [where x="««A»»"] prove_HRP prove_SubstFormP)
lemma KRP_unique: "{KRP v x y, KRP v x y'} ⊢ y' EQ y"
proof -
obtain u::name and u'::name where "atom u ♯ (v,x,y,y')" "atom u' ♯ (v,x,y,y',u)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: KRP.simps [of u v x y] KRP.simps [of u' v x y']
intro: SubstFormP_cong [THEN Iff_MP2_same]
SubstFormP_unique [THEN cut2] HRP_unique [THEN cut2])
qed
lemma KRP_subst_fm: "{KRP «Var i» «β» (Var j)} ⊢ Var j EQ «β(i::=«β»)»"
by (metis KRP_unique cut0 prove_KRP)
section‹The Diagonal Lemma and Gödel's Theorem›
lemma diagonal:
obtains δ where "{} ⊢ δ IFF α(i::=«δ»)" "supp δ = supp α - {atom i}"
proof -
obtain k::name and j::name
where atoms: "atom k ♯ (i,j,α)" "atom j ♯ (i,α)"
by (metis obtain_fresh)
define β where "β = Ex j (KRP «Var i» (Var i) (Var j) AND α(i ::= Var j))"
hence 1: "{} ⊢ β(i ::= «β») IFF (Ex j (KRP «Var i» (Var i) (Var j) AND α(i ::= Var j)))(i ::= «β»)"
by (metis Iff_refl)
have 2: "{} ⊢ (Ex j (KRP «Var i» (Var i) (Var j) AND α(i ::= Var j)))(i ::= «β») IFF
Ex j (Var j EQ «β(i::=«β»)» AND α(i::=Var j))"
using atoms
apply (auto intro!: Ex_cong Conj_cong KRP_subst_fm)
apply (rule Iff_MP_same [OF Var_Eq_subst_Iff])
apply (auto intro: prove_KRP thin0)
done
have 3: "{} ⊢ Ex j (Var j EQ «β(i::=«β»)» AND α(i::=Var j)) IFF α(i::=«β(i::=«β»)»)"
using atoms
apply auto
apply (rule cut_same [OF Iff_MP2_same [OF Var_Eq_subst_Iff AssumeH(2)]])
apply (auto intro: Ex_I [where x="«β(i::=«β»)»"])
done
have "supp (β(i ::= «β»)) = supp α - {atom i}" using atoms
by (auto simp: fresh_at_base ground_fm_aux_def β_def supp_conv_fresh)
thus ?thesis using atoms
by (metis that 1 2 3 Iff_trans)
qed
text‹Gödel's first incompleteness theorem: Our theory is incomplete. NB it is provably consistent›
theorem Goedel_I:
obtains δ where "{} ⊢ δ IFF Neg (PfP «δ»)" "¬ {} ⊢ δ" "¬ {} ⊢ Neg δ"
"eval_fm e δ" "ground_fm δ"
proof -
fix i::name
obtain δ where "{} ⊢ δ IFF Neg ((PfP (Var i))(i::=«δ»))"
and suppd: "supp δ = supp (Neg (PfP (Var i))) - {atom i}"
by (metis SyntaxN.Neg diagonal)
then have diag: "{} ⊢ δ IFF Neg (PfP «δ»)"
by simp
then have np: "¬ {} ⊢ δ ∧ ¬ {} ⊢ Neg δ"
by (metis Iff_MP_same NegNeg_D Neg_D Neg_cong consistent proved_iff_proved_PfP)
then have "eval_fm e δ" using hfthm_sound [where e=e, OF diag]
by simp (metis Pf_quot_imp_is_proved)
moreover have "ground_fm δ" using suppd
by (simp add: supp_conv_fresh ground_fm_aux_def subset_eq) (metis fresh_ineq_at_base)
ultimately show ?thesis
by (metis diag np that)
qed
end