2023-05-21

285: Some Parts of Legitimate Formulas for ZFC Set Theory

<The previous article in this series | The table of contents of this series | The next article in this series>
A description/proof of some parts of legitimate formulas for ZFC set theory

Topics


About: set

The table of contents of this article

Starting Context

Target Context


  • The reader will have a description and a proof of the proposition that some expressions can be parts of legitimate formulas for the ZFC set theory.

Orientation


There is a list of definitions discussed so far in this site.

There is a list of propositions discussed so far in this site.

Main Body

1: Note


The subset axiom states that when \(S\) is a set, \(S_1: = \{s \in S\vert \phi (s, A_1, A_2, . . ., A_n)\}\) is a set where \(A_i\) is any set that is not \(S_1\) and \(\phi\) is something called formula. The reason why \(A_i\) is not allowed to be \(S_1\) is that otherwise, \(\phi (s, S_1) = s \in S_1\) would be allowed, which would not really determine what would be in \(S_1\). Likewise, the replacement axiom involves a formula.

Let us note that \(A_i\) is externally determined, which means that \(A_i\) cannot be constructed base on \(s\). For example, \(A_i\) cannot be like \(A_2 = A_1 \cap s\) or \(A_2 = \{a \in s\vert a \gt 2\}\).

Any formula in the ZFC set theory has to be legitimate, which means that the formula uses only the argument sets, some other set variables defined legitimately inside the formula, \(\in, =, \forall, \exists, \land, \lor, \lnot, \implies, \iff\), and (~) as to avoid ambiguity, where any 'other set variable defined legitimately inside the formula' is \(\exists p \text{ } \psi (p, . . .)\) or \(\forall p \text{ } \psi (p, . . .)\) where \(\psi (p, . . .)\) is a legitimate part. Let us mean by 'legitimate set variable' an argument variable or a set variable defined legitimately inside the formula, hereafter.

It is not so obvious whether an expression like '\(\exists p \text{ } p \in \{. . .\}\)' where \(\{. . .\}\) is a set is a part of a legitimate formula, because \(\{~\}\) is not declared to be usable in legitimate formulas by definition: \(\{. . .\}\) being a set is not enough; it has to be able to be expressed legitimately with only the certified elements.

But once an expression like \(\exists p \text{ } p = \{. . .\}\), is confirmed to be legitimate, \(p\) can be used representing \(\{. . .\}\) thereafter. That is the reason why we deal with such expressions in Descriptions.

If the requirement for such a formula seems to be too restrictive (and too arbitrary), I understand that the ZFC theory is only listing what can be safely called sets, not saying that what cannot be expressed with a legitimate formula cannot be a set (there is an article that argues my thoughts on that point). Anyway, we stick to what the ZFC theory guarantees in this article.

2: Description 1


For any legitimate set variable, \(p\), and any expression, \(e\), if \(p \in e\) is legitimate, \(p = e\) is legitimate where \(e\) is \(\{s \in S\vert \phi (s, . . .)\}\) for example.

On the other hand, if \(p = e\) is legitimate, \(p \in e\) is legitimate.

In fact, if \(p = e\) is legitimate, \(e \in p\) is legitimate.

Furthermore, if \(p = e\) and \(p = e'\) are legitimate, \(e \in e'\) and \(e = e'\) are legitimate.

So, in the following Descriptions, if a 1 form is described, also the other forms ares implied, even if without being mentioned.

3: Proof 1


Let us suppose that \(p \in e\) is legitimate. \(p = e\) is \((\forall p' \in p, p' \in e) \land (\forall p' \in e, p' \in p)\), but \(p' \in e\) is a legitimate part.

Let us suppose that \(p = e\) is legitimate. \(p \in e\) is \(\exists p' = e, p \in p'\), but \(p' = e\) is a legitimate part.

Let us suppose that \(p = e\) is legitimate. \(e \in p\) is \(\exists p' = e, p' \in p\).

Let us suppose that \(p = e\) and \(p = e'\) are legitimate. \(e \in e'\) is \(\exists p = e, \exists p' = e', p \in p'\). \(e = e'\) is \(\exists p = e, \exists p' = e', p = p'\).

4: Description 2


For any legitimate set variable, \(p\), any expression, \(\phi_1 (...)\), such that \(s \in \phi_1 (...)\) is legitimate when \(s\) is any legitimate set variable, and any legitimate expression, \(\phi_2 (s, . . .)\), \(p \in \{s \in \phi_1 (...)\vert \phi_2 (s, . . .)\}\) is legitimate.

5: Proof 2


\(p \in \{s \in \phi_1 (...)\vert \phi_2 (s, . . .)\}\) is \((p \in \phi_1 (...)) \land \phi_2 (p, . . .)\).

6: Description 3


For any legitimate set variables, \(p, S_1, S_2, . . ., S_n\), \(p \in \{S_1, S_2, . . ., S_n\}\) is legitimate.

7: Proof 3


\(p \in \{S_1, S_2, . . ., S_n\}\) is \((p = S_1) \lor (p = S_2) \lor . . . \lor (p = S_n)\).

8: Description 4


For any legitimate set variables, \(p, S_1, S_2\), \(p \in \langle S_1, S_2 \rangle\) is legitimate.

9: Proof 4


\(\langle S_1, S_2 \rangle\) is \(\{S_1, \{S_1, S_2\}\}\). \(p \in \{S_1, \{S_1, S_2\}\}\) is \((p = S_1) \lor (p = \{S_1, S_2\})\), and \(p = \{S_1, S_2\}\) is legitimate by Description 3 and Description 1.

10: Description 5


For any legitimate set variables, \(p, S\), \(p \in Pow (S)\) is legitimate where \(Pow (\bullet)\) means the power set of the argument.

11: Proof 5


\(p \in Pow (S)\) is \(p \subseteq S\), so, is legitimate.

12: Description 6


For any legitimate set variables, \(p, S_1, S_2, . . ., S_n\), \(p \in S_1 \times S_2 \times . . . \times S_n\) is legitimate.

13: Proof 6


As is shown in the proof of the proposition that the product of any finite number of sets is a set, \(S_1 \times S_2 = \{s \in Pow (Pow (S_1 \cup S_2))\vert \exists s_1 \in S_1, \exists s_2 \in S_2, s = \langle s_1, s_2 \rangle\}\). But \(s \in Pow (Pow (S_1 \cup S_2))\) is \((\exists s' = Pow (S_1 \cup S_2)) \land (s \in Pow s')\) and is legitimate, because \(s' = Pow (S_1 \cup S_2)\) and \(s \in Pow s'\) are legitimate by Description 5 and Description 1. \(s = \langle \bullet, \bullet \rangle\) is legitimate by Description 4 and Description 1. Then, \(p \in S_1 \times S_2\) is legitimate by Description 2.

\(p \in S_1 \times S_2 \times S_3\) is \((\exists p' = (S_1 \times S_2)) \land (p \in (p' \times S_3))\), which is legitimate by the previous paragraph and Description 1, and so on.

14: Description 7


For any legitimate set variables, \(p, S_1, S_2\), '\(p\) is a relation from \(S_1\) to \(S_2\)' is legitimate.

15: Proof 7


'\(p\) is a relation from \(S_1\) to \(S_2\)' is \(p \in Pow (S_1 \times S_2)\), which is \((\exists p' = S_1 \times S_2) \land (p \in Pow p')\). \(p' = S_1 \times S_2\) and \(p \in Pow p'\) are legitimate by Descriptions 5, 6, and 1.

16: Description 8


For any legitimate set variables, \(p, S_1, S_2\), '\(p\) is a function from \(S_1\) to \(S_2\)' is legitimate.

17: Proof 8


The set of all such possible functions is \(F = \{f \in Pow (S_1 \times S_2)\vert (\forall s_1 \in S_1, \exists s_2 \in S_2, \langle s_1, s_2 \rangle \in f) \land ((\exists s_1 \in S_1, \exists s_2 \in S_2, \exists {s_2}' \in S_2, (\langle s_1, s_2 \rangle \in f) \land (\langle s_1, {s_2}' \rangle \in f)) \implies (s_2 = {s_2}'))\}\). So, \(p \in F\), which is '\(p\) is a function from \(S_1\) to \(S_2\)', is legitimate by Descriptions 1, 2, 4, 5, and 6.

18: Description 9


For any legitimate set variables, \(p, f, S_1, S_2, S_3\), where \(f\) is a function, \(f: S_1 \rightarrow S_2\), \(p \in f\vert S_3\), where \(f\vert S_3\) is the restriction of \(f\), is legitimate.

19: Proof 9


\(f\vert_{S_3} = \{s \in f\vert \exists s_3 \in S_3, \exists s_2 \in S_2, s = \langle s_3, s_2 \rangle\}\). So, \(p \in f\vert S_3\) is legitimate by Descriptions 1, 2, and 4.

20: Description 10


For any legitimate set variables, \(p, f, S\), where \(f\) is a function, \(p = f (S)\) is legitimate when \(S\) is a member of the domain of \(f\).

21: Proof 10


\(p = f (S)\) is \(\exists p' \in f, p' = \langle S, p \rangle\), which is legitimate by Descriptions 1 and 4.

22: Description 11


For any legitimate set variables, \(p, S\), and any ordering, \(\lt\), that can apply to \(p\) and \(S\), \(p \lt S\) or \(p \leq S\) is legitimate, if the ordering is legitimately defined, which means that as the ordering is really a relation, which is a set, the relation has to be able to be expressed as a legitimate set variable.

23: Proof 11


As \(\lt\) is really a relation, \(R\), \(p \lt S\) or \(p \leq S\) is \(\langle p, S \rangle \in R\) or \(\langle p, S \rangle \in R \lor p = S\), respectively, which is legitimate by Description 4.

24: Description 12


For any legitimate set variables, \(p, f\), where \(f\) is a function, \(p \in img (f)\) is legitimate where \(img (\bullet)\) is the image of the argument.

25: Proof 12


\(p \in img (f)\) is \(\exists p', \langle p', p \rangle \in f\), which is legitimate by Description 4.

26: Description 13


For any legitimate set variables, \(p, f\), where \(f\) is a function, \(p \in dom (f)\) is legitimate where \(dom (\bullet)\) is the domain of the argument.

27: Proof 13


\(p \in dom (f)\) is \(\exists p', \langle p, p' \rangle \in f\), which is legitimate by Description 4.

28: Description 14


For any legitimate set variables, \(p, S, s\), where \(s \in S\), and any ordering, \(\lt\), \(p \in seg (S, \lt, s)\), which is the initial segment of \(S\) with respect to \(\lt\) and \(s\), is legitimate.

29: Proof 14


\(p \in seg (S, \lt, s)\) is \(p \in \{p' \in S\vert p' \lt s\}\), which is legitimate by Descriptions 2 and 11.

30: Description 15


For any legitimate set variables, \(\lt, S\), '\(\lt\) is a linear ordering on \(S\)' is legitimate.

31: Proof 15


'\(\lt\) is a linear ordering on \(S\)' is \(\lt \in Pow (S \times S) \land \forall s_1, s_2, s_3 \in S (\langle s_1, s_2 \rangle \in \lt \land \langle s_2, s_3 \rangle \in \lt) \langle s_1, s_3 \rangle \in \lt \land \forall s_1 \in S, \langle s_1, s_1 \rangle \notin \lt \land \forall s_1 \in S (\forall s_2 \in S, \lnot s_1 = s_2) ((\langle s_1, s_2 \rangle \in \lt \lor \langle s_2, s_1 \rangle \in \lt) \land \lnot (\langle s_1, s_2 \rangle \in \lt \land \langle s_2, s_1 \rangle \in \lt))\).

32: Description 16


For any legitimate set variables, \(\lt, S\), '\(\lt\) is a well-ordering on \(S\)' is legitimate.

33: Proof 16


'\(\lt\) is a well-ordering on \(S\)' is '\(\lt\) is a linear ordering on \(S\)' \(\land \forall S' \subseteq S (\exists m \in S' (\forall s \in S', (\lnot m = s), \langle m, s \rangle \in \lt)\).

34: Description 17


For any legitimate set variables, \(f, S_1, S_2\), '\(f\) is an injective function from \(S_1\) into \(S_2\)' is legitimate.

35: Proof 17


'\(f\) is an injective function from \(S_1\) into \(S_2\)' is '\(f\) is an function from \(S_1\) into \(S_2\)' \(\land (\forall p_1 \in S_1 (\forall p_2 \in S_1, \lnot p_2 = p_1) (\exists p_3 \in S_2, \langle p_1, p_3 \rangle \in f, \exists p_4 \in S_2, \langle p_2, p_4 \rangle \in f, \lnot p_3 = p_4))\). Note that as the condition that \(f\) is a function is in place, it is guaranteed that there are unique \(p_3\) and \(p_4\), so, if the found \(p_3\) and \(p_4\) satisfy \(\lnot p_3 = p_4\), it will be OK.

36: Description 18


For any legitimate set variables, \(f, S_1, S_2\), '\(f\) is a surjective function from \(S_1\) onto \(S_2\)' is legitimate.

37: Proof 18


'\(f\) is an surjective function from \(S_1\) onto \(S_2\)' is '\(f\) is an function from \(S_1\) into \(S_2\)' \(\land \forall p_2 \in S_2, \exists p_1 \in S_1, \langle p_1, p_2 \rangle \in f\).

38: Description 19


For any legitimate set variables, \(f, S_1, S_2\), '\(f\) is a bijective function from \(S_1\) onto \(S_2\)' is legitimate.

39: Proof 19


'\(f\) is a bijective function from \(S_1\) onto \(S_2\)' is '\(f\) is an injective function from \(S_1\) into \(S_2\)' \(\land\) '\(f\) is a surjective function from \(S_1\) onto \(S_2\)'.

40: Description 20


For any legitimate set variables, \(p, S\), '\(p\) is equinumerous with \(S\)', denoted as \(p \approx S\), is legitimate.

41: Proof 20


\(p \approx S\) is '\(\exists p', p'\) is a bijective function from \(p\) onto \(S\)'.

42: Description 21


For any legitimate set variable, \(p\), '\(p\) is an ordinal number' is legitimate.

43: Proof 21


'\(p\) is an ordinal number' is \(\exists S \exists \lt\), '\(\lt\) is a well-ordering on \(S\)', '\(p\) is the \(\epsilon\)-image of \((S, \lt)\)'. '\(p\) is the \(\epsilon\)-image of \((S, \lt)\)' is \(\exists S_1 (\exists f\), '\(f\) is a function from \(S\) to \(S_1\)', \(\forall s \in S, f (s) = \{s' \in S_1\vert \exists s'' \lt s, s' = f (s'')\})\) \(p = img f\).

44: Description 22


For any legitimate set variables, \(p, S\), '\(p\) is a cardinal number of \(S\)' is legitimate.

45: Proof 22


'\(p\) is a cardinal number of \(S\)' is '\(p\) is the least ordinal number equinumerous to \(S\)', which is '\(p\) is an ordinal number' \(\land\) \(p \approx S\) \(\land (\forall p', 'p'\) is an ordinal number' \(p' \approx S, \lnot p' = p) p \lt p'\).

46: Description 23


For any legitimate set variable, \(p\), '\(p\) is a cardinal number' is legitimate.

47: Proof 23


'\(p\) is a cardinal number' is \(\exists S, 'p\) is a cardinal number of \(S\)'.

48: Description 24


For any legitimate set variable, \(S\), and any net, \(n: D \rightarrow T\) where \(D\) is any directed set and \(T\) is any topological space, '\(n\) is frequently in \(S\)' is legitimate.

49: Proof 24


'\(n\) is frequently in \(S\)' is \(\forall d \in D (\exists d' \in D, d \leq d') n (d') \in S\).

50: Description 25


For any legitimate set variable, \(S\), and any net, \(n: D \rightarrow T\) where \(D\) is any directed set and \(T\) is any topological space, '\(n\) is eventually in \(S\)' is legitimate.

51: Proof 25


'\(n\) is eventually in \(S\)' is \(\exists d \in D (\forall d' \in D, d \leq d') n (d') \in S\).

52: Description 26


For any legitimate set variables, \(p, S_1, S_2, . . ., S_n\), \(p \in S_1 \cup S_2 \cup . . . \cup S_n\) is legitimate.

53: Proof 26


'\(p \in S_1 \cup S_2 \cup . . . \cup S_n\)' is '\(p \in S_1 \lor p \in S_2 \lor . . . \lor p \in S_n\)'.

54: Description 27


For any legitimate set variables, \(p, S\), and any legitimate function variable, \(f\), '\(p \in \cup_{\forall s \in S} f (s)\)' is legitimate.

55: Proof 27


'\(p \in \cup_{\forall s \in S} f (s)\)' is '\(\exists s \in S, p \in f (s)\)'.

56: Description 28


For any legitimate set variable, \(p\), and any ordinal number variable, \(o\), \(p \in V_o\), where \(V_o\) means the set of sets defined by \(V_0 = \emptyset, V_o = \cup_{o' \in o} Pow V_{o'}\), is legitimate.

57: Proof 28


'\(p \in V_o\)' is '\(\exists \delta, '\delta \text{ is an ordinal number' }, o \in \delta, \exists S \exists V, '\text{V is a function from }\delta\text{ to }S', \forall \alpha \in \delta, V (\alpha) = \cup_{{\alpha}' \in \alpha} Pow V ({\alpha}'), p \in V (o)\)'.

58: Description 29


For any legitimate set variable, \(p\), '\(p\) is grounded' is legitimate.

59: Proof 29


'\(p\) is grounded' is '\(\exists o, o \text{ is an ordinal number }, p \subseteq V_o\)'.

60: Description 30


For any legitimate set variables, \(p, S\), '\(p = rank S\)' is legitimate.

61: Proof 30


'\(p = rank S\)' is '\(p \text{ is an ordinal number } \land S \subseteq V_p \land \lnot (\exists o \in p, S \subseteq V_o)\)'.

62: Description 31


For any legitimate set variables, \(p, S\), '\(p \notin S\)' is legitimate.

63: Proof 31


'\(p \notin S\)' is '\(\lnot p \in S\)'.

64: Description 32


For any legitimate set variable, \(S\), '\(S\) is an open interval on \(\mathbb{R}\)' is legitimate.

65: Proof 32


'\(S\) is an open interval on \(\mathbb{R}\)' is '\(\exists p_1, p_2 (p_1, p_2 \in \mathbb{R} \land p_1, p_2 \notin S \land p_1 \le p_2 \land \forall p_3 \in \mathbb{R} (p_3 \in S \iff p_1 \lt p_3 \lt p_2))\)'.

66: Description 33


For any legitimate set variable, \(S\), '\(S\) is a closed interval on \(\mathbb{R}\)' is legitimate.

67: Proof 33


'\(S\) is a closed interval on \(\mathbb{R}\)' is '\(\exists p_1, p_2 (p_1, p_2 \in \mathbb{R} \land p_1, p_2 \in S \land p_1 \le p_2 \land \forall p_3 \in \mathbb{R} (p_3 \in S \iff p_1 \le p_3 \le p_2))\)'.

68: Description 34


For any legitimate set variable, \(S\), '\(S\) is a left-open-right-closed interval on \(\mathbb{R}\)' is legitimate.

69: Proof 34


'\(S\) is a left-open-right-closed interval on \(\mathbb{R}\)' is '\(\exists p_1, p_2 (p_1, p_2 \in \mathbb{R} \land p_1 \notin S \land p_2 \in S \land p_1 \le p_2 \land \forall p_3 \in \mathbb{R} (p_3 \in S \iff p_1 \lt p_3 \le p_2))\)'.

70: Description 35


For any legitimate set variable, \(S\), '\(S\) is a left-closed-right-open interval on \(\mathbb{R}\)' is legitimate.

71: Proof 35


'\(S\) is a left-closed-right-open interval on \(\mathbb{R}\)' is '\(\exists p_1, p_2 (p_1, p_2 \in \mathbb{R} \land p_1 \in S \land p_2 \notin S \land p_1 \le p_2 \land \forall p_3 \in \mathbb{R} (p_3 \in S \iff p_1 \le p_3 \lt p_2))\)'.

72: Note


All the text books I have read (I do not say all the text books in the world) is like "Any formula has to be legitimate." and begin to present formulas that are not so obvious how they are legitimate, at least for me. For example, they begin to use \(\{. . .\}\) which is not any elementary component.

So, I had to list what compounds could be safely used in legitimate formulas.

Of course, those listed above are only what I have particularly noticed so far.

References
<The previous article in this series | The table of contents of this series | The next article in this series>
Posted by at
Labels: