7 theory Wellorderings imports Relative begin |
7 theory Wellorderings imports Relative begin |
8 |
8 |
9 text\<open>We define functions analogous to @{term ordermap} @{term ordertype} |
9 text\<open>We define functions analogous to @{term ordermap} @{term ordertype} |
10 but without using recursion. Instead, there is a direct appeal |
10 but without using recursion. Instead, there is a direct appeal |
11 to Replacement. This will be the basis for a version relativized |
11 to Replacement. This will be the basis for a version relativized |
12 to some class @{text M}. The main result is Theorem I 7.6 in Kunen, |
12 to some class \<open>M\<close>. The main result is Theorem I 7.6 in Kunen, |
13 page 17.\<close> |
13 page 17.\<close> |
14 |
14 |
15 |
15 |
16 subsection\<open>Wellorderings\<close> |
16 subsection\<open>Wellorderings\<close> |
17 |
17 |
30 "linear_rel(M,A,r) == |
30 "linear_rel(M,A,r) == |
31 \<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow> <x,y>\<in>r | x=y | <y,x>\<in>r)" |
31 \<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow> <x,y>\<in>r | x=y | <y,x>\<in>r)" |
32 |
32 |
33 definition |
33 definition |
34 wellfounded :: "[i=>o,i]=>o" where |
34 wellfounded :: "[i=>o,i]=>o" where |
35 --\<open>EVERY non-empty set has an @{text r}-minimal element\<close> |
35 \<comment>\<open>EVERY non-empty set has an \<open>r\<close>-minimal element\<close> |
36 "wellfounded(M,r) == |
36 "wellfounded(M,r) == |
37 \<forall>x[M]. x\<noteq>0 \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))" |
37 \<forall>x[M]. x\<noteq>0 \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))" |
38 definition |
38 definition |
39 wellfounded_on :: "[i=>o,i,i]=>o" where |
39 wellfounded_on :: "[i=>o,i,i]=>o" where |
40 --\<open>every non-empty SUBSET OF @{text A} has an @{text r}-minimal element\<close> |
40 \<comment>\<open>every non-empty SUBSET OF \<open>A\<close> has an \<open>r\<close>-minimal element\<close> |
41 "wellfounded_on(M,A,r) == |
41 "wellfounded_on(M,A,r) == |
42 \<forall>x[M]. x\<noteq>0 \<longrightarrow> x\<subseteq>A \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))" |
42 \<forall>x[M]. x\<noteq>0 \<longrightarrow> x\<subseteq>A \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))" |
43 |
43 |
44 definition |
44 definition |
45 wellordered :: "[i=>o,i,i]=>o" where |
45 wellordered :: "[i=>o,i,i]=>o" where |
46 --\<open>linear and wellfounded on @{text A}\<close> |
46 \<comment>\<open>linear and wellfounded on \<open>A\<close>\<close> |
47 "wellordered(M,A,r) == |
47 "wellordered(M,A,r) == |
48 transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)" |
48 transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)" |
49 |
49 |
50 |
50 |
51 subsubsection \<open>Trivial absoluteness proofs\<close> |
51 subsubsection \<open>Trivial absoluteness proofs\<close> |