Basic Mathematics - 2021-08-14

F. Zer

01:35

∀x∈ℚ ∃p,q∈ℤ ( q > 0 ∧ p = q·x ) [ℚ = ℤ/ℤ+]
  Given x ∈ ℚ:
    Let p', q' ∈ ℤ such that q' ≠ 0 ∧ p' = q'·x [ℚ = ℤ/ℤ*]
    If q' ∈ ℕ:
      q' ≥ 0
      q' > 0
      q' > 0 ∧ p' = q'·x
      ∃p,q∈ℤ ( q > 0 ∧ p = q·x )
    If –q ∈ ℕ:
      (–1)·p' = (–1)·q'·x
      –q' > 0 ∧ –p' = –q'·x
      ∃p,q∈ℤ ( q > 0 ∧ p = q·x )
    ∃p,q∈ℤ ( q > 0 ∧ p = q·x )
  ∀x∈ℚ ∃p,q∈ℤ ( q > 0 ∧ p = q·x )

@user21820 I leave here this proof.

Could you tell me what do you think ?

user21820

02:51

@F.Zer That's right.

yh05

03:21

Hello @user21820. I've taken a first course in Real Analysis. It covered analysis on R. I want to learn analysis on R^n. Do you know of any good undergraduate textbook for self-studying? I'm currently reading Robert S. Strichartz - The way of analysis to refresh my memory on Real Analysis I. Is the book material sufficient to learn analysis on R^n?

After learning analysis on R^n, what else do I need to learn before learning measure theory (enough to learn probability theory)?

user21820

04:04

@yh05 You don't need to learn analysis on ℝ^n to learn measure theory. The key is just that you must have finished real analysis at the level of rigour of Spivak's, and can easily handle many nested quantifiers. Then you would actually be able to do measure theory already.

yh05

05:05

@user21820 Spivak's as in Spivak's Calculus?

Can you recommend a good undergraduate book to learn analysis on R^n? My Real Analysis 1 course didn't cover that.

shintuku

there's Ted Shifrin's Multivariable Mathematics, which is nice because he has a two-semesters lecture uploaded on youtube where he uses that book

yh05

@shintuku I think the book is more suitable for a multivariable calculus course than a second course in analysis.

shintuku

personally I would not recommend this book for multivariable calculus, since it is theorem-proof format

user21820

07:52

@yh05 Yes Spivak's Calculus. Sorry I don't have recommendation for real analysis on ℝ^n, partly because I never went in that direction. (And that's also why I know it's not necessary for measure theory because I did do measure theory.) I searched for Ted Shifrin's book that shintuku recommended, but I personally wouldn't buy it at that crazy price. Incidentally, that same google scholar search also gave Spivak's Calculus on Manifolds.

I obviously don't know how good Spivak's book is, nor whether it covers what you're interested in, but if it were me I would look through since it's free. =)

Searching Math SE also brings up this post suggesting Advanced calculus by Sternberg Loomis.

Prithu biswas

14:56

If ∀x∈B∀y∈B∀z∈B(p(x)=p(y)∧p(y)=p(z)⇒x=y∨y=z∨z=x)
   Given a∈S
      If ¬∃x∈B(p(x)=a)
         Given d∈s
            If P(d)=a
               If ¬(d=a)
                  P(d)=a
                  ∃x∈B(p(x)=a)
                  ¬∃x∈B(p(x)=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)
      Let b%S such that p(b)=a

@user21820 attempt at Q8.

user21820

@Prithubiswas Um, you might want to find a better way of writing these proofs if you keep making replacement errors. It makes your attempts look very untidy.

Anyway, give me a moment to check it.

In the second case, why do you use "If ¬(d=b∨d=c)", when you can just do two ∨-elims?

Not much difference, but just pointing out.

Prithu biswas

Indentation error after "If ∃x∈B(p(x)=a)".

user21820

Oh yes, I didn't check what you previously showed me, so I missed that.

The third case is fine too. So once you fix these not serious errors, you've completed the exercise!

F. Zer

@user21820 Hello. I hope you are well, today. Can I ask you a question ?

user21820

@Prithubiswas: Did it teach you how explicit counts (here 0,1,2,3) can be encoded and handled in FOL?

@F.Zer I am, thanks for asking! Sure.

Prithu biswas

15:10

@user21820 No.

F. Zer

@user21820 That's great. Could you check my attempt ?

Prithu biswas

@user21820 Not quite apperent to me how to use two ∨-elims .Can you show me?

F. Zer

