Basic Mathematics - 2021-07-30

« first day (1179 days earlier) ← previous day next day → last day (1020 days later) »

9:54 AM

@F.Zer There are a lot of gaps, the biggest of which is "m is odd or m is even". You didn't prove that, and it's a critical piece. Using that, there is actually a much easier proof via ∀m,n∈ℤ ( ¬even(m) ∧ ¬even(n) ⇒ ¬even(m·n) ).

But it's an interesting idea that you had, which boils down to: If m = 2·l+1 then m·n = 2·l·n+n and that's why you wanted to subtract 2·l·n from both sides.

@F.Zer The axioms for ℝ are same as the axioms for ℚ (change every "ℚ" to "ℝ") except that the last two are ∀x∈ℚ ( x∈ℝ ) and the dedekind-completeness axiom:

> ∀S⊆ℝ ( ∃u∈ℝ ∀x∈S ( x≤u ) ⇒ ∃m∈ℝ ( ∀x∈S ( x≤m ) ∧ ∀u∈ℝ ( ∀x∈S ( x≤u ) ⇒ m≤u ) ) ).

If you abuse notation a bit and write "S≤u" to mean "∀x∈S ( x≤u )" where x is an unused variable, then this is:

> ∀S⊆ℝ ( ∃u∈ℝ S≤u ⇒ ∃m∈ℝ ( S≤m ∧ ∀u∈ℝ ( S≤u ⇒ m≤u ) ) ).

Which says "every subset of ℝ with an upper bound has a minimum upper bound".

Of course, "S⊆ℝ" means "S∈P(ℝ)" where "P" here is the power-set operation.

I forgot; we need one more axiom for both ℚ and ℝ for existence of multiplicative inverse.

∀x∈ℚ ( x≠0 ⇒ ∃y∈ℚ ( x·y=1 ) ). ∀x∈ℝ ( x≠0 ⇒ ∃y∈ℝ ( x·y=1 ) ).

So the axioms I have given you for ℚ minus "∀x∈ℚ ∃p,q∈ℤ ( q ≠ 0 ∧ p = q·x )" are the axioms for ordered fields that contain ℤ. (And every ordered field contains a copy of ℤ, but you don't need to care about that now.) Both ℚ and ℝ are ordered fields that contain ℤ, so they both satisfy every theorem you can prove from the ordered field axioms. These theorems also include the exercise you asked me about.

Notice that the (dedekind-)completeness axiom is the only axiom that goes beyond the structures involved. The others are all about ℕ,ℤ,ℚ,ℝ, so what you can prove from them don't involve set theory, since you can treat ℕ,ℤ,ℚ,ℝ as mere types. However, the completeness axiom involves set theory because it is useless without any axioms that allow you to prove existence of members of P(ℝ).

10:39 AM

@user21820 I asked about a textbook for Natural Deduction (fitch style).
https://math.stackexchange.com/questions/4207404/textbook-for-fitch-style-natural-deduction
And someone suggested me a book:
https://forallx.openlogicproject.org/forallxyyc.pdf
If you have read this book before , do you know if there are any conceptual errors?

11:19 AM

@Prithubiswas Yes, do NOT refer to that book. It has serious conceptual errors that caused multiple people to have conceptual errors that I only discovered when then asked me in my chat-rooms, which I then had to correct.

Also ignore that DC's proof software, as it is useless for practical mathematics and the author is almost a crank.

@user21820 Can you show me some of the conceptual errors of the book?

DC has the very obnoxious habit of spamming almost every thread on Math SE about introductory FOL with his advertisement, yet it's a useless software.

Regarding forallx, here are some serious issues that I mentioned before in my chat-rooms:

in Logic, May 28 '18 at 7:42, by user21820

@BillyRubina Actually I recommended forallx because it seemed to have a chapter describing a Fitch-style deductive system for first-order logic. Unfortunately, as I told you, after a few people asked me about it, I found mistakes (see here and here). After that, I decided I should not recommend it since readers would have all those misconceptions.

Nov 5 '20 at 14:20, by user21820

Not that forallx is wrong here; it isn't (because indeed ∧intro is a schema). Just that forallx is very wrong when it comes to some other parts.

The second one is not a mistake per se, but it is very poorly explained.

@Prithubiswas: Anyway, you need to stick to one deductive system. I strongly suggest you learn mine, but if you want to learn another one then learn LPL's and do not learn mine at the same time. This is because my system and LPL's, although both Fitch-style, have some differences that make them fundamentally incompatible. So you would be wasting your time and my time if you get confused due to the incompatibility.

I do guarantee that if you learn my system it is the fastest way to get all the way up to a full ZFC-strength foundation for mathematics, and I don't think any other system comes anywhere close. As you can see from what F.Zer and I have been discussing, we have already started doing ordinary mathematics while staying quite strictly within the same deductive system.

@user21820 Because forallx seems to have many inaccuracies and mistakes , and LPL seems to be a bit too wordy and has exercises which requires programmes that come with the paid version with the book , I will learn yours.

@Prithubiswas Ok. So have you finished more of my exercises yet? =)

