# How rigorous must my set theory proof be?

I'm working on a problem from the book "Introduction to Topology" by Bert Mendelson:

If $A_1\subset A_2, A_2\subset A_3, \ldots , A_{n-1}\subset A_n$, and $A_n \subset A_1$, prove that $A_1=A_2=\cdots=A_n$.

I know how to prove this, but my question is how rigorous my proof should be. For example, to make my proof easier, I proved the following "lemma":

If $H$ and $J$ are sets, $H \subset J$, and $J\subset H$, then $H=J$.

My proof went like this:

From the givens, we can determine that $$\alpha \in J, \forall \alpha \in H$$ $$\beta \in H, \forall \beta \in J$$ Which means that $$\alpha \in J, \forall \alpha \in H$$ $$\neg \beta \notin H, \forall \beta \in J$$ and so $H=J$.

I then went on to prove that $$A_k\subset A_{k+1}, A_{k+1}\subset A_k, \forall k \le n$$

Is my "lemma" proof enough of a proof? This is such a basic lemma that it seems like it should be obvious... but then again, when something seems obvious, it sometimes isn't. Is this rigorous enough? Is it too rigorous?

• What is your definition of "A= B" for A and B sets? Usually, "$A\subseteq B$" and "$B\subseteq A$" is the definition of "A= B". – user247327 Jul 7 '17 at 17:29
• @user247327 That's why I'm asking... I don't have a rigid definition of that. – Frpzzd Jul 7 '17 at 17:30
• There are really two non-obvious ideas in the proof here for a set theory beginner. The first is the notion that to prove $A=B$, you have to say "let $x\in A$" and show $x\in B$, and vice-versa; the second is the idea of "wrapping around" from $A_{k+1}$ to $A_k$ by walking along the chain of inclusions to show $A_{k+1}\subset A_k$. As long as you bring out those two key ideas in your proof, I think you've done the important part. – Jack M Jul 7 '17 at 19:28
• @Wildcard In many literatures the proper subset symbol is defined instead to allow improper subsets so it's a matter of convention. – Henricus V. Jul 8 '17 at 6:25
• @Wildcard, you are using “by definition” incorrectly. – Carsten S Jul 8 '17 at 8:59

## 9 Answers

In set-theory the notation $A\subseteq B$ is actually an abbreviation for:$$\forall x[x\in A\implies x\in B]$$

This makes $\subseteq$ a preorder on the sets (reflexive and transitive).

Then the axiom of extensionality is the statement that this relation is also anti-symmetric: $$A\subseteq B\wedge B\subseteq A\implies A=B\tag1$$ This makes the relation $\subseteq$ a partial order.

In my view $(1)$ is not a statement that can be proved, but is a statement based on an abbreviation and an axiom.

• Your answer is absolutely fine for a first introduction to topology, but if this were, say, a serious course in set theory or logic then I think you would usually be wrong that $(1)$ can't be proved. In a first-order logic, $=$ is usually fundamental, and the axiom of extensionality ties that to $A$ and $B$ having the same elements. Then by abbreviation/definition/however you think of $\subseteq$, you would cite the axiom of extensionality to prove $(1)$. – Mark S. Jul 8 '17 at 15:20
• @MarkS "cite the axiom of extensionality to prove $(1)$" Do you mean something like: "here we have $A\subseteq B\wedge B\subseteq A$ and on base of the axiom of extensionality we conclude that $A=B$" (so a proof based on the axiom)? Actually $(1)$ is not the axiom itself, because (only) quantifiers are lacking. Axioms cannot be proved. $(1)$ can be called an instance of the axiom. Do they need a proof (in the form of cite of the axiom)? – drhab Jul 8 '17 at 16:14
• "do you mean something like..." Yes, that is what I mean. A version of the proof might go something like: "rewrite $\subseteq$, use a logical fact to turn $\Rightarrow\land\Leftarrow$ into $\Leftrightarrow$, cite axiom of extensionality to conclude $A=B$". I agree that $(1)$ is not an axiom since $\subseteq$ is usually not part of any axiom. I don't think $(1)$ is an instance of any axiom scheme. I don't think the level of an "introduction to topology" book requires citing any axioms of set theory, but if this were in a set theory course, then it might. – Mark S. Jul 8 '17 at 16:26

