« first day (1191 days earlier)      last day (998 days later) » 

12:34 AM
And these are the modified ℝ axioms:
Add the type ℝ, ℝ[≠0] = { x : x∈ℝ ∧ x≠0 }, the symbols and operations of PA and the operations of ℚ (ℝ is an ordered field).
[closure] ∀x,y∈ℝ (x+y∈ℝ).
[closure] ∀x,y∈ℝ (x⋅y∈ℝ).
[closure] ∀x,y∈ℝ (x-y∈ℝ).
...
[ℚ ⊆ ℝ] ∀x∈ℚ ( x∈ℝ )
[field] ∀x∈ℝ ∀y∈ℝ[≠0] ( x = y·(x/y) ) @axiom
[complete] ∀S⊆ℝ ( ∃u∈ℝ ∀x∈S ( x≤u ) ⇒ ∃m∈ℝ ( ∀x∈S ( x≤m ) ∧ ∀u∈ℝ ( ∀x∈S ( x≤u ) ⇒ m≤u ) ) )
 
 
13 hours later…
1:39 PM
@F.Zer If you want division, then you need a closure axiom for /, otherwise even ∀x∈ℚ ∀y∈ℚ[≠0] ( x = y·(x/y) ) fails to control the behaviour of "x/y" even for x∈ℚ and y∈ℚ[≠0].
Similarly for division for ℝ.
I would also be more careful to say "reuse the symbols of PA" since we literally want to reuse them (not add them). And you should make a note there that it so happens that we can axiomatize ℕ,ℤ,ℚ,ℝ this way and that it is non-trivial to actually construct ℤ,ℚ,ℝ in the base system (PA plus Set Theory) and extend the operations on ℕ to them in the manner that satisfies the axiomatizations here.
 
2:06 PM
@user21820 Fantastic. Thank you. This is my next attempt.
Add the type ℝ, ℝ[≠0] = { x : x∈ℝ ∧ x≠0 }, reuse the symbols and operations of PA and the operations of ℚ (ℝ is an ordered field).
We can axiomatize ℕ,ℤ,ℚ,ℝ this way and it is non-trivial to actually construct ℤ,ℚ,ℝ in the base system (PA plus Set Theory) and extend the operations on ℕ to them in the manner that satisfies the axiomatizations here.
[closure] ∀x,y∈ℝ (x+y∈ℝ).
[closure] ∀x,y∈ℝ (x⋅y∈ℝ).
[closure] ∀x,y∈ℝ (x-y∈ℝ).
[closure] ∀x∈ℝ ∀y∈ℝ[≠0] (x/y∈ℝ).
 
@F.Zer Right. That closure axiom is precisely what you need.
Same for ℚ!
 
Hello
 
@Christina Hello!
 
Add the type ℚ, ℚ[≠0] = { x : x∈ℚ ∧ x≠0 }, reuse the symbols and operations of PA and the operations of ℤ (ℚ is an ordered field).
We can axiomatize ℕ,ℤ,ℚ,ℝ this way and it is non-trivial to actually construct ℤ,ℚ,ℝ in the base system (PA plus Set Theory) and extend the operations on ℕ to them in the manner that satisfies the axiomatizations here.
[closure] ∀x,y∈ℚ (x+y∈ℚ).
[closure] ∀x,y∈ℚ (x⋅y∈ℚ).
[closure] ∀x,y∈ℚ (x-y∈ℚ).
[closure] ∀x∈ℚ ∀y∈ℚ[≠0] (x/y∈ℚ).
 
3 messages moved to Sandbox
 