∀x∈ℚ ∃p,q∈ℤ ( q > 0 ∧ p = q·x ∧ ∀d∈ℕ ( d | p,q ⇒ d = 1 ) ), where "d | p,q" is short-hand for "d | p ∧ d | q"
  Given x ∈ ℚ:
    ∃p,q∈ℤ ( q > 0 ∧ p = q·x ) [ℚ = ℤ/ℤ+]
    Let a, b ∈ ℤ such that b > 0 ∧ a = b·x
    Define P(m) ≡ m > 0 ∧ a = m·x
    ∃k∈ℕ ( P(k) ) ⇒ ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ) [well-ordering]
    b > 0 ∧ a = b·x
    ∃k∈ℕ ( k > 0 ∧ a = k·x )
    ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )
    Let m' ∈ ℕ such that P(m') ∧ ∀k∈ℕ ( P(k) ⇒ k≥m' )
    P(m')
    m' > 0 ∧ a = m'·x
    ∀k∈ℕ ( P(k) ⇒ k≥m' )

user21820

@Prithubiswas After b = c ∨ ( c = d ∨ d = b ), you do one ∨elim on that, and under "If b = c:" you get ⊥ and then "d = b ∨ d = c" as desired. The other case is trivial.

@Prithubiswas Those case-splits and the original premise are expressing comparisons with 0,1,2,3.

@F.Zer Indeed; well-ordering is precisely how you can pick a minimum denominator, once you know it is in ℕ. But why couldn't you finish the cases?

Prithu biswas

@user21820 I dont really know of any good way of writing my proofs besides opening notepad , writing the proofs , replacing my own symbols (like %,n,F,E) with there appropriate symbols. A lot of times I just forget to replace them which makes the proof very untidy (I hope that is what you meant). Sometimes the types get switched up (like using Given d∈s instead of Given d∈B).Keeping track of indentation using notepad is also hard.

You did mention a autohotkey method but that is probably beyond my skills.

user21820

15:24

@Prithubiswas Symbols aside, you should really be using an editor that does auto-indentation. What OS are you using? For Windows I'm using Programmer's notepad, which you can use just for the indentation feature even if nothing else.

Prithu biswas

@user21820 You proved me wrong. The graph intuition can be useful for solving FOL problems.

@user21820 I am using windows 10.

F. Zer

@user21820 Thank you for your comment. I will think more about how can I finish the cases and come back.

Prithu biswas

A couple of weeks ago , I downloaded a text editor called atom. It could have been useful for indentation if I knew all of its features. But now it stopped working completely for some reason.

user21820

@Prithubiswas PN is free and easy to use.

Prithu biswas

@user21820 I have download the Auto hotkey program. Is there a tutorial for it?

user21820

15:34

@Prithubiswas Yes all you need is the hotstrings feature of AHK.

For example, I have the following lines (and many others) in my AHK script:

	::\ne ::≠
	::\le ::≤
	::\ge ::≥
	::\pm ::±
	::\nn ::ℕ
	::\zz ::ℤ
	::\qq ::ℚ
	::\rr ::ℝ
	::\cc ::ℂ
	::\pp ::ℙ

The first line means that whenever I type "\ne " (with the final space) it gets changed into "≠".

If you want to be able to turn it off easily whenever you don't want it running (such as when you are typing LaTeX code on Math SE), you can use the following code:

Prithu biswas

@user21820 I am using the programmers notepad. It puts lines for the indentation which is helpful. I putted the entire proof of Q8 in PN but it seems like it replaced all of the logical symbols with "?".

user21820

@Prithubiswas You need to change the font (tools > options) to a unicode font, and you must make sure file > encoding is UTF8.

global escape:=true
messageoff:
	tooltip
return
message(text)
{
	tooltip % text
	settimer messageoff,-1000
}
LShift & RShift::
	escape:=!escape
	message( "Escape " ( escape ? "On" : "Off" ) )
return
#if escape
	::\ne ::≠
	::\le ::≤
	::\ge ::≥

In the above AHK code that I just pasted, the first part defines messageoff and message(text), which you can ignore. "LShift & RShift::" means "when you press left-shift+right-shift", and it toggles the value of escape.

The "#if escape" says that all the hotstrings under it will only be active if escape is true.

So whenever you want to turn these hotstrings on/off, you press left-shift+right-shift.

If you prefer another shortcut-key for toggling this, you can choose your own by referring to hotkeys.

@Prithubiswas: By the way, if you find the linked documentation pages for AHK overwhelming, don't worry. I also do. So if you have any trouble you can ask me and I'll try to help.

F. Zer

16:37

@user21820 I gave it more thought, but I can't seem to find a way.

user21820

@F.Zer As usual, try small cases to test out the cases you have. Obviously you would have to suppress some assumptions, such as the minimality of m.

F. Zer

@user21820 I will make an attempt at your suggestion. Thank you.

F. Zer

16:50

@user21820 I've just realised the problem. I do not know how to try small cases in this problem. My attempt would be giving values to the variables inside the contexts. Could you teach me the correct way ?

Given x ∈ ℚ:
	Given d ∈ ℕ:
		If d | a ∧ d | m':
			If d > 1:
				a = 6
				m' = 3
				x = 2
				a = m'·x
				6 = 3·2

I pasted my intuitive attempt, so you can take a look at the issue.

user21820

@F.Zer Yes so you're supposed to then find something that contradicts the minimality of m'.

"Given x∈ℚ" means you can take any x∈ℚ, and you have taken x = 2. You have also chosen a,m' satisfying the other criteria except for minimality. So all you need to do is to figure out why your m' is not minimal.

F. Zer

@user21820 That's good. That's exactly what I am trying to do. Thank you.

@user21820 I have this question since long time ago. Could you tell me how would you deal with variable "d" ? Should I choose some value that satisfies "d | a ∧ d | m',", for example, 1 ?. Then, do I simply replace that 1 inside "If d > 1:", and get "If 1 > 1:" ?

Prithu biswas

@user21820 I am able to write ≠ ≠ ≠ ≠ using the script. But I cant turn it off even after deleting the script. Is there a way to turn it off?

user21820

17:15

@Prithubiswas The thing that is actually running can be accessed from the system tray. Deleting the script source won't do anything.

That's why I suggested you use the code I provided, so that you can turn it on/off using a shortcut-key, instead of going to the system tray.

@F.Zer How can you test a case with something that does not satisfy that case?

You're a programmer, to test a case you need it to actually fire.

F. Zer

@user21820 Makes complete sense. I am still struggling to connect programming and formal proofs. Thanks for the pointer.

user21820

@F.Zer There's no formal connection that I'm making. I'm just saying that you ought to apply your own relevant experience.

If you wouldn't do something when testing a program, it makes no sense to do an analogous thing when testing a case-split in a proof.

F. Zer

@user21820 Yes, of course. It's just that I always struggle to make an intuitive connection between what I do when programming and doing formal proofs. I struggled a whole lot with the concept of "local declaration" (Let) until you pointed out the similarity with programming.

Then, it clicked.

@user21820 I found the solution. Thank you for not spoiling it !

As always, testing small cases gave insight :-)

I will post the full solution.

user21820

@F.Zer Excellent.

F. Zer

I will make a big note about "try small cases", in addition to "always add" :-)

user21820

17:34

@F.Zer: Well I need to go soon. Are you posting your solution now?

F. Zer

Given x ∈ ℚ:
  Given d ∈ ℕ:
    If d | a ∧ d | m':
      If d > 1:
        Let z ∈ ℕ such that a = d·z
        Let z' ∈ ℕ such that m' = d·z'
        a = m'·x = (d·z')·x
        d·z = (d·z')·x
        d·z = d·(z'·x)
        z = z'·x
        z' > 0
        z = z'·x ∧ z' > 0
        P(z')
        P(z') ⇒ z' ≥ m'
        z' ≥ m'
        z' < m'
        ⊥

@user21820 There is something I do not like, there.

user21820

@F.Zer What?

F. Zer

My P(m) has "a" fixed.

@user21820 I pasted only the relevant lines.

user21820

Well you have:

F. Zer

I will post the full solution when/if I solve that issue inside the case "If d > 1:"

user21820

17:36

  Given x ∈ ℚ:
    ∃p,q∈ℤ ( q > 0 ∧ p = q·x ) [ℚ = ℤ/ℤ+]
    Let a, b ∈ ℤ such that b > 0 ∧ a = b·x
    Define P(m) ≡ m > 0 ∧ a = m·x

So your P is defined after you have declared a. So it's fine as it is.

As I said before, you should always treat your properties as mere short-hand. If you don't like it, you can just replace each instance of P with its expansion to see that it's fine.

F. Zer

@user21820 Of course, the problem is that I derived: "z = z'·x".

That is certainly not P(z').

user21820

@F.Zer Oh, then your proof is wrong. Sorry wasn't thinking.

F. Zer

@user21820 Good. I suspected about that :-)

@user21820 So, is my definition of P wrong ?

user21820

Yes your P won't work for the very reason you stated.

What you need is:

Given x ∈ ℚ:
  Define P(k) ≡ k > 0 ∧ ∃j∈ℤ ( j = k·x ).

F. Zer

@user21820 That makes complete sense. I was a little far from that definition. I will continue working. Have a good day and thank you !

user21820

17:42

Ok bye!

F. Zer

18:33

∀x∈ℚ ∃p,q∈ℤ ( q > 0 ∧ p = q·x ∧ ∀d∈ℕ ( d | p,q ⇒ d = 1 ) ), where "d | p,q" is short-hand for "d | p ∧ d | q"
  Given x ∈ ℚ:
    ∃p,q∈ℤ ( q > 0 ∧ p = q·x ) [ℚ = ℤ/ℤ+]
    Let a, b ∈ ℤ such that b > 0 ∧ a = b·x
    Define P(k) ≡ k > 0 ∧ ∃j∈ℤ ( j = k·x )
    ∃k∈ℕ ( P(k) ) ⇒ ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ) [well-ordering]
    b > 0 ∧ a = b·x
    a = b·x
    ∃j∈ℤ ( j = b·x )
    b > 0 ∧ ∃j∈ℤ ( j = b·x )
    P(b)
    ∃k∈ℕ ( P(k) )
    ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )
    Let m' ∈ ℕ such that P(m') ∧ ∀k∈ℕ ( P(k) ⇒ k≥m' )

@user21820 Here is the full proof. What do you think ?

Transcript for

♦ $Mathematics$ Basic Mathematics

Transcript for

♦ Basic Mathematics

♦ $Mathematics$ Basic Mathematics