If you really wanted formal, get rid of the $\ldots$ and prove it by induction:

For $n=2$ (the minimal case) we have $A_1 \subset A_2$ and $A_2 \subset A_1$. This means $A_1 = A_2$ by definition of $=$.

Suppose we have the statement holding for $n$ sets, and take $n+1$ sets obeying the hypotheses: $A_1 \subset A_2 \subset, \ldots \subset A_{n-1} \subset A_n \subset A_{n+1}$ and $A_{n+1} \subset A_1$. As $A_n \subset A_{n+1} \subset A_1$ simple transitivity of $\subset$ gives us $A_n \subset A_1$. But then forgetting $A_{n+1}$ for a while, we have $n$ sets obeying the hypotheses, and so we are allowed to conclude $A_1 = A_n$. So $A_{n+1} \subset A_1 = A_n \subset A_{n+1}$ and we have $A_1 = A_{n+1}$ as required. This concludes the induction step.

So it holds for all $n$.

• It is also possible to start the induction at $n=1$. – user133281 Jul 8 '17 at 10:00
• @user133281 $n=1$ isn't really possible. There are at least two sets involved. – Henno Brandsma Jul 8 '17 at 12:34
• I think that it is perfectly reasonable to view the statement for $n = 1$ as having a vacuous hypothesis, and the conclusion that $A_1 = A_1$. Indeed, your inductive step, applied to $n + 1$ when $n = 1$, really only uses that as input. (More generally, I really like having a trivial base case, rather than using substantially the same idea of argument to establish an interesting base case and the inductive step.) – LSpice Mar 21 '18 at 23:25

Opinion based answer.

I think you are confusing "rigor" with "write stuff using quantification symbols and other symbols rather than words".

You ask about your lemma, which is indeed nearly obvious. If I were required to prove it I'd say

To prove two sets equal I have to prove they contain the same elements. The first inclusion says that every element of $H$ is in $J$, the second says that every element of $J$ is in $H$, so done.

• Upvoted, but if I were asked to prove it in the context of an introductory course on ZFC, I would expect to get marked down for an answer like that ("Where are the axioms? Are you trying to do naive set theory?"). It all depends on your audience. – Kevin Jul 8 '17 at 1:28
• @Kevin Agreed. The appropriate level of formality depends on context. But even in a course on formal logic I'd prefer words to symbols where possible - as long as the words correctly described the situation. – Ethan Bolker Jul 8 '17 at 13:05

I would say this depends on your audience.

One kind of audience may be familiar enough with that Lemma that you don't have to provide a whole separate proof for it. And indeed, for some audiences, once you have shown that $A_1\subset A_2, A_2\subset A_3, \ldots , A_{n-1}\subset A_n$, and $A_n \subset A_1$, then to them it is immediately obvious that $A_1=A_2=\cdots=A_n$, so there is nothing to prove here at all. But for others (possibly your instructor who grades the proof!), more detail is required.

Presumably the context (e.g. the 'level' at which the textbook is written ... and how much detail has gone into other proofs in the text) will give you a fairly good idea as how detailed you should be.

My book defines the axiom of extensionality (i.e. the axiom that defines what it means for sets to be identical) as:

$\forall A \ \forall B \ (\forall x (x \in A \leftrightarrow x \in B) \rightarrow A = B)$

and $A \subseteq B$ is defined as:

$\forall A \ \forall B \ (A \subseteq B \rightarrow \forall x (x \in A \rightarrow x \in B))$

so with these, you can derive $A=B$ from $A \subseteq B$ and $B \subseteq A$