@F.Zer: I keep forgetting that the completeness axiom is for non-empty set. I don't want to give an excuse, but perhaps one reason I keep forgetting is that this condition isn't needed for the extended reals (which includes −∞,∞ but is not a field, but is very useful in real analysis and measure theory). Here is the corrected completeness axiom:

> ∀S⊆ℝ ( S≠∅ ∧ ∃u∈ℝ ∀x∈S ( x≤u ) ⇒ ∃m∈ℝ ( ∀x∈S ( x≤m ) ∧ ∀u∈ℝ ( ∀x∈S ( x≤u ) ⇒ m≤u ) ) ).

And the shortened form:

> ∀S⊆ℝ ( S≠∅ ∧ ∃u∈ℝ ( S≤u ) ⇒ ∃m∈ℝ ( S≤m ∧ ∀u∈ℝ ( S≤u ⇒ m≤u ) ) ).

For example, you can prove ¬∃x∈ℚ ( x·x = 2 ) by using (PA4).

But you can also prove ∃x∈ℝ ( x·x = 2 ). These two demonstrate the simplest difference between ℚ and ℝ, and is what historically motivated investigation into irrational numbers.

However, the actual existence of the square-root of 2 was never proven axiomatically until much much later; it was just taken for granted that whatever length was constructible (using compass and straightedge given two points with distance 1) was also a real number. But since Galois, more than a millenia after Pythagoras, it is now known that the cube-root of 2 is not constructible... So arguably our real understanding of ℝ could only come after the axiomatization of reals, in Dedekind's time.

I will now give a proof of ∃x∈ℝ ( x·x = 2 ), just to demonstrate how the completeness axiom is used.

11:43 AM

Given x∈S
   Given y∈S
      Given z∈S
         If x=z ∧ y=z
            x=z
            y=z
            If ¬(y=z)
               ¬(x=z)
               x=z
               ⊥
            x=y
         x=z ∧ y=z ⇒ x=y

@user21820 attempt at Q4

@Prithubiswas This can't be right; you have the wrong conclusion after coming out from "If ¬(y=z)"..

Probably careless.

@user21820 Oh I think I wrote "If ¬(y=z)" instead of "If ¬(x=y)".

But you shouldn't be able to get a proof that way. Try and see.

Given x∈S
   Given y∈S
      Given z∈S
         If x=z ∧ y=z
            x=z
            y=z
            If ¬(x=y) [P := ¬(x=?)]
               ¬(x=z) [because y=z and P(y) with "=elim"]
               x=z
               ⊥
            x=y
         x=z ∧ y=z ⇒ x=y

@user21820 I still cant see where I am getting it wrong.Can you show where I am making a flase leap?

Oh wait, you're clever.

You couldn't do =elim directly because of the lack of symmetry, but you used contradiction to reverse it. Clever, clever.

A direct proof is possible:

Mar 23 at 14:00, by F. Zer

(Q4): ∀ x, y, z ∈ S ( x = z ∧ y = z ⇒ x = y)
Given x ∈ S:
	Given y ∈ S:
		Given z ∈ S:
			If x = z ∧ y = z:
				y = z
				y = y
				z = y
				x = z
				x = y
			 x = z ∧ y = z ⇒ x = y
		∀ z ∈ S  (x = z ∧ y = z ⇒ x = y)
	∀ y, z ∈ S ( x = z ∧ y = z ⇒ x = y)
∀ x, y, z ∈ S ( x = z ∧ y = z ⇒ x = y)

@Prithubiswas: So you found a proof without using =intro, while @F.Zer found a proof without contradiction.

12:10 PM

@user21820 I am having trouble understanding the part of FZer proof:

y = y
z = y

Here I think the property is P := ? = y.But doesn't that mean we can't write down P(y) [(y=y)] because there is an occurrence of y in property P.

I dont know if this is related or not , but you once said:

"Do you mean like P(t) ≡ t=x? Then ∀x∈S ( P(x) ) ≡ ∀x∈S ( x=x ) but we cannot rename to ∀y∈S ( P(y) ) ≡ ∀y∈S ( y=x ).
It is important that x does not appear in P at all, so that when you rename x to y, you do not miss any x and there is no conflict with any quantified variables in P.

@Prithubiswas That restriction was for the variable involved in the renaming. Properties in general may have any of the used variables.

The property here is P(?) ≡ ? = y, and it is allowed because the =elim rule only requires "unused variables appearing in P must not appear in F", which you can ignore for now as it is relevant only for set-builder notation.

