8
$\begingroup$

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?

$\endgroup$
  • 3
    $\begingroup$ 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". $\endgroup$ – user247327 Jul 7 '17 at 17:29
  • 1
    $\begingroup$ @user247327 That's why I'm asking... I don't have a rigid definition of that. $\endgroup$ – Frpzzd Jul 7 '17 at 17:30
  • 1
    $\begingroup$ 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. $\endgroup$ – Jack M Jul 7 '17 at 19:28
  • 5
    $\begingroup$ @Wildcard In many literatures the proper subset symbol is defined instead to allow improper subsets so it's a matter of convention. $\endgroup$ – Henricus V. Jul 8 '17 at 6:25
  • 1
    $\begingroup$ @Wildcard, you are using “by definition” incorrectly. $\endgroup$ – Carsten S Jul 8 '17 at 8:59
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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)$. $\endgroup$ – Mark S. Jul 8 '17 at 15:20
  • $\begingroup$ @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)? $\endgroup$ – drhab Jul 8 '17 at 16:14
  • $\begingroup$ "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. $\endgroup$ – Mark S. Jul 8 '17 at 16:26
10
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ It is also possible to start the induction at $n=1$. $\endgroup$ – user133281 Jul 8 '17 at 10:00
  • $\begingroup$ @user133281 $n=1$ isn't really possible. There are at least two sets involved. $\endgroup$ – Henno Brandsma Jul 8 '17 at 12:34
  • $\begingroup$ 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.) $\endgroup$ – LSpice Mar 21 '18 at 23:25
7
$\begingroup$

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.

$\endgroup$
  • 5
    $\begingroup$ 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. $\endgroup$ – Kevin Jul 8 '17 at 1:28
  • 1
    $\begingroup$ @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. $\endgroup$ – Ethan Bolker Jul 8 '17 at 13:05
4
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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$

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Eric Towers Jul 12 '17 at 3:57
  • $\begingroup$ @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$ $\endgroup$ – Bram28 Jul 12 '17 at 11:13
4
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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
$\endgroup$
  • $\begingroup$ Oh, jesus. +1, on your third answer. :P $\endgroup$ – Frpzzd Jul 8 '17 at 16:30
  • $\begingroup$ @Nilknarf Ha! Your +1 made my 2 hours of effort totally worth it! :) $\endgroup$ – Bram28 Jul 8 '17 at 18:41
  • $\begingroup$ I looked over the proof (well, kind of) and I would guess that it re-indexed the subscripts. True or not a meaningful question? $\endgroup$ – CopyPasteIt Jul 8 '17 at 19:28
  • $\begingroup$ @MikeMathMan Do you think that because for my inductive bases I use $0$ instead of $1$? $\endgroup$ – Bram28 Jul 8 '17 at 19:32
  • 1
    $\begingroup$ @MikeMathMan No, the Fitch system is really a bare bones system of pure logic, so there are no built-in structures like sequences. $\endgroup$ – Bram28 Jul 8 '17 at 20:14
1
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Frpzzd Jul 8 '17 at 18:46
  • $\begingroup$ 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. $\endgroup$ – CopyPasteIt Jul 8 '17 at 19:09
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.