# Theory Pf_Predicates

```chapter‹Formalizing Provability›

theory Pf_Predicates
imports Coding_Predicates
begin

section ‹Section 4 Predicates (Leading up to Pf)›

subsection ‹The predicate ‹SentP›, for the Sentiential (Boolean) Axioms›

nominal_function SentP :: "tm ⇒ fm"
where "⟦atom y ♯ (z,w,x); atom z ♯ (w,x); atom w ♯ x⟧ ⟹
SentP x = Ex y (Ex z (Ex w (FormP (Var y) AND FormP (Var z) AND FormP (Var w) AND
( (x EQ Q_Imp (Var y) (Var y)) OR
(x EQ Q_Imp (Var y) (Q_Disj (Var y) (Var z)) OR
(x EQ Q_Imp (Q_Disj (Var y) (Var y)) (Var y)) OR
(x EQ Q_Imp (Q_Disj (Var y) (Q_Disj (Var z) (Var w)))
(Q_Disj (Q_Disj (Var y) (Var z)) (Var w))) OR
(x EQ Q_Imp (Q_Disj (Var y) (Var z))
(Q_Imp (Q_Disj (Q_Neg (Var y)) (Var w)) (Q_Disj (Var z) (Var w)))))))))"
by (auto simp: eqvt_def SentP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SentP_fresh_iff [simp]: "a ♯ SentP x ⟷ a ♯ x"                  (is ?thesis1)
and SentP_sf [iff]:         "Sigma_fm (SentP x)"                     (is ?thsf)
proof -
obtain y::name and z::name and w::name  where "atom y ♯ (z,w,x)" "atom z ♯ (w,x)" "atom w ♯ x"
by (metis obtain_fresh)
thus ?thesis1 ?thsf
by auto
qed

subsection ‹The predicate ‹Equality_axP›, for the Equality Axioms›

function Equality_axP :: "tm ⇒ fm"
where "Equality_axP x =
x EQ «refl_ax» OR x EQ «eq_cong_ax» OR x EQ «mem_cong_ax» OR x EQ «eats_cong_ax»"
by auto

termination
by lexicographic_order

subsection ‹The predicate ‹HF_axP›, for the HF Axioms›

function HF_axP :: "tm ⇒ fm"
where "HF_axP x = x EQ «HF1» OR x EQ «HF2»"
by auto

termination
by lexicographic_order

lemma HF_axP_sf [iff]: "Sigma_fm (HF_axP t)"
by auto

subsection ‹The specialisation axioms›

subsubsection ‹Defining the syntax›

nominal_function Special_axP :: "tm ⇒ fm" where
"⟦atom v ♯ (p,sx,y,ax,x); atom x ♯ (p,sx,y,ax);
atom ax ♯ (p,sx,y); atom y ♯ (p,sx); atom sx ♯ p⟧ ⟹
Special_axP p = Ex v (Ex x (Ex ax (Ex y (Ex sx
(FormP (Var x) AND VarP (Var v) AND TermP (Var y) AND
AbstFormP (Var v) Zero (Var x) (Var ax) AND
SubstFormP (Var v) (Var y) (Var x) (Var sx) AND
p EQ Q_Imp (Var sx) (Q_Ex (Var ax)))))))"
by (auto simp: eqvt_def Special_axP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows Special_axP_fresh_iff [simp]: "a ♯ Special_axP p ⟷ a ♯ p" (is ?thesis1)
and Special_axP_sf [iff]:       "Sigma_fm (Special_axP p)" (is ?thesis3)
proof -
obtain v::name and x::name and ax::name and y::name and sx::name
where "atom v ♯ (p,sx,y,ax,x)" "atom x ♯ (p,sx,y,ax)"
"atom ax ♯ (p,sx,y)" "atom y ♯ (p,sx)" "atom sx ♯ p"
by (metis obtain_fresh)
thus ?thesis1 ?thesis3
by auto
qed

subsection ‹The induction axioms›

subsubsection ‹Defining the syntax›

nominal_function Induction_axP :: "tm ⇒ fm" where
"⟦atom ax ♯ (p,v,w,x,x0,xw,xevw,allw,allvw);
atom allvw ♯ (p,v,w,x,x0,xw,xevw,allw); atom allw ♯ (p,v,w,x,x0,xw,xevw);
atom xevw ♯ (p,v,w,x,x0,xw); atom xw ♯ (p,v,w,x,x0);
atom x0 ♯ (p,v,w,x); atom x ♯ (p,v,w);
atom w ♯ (p,v); atom v ♯ p⟧ ⟹
Induction_axP p = Ex v (Ex w (Ex x (Ex x0 (Ex xw (Ex xevw (Ex allw (Ex allvw (Ex ax
((Var v NEQ Var w) AND VarNonOccFormP (Var w) (Var x) AND
SubstFormP (Var v) Zero (Var x) (Var x0) AND
SubstFormP (Var v) (Var w) (Var x) (Var xw) AND
SubstFormP (Var v) (Q_Eats (Var v) (Var w)) (Var x) (Var xevw) AND
AbstFormP (Var w) Zero (Q_Imp (Var x) (Q_Imp (Var xw) (Var xevw))) (Var allw) AND
AbstFormP (Var v) Zero (Q_All (Var allw)) (Var allvw) AND
AbstFormP (Var v) Zero (Var x) (Var ax) AND
p EQ Q_Imp (Var x0) (Q_Imp (Q_All (Var allvw)) (Q_All (Var ax))))))))))))"
by (auto simp: eqvt_def Induction_axP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows Induction_axP_fresh_iff [simp]: "a ♯ Induction_axP p ⟷ a ♯ p" (is ?thesis1)
and Induction_axP_sf [iff]: "Sigma_fm (Induction_axP p)" (is ?thesis3)
proof -
obtain v::name and w::name and x::name and x0::name and xw::name and xevw::name
and allw::name and allvw::name and ax::name
where atoms: "atom ax ♯ (p,v,w,x,x0,xw,xevw,allw,allvw)"
"atom allvw ♯ (p,v,w,x,x0,xw,xevw,allw)" "atom allw ♯ (p,v,w,x,x0,xw,xevw)"
"atom xevw ♯ (p,v,w,x,x0,xw)" "atom xw ♯ (p,v,w,x,x0)" "atom x0 ♯ (p,v,w,x)"
"atom x ♯ (p,v,w)" "atom w ♯ (p,v)" "atom v ♯ p"
by (metis obtain_fresh)
thus ?thesis1 ?thesis3
by auto
qed

subsection ‹The predicate ‹AxiomP›, for any Axioms›

definition AxiomP :: "tm ⇒ fm"
where "AxiomP x ≡ x EQ «extra_axiom» OR SentP x OR Equality_axP x OR
HF_axP x OR Special_axP x OR Induction_axP x"

lemma AxiomP_I:
"{} ⊢ AxiomP «extra_axiom»"
"{} ⊢ SentP x ⟹ {} ⊢ AxiomP x"
"{} ⊢ Equality_axP x ⟹ {} ⊢ AxiomP x"
"{} ⊢ HF_axP x ⟹ {} ⊢ AxiomP x"
"{} ⊢ Special_axP x ⟹ {} ⊢ AxiomP x"
"{} ⊢ Induction_axP x ⟹ {} ⊢ AxiomP x"
unfolding AxiomP_def
by (rule Disj_I1, rule Refl,
rule Disj_I2, rule Disj_I1, assumption,
rule Disj_I2, rule Disj_I2, rule Disj_I1, assumption,
rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I1, assumption,
rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I1, assumption,
rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I2, assumption)

lemma AxiomP_eqvt [eqvt]: "(p ∙ AxiomP x) = AxiomP (p ∙ x)"

lemma AxiomP_fresh_iff [simp]: "a ♯ AxiomP x ⟷ a ♯ x"
by (auto simp: AxiomP_def)

lemma AxiomP_sf [iff]: "Sigma_fm (AxiomP t)"
by (auto simp: AxiomP_def)

subsection ‹The predicate ‹ModPonP›, for the inference rule Modus Ponens›

definition ModPonP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "ModPonP x y z = (y EQ Q_Imp x z)"

lemma ModPonP_eqvt [eqvt]: "(p ∙ ModPonP x y z) = ModPonP (p ∙ x) (p ∙ y) (p ∙ z)"

lemma ModPonP_fresh_iff [simp]: "a ♯ ModPonP x y z ⟷ a ♯ x ∧ a ♯ y ∧ a ♯ z"
by (auto simp: ModPonP_def)

lemma ModPonP_sf [iff]: "Sigma_fm (ModPonP t u v)"
by (auto simp: ModPonP_def)

lemma ModPonP_subst [simp]:
"(ModPonP t u v)(i::=w) = ModPonP (subst i w t) (subst i w u) (subst i w v)"
by (auto simp: ModPonP_def)

subsection ‹The predicate ‹ExistsP›, for the existential rule›
subsubsection ‹Definition›

(*  "⊢ A IMP B ⟹ atom i ♯ B ⟹  ⊢ (Ex i A) IMP B" *)
nominal_function ExistsP :: "tm ⇒ tm ⇒ fm" where
"⟦atom x ♯ (p,q,v,y,x'); atom x' ♯ (p,q,v,y);
atom y ♯ (p,q,v); atom v ♯ (p,q)⟧ ⟹
ExistsP p q = Ex x (Ex x' (Ex y (Ex v (FormP (Var x) AND
VarNonOccFormP (Var v) (Var y) AND
AbstFormP (Var v) Zero (Var x) (Var x') AND
p EQ Q_Imp (Var x) (Var y) AND
q EQ Q_Imp (Q_Ex (Var x')) (Var y)))))"
by (auto simp: eqvt_def ExistsP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows ExistsP_fresh_iff [simp]: "a ♯ ExistsP p q ⟷ a ♯ p ∧ a ♯ q"    (is ?thesis1)
and ExistsP_sf [iff]:       "Sigma_fm (ExistsP p q)"   (is ?thesis3)
proof -
obtain x::name and x'::name and y::name and v::name
where "atom x ♯ (p,q,v,y,x')"  "atom x' ♯ (p,q,v,y)" "atom y ♯ (p,q,v)"  "atom v ♯ (p,q)"
by (metis obtain_fresh)
thus ?thesis1 ?thesis3
by auto
qed

lemma ExistsP_subst [simp]: "(ExistsP p q)(j::=w) = ExistsP (subst j w p) (subst j w q)"
proof -
obtain x::name and x'::name and y::name and v::name
where "atom x ♯ (j,w,p,q,v,y,x')"   "atom x' ♯ (j,w,p,q,v,y)"
"atom y ♯ (j,w,p,q,v)"   "atom v ♯ (j,w,p,q)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: ExistsP.simps [of x _ _ x' y v])
qed

subsection ‹The predicate ‹SubstP›, for the substitution rule›

text‹Although the substitution rule is derivable in the calculus, the derivation is
too complicated to reproduce within the proof function. It is much easier to
provide it as an immediate inference step, justifying its soundness in terms
of other inference rules.›

subsubsection ‹Definition›

nominal_function SubstP :: "tm ⇒ tm ⇒ fm" where
"⟦atom u ♯ (p,q,v); atom v ♯ (p,q)⟧ ⟹
SubstP p q = Ex v (Ex u (SubstFormP (Var v) (Var u) p q))"
by (auto simp: eqvt_def SubstP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SubstP_fresh_iff [simp]: "a ♯ SubstP p q ⟷ a ♯ p ∧ a ♯ q"        (is ?thesis1)
and SubstP_sf [iff]: "Sigma_fm (SubstP p q)"                           (is ?thesis3)
proof -
obtain u::name and v::name  where "atom u ♯ (p,q,v)" "atom v ♯ (p,q)"
by (metis obtain_fresh)
thus ?thesis1 ?thesis3
by auto
qed

lemma SubstP_subst [simp]: "(SubstP p q)(j::=w) = SubstP (subst j w p) (subst j w q)"
proof -
obtain u::name and v::name  where "atom u ♯ (j,w,p,q,v)"  "atom v ♯ (j,w,p,q)"
by (metis obtain_fresh)
thus ?thesis
by (simp add: SubstP.simps [of u _ _ v])
qed

subsection ‹The predicate ‹PrfP››

(*Prf(s,k,t) ≡ LstSeq(s,k,t) ∧ (∀n∈k)[Sent (s n) ∨ (∃m,l∈n)[ModPon (s m) (s l) (s n)]]*)
nominal_function PrfP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,sl,m,n,sm,sn); atom sl ♯ (s,m,n,sm,sn);
atom m ♯ (s,n,sm,sn); atom n ♯ (s,k,sm,sn);
atom sm ♯ (s,sn); atom sn ♯ (s)⟧ ⟹
PrfP s k t =
LstSeqP s k t AND
All2 n (SUCC k) (Ex sn (HPair (Var n) (Var sn) IN s AND (AxiomP (Var sn) OR
Ex m (Ex l (Ex sm (Ex sl (Var m IN Var n AND Var l IN Var n AND
HPair (Var m) (Var sm) IN s AND HPair (Var l) (Var sl) IN s AND
(ModPonP (Var sm) (Var sl) (Var sn) OR
ExistsP (Var sm) (Var sn) OR
SubstP (Var sm) (Var sn)))))))))"
by (auto simp: eqvt_def PrfP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows PrfP_fresh_iff [simp]: "a ♯ PrfP s k t ⟷ a ♯ s ∧ a ♯ k ∧ a ♯ t"      (is ?thesis1)
and PrfP_imp_OrdP [simp]:    "{PrfP s k t} ⊢ OrdP k"         (is ?thord)
and PrfP_imp_LstSeqP [simp]: "{PrfP s k t} ⊢ LstSeqP s k t"  (is ?thlstseq)
and PrfP_sf [iff]:           "Sigma_fm (PrfP s k t)"         (is ?thsf)
proof -
obtain l::name and sl::name and m::name and n::name and sm::name and sn::name
where atoms: "atom l ♯ (s,sl,m,n,sm,sn)"   "atom sl ♯ (s,m,n,sm,sn)"
"atom m ♯ (s,n,sm,sn)"   "atom n ♯ (s,k,sm,sn)"
"atom sm ♯ (s,sn)"   "atom sn ♯ (s)"
by (metis obtain_fresh)
thus ?thesis1 ?thord ?thlstseq ?thsf
by (auto intro: LstSeqP_OrdP)
qed

lemma PrfP_subst [simp]:
"(PrfP t u v)(j::=w) = PrfP (subst j w t) (subst j w u) (subst j w v)"
proof -
obtain l::name and sl::name and m::name and n::name and sm::name and sn::name
where "atom l ♯ (t,u,v,j,w,sl,m,n,sm,sn)"   "atom sl ♯ (t,u,v,j,w,m,n,sm,sn)"
"atom m ♯ (t,u,v,j,w,n,sm,sn)"   "atom n ♯ (t,u,v,j,w,sm,sn)"
"atom sm ♯ (t,u,v,j,w,sn)"   "atom sn ♯ (t,u,v,j,w)"
by (metis obtain_fresh)
thus ?thesis
by (simp add: PrfP.simps [of l _ sl m n sm sn])
qed

subsection ‹The predicate ‹PfP››

nominal_function PfP :: "tm ⇒ fm"
where "⟦atom k ♯ (s,y); atom s ♯ y⟧ ⟹
PfP y = Ex k (Ex s (PrfP (Var s) (Var k) y))"
by (auto simp: eqvt_def PfP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows PfP_fresh_iff [simp]: "a ♯ PfP y ⟷ a ♯ y"           (is ?thesis1)
and PfP_sf [iff]: "Sigma_fm (PfP y)"                      (is ?thsf)
proof -
obtain k::name and s::name where "atom k ♯ (s,y)" "atom s ♯ y"
by (metis obtain_fresh)
thus ?thesis1 ?thsf
by auto
qed

lemma PfP_subst [simp]: "(PfP t)(j::=w) = PfP (subst j w t)"
proof -
obtain k::name and s::name where "atom k ♯ (s,t,j,w)" "atom s ♯ (t,j,w)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: PfP.simps [of k s])
qed

lemma ground_PfP [simp]: "ground_fm (PfP y) = ground y"
by (simp add: ground_aux_def ground_fm_aux_def supp_conv_fresh)

end

```