• Interestingly, since your axiom of extensionality is an implication, there may be sets $A$, $B$ with $A = B$ and not also $\forall x (x \in A \iff x \in B)$. So you don't actually have a definition of "$A = B$". If given $A = B$, you cannot deduce just "$\forall x (x \in A \iff x \in B)$" because this definition allows alternative antecedents in the implication. This exactly captures the inadequacy of if-then definitions. – Eric Towers Jul 12 '17 at 3:57
• @EricTowers Hey, don't shoot the messenger! :) I actually completely agree with you and think it should be a $\leftrightarrow$ as well. I think the book used the $\rightarrow$ since if $A =B$, then you can use $= Elim$ to go the other way. ... though I am not a big fan of that myself either, for that treats the set identity as if it were a true identity, and I regard sets having the same elements as a 'mere' qualitative identity. Indeed, I would prefer seeing a separate symbol for this kind of identity ... which means all the more reason to use a $\leftrightarrow$ – Bram28 Jul 12 '17 at 11:13

If you really wanted to be formal, you'd write:

-- Agda version 2.5.2
data List (A : Set) : Set where
Nil : List A
Cons : A → List A → List A

record ⊤ : Set where
constructor tt

record _∧_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B

All : {A : Set} → List A → (A → Set) → Set
All Nil P = ⊤
All (Cons x xs) P = P x ∧ All xs P

chain : {A : Set} → (A → A → Set) → List A → Set
chain op Nil = ⊤
chain {A} op (Cons x ss) = go x ss
where go : A → List A → Set
go s Nil = ⊤
go s (Cons x ss) = op s x ∧ go x ss

append : {A : Set} → A → List A → List A
append x Nil = Cons x Nil
append x (Cons y xs) = Cons y (append x xs)

thm : {A : Set} → (R : A → A → Set) → ({x y z : A} → R x y → R y z → R x z)
→ (x : A) → (xs : List A) → chain R (Cons x (append x xs)) → All xs (λ y → R x y ∧ R y x)
thm R trans x Nil p = tt
thm {A} R trans x (Cons y xs) (rxy , rs) = let (ryx , p) = go y xs rxy rs in (rxy , ryx) , p
where go : (y : A) → (xs : List A) → R x y → chain R (Cons y (append x xs)) → R y x ∧ All xs (λ z → R x z ∧ R z x)
go y Nil rxy (ryx , tt) = ryx , tt
go y (Cons z xs) rxy (ryz , rs) = let (rzx , p) = go z xs (trans rxy ryz) rs in trans ryz rzx , ((trans rxy ryz , rzx) , p)


Which (constructively) proves for any transitive relation $\sqsubseteq$, if $x_0 \sqsubseteq x_1 \land x_1 \sqsubseteq x_2 \land \cdots \land x_n \sqsubseteq x_0$ then $x_0 \sqsubseteq x_i \land x_i \sqsubseteq x_0$ for all $i\in\{1,\dots,n\}$. For $\sqsubseteq\,=\,\subseteq$, this almost your result. It proves that $x_0 = x_i$ for all $i\in\{1,\dots,n\}$ which clearly implies that they are all equal to each other.

And for absolute craziness, below is a complete formal proof in a Fitch system.

Lines 6 through 12 are number-theoretic lemma's that can all be derived from the Peano Axioms but I figured this was insane enough.

And sorry, but I couldn't show the indentations for the subproofs to show up, but I doubt anyone is really to check this proof anyway (it checks out in my prover, I swear!) and it serves just fine to illustrate the point that demanding too much rigor can be a really bad thing if your goal is human understanding.

1. ∀x ((0 < x ∧ x < n) → set(x) ⊆ set(s(x))) (given)
2. set(n) ⊆ set(s(0)) (given)
3. 0 < n (given)
4. ∀x ∀y (∀z (z ∈ x ↔ z ∈ y) → x = y) (axiom of extensionality)
5. ∀x ∀y (x ⊆ y ↔ ∀z (z ∈ x → z ∈ y)) (definition ⊆)
6. ∀x ¬x < x (lemma)
7. ∀x ∀y (s(x) < s(y) → x < y) (lemma)
8. ∀x x < s(x) (lemma)
9. ∀x ∀y ∀z ((x < y ∧ y < z) → x < z) (lemma)
10. ∀x (x = 0 ∨ 0 < x) (lemma)
11. ∀x ∀y (x < s(y) → (x = y ∨ x < y)) (lemma)
12. ∀x ¬x < 0 (lemma)
13. ¬0 < 0 ∀ Elim : 6
14. :a
15. :b b ∈ a
16. ∀z (z ∈ a → z ∈ a) ∀ Intro : 15-15
17. a ⊆ a ↔ ∀z (z ∈ a → z ∈ a) ∀ Elim : 5
18. a ⊆ a ↔ Elim : 16, 17
19. ∀x x ⊆ x ∀ Intro : 14-18
20. :a :b :c a ⊆ b ∧ b ⊆ c
21. a ⊆ b ∧ Elim : 20
22. b ⊆ c ∧ Elim : 20
23. a ⊆ b ↔ ∀z (z ∈ a → z ∈ b) ∀ Elim : 5
24. ∀z (z ∈ a → z ∈ b) ↔ Elim : 21, 23
25. b ⊆ c ↔ ∀z (z ∈ b → z ∈ c) ∀ Elim : 5
26. ∀z (z ∈ b → z ∈ c) ↔ Elim : 22, 25
27. :d d ∈ a
28. d ∈ a → d ∈ b ∀ Elim : 24
29. d ∈ b → Elim : 27, 28
30. d ∈ b → d ∈ c ∀ Elim : 26
31. d ∈ c → Elim : 29, 30
32. ∀z (z ∈ a → z ∈ c) ∀ Intro : 27-31
33. a ⊆ c ↔ ∀z (z ∈ a → z ∈ c) ∀ Elim : 5
34. a ⊆ c ↔ Elim : 32, 33
35. ∀x ∀y ∀z ((x ⊆ y ∧ y ⊆ z) → x ⊆ z) ∀ Intro : 20-34
36. :a :b a ⊆ b ∧ b ⊆ a
37. a ⊆ b ∧ Elim : 36
38. b ⊆ a ∧ Elim : 36
39. a ⊆ b ↔ ∀z (z ∈ a → z ∈ b) ∀ Elim : 5
40. ∀z (z ∈ a → z ∈ b) ↔ Elim : 37, 39
41. b ⊆ a ↔ ∀z (z ∈ b → z ∈ a) ∀ Elim : 5
42. ∀z (z ∈ b → z ∈ a) ↔ Elim : 38, 41
43. :c
44. c ∈ a
45. c ∈ a → c ∈ b ∀ Elim : 40
46. c ∈ b → Elim : 44, 45
47. c ∈ b
48. c ∈ b → c ∈ a ∀ Elim : 42
49. c ∈ a → Elim : 47, 48
50. c ∈ a ↔ c ∈ b ↔ Intro : 44-46, 47-49
51. ∀z (z ∈ a ↔ z ∈ b) ∀ Intro : 43-50
52. ∀z (z ∈ a ↔ z ∈ b) → a = b ∀ Elim : 4
53. a = b → Elim : 51, 52
54. ∀x ∀y ((x ⊆ y ∧ y ⊆ x) → x = y) ∀ Intro : 36-53
55. :a :b a = b
56. a ⊆ a ∀ Elim : 19
57. a ⊆ b = Elim : 55, 56
58. ∀x ∀y (x = y → x ⊆ y) ∀ Intro : 55-57
59. 0 < 0 ∧ 0 < s(n)
60. 0 < 0 ∧ Elim : 59
61. ¬0 < 0 ∀ Elim : 6
62. ⊥ ⊥ Intro : 60, 61
63. set(s(0)) ⊆ set(0) ⊥ Elim : 62
64. (0 < 0 ∧ 0 < s(n)) → set(s(0)) ⊆ set(0) → Intro : 59-63
65. :a (0 < a ∧ a < s(n)) → set(s(0)) ⊆ set(a)
66. 0 < s(a) ∧ s(a) < s(n)
67. s(a) < s(n) ∧ Elim : 66
68. s(a) < s(n) → a < n ∀ Elim : 7
69. a < n → Elim : 67, 68
70. n < s(n) ∀ Elim : 8
71. a < n ∧ n < s(n) ∧ Intro : 69, 70
72. (a < n ∧ n < s(n)) → a < s(n) ∀ Elim : 9
73. a < s(n) → Elim : 71, 72
74. a = 0 ∨ 0 < a ∀ Elim : 10
75. a = 0
76. set(s(0)) ⊆ set(s(0)) ∀ Elim : 19
77. set(s(0)) ⊆ set(s(a)) = Elim : 75, 76
78. 0 < a
79. 0 < a ∧ a < s(n) ∧ Intro : 78, 73
80. set(s(0)) ⊆ set(a) → Elim : 65, 79
81. 0 < a ∧ a < n ∧ Intro : 78, 69
82. (0 < a ∧ a < n) → set(a) ⊆ set(s(a)) ∀ Elim : 1
83. set(a) ⊆ set(s(a)) → Elim : 81, 82
84. set(s(0)) ⊆ set(a) ∧ set(a) ⊆ set(s(a)) ∧ Intro : 80, 83
85. (set(s(0)) ⊆ set(a) ∧ set(a) ⊆ set(s(a))) → set(s(0)) ⊆ set(s(a)) ∀ Elim : 35
86. set(s(0)) ⊆ set(s(a)) → Elim : 84, 85
87. set(s(0)) ⊆ set(s(a)) ∨ Elim : 74, 75-77, 78-86
88. (0 < s(a) ∧ s(a) < s(n)) → set(s(0)) ⊆ set(s(a)) → Intro : 66-87
89. ∀x ((0 < x ∧ x < s(n)) → set(s(0)) ⊆ set(x)) Peano Induction : 64, 65-88
90. n < s(n) ∀ Elim : 8
91. 0 < n ∧ n < s(n) ∧ Intro : 3, 90
92. (0 < n ∧ n < s(n)) → set(s(0)) ⊆ set(n) ∀ Elim : 89
93. set(s(0)) ⊆ set(n) → Elim : 91, 92
94. set(n) ⊆ set(s(0)) ∧ set(s(0)) ⊆ set(n) ∧ Intro : 2, 93
95. (set(n) ⊆ set(s(0)) ∧ set(s(0)) ⊆ set(n)) → set(n) = set(s(0)) ∀ Elim : 54
96. set(n) = set(s(0)) → Elim : 94, 95
1. 0 < 0
97. ¬0 < 0 ∀ Elim : 6
98. ⊥ ⊥ Intro : 98, 99
99. (∀x ((0 < x ∧ x < 0) → set(x) ⊆ set(s(x))) ∧ set(0) ⊆ set(s(0))) → ∀x ((0 < x ∧ x < 0) → set(x) = set(s(x))) ⊥ Elim : 100
100. 0 < 0 → ((∀x ((0 < x ∧ x < 0) → set(x) ⊆ set(s(x))) ∧ set(0) ⊆ set(s(0))) → ∀x ((0 < x ∧ x < 0) → set(x) = set(s(x)))) → Intro : 98-101
101. :a 0 < a → ((∀x ((0 < x ∧ x < a) → set(x) ⊆ set(s(x))) ∧ set(a) ⊆ set(s(0))) → ∀x ((0 < x ∧ x < a) → set(x) = set(s(x))))
102. 0 < s(a)
103. a = 0 ∨ 0 < a ∀ Elim : 10
104. ∀x ((0 < x ∧ x < s(a)) → set(x) ⊆ set(s(x))) ∧ set(s(a)) ⊆ set(s(0))
105. ∀x ((0 < x ∧ x < s(a)) → set(x) ⊆ set(s(x))) ∧ Elim : 106
106. set(s(a)) ⊆ set(s(0)) ∧ Elim : 106
107. :b 0 < b ∧ b < s(a)
108. 0 < b ∧ Elim : 109
109. b < s(a) ∧ Elim : 109
110. a = 0
111. b < s(0) = Elim : 112, 111
112. b < s(0) → (b = 0 ∨ b < 0) ∀ Elim : 11
113. b = 0 ∨ b < 0 → Elim : 113, 114
114. b = 0
115. 0 < 0 = Elim : 116, 110
116. ⊥ ⊥ Intro : 117, 13
117. b < 0
118. ¬b < 0 ∀ Elim : 12
119. ⊥ ⊥ Intro : 119, 120
120. ⊥ ∨ Elim : 115, 116-118, 119-121
121. set(b) = set(s(b)) ⊥ Elim : 122
122. 0 < a
123. (∀x ((0 < x ∧ x < a) → set(x) ⊆ set(s(x))) ∧ set(a) ⊆ set(s(0))) → ∀x ((0 < x ∧ x < a) → set(x) = set(s(x))) → Elim : 103, 124
124. :c 0 < c ∧ c < a
125. 0 < c ∧ Elim : 126
126. c < a ∧ Elim : 126
127. a < s(a) ∀ Elim : 8
128. c < a ∧ a < s(a) ∧ Intro : 128, 129
129. (c < a ∧ a < s(a)) → c < s(a) ∀ Elim : 9
130. c < s(a) → Elim : 130, 131
131. 0 < c ∧ c < s(a) ∧ Intro : 127, 132
132. (0 < c ∧ c < s(a)) → set(c) ⊆ set(s(c)) ∀ Elim : 107
133. set(c) ⊆ set(s(c)) → Elim : 133, 134
134. ∀x ((0 < x ∧ x < a) → set(x) ⊆ set(s(x))) ∀ Intro : 126-135
135. a < s(a) ∀ Elim : 8
136. 0 < a ∧ a < s(a) ∧ Intro : 124, 137
137. (0 < a ∧ a < s(a)) → set(a) ⊆ set(s(a)) ∀ Elim : 107
138. set(a) ⊆ set(s(a)) → Elim : 138, 139
139. set(a) ⊆ set(s(a)) ∧ set(s(a)) ⊆ set(s(0)) ∧ Intro : 140, 108
140. (set(a) ⊆ set(s(a)) ∧ set(s(a)) ⊆ set(s(0))) → set(a) ⊆ set(s(0)) ∀ Elim : 35
141. set(a) ⊆ set(s(0)) → Elim : 141, 142
142. ∀x ((0 < x ∧ x < a) → set(x) ⊆ set(s(x))) ∧ set(a) ⊆ set(s(0)) ∧ Intro : 136, 143
143. ∀x ((0 < x ∧ x < a) → set(x) = set(s(x))) → Elim : 125, 144
144. b < s(a) → (b = a ∨ b < a) ∀ Elim : 11
145. b = a ∨ b < a → Elim : 111, 146
146. b = a
147. 0 < 0 ∧ 0 < s(a)
148. 0 < 0 ∧ Elim : 149
149. ⊥ ⊥ Intro : 150, 13
150. set(s(0)) = set(0) ⊥ Elim : 151
151. (0 < 0 ∧ 0 < s(a)) → set(s(0)) = set(0) → Intro : 149-152
152. :c (0 < c ∧ c < s(a)) → set(s(0)) = set(c)
153. 0 < s(c) ∧ s(c) < s(a)
154. s(c) < s(a) ∧ Elim : 155
155. s(c) < s(a) → c < a ∀ Elim : 7
156. c < a → Elim : 156, 157
157. c = 0 ∨ 0 < c ∀ Elim : 10
158. c = 0
159. set(s(0)) = set(s(0)) = Intro
160. set(s(0)) = set(s(c)) = Elim : 160, 161
161. 0 < c
162. a < s(a) ∀ Elim : 8
163. c < a ∧ a < s(a) ∧ Intro : 158, 164
164. (c < a ∧ a < s(a)) → c < s(a) ∀ Elim : 9
165. c < s(a) → Elim : 165, 166
166. 0 < c ∧ c < s(a) ∧ Intro : 163, 167
167. set(s(0)) = set(c) → Elim : 154, 168
168. 0 < c ∧ c < a ∧ Intro : 163, 158
169. (0 < c ∧ c < a) → set(c) = set(s(c)) ∀ Elim : 145
170. set(c) = set(s(c)) → Elim : 170, 171
171. set(s(0)) = set(s(c)) = Elim : 169, 172
172. set(s(0)) = set(s(c)) ∨ Elim : 159, 160-162, 163-173
173. (0 < s(c) ∧ s(c) < s(a)) → set(s(0)) = set(s(c)) → Intro : 155-174
174. ∀x ((0 < x ∧ x < s(a)) → set(s(0)) = set(x)) Peano Induction : 154-175, 153
175. (0 < a ∧ a < s(a)) → set(s(0)) = set(a) ∀ Elim : 176
176. set(s(0)) = set(a) → Elim : 177, 138
177. set(s(0)) = set(a) → set(s(0)) ⊆ set(a) ∀ Elim : 58
178. set(s(0)) ⊆ set(a) → Elim : 178, 179
179. set(s(a)) ⊆ set(s(0)) ∧ set(s(0)) ⊆ set(a) ∧ Intro : 108, 180
180. (set(s(a)) ⊆ set(s(0)) ∧ set(s(0)) ⊆ set(a)) → set(s(a)) ⊆ set(a) ∀ Elim : 35
181. set(s(a)) ⊆ set(a) → Elim : 181, 182
182. set(a) ⊆ set(s(a)) ∧ set(s(a)) ⊆ set(a) ∧ Intro : 140, 183
183. (set(a) ⊆ set(s(a)) ∧ set(s(a)) ⊆ set(a)) → set(a) = set(s(a)) ∀ Elim : 54
184. set(a) = set(s(a)) → Elim : 184, 185
185. set(b) = set(s(b)) = Elim : 148, 186
186. b < a
187. 0 < b ∧ b < a ∧ Intro : 110, 188
188. (0 < b ∧ b < a) → set(b) = set(s(b)) ∀ Elim : 145
189. set(b) = set(s(b)) → Elim : 189, 190
190. set(b) = set(s(b)) ∨ Elim : 147, 148-187, 188-191
191. set(b) = set(s(b)) ∨ Elim : 105, 112-123, 124-192
192. ∀x ((0 < x ∧ x < s(a)) → set(x) = set(s(x))) ∀ Intro : 109-193
193. (∀x ((0 < x ∧ x < s(a)) → set(x) ⊆ set(s(x))) ∧ set(s(a)) ⊆ set(s(0))) → ∀x ((0 < x ∧ x < s(a)) → set(x) = set(s(x))) → Intro : 106-194
194. 0 < s(a) → ((∀x ((0 < x ∧ x < s(a)) → set(x) ⊆ set(s(x))) ∧ set(s(a)) ⊆ set(s(0))) → ∀x ((0 < x ∧ x < s(a)) → set(x) = set(s(x)))) → Intro : 104-195
195. ∀y (0 < y → ((∀x ((0 < x ∧ x < y) → set(x) ⊆ set(s(x))) ∧ set(y) ⊆ set(s(0))) → ∀x ((0 < x ∧ x < y) → set(x) = set(s(x))))) Peano Induction : 102, 103-196
• Oh, jesus. +1, on your third answer. :P – Frpzzd Jul 8 '17 at 16:30
• @Nilknarf Ha! Your +1 made my 2 hours of effort totally worth it! :) – Bram28 Jul 8 '17 at 18:41
• I looked over the proof (well, kind of) and I would guess that it re-indexed the subscripts. True or not a meaningful question? – CopyPasteIt Jul 8 '17 at 19:28
• @MikeMathMan Do you think that because for my inductive bases I use $0$ instead of $1$? – Bram28 Jul 8 '17 at 19:32
• @MikeMathMan No, the Fitch system is really a bare bones system of pure logic, so there are no built-in structures like sequences. – Bram28 Jul 8 '17 at 20:14

Assume $(A_i)$ is an indexed family of $n$ sets, with $i \in \Bbb Z_n$ (mod n addition) and that for every $i$, $A_i \subset A_{i+1}$.

If we can show that for any $i, j \in \Bbb Z_n$, $A_i \text{( = B)} \subset A_j \text{( = C)}$, then we will have proved that all the sets are equal. If $j = i +1$, no demonstration is necessary. So assume $j \ne i +1$. Since $A_i \subset A_{i+1}$ and $A_{i+1} \subset A_{i+2}$, $\;A_i \subset A_{i+2}$. We can therefore remove $A_{i+1}$ and reindex the cyclic inclusion chain with a new $\Bbb Z_{n-1}$, keeping track of the index assigned to both $B$ and $C$.

Now simply continue removing sets until $C$ is 'on the right' of $B$.

• No, I did a proof for that part. I was merely asking whether the proof of my lemma was sufficient as a proof of that lemma in particular, not sufficient to prove the entire thing. – Frpzzd Jul 8 '17 at 18:46
• OK, got rid of my opening remarks. I must be going crazy worrying about something so simple!!! I just gave another formal proof (different answer). I call my approach, not naive set theory, but circumspect set theory. I want something that works in 'any reasonable' set theoretic framework. – CopyPasteIt Jul 8 '17 at 19:09

Two Formal Proof (no re-indexing of the set subscripts is necessary here) depending on the same lemma.

Let $(A_i)$ be a fixed indexed family of $n$ sets, with $i \in [1, n]$, such that for every $i \lt n$,
$A_i \subset A_{i+1} \text{ AND } A_n \subset A_1$.

Lemma: If $n \gt 2$, then the indexed family $(A_i)$ with $i \in [1, n-1]$ satisfies the same cyclic inclusion chain: for every $i \lt n-1$, $\,A_i \subset A_{i+1} \text{ AND } A_{n-1} \subset A_1$.
Proof: Use transitivity of the inclusion relation.

Note that you can keep applying this lemma until you are 'down to' just two sets, $A_1$ and $A_2$ each contained in the other, so that $A_1 = A_2$.

Proof 1:

The equality relation is (always) transitive, so in particular,
$\text{IF } z = x \text{ AND } x = y \text{ THEN } z = y$

So, if we can show that $A_i = A_1$ for all $i$, the proof will be complete. To obtain a contradiction, suppose we have $A_1 = A_{i}$ for $1 \lt i \lt k \le n$, but $A_1 \ne A_k$. By the lemma, we can assume $k = n$ since the setup still holds. But if $k = n$ we have $A_k = A_n \subset A_1$, and $A_1 = A_{k-1} \subset A_k$, so that $A_1 = A_k$, a contradiction.

Proof 2:

Using the lemma you get that $A_1 = A_2$. But letting $n$ back up to $3$, there are now only two sets (to examine), and since each is contained in the other, they are equal. Now let $n$ ascend, one step at a time, back up to the full $n$ sets under consideration, and checking just two at a time, they will all be equal.