2:13 PM
It should be correct, now.
@user21820, I've proved two theorems (one without using induction and the other using it. Do you think they are correct ?
Theorem. For every integer x, the remainder when x^2 is divided by 4 is either 0 or 1. From: Daniel J. Velleman. "*HOW TO PROVE IT: A Structured Approach, Second Edition*" (p. 153)
  Given x ∈ ℤ:
    ∀m∈ℤ ( even(m) ⋁ odd(m) ) [lemma]
    even(x) ⋁ odd(x) [lemma]
    If even(x):
      Let k ∈ ℤ such that x = 2·k
      x·x = 2·k·x
      2·k·x = 4·k·k
      x·x = 4·k·k
      x·x = 4·(k·k) ∨ x·x = 4·(k·k) + 1
      ∃m ∈ ℤ ( x·x = 4·m ⋁ x·x = 4·m + 1 )
    If odd(x):
      Let a ∈ ℤ such that x = 2·a+1
For every natural x, the remainder when x^2 is divided by 4 is either 0 or 1.
  P(x) ≡ ∃ m ∈ ℕ ( x^2 = 4·m ⋁ x^2 = 4·m + 1 )
  x^2 = 4·0
  x^2 = 4·0 ⋁ x^2 = 4·0 + 1
  ∃ m ∈ ℕ ( x^2 = 4·m ⋁ x^2 = 4·m + 1 )
  P(0)
  Given k ∈ ℕ:
    If P(k):
      ∃ m ∈ ℕ ( k^2 = 4·m ⋁ k^2 = 4·m + 1 )
      Let a ∈ ℕ such that k^2 = 4·a ⋁ k^2 = 4·a + 1
      If k^2 = 4·a:
        ∀k∈ℕ ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 )
        ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 )
        k = 2·b ∨ k = 2·b +1
        If k = 2b:
          (k+1)^2 = k^2 + 2k + 1
 
@F.Zer Wait. Your parenthetical remark would more appropriately be "(ℚ is an ordered ring containing ℤ)", and you need to say that you add "/".
And similarly for ℝ "(ℝ is an ordered field containing ℚ)".
 
@user21820 Add the type ℚ, ℚ[≠0] = { x : x∈ℚ ∧ x≠0 }, reuse the symbols and operations of PA, add the binary operation / (ℚ is an ordered ring containing ℤ).
 
@F.Zer Correct. Don't you recall doing essentially the same thing when you proved (PA2) using (PA1)?
@F.Zer If you put the parenthetical remark at that point, you should say "ordered field".
 
@user21820 Add the type ℝ, ℝ[≠0] = { x : x∈ℝ ∧ x≠0 }, reuse the symbols and operations of PA, add the binary operation / (ℝ is an ordered field containing ℚ).
 
We reuse the symbols because ℚ contains ℤ and is also an ordered ring, and we add / because ℚ is a field.
 
2:18 PM
@user21820 Fixed it. Thank you.
@user21820 Saying "ℚ is an ordered ring containing ℤ" implies we can reuse the operations of ℤ ? So, we don't have to explicitly say it ?
 
@F.Zer Your induction proof is broken because you claim "x^2 = 4·0"...
@F.Zer No it doesn't imply that.
It's merely the pragmatic reason why we reuse the operations.
 
@user21820 Good. I understand. Then, we are explicitly adding the axioms. So, it is clear that we are reusing the operations.
@user21820 Let me check.
 
@F.Zer And it's also broken for other much more serious reasons...
 
@user21820, I forgot to add the header for ℤ.
Add the type ℤ, reuse the symbols and operations of PA, add the unary operation – and the binary operation – (ℤ is an ordered ring containing ℕ).
We can axiomatize ℕ,ℤ,ℚ,ℝ this way and it is non-trivial to actually construct ℤ,ℚ,ℝ in the base system (PA plus Set Theory) and extend the operations on ℕ to them in the manner that satisfies the axiomatizations here.
[closure] ∀x,y∈ℤ (x+y∈ℤ).
[closure] ∀x,y∈ℤ (x⋅y∈ℤ).
[closure] ∀x,y∈ℤ (x–y∈ℤ).
@user21820 Yes, I recall !
I will fix everything in my induction proof.
@user21820 I will prove the base case. Could you tell me what do you think ?
Define P(x) ≡ ∃ m ∈ ℕ ( x^2 = 4·m ⋁ x^2 = 4·m + 1 )
0^2 = 4·0
0^2 = 4·0 ⋁ 0^2 = 4·0 + 1
∃ m ∈ ℕ ( 0^2 = 4·m ⋁ 0^2 = 4·m + 1 )
P(0)
I see one of my errors. I dragged the lemma "∀k∈ℕ ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 )" below "Given k:"..."k" appears in a ∀ header, so it is used.
For every natural x, the remainder when x^2 is divided by 4 is either 0 or 1.
  Define P(x) ≡ ∃ m ∈ ℕ ( x^2 = 4·m ⋁ x^2 = 4·m + 1 )
  0^2 = 4·0
  0^2 = 4·0 ⋁ 0^2 = 4·0 + 1
  ∃ m ∈ ℕ ( 0^2 = 4·m ⋁ 0^2 = 4·m + 1 )
  P(0)
  Given k ∈ ℕ:
    If P(k):
      ∃ m ∈ ℕ ( k^2 = 4·m ⋁ k^2 = 4·m + 1 )
      Let a ∈ ℕ such that k^2 = 4·a ⋁ k^2 = 4·a + 1
      If k^2 = 4·a:
        ∀k'∈ℕ ∃m∈ℕ ( k' = m·2 ∨ k' = m·2+1 )
        ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 )
        Let b ∈ ℕ such that k = 2·b ∨ k = 2·b +1
        If k = 2b:
@user21820, My induction proof was an absolute disaster. I've corrected everything.
 
2:45 PM
No you haven't. The absolute disaster is still there. The other errors are actually not as bad as the remaining one.
 
@user21820 Ok. Will fix it.
 
Besides, it makes no sense to use induction when the statement is just (PA2), which you already proved using (PA1).
Not exactly the same, but almost.
 
@user21820 I assumed k^2 = 4·a...
That's the error.
My outline is so big, that I sometimes lose the place and copy wrong statements. I will look for other ways of dealing with it.
I will do it from scratch.
 
But why is your first proof not good enough? Furthermore, your first proof works for ℤ.
 
@user21820 I have to solve my induction proof. Don't want to move away from such an important concept :-)
 
2:54 PM
Lol but once you use the odd/even fact the induction becomes completely useless!
It's like you already put glue to seal the envelope but then you still take up a hammer to bang it shut.
 
@user21820 Haha. Is it possible to do it without that fact ?
@user21820 What does "bang it shut" mean ?
 
Jun 5 at 16:14, by user21820
You tried to use an induction axiom of that sort for (PA2). You failed to find a proof. That's not surprising, because PA1's proof uses an induction axiom that doesn't look like (PA2).
@F.Zer It's possible to do an induction proof for (PA2) without using (PA1), and it's up to you if you want to try.
I didn't encourage you earlier because it's the 'wrong' approach. But since you so badly want to try, why not.
@F.Zer "hit it with a bang to make it shut/close".
It was supposed to be an analogy: Hammers are meant for banging nails, not for banging everything you see around you. =)
 
@user21820 Hahaha. That's very funny.
 
I still think you shouldn't bother trying to get a proof for (PA2) without using (PA1). If you do try, it should be only to experience why it is the wrong approach, and not to try to find a way to make it work.
 
@user21820 Thank you for the advice. I will not bother, then. I will make one or two attempts only if I have some spare time.
 
3:04 PM
Basically, the issue is that you would have get ( 4 | k^2 ∨ 4 | k^2+3 ⊢ 4 | (k+1)^2 ∨ 4 | (k+1)^2+3 ), but every way to do this begs for (PA1) to be used.
 
In the meantime, this is the corrected proof using PA1.
@user21820, I am surprised this didn't use the induction hypothesis. What do you think ?
For every natural x, the remainder when x^2 is divided by 4 is either 0 or 1.
  Define P(x) ≡ ∃ m ∈ ℕ ( x^2 = 4·m ⋁ x^2 = 4·m + 1 )
  0^2 = 4·0
  0^2 = 4·0 ⋁ 0^2 = 4·0 + 1
  ∃ m ∈ ℕ ( 0^2 = 4·m ⋁ 0^2 = 4·m + 1 )
  P(0)
  Given k ∈ ℕ:
    If P(k):
      ∀k'∈ℕ ∃m∈ℕ ( k' = m·2 ∨ k' = m·2+1 )
      ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 )
      Let b ∈ ℕ such that k = 2·b ∨ k = 2·b +1
      If k = 2b:
        (k+1)^2 = 4·(b^2 + b) + 1
        (k+1)^2 = 4·(b^2 + b) ∨ 4·(b^2 + b) + 1
        ∃ m ∈ ℕ ( (k+1)^2 = 4·m ⋁ (k+1)^2 = 4·m + 1 )
 
11 mins ago, by user21820
Lol but once you use the odd/even fact the induction becomes completely useless!
 
@user21820, Because there is no need to use induction ! I understood !
 
Right.
 
Clicked
 
3:06 PM
You already did the same in your (PA2) proof.
 
@user21820 Yes, although this time it really clicked on me.
 
Good!
 
@user21820 I will go out a moment. Thank you and see you !
 
You're welcome. See you!
 
3:24 PM
1 ∀x ∈ S ∀y ∈ S: (Pxy -> Qx)
2 ∀x ∈ S ∃y ∈ S: Pxy

3 Given w ∈ S:
4	∃y ∈ S Pwy \\from 2,3
5	Let z ∈ S s.t. Pwz
6	Pwz -> Qz \\from 1
7	∃y ∈ S Pwy -> Qw
8 ∀x ∈ S ∃y ∈ S: Pxy -> Qx
quick question! would the above reasoning be correct?
I need to prove that, given 1 and 2, it follows that 8. I've begun using your system of proof for all my math hehe
 
3:56 PM
∀x∈B∀y∈B∀z∈B(p(x)=p(y)∧p(y)=p(z)⇒x=y∨y=z∨z=x)
Give¬ a∈S
   If ¬∃x∈B(p(x)=a)
      Give¬ d∈s
         If P(d)=a
            If ¬(d=a)
               ¬∃x∈B(p(x)=a)
               ¬∃x∈B(p(x)=a)⇒∀x∈B(¬(p(x)=a)).
               ∀x∈B(¬(p(x)=a)).
               ¬(p(d)=a)
               ⊥
            d=a
            d=a∨d=a
         p(d)=a⇒d=a∨d=a
      ∀d∈B(p(d)=a⇒d=a∨d=a)
      ∀w∈B(p(w)=a⇒w=a∨w=a) [rename]
      ∃z∈B∀w∈B(p(w)=a⇒w=a∨w=z)
      ∃y∈B∃z∈B∀w∈B(p(w)=a⇒w=y∨w=z)


   If ∃x∈B(p(x)=a)
      .
@user21820 Is the first half of the case split correct?
 
@shintuku That's correct!
 
nice! thank you very much!
I'm finally getting a hang of it, thanks for the help!
 
@Prithubiswas That's correct! You realized that when there is no in-edge to a then you can use a as the witness for the desired claim. However, you can save a few lines because from "p(d)=a" you already get "∃x∈B ( p(x)=a )" which yields the contradiction you want.
(You don't have to go through ( ¬∃ ⇒ ∀¬ ).)
 
4:13 PM
user21820, i've begun building zfc set theory in your system. I was wondering, what's the justification for [{x,y} ∈ A] -> [x ∈ {x,y} ∈ A]? Is it the axiom of choice?
and it would be so cool if you had set theory exercises! i would do them all!
 
4:41 PM
@shintuku I don't understand the question. "a∈b∈c" is merely short-hand for "a∈b ∧ b∈c".
And x∈{x,y} is trivial (by Pairing).
 
oh, right. But we wouldn't be able to use pairing for x ∈ {x,y,z}, right?
 
Yes, but you can take Union({{x,y},{y,z}}).
 
niiiice, good idea
thank you very much
 

« first day (1191 days earlier)      last day (998 days later) »