Concerning the second part of my comment that you quoted, note that I said "there should not be any free variables", but here the "y" is a used variable, because you are under "Given y∈S:". So inside that subcontext P(?) ≡ ? = y does define a valid property.

@user21820 Can you show the definition of free and bound variables for your system?

It turns out that I already did. All you need are these:

> Used variable: A variable that is declared in the header of some containing ∀-subcontext or declared in some previous ∃-elimination ("let") step in the current context or some containing context.

> Unused variable: A variable that is not used.

And the FOL deductive rules, and the syntax rules for forming properties.

Let's explicitly see the proof of that property we're talking about via the syntax rules! (Refer here for the syntax rules for sentences, and modify accordingly to get properties.)

Given x,y,z∈S:
	y : term  [since x is a used variable]
	? : ?term
	? = y : ?bool

Here "?term" is used to indicate that it is a term that may have blanks, and same for "?bool". The rules for "?term" and "?bool" are identical to the rules for sentences except that you change every ": term" and every ": bool" to ": ?term" and ": ?bool" respectively, and you add:

> ? : ?term

Then a property is exactly all those things that you can deduce in front of ": ?bool".

@Prithubiswas: Is this clear enough?

12:35 PM

@user21820 I think you answered A different question (I will definitely read it because it seems important). You did define "Used variable" and "Unused variable" but haven't explicitly defined the terms "free" and "bound" in your Natural Deduction post.For example:

"The above rules avoid the usual trouble that most other systems have, where variables used for witnesses of existential statements must be distinguished from variables used for arbitrary objects. The reason is that every variable here is either specified by a ∀-subcontext or by a "let"-statement; in other words there are no **f…

@Prithubiswas Oh, you're not supposed to read "Notes" when you're just learning to use the system. =)

Basically, there isn't even a concept of "free variable" in my system, since you're only allowed to use a variable that is either declared in some ∀-subcontext header or in some ∃-elim step. So every variable in my system is in some sense "bound".

In other systems, which you can look at after you have fully understood my system, they may make different design choices. One design choice is whether to allow "free variables" or not. (This choice also shows up in programming languages, which unfortunately you don't know, but for reference C/C++/Java do not allow free variables whereas Javascript does.)

In particular, in other systems you may be able to prove the theorem "x = x" just like that, with no quantifiers at all. This is impossible in my system; the corresponding theorem that you can prove is "∀x∈obj ( x = x )".

@Prithubiswas: Anyway just to make sure you understand the precise meaning of properties, here is a more interesting example:

Given k∈ℕ:
	?,k : ?term
	? > k : ?bool
	Given d,x∈ℕ:
		1,d,? : ?term
		d·x : ?term
		1 < d , d < ? , ? = d·x : ?bool
		1 < d < ? ∧ ? = d·x : ?bool
	∃d,x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool
	¬∃d,x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool
	? > k ∧ ¬∃d,x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool

So in the context where k∈ℕ, we have a valid property "? > k ∧ ¬∃d,x∈ℕ ( 1 < d < ? ∧ ? = d·x )" which says "? is a prime bigger than k".

And this property can vary with the (used) variable k.

@F.Zer: Ok now I'm going to give you the proof I promised. Give me a moment.

Before that, let us define division / for ℝ×ℝ[≠0] via this mechanism just as we did with subtraction and negation, for convenience. That is, we can define the type ℝ[≠0] = { x : x∈ℝ ∧ x≠0 } and use the theorem ∀x∈ℝ ∀y∈ℝ[≠0] ∃z∈ℝ ( x = y·z ), which you can prove from the field axioms, and apply the rule to get ∀x∈ℝ ∀y∈ℝ[≠0] ( x = y·(x/y) ).

We can then prove some simple facts, such as:

> ∀x∈ℝ ( x/1 = x ).
> ∀x,z∈ℝ ∀y,w∈ℝ[≠0] ( (x/y)·(z/w) = (x·z)/(y·w) ).
> ∀x,y∈ℝ[≠0] ( 1/(x/y) = y/x ).

Also, note that ℝ[≠0] is a set (by comprehension), although we don't need that fact when just using the ordered field axioms.

One more important fact that you should prove:

> ∀x∈ℝ[≠0] ( x·x > 0 ).

For now I will stick to not using the exponentiation symbol, just to make it clear that we are not using anything more than multiplication.

1:10 PM

Thank you so much, @user21820. I will carefully review your explanations.

Here is the proof:

Let S = { x : x∈ℝ ∧ x·x ≤ 2 }.
(4/3)·(4/3) ≤ 2.
4/3 ∈ S.
S ≠ ∅.
Given x∈S:
	If x > 3/2:
		x > 0.
		3/2 > 0.
		x·x > x·(3/2) > (3/2)·(3/2) = 9/4 > 2 ≥ x·x.
		⊥.
	x ≤ 3/2.
S ≤ 3/2.
Let m∈ℝ such that S ≤ m ∧ ∀u∈ℝ ( S ≤ u ⇒ m ≤ u ).  [completeness]
4/3 ≤ m.  [by S ≤ m]
m ≤ 3/2.  [by ∀u∈ℝ ( S ≤ u ⇒ m ≤ u ) and S ≤ 3/2]
If m·m > 2:
	[we shall show that m is not the least upper bound for S]
	Let e = (m·m−2)/2.
	e > 0.
	e/m > 0.  [otherwise e = (e/m)·m ≤ 0·m = 0]
	m−e/m < m.
	m−e/m > 0.  [because e ≤ e·2 = m·m−2 ≤ (3/2)·(3/2)−2 = 1/4 and m·m ≥ (4/3)·(4/3) = 16/9]

Every good textbook on real analysis will give (their own) proof of the existence of sqrt(2) or something like that. There are many ways. Another way is to first prove some higher-powered results like IVT (intermediate value theorem for continuous functions), and then apply it to the function f : ℝ→ℝ given by f(x) = x^2−2 for each x∈ℝ, after proving that this f is continuous. This is certainly more complicated than the proof I just gave you, but in time you will get to these results.

1:25 PM

I need help understanding the first part of his answer, https://math.stackexchange.com/a/18087/695930
how does the orthonormality and the fact that x is reell implicate that A is the complex conjugate of B ?

@MadSpaces Let's just say it's circular, because proving that ( ℝ t ↦ exp(iωt) ) and ( ℝ t ↦ exp(−iωt) ) are orthonormal, which is the real claim needed, is just as difficult as proving the original question. Circular answers get high upvotes on Math SE all the time.

What d you mean with circular?

I am not really interested in a genuine mathematical rigerious proof, more of an intution kind of proof

@MadSpaces I already explained; the orthonormality is just as difficult to prove, so it is circular to use.

Intuition is not mathematics. If you're interested in a proper proof, I can give you one, but if you're not interested then this is not the right room.

i know

I am interested in some kind of mathematical intution, without doing the proof, makes sense?

So what do you want? Proof or no proof?

@MadSpaces It makes sense, but is frankly the wrong way around in this case, because only the rigorous proof will shed real light on the right intuition you need here.

1:32 PM

I understand, would you be interested nevertheless in "trying" to provide this mathematical intution without doing a proof step for step, or are you determined to not reply, other with a rigerious proof, which i understand if you choose to.

Orthogonality literally says that every pair (A,B) gives a unique function ( ℝ t ↦ A·exp(iωt)+B·exp(−iωt) ), so you can match coefficients if two pairs give the same function, otherwise some nonzero pair gives the zero function. But if you can't prove the original fact directly, trying to rely on such intuitive crutches will just result in worse mathematical understanding.

And "rigerious" ≠ "rigorous".

Alright mate, thanks for the help.

2:05 PM

@user21820 Here is my revised proof.

∀m,n∈ℤ ( ¬even(m) ∧ ¬even(n) ⇒ ¬even(m·n) ).
  Given m,n ∈ ℤ:
    If ¬even(m) ∧ ¬even(n):
      ∀k∈ℕ ( even(k) ⋁ odd(k) ) [Lemma]
      even(m) ∨ odd(m)
      odd(m)
      Let k ∈ ℤ such that m = 2·k+1
      If even(m·n):
        Let l ∈ ℤ such that m·n = 2·l
        m·n = 2·l·n+n
        2·l = 2·l·n+n
        (-2·l·n) ∈ ℤ
        2·l + (-2·l·n) = 2·l·n+n+(-2·l·n)
        2·l + (-2·l·n) = n
        2·((-1)·l·n) = n
        even(n)
        ⊥
      ¬even(m·n)
    ¬even(m) ∧ ¬even(n) ⇒ ¬even(m·n)
  ∀m,n∈ℤ ( ¬even(m) ∧ ¬even(n) ⇒ ¬even(m·n) )

And, the lemma used...

∀k∈ℕ ( Even(k) ⋁ Odd(k) ) [Lemma]
  Given k ∈ ℕ:
    ∀k∈ℕ ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 ) [PA1]
    ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 )
    Let m' such that k = m'·2 ⋁ k = m'·2+1
    If k = m'·2:
      ∃ y ∈ ℕ ( k = 2·y )
      Even(k)
      Even(k) ⋁ Odd(k)
    If k = m'·2+1:
      Odd(k)
      Even(k) ⋁ Odd(k)
    Even(k) ⋁ Odd(k)
  ∀k∈ℕ ( Even(k) ⋁ Odd(k) )

@F.Zer No no, how can you use a lemma for ℕ and apply it to ℤ?

@user21820 Sorry !

I will fix it.

@F.Zer That's why it's a big piece, because you need to use the axiom that relates ℤ with ℕ in order to apply (PA1).

Good.

I felt something was unexpectedly easy :-)

I don't know what Velleman expects, because I don't recall him being clear about what axioms one can use, but I suspect he just wanted a simple handwaving argument like "If m·n is even, then it cannot be that both m,n are odd since odd times odd is odd.".......

I mean, at the target audience level of that book (i.e. end of high-school), students sort of just assume all these 'basic facts' about integers.

@F.Zer So what you're doing, ironically, is already probably more complicated than what the book author wanted, but of course is what is necessary if you want to truly build from foundation up.

2:15 PM

@user21820 You're absolutely right. That's roughly the proof he gives.

user image

@user21820 Yes, I would like to build a good foundation.

@F.Zer Yea so just to be clear about what is the biggest gap, it is when he assumes that a non-even integer is equal to 2 times some integer plus 1. This cannot be proven without using induction, as we vaguely saw before using the interesting polynomials (but it's ok if you have forgotten).

@user21820 I remember about the proof using induction. On the other hand, I do not remember about the interesting polynomials.

Just to mention one intuitive argument that is a bit different from the induction: Intuitively, you can split into positive and negative case, and for positive you can keep subtracting 2 until it goes below 2, and then it must leave remainder 1. If you recall, this kind of idea is the same as the one behind the canonicalization tricks in (PA5).

Of course, there is no guarantee that you won't keep subtracting forever; that's what you need induction or well-ordering to exclude.

@user21820 Can I use induction in ℤ ? Perhaps, you are suggesting that I should use ∀x∈ℤ ( x∈ℕ ∨ −x∈ℕ ) in connection with PA1.

@F.Zer Yes.

2:21 PM

Good.

∀k∈ℤ ( even(k) ⋁ odd(k) ) [Lemma]
  ∀x∈ℕ ( x∈ℤ )
  ∀x∈ℤ ( x∈ℕ ∨ −x∈ℕ )
  Given k ∈ ℤ:
    k ∈ ℕ ∨ -k ∈ ℕ
    If k ∈ ℕ:
      ∀k∈ℕ ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 ) [PA1]
      ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 )
      Let m' such that k = m'·2 ⋁ k = m'·2+1
      If k = m'·2:
        ∃ y ∈ ℕ ( k = 2·y )
        even(k)
        even(k) ⋁ Odd(k)
      If k = m'·2+1:
        odd(k)
        even(k) ⋁ odd(k)
      even(k) ⋁ odd(k)
    If -k ∈ ℕ:
      ∀ k ∈ ℤ ( (-1)·k = -k ) [Lemma]
      ∀ k ∈ ℤ ( -(-k) = k ) [Lemma]

@user21820, this is the proof of the lemma. My second line is useless, I should note.

@F.Zer Nope. Your last few lines are wrong.

@user21820 I missed one line, I think.

k = (-1)·m'·2 + 1
∃ y ∈ ℕ ( k = 2·y + 1 )
odd(k)

No it's not about missing lines, but actual false statements you wrote.

Anyway, it is better to use addition and subtraction than to multiply by (−1), so that you don't need all those pesky lemmas.

@user21820 I will check.

Anyway, if something is missing I will ask for justification. When I say "wrong" it means "clearly erroneous deduction". =)

2:36 PM

@user21820 Yes, I see. m' ∈ ℕ and I am multiplying it by (-1).

@F.Zer That's not a problem. ℕ⊆ℤ.

@user21820 Oh, seems a very efficient method :-)

Just do the addition and subtraction to see what you should have gotten, and then you'll know what your error was.

@user21820 Good. I should add 2·k to both sides. I will do it.

@user21820 I know -k ∈ ℕ. However, I do not know k ∈ ℕ...

I cannot mix different types when doing addition (or multiplication). There are different sets of axioms.

@F.Zer That's not the error. I said already that ℕ⊆ℤ, so if you want to do arithmetic in ℤ you just check that everything is already in ℤ.

2:44 PM

@user21820 I see. Thank you.

@F.Zer And that's not what I wanted you to do, though that works and is simpler. I mean that in elementary school when you have −k = ... and you want to get k, you can just add and subtract appropriately.

Then you will get k = something and see your error in your original computation.

Although it turns out that in this special case you can just add 2·k because all you want is to show that k is odd so you don't care what mess you get on the other side.

@user21820 Mmm...I do not remember that trick. Will think.

... It's not that you don't remember. It's that you can't imagine yourself in elementary school again.

I should add k to both sides and subtract m'·2 from both sides.

-k + k = k + m'·2
-k + k + (-m'·2) = k + m'·2 + (-m'·2)
-m'·2 = k
even(k)

@user21820, this is what I got.

@F.Zer Correct. Your earlier argument using multiplication by (−1) was also correct. Now do the same (add and subtract) for the other case, for which your argument was wrong.

2:59 PM

k + k = m'·2+1+k
-k + k +(-m'·2) = m'·2+1+k+(-m'·2)
-m'·2 = k + 1
...
odd(k)

@user21820 Thank you. It is clear, now.

This is wrong, of course. "(-1)(-k) = (-1)·m'·2 + 1"

Yes.

On the other hand, as you noticed later, there is an easier way than subtracting, because you can just get from −k = m'·2+1 to k = k·2+m'·2+1 = (k+m')·2+1. So easy.

Even the addition is easy: −k+k·2 = −k+k+k = 0+k = k.

@user21820, Excellent.

-k + 2·k = m'·2+1+2k
k = 2·(m'+k) + 1
odd(k)

∀k∈ℤ ( even(k) ⋁ odd(k) ) [Lemma]
  ∀x∈ℤ ( x∈ℕ ∨ −x∈ℕ )
  Given k ∈ ℤ:
    k ∈ ℕ ∨ -k ∈ ℕ
    If k ∈ ℕ:
    If -k ∈ ℕ:
      ∀k∈ℕ ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 ) [PA1]
      ∃m∈ℕ ( -k = m·2 ∨ -k = m·2+1 )
      Let m' ∈ ℕ such that -k = m'·2 ⋁ -k = m'·2+1
      If -k = m'·2:
        -k + k = k + m'·2
        -k + k + (-m'·2) = k + m'·2 + (-m'·2)
        -m'·2 = k
        even(k)
        even(k) ⋁ odd(k)
      If -k = m'·2+1:
         -k + 2·k = m'·2+1+2k
        k = 2·(m'+k) + 1
        odd(k)
        even(k) ⋁ odd(k)

So, good, you now know precisely why every integer is either even or odd.

Yes. I do know, now.

And then some spectator who happens to read this transcript scratches the head wondering why it needs to be proven.

3:06 PM

@user21820 :-)

@user21820 You already explained, but I will ask you again if you don't mind (I don't understand). Why am I allowed to add 2·k to both sides ? From -k ∈ ℕ, how can I go to 2·k ∈ ℕ ?

@F.Zer −k∈ℕ. −k∈ℤ.

I didn't use k·2∈ℕ. I used k·2∈ℤ...

You are "Given k∈ℤ".

ℤ is closed under addition.

Basically, when dealing with ℕ,ℤ,ℚ,ℝ, just do each computation in whichever type is big enough to support it.

@user21820 Perfect. So, 2·k ∈ ℤ, -k ∈ ℕ ⇒ -k ∈ ℤ, 1 ∈ ℕ ⇒ 1 ∈ ℤ and 2·m' ∈ ℕ ⇒ 2·m' ∈ ℤ. Basically, every guest is invited to join ℤ :-)

And, we can perform addition in ℤ.

@user21820, do you feel this leap should be justified ?

2·l + (-2·l·n) = n
2·((-1)·l·n) = n
even(n)

Perhaps, using this lemma: ∀ x ∈ ℤ ( -x = (-1)·x )) ?

∀ x ∈ ℤ ( -x = (-1)·x )) [Lemma]
  Given x ∈ ℤ:
    ∀ x ∈ ℤ ( x·0 = 0 ) [Lemma]
      Given x ∈ ℤ:
        0 + 0 = 0
        x·(0 + 0) = x·0
        x·0 + x·0 = x·0
        (x·0 + x·0) + (-x·0) = x·0 + (-x·0)
        x·0 + (x·0 + (-x·0)) = x·0 + (-x·0)
        x·0 = 0
      ∀ x ∈ ℤ ( x·0 = 0 )
    x·0 = 0
    x·(1 + (-1)) = 0
    1·x + (-1)·x = 0
    -x + 1·x + (-1)·x = -x
    -x + x + (-1)·x = -x
    (-1)·x = -x
    -x = (-1)·x
  ∀ x ∈ ℤ ( -x = (-1)·x ))

3:22 PM

@F.Zer You mixed up something bad. If m·n = 2·l you certainly do not have m·n = 2·l·n+n...

But you don't need any pesky lemmas. Just stick to elementary stuff! Also, that approach doesn't need the outer contradiction:

@user21820, that colon indicates you're about to write something, I think. So, I'll save my question.

Given m,n∈ℤ:
	If even(m·n):
		even(m) ∨ odd(m).  [lemma]
		If even(m):
			even(m) ∨ even(n).
		If odd(m).
			Let k∈ℤ such that m = k·2+1.
			Let l∈ℤ such that m·n = l·2.
			l·2 = m·n = (k·2+1)·n.
			l·2+n = k·2·n+n+n = k·2+n·2.
			l·2+(−l)·2 = l+l+(−l)+(−l) = l+0+(−l) = l+(−l) = 0.
			n = n+0 = n+l·2+(−l)·2 = k·2+n·2+(−l)·2 = (k+n+(−l))·2.
			even(n).
			even(m) ∨ even(n).
		even(m) ∨ even(n).

See, so short! =)

I added just a little bit in case it's not clear what I was doing.

@user21820 Fantastic. I've just understood it.

@user21820 This explanations about Reals are a little bit above my head. I'll try to do some simple exercises and see if I can understand. Also, I didn't the subsets of Reals part.

@user21820, I should go in a moment. Thank you for your logic teachings! See you !

3:41 PM

@F.Zer Simple exercises almost never use the completeness axiom, and so you would only be proving facts about ordered fields, such as ℚ. Of course, you should do those first, but you should also work slowly through the proof I gave and see whether you get it, as it is the easiest non-trivial fact that separates ℝ from ℚ.

6 hours ago, by user21820

Of course, "S⊆ℝ" means "S∈P(ℝ)" where "P" here is the power-set operation.

@user21820 Is this exercise "Suppose that a and b are nonzero real numbers. Prove that if a < 1/a < b < 1/b then a < -1" a good one to start ?

5 hours ago, by user21820

So the axioms I have given you for ℚ minus "∀x∈ℚ ∃p,q∈ℤ ( q ≠ 0 ∧ p = q·x )" are the axioms for ordered fields that contain ℤ. (And every ordered field contains a copy of ℤ, but you don't need to care about that now.) Both ℚ and ℝ are ordered fields that contain ℤ, so they both satisfy every theorem you can prove from the ordered field axioms. These theorems also include the exercise you asked me about.

So yes go ahead.

Good !

Though maybe you should prove all those simple facts first:

3 hours ago, by user21820

> ∀x∈ℝ ( x/1 = x ).
> ∀x,z∈ℝ ∀y,w∈ℝ[≠0] ( (x/y)·(z/w) = (x·z)/(y·w) ).
> ∀x,y∈ℝ[≠0] ( 1/(x/y) = y/x ).

3 hours ago, by user21820

> ∀x∈ℝ[≠0] ( x·x > 0 ).

@user21820 Excellent.

3:45 PM

@F.Zer You're welcome and see you!

2 hours later…

5:41 PM

@user21820, I leave here the proof of the first fact.

∀x∈ℝ ( x/1 = x ).
  Define the type ℝ[≠0] = { x : x∈ℝ ∧ x≠0 }
  Given x ∈ ℝ:
    ∀y∈ℝ[≠0] ( x = y·(x/y) )
    1 ∈ ℕ ⇒ 1 ∈ ℤ
    1 ∈ ℤ ⇒ 1 ∈ ℚ
    1 ∈ ℚ ⇒ 1 ∈ ℝ
    1 ∈ ℝ ∧ 1 ≠ 0
    1 ∈ ℝ[≠0]
    x = 1·(x/1)
    ∀ x ∈ ℝ ( x·1 = x )
    (x/1)·1 = x/1
    x = x/1
    x/1 = x
  ∀x∈ℝ ( x/1 = x )

6:24 PM

∀x,z∈ℝ ∀y,w∈ℝ[≠0] ( (x/y)·(z/w) = (x·z)/(y·w) ).
  Given x,z ∈ ℝ:
    Given y,w ∈ ℝ[≠ 0]:
      ∀x∈ℝ ∀y∈ℝ[≠0] ( x = y·(x/y) )
      x = y·(x/y)
      z = w·(z/w)
      (x/y)·(z/w) = (y·(x/y)/y)·(w·(z/w)/w)
      ...
  ∀x,z∈ℝ ∀y,w∈ℝ[≠0] ( (x/y)·(z/w) = (x·z)/(y·w) )

@user21820, I leave here the proof skeleton of the second fact.

Of course, y·(x/y)/y = x/y. But I should prove it from the axioms :-)

6:47 PM

Found the solution, I think.

0

A: How does one tutor an A-level student past the derivative paradox?

So many answers, but not yet pointed out is that your proposed proof of the derivative of $x^n$ with respect to $x$ is wrong because it uses the wrong notation. There is a difference between Big-O and little-o (see the formal definitions of Landau notation for details). $ \def\lfrac#1#2{{\large\f...

^ Anyone want to read this so that they can upvote it if they like it to prevent it from languishing in obscurity beneath 12 earlier answers? =)

@F.Zer I already defined ℝ[≠0] in the global context, so you should put that definition outside of your theorems. Your proof is correct.

→ 2 messages moved to Sandbox

@user21820 Thank you. Noted your remark.

I found the following equivalence x/y = y·((x/y)/y)

@F.Zer Yes that's right.

I haven't actually tried proving the exercises I gave you. I did mentally prove that they can be proven, though. =P

:-)

@user21820 Just out of curiosity, why do you move messages to the Sandbox rather than the Trash? There's nothing wrong with it, since the Sandbox has no topic or anything but I am just wondering if there's a reason you choose the Sandbox.

6:57 PM

@hyper-neutrino People don't like getting invited to "Trash", as it implies that what they say is trash, even though that is just the technical issue with SE chat mechanics.

So unless it is spam/abuse, I move to "Sandbox".

Ah. Fair enough.

The misunderstanding about "Trash" happened enough times to me that I decided it was better just to avoid it as far as reasonable.

@F.Zer: I think the easiest natural way to prove the exercise you are stuck on is to first prove ∀x,y∈ℝ ∀z∈ℝ[≠0] ( x·(y/z) = (x·y)/z ). The natural idea is to attempt to prove it when both sides are multiplied by z, and that works: z·(x·(y/z)) = z·x·(y/z) = x·z·(y/z) = x·y = z·((x·y)/z). We can divide both sizes by z by multiplying by (1/z) to get (1/z)·z·(x·(y/z)) = (1/z)·z·((x·y)/z) and hence the desired result.

@user21820 I will try your suggestion.

Wait a minute. The original exercise was easier lol: (x/y)·(z/w)·y·w = x·z by rearranging and using definition of /. Then multiply both sides by 1/(y·w) and we are done.

And what I just said is an easy consequence LOL: x·(y/z) = (x/1)·(y/z) = (x·y)/(1·z) = (x·y)/z.

So, the exercises are easier than I thought.

@user21820 I'd like one clarification, please. When you say "attempt to prove it when both sides are multiplied by z". Are you multiplying both sides of the conclusion by z ? I am missing something.

Oh, no. You are multiplying both sides of (introduced via =I) x·(y/z) = x·(y/z), I think.

Is that right ?

7:10 PM

@F.Zer I meant the conclusion, yes. If you can prove that, and then manage to divide again, then you get the desired conclusion.

If you fail to do the division, then of course you can't reach the desired conclusion. For example, if you multiply the conclusion by zero, it would be useless even if you can prove it.

@user21820 What ? How are you manipulating the conclusion? Isn't that what we are trying to prove ? Please, clarify

@user21820 Is this a proof technique ? Seems convenient but I can't grasp it, now.

@F.Zer Just follow the steps I gave, in the order I gave them. They will bring you to the desired conclusion.

I need to go.

Bye!

@user21820 Thank you ! Bye !

3 hours later…

10:20 PM

@user21820, I leave the proofs of the second and third facts, below.

∀x,z∈ℝ ∀y,w∈ℝ[≠0] ( (x/y)·(z/w) = (x·z)/(y·w) ).
  ∀x,y∈ℝ ∀z∈ℝ[≠0] ( x·(y/z) = (x·y)/z )
  Given x,z ∈ ℝ:
    Given y,w ∈ ℝ[≠ 0]:
      ∀x∈ℝ ∀y∈ℝ[≠0] ( x = y·(x/y) )
      (x/y)·(z/w)·y·w = y·(x/y)·w·(z/w) = x·z
      (1/(y·w))·(x/y)·(z/w)·y·w = (x·z)·1/(y·w)
      (y·w)·(1/(y·w))·(x/y)·(z/w)= (x·z)·1/(y·w)
      (x/y)·(z/w) = (x·z)/(y·w)
  ∀x,z∈ℝ ∀y,w∈ℝ[≠0] ( (x/y)·(z/w) = (x·z)/(y·w) )

∀x,y∈ℝ[≠0] ( 1/(x/y) = y/x ).
  Given x,y ∈ ℝ[≠ 0]:
    (y/x)·(x/y) = ((y/x)·x)/y) = (x·(y/x))/y = y/y = 1 [Justification ?]
    1/(x/y) = (x/y)·(y/x)/(x/y) = y/x
  ∀x,y∈ℝ[≠0] ( 1/(x/y) = y/x )

Should I provide a justification for y/y = 1 ?

« first day (1179 days earlier) ← previous day next day → last day (1020 days later) »

Transcript for

Jul '2130

♦ $Mathematics$ Basic Mathematics

This room is meant for all basic mathematical discussion, incl...

join this room
about this room

00:00

06:00

12:00

18:00

all times are UTC

$Mathematics$

site design / logo © 2024 Stack Exchange Inc; legal

mobile