763 |
763 |
764 subsection\<open>Relativization and Absoluteness for the @{term formula} Constructors\<close> |
764 subsection\<open>Relativization and Absoluteness for the @{term formula} Constructors\<close> |
765 |
765 |
766 definition |
766 definition |
767 is_Member :: "[i=>o,i,i,i] => o" where |
767 is_Member :: "[i=>o,i,i,i] => o" where |
768 \<comment>\<open>because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}\<close> |
768 \<comment> \<open>because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}\<close> |
769 "is_Member(M,x,y,Z) == |
769 "is_Member(M,x,y,Z) == |
770 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" |
770 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" |
771 |
771 |
772 lemma (in M_trivial) Member_abs [simp]: |
772 lemma (in M_trivial) Member_abs [simp]: |
773 "[|M(x); M(y); M(Z)|] ==> is_Member(M,x,y,Z) \<longleftrightarrow> (Z = Member(x,y))" |
773 "[|M(x); M(y); M(Z)|] ==> is_Member(M,x,y,Z) \<longleftrightarrow> (Z = Member(x,y))" |
777 "M(Member(x,y)) \<longleftrightarrow> M(x) & M(y)" |
777 "M(Member(x,y)) \<longleftrightarrow> M(x) & M(y)" |
778 by (simp add: Member_def) |
778 by (simp add: Member_def) |
779 |
779 |
780 definition |
780 definition |
781 is_Equal :: "[i=>o,i,i,i] => o" where |
781 is_Equal :: "[i=>o,i,i,i] => o" where |
782 \<comment>\<open>because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}\<close> |
782 \<comment> \<open>because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}\<close> |
783 "is_Equal(M,x,y,Z) == |
783 "is_Equal(M,x,y,Z) == |
784 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" |
784 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" |
785 |
785 |
786 lemma (in M_trivial) Equal_abs [simp]: |
786 lemma (in M_trivial) Equal_abs [simp]: |
787 "[|M(x); M(y); M(Z)|] ==> is_Equal(M,x,y,Z) \<longleftrightarrow> (Z = Equal(x,y))" |
787 "[|M(x); M(y); M(Z)|] ==> is_Equal(M,x,y,Z) \<longleftrightarrow> (Z = Equal(x,y))" |
790 lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) \<longleftrightarrow> M(x) & M(y)" |
790 lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) \<longleftrightarrow> M(x) & M(y)" |
791 by (simp add: Equal_def) |
791 by (simp add: Equal_def) |
792 |
792 |
793 definition |
793 definition |
794 is_Nand :: "[i=>o,i,i,i] => o" where |
794 is_Nand :: "[i=>o,i,i,i] => o" where |
795 \<comment>\<open>because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}\<close> |
795 \<comment> \<open>because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}\<close> |
796 "is_Nand(M,x,y,Z) == |
796 "is_Nand(M,x,y,Z) == |
797 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" |
797 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" |
798 |
798 |
799 lemma (in M_trivial) Nand_abs [simp]: |
799 lemma (in M_trivial) Nand_abs [simp]: |
800 "[|M(x); M(y); M(Z)|] ==> is_Nand(M,x,y,Z) \<longleftrightarrow> (Z = Nand(x,y))" |
800 "[|M(x); M(y); M(Z)|] ==> is_Nand(M,x,y,Z) \<longleftrightarrow> (Z = Nand(x,y))" |
803 lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) \<longleftrightarrow> M(x) & M(y)" |
803 lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) \<longleftrightarrow> M(x) & M(y)" |
804 by (simp add: Nand_def) |
804 by (simp add: Nand_def) |
805 |
805 |
806 definition |
806 definition |
807 is_Forall :: "[i=>o,i,i] => o" where |
807 is_Forall :: "[i=>o,i,i] => o" where |
808 \<comment>\<open>because @{term "Forall(x) \<equiv> Inr(Inr(p))"}\<close> |
808 \<comment> \<open>because @{term "Forall(x) \<equiv> Inr(Inr(p))"}\<close> |
809 "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" |
809 "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" |
810 |
810 |
811 lemma (in M_trivial) Forall_abs [simp]: |
811 lemma (in M_trivial) Forall_abs [simp]: |
812 "[|M(x); M(Z)|] ==> is_Forall(M,x,Z) \<longleftrightarrow> (Z = Forall(x))" |
812 "[|M(x); M(Z)|] ==> is_Forall(M,x,Z) \<longleftrightarrow> (Z = Forall(x))" |
813 by (simp add: is_Forall_def Forall_def) |
813 by (simp add: is_Forall_def Forall_def) |
819 |
819 |
820 subsection \<open>Absoluteness for @{term formula_rec}\<close> |
820 subsection \<open>Absoluteness for @{term formula_rec}\<close> |
821 |
821 |
822 definition |
822 definition |
823 formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i" where |
823 formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i" where |
824 \<comment>\<open>the instance of @{term formula_case} in @{term formula_rec}\<close> |
824 \<comment> \<open>the instance of @{term formula_case} in @{term formula_rec}\<close> |
825 "formula_rec_case(a,b,c,d,h) == |
825 "formula_rec_case(a,b,c,d,h) == |
826 formula_case (a, b, |
826 formula_case (a, b, |
827 \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, |
827 \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, |
828 h ` succ(depth(v)) ` v), |
828 h ` succ(depth(v)) ` v), |
829 \<lambda>u. d(u, h ` succ(depth(u)) ` u))" |
829 \<lambda>u. d(u, h ` succ(depth(u)) ` u))" |
879 subsubsection\<open>@{term is_formula_case}: relativization of @{term formula_case}\<close> |
879 subsubsection\<open>@{term is_formula_case}: relativization of @{term formula_case}\<close> |
880 |
880 |
881 definition |
881 definition |
882 is_formula_case :: |
882 is_formula_case :: |
883 "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o" where |
883 "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o" where |
884 \<comment>\<open>no constraint on non-formulas\<close> |
884 \<comment> \<open>no constraint on non-formulas\<close> |
885 "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == |
885 "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == |
886 (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) \<longrightarrow> finite_ordinal(M,y) \<longrightarrow> |
886 (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) \<longrightarrow> finite_ordinal(M,y) \<longrightarrow> |
887 is_Member(M,x,y,p) \<longrightarrow> is_a(x,y,z)) & |
887 is_Member(M,x,y,p) \<longrightarrow> is_a(x,y,z)) & |
888 (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) \<longrightarrow> finite_ordinal(M,y) \<longrightarrow> |
888 (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) \<longrightarrow> finite_ordinal(M,y) \<longrightarrow> |
889 is_Equal(M,x,y,p) \<longrightarrow> is_b(x,y,z)) & |
889 is_Equal(M,x,y,p) \<longrightarrow> is_b(x,y,z)) & |
913 |
913 |
914 subsubsection \<open>Absoluteness for @{term formula_rec}: Final Results\<close> |
914 subsubsection \<open>Absoluteness for @{term formula_rec}: Final Results\<close> |
915 |
915 |
916 definition |
916 definition |
917 is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" where |
917 is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" where |
918 \<comment>\<open>predicate to relativize the functional @{term formula_rec}\<close> |
918 \<comment> \<open>predicate to relativize the functional @{term formula_rec}\<close> |
919 "is_formula_rec(M,MH,p,z) == |
919 "is_formula_rec(M,MH,p,z) == |
920 \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & |
920 \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & |
921 successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)" |
921 successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)" |
922 |
922 |
923 |
923 |