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?

|cite|improve this question
$\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.

|cite|improve this answer
$\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$.

|cite|improve this answer
$\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.

|cite|improve this answer
$\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.

|cite|improve this answer
$\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$

|cite|improve this answer
$\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.

|cite|improve this answer
$\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
  98. ¬0 < 0 ∀ Elim : 6
  99. ⊥ ⊥ Intro : 98, 99
  100. (∀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
  101. 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
  102. :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))))
  103. 0 < s(a)
  104. a = 0 ∨ 0 < a ∀ Elim : 10
  105. ∀x ((0 < x ∧ x < s(a)) → set(x) ⊆ set(s(x))) ∧ set(s(a)) ⊆ set(s(0))
  106. ∀x ((0 < x ∧ x < s(a)) → set(x) ⊆ set(s(x))) ∧ Elim : 106
  107. set(s(a)) ⊆ set(s(0)) ∧ Elim : 106
  108. :b 0 < b ∧ b < s(a)
  109. 0 < b ∧ Elim : 109
  110. b < s(a) ∧ Elim : 109
  111. a = 0
  112. b < s(0) = Elim : 112, 111
  113. b < s(0) → (b = 0 ∨ b < 0) ∀ Elim : 11
  114. b = 0 ∨ b < 0 → Elim : 113, 114
  115. b = 0
  116. 0 < 0 = Elim : 116, 110
  117. ⊥ ⊥ Intro : 117, 13
  118. b < 0
  119. ¬b < 0 ∀ Elim : 12
  120. ⊥ ⊥ Intro : 119, 120
  121. ⊥ ∨ Elim : 115, 116-118, 119-121
  122. set(b) = set(s(b)) ⊥ Elim : 122
  123. 0 < a
  124. (∀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
  125. :c 0 < c ∧ c < a
  126. 0 < c ∧ Elim : 126
  127. c < a ∧ Elim : 126
  128. a < s(a) ∀ Elim : 8
  129. c < a ∧ a < s(a) ∧ Intro : 128, 129
  130. (c < a ∧ a < s(a)) → c < s(a) ∀ Elim : 9
  131. c < s(a) → Elim : 130, 131
  132. 0 < c ∧ c < s(a) ∧ Intro : 127, 132
  133. (0 < c ∧ c < s(a)) → set(c) ⊆ set(s(c)) ∀ Elim : 107
  134. set(c) ⊆ set(s(c)) → Elim : 133, 134
  135. ∀x ((0 < x ∧ x < a) → set(x) ⊆ set(s(x))) ∀ Intro : 126-135
  136. a < s(a) ∀ Elim : 8
  137. 0 < a ∧ a < s(a) ∧ Intro : 124, 137
  138. (0 < a ∧ a < s(a)) → set(a) ⊆ set(s(a)) ∀ Elim : 107
  139. set(a) ⊆ set(s(a)) → Elim : 138, 139
  140. set(a) ⊆ set(s(a)) ∧ set(s(a)) ⊆ set(s(0)) ∧ Intro : 140, 108
  141. (set(a) ⊆ set(s(a)) ∧ set(s(a)) ⊆ set(s(0))) → set(a) ⊆ set(s(0)) ∀ Elim : 35
  142. set(a) ⊆ set(s(0)) → Elim : 141, 142
  143. ∀x ((0 < x ∧ x < a) → set(x) ⊆ set(s(x))) ∧ set(a) ⊆ set(s(0)) ∧ Intro : 136, 143
  144. ∀x ((0 < x ∧ x < a) → set(x) = set(s(x))) → Elim : 125, 144
  145. b < s(a) → (b = a ∨ b < a) ∀ Elim : 11
  146. b = a ∨ b < a → Elim : 111, 146
  147. b = a
  148. 0 < 0 ∧ 0 < s(a)
  149. 0 < 0 ∧ Elim : 149
  150. ⊥ ⊥ Intro : 150, 13
  151. set(s(0)) = set(0) ⊥ Elim : 151
  152. (0 < 0 ∧ 0 < s(a)) → set(s(0)) = set(0) → Intro : 149-152
  153. :c (0 < c ∧ c < s(a)) → set(s(0)) = set(c)
  154. 0 < s(c) ∧ s(c) < s(a)
  155. s(c) < s(a) ∧ Elim : 155
  156. s(c) < s(a) → c < a ∀ Elim : 7
  157. c < a → Elim : 156, 157
  158. c = 0 ∨ 0 < c ∀ Elim : 10
  159. c = 0
  160. set(s(0)) = set(s(0)) = Intro
  161. set(s(0)) = set(s(c)) = Elim : 160, 161
  162. 0 < c
  163. a < s(a) ∀ Elim : 8
  164. c < a ∧ a < s(a) ∧ Intro : 158, 164
  165. (c < a ∧ a < s(a)) → c < s(a) ∀ Elim : 9
  166. c < s(a) → Elim : 165, 166
  167. 0 < c ∧ c < s(a) ∧ Intro : 163, 167
  168. set(s(0)) = set(c) → Elim : 154, 168
  169. 0 < c ∧ c < a ∧ Intro : 163, 158
  170. (0 < c ∧ c < a) → set(c) = set(s(c)) ∀ Elim : 145
  171. set(c) = set(s(c)) → Elim : 170, 171
  172. set(s(0)) = set(s(c)) = Elim : 169, 172
  173. set(s(0)) = set(s(c)) ∨ Elim : 159, 160-162, 163-173
  174. (0 < s(c) ∧ s(c) < s(a)) → set(s(0)) = set(s(c)) → Intro : 155-174
  175. ∀x ((0 < x ∧ x < s(a)) → set(s(0)) = set(x)) Peano Induction : 154-175, 153
  176. (0 < a ∧ a < s(a)) → set(s(0)) = set(a) ∀ Elim : 176
  177. set(s(0)) = set(a) → Elim : 177, 138
  178. set(s(0)) = set(a) → set(s(0)) ⊆ set(a) ∀ Elim : 58
  179. set(s(0)) ⊆ set(a) → Elim : 178, 179
  180. set(s(a)) ⊆ set(s(0)) ∧ set(s(0)) ⊆ set(a) ∧ Intro : 108, 180
  181. (set(s(a)) ⊆ set(s(0)) ∧ set(s(0)) ⊆ set(a)) → set(s(a)) ⊆ set(a) ∀ Elim : 35
  182. set(s(a)) ⊆ set(a) → Elim : 181, 182
  183. set(a) ⊆ set(s(a)) ∧ set(s(a)) ⊆ set(a) ∧ Intro : 140, 183
  184. (set(a) ⊆ set(s(a)) ∧ set(s(a)) ⊆ set(a)) → set(a) = set(s(a)) ∀ Elim : 54
  185. set(a) = set(s(a)) → Elim : 184, 185
  186. set(b) = set(s(b)) = Elim : 148, 186
  187. b < a
  188. 0 < b ∧ b < a ∧ Intro : 110, 188
  189. (0 < b ∧ b < a) → set(b) = set(s(b)) ∀ Elim : 145
  190. set(b) = set(s(b)) → Elim : 189, 190
  191. set(b) = set(s(b)) ∨ Elim : 147, 148-187, 188-191
  192. set(b) = set(s(b)) ∨ Elim : 105, 112-123, 124-192
  193. ∀x ((0 < x ∧ x < s(a)) → set(x) = set(s(x))) ∀ Intro : 109-193
  194. (∀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
  195. 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
  196. ∀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
|cite|improve this answer
$\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$.

|cite|improve this answer
$\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.

|cite|improve this answer
$\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.