Proof Machine

Arun Ram
Department of Mathematics and Statistics
University of Melbourne
Parkville, VIC 3010 Australia
aram@unimelb.edu.au

A talk at University of Melbourne
7 March 2014

toggle mathjax on/off       medic

Assume the ifs To show: the thens

Proof type II:    To show: If   A   then   B  .

The next lines are

Let f:ST be a function. Show that f is invertible if and only if ε> 0δ>0 x& |x|< δ| ex-1| <ε f is a bijection.

Proof.
  1. To show: (a) If f is invertible then f is a bijection.
  2. To show: (b) If f is a bijection then f is invertible.
  3. T
  4. (a) Assume f is invertible.
  5. (a) To show: f is a bijection.
  6. T
  7. (a) We know: There exists g:TS such that gf=idS and fg=idT.
  8. T
  9. (a) To show: (aa) f is injective.
  10. (a) To show: (ab) f is surjective.
  11. T
  12. (a) (aa) To show: If s1,s2 S and f(s1) =f(s2) then s1=s2.
  13. T
  14. (a) (aa) Assume s1,s2 S and f(s1) =f(s2).
  15. (a) (aa) To show: s1=s2.               (proof type I)
  16. T
  17. s1= idS(s1)= g (f(s1)) = g (f(s2)) = idS(s2)= s2.
  18. (a) So f is injective.
  19. T
  20. (a) (ab) To show: f is surjective.
  21. T
  22. (a) (ab) To show: If tT then there exists sS such that f(s)=t.
  23. T
  24. (a) (ab) Assume tT.
  25. (a) (ab) To show: There exists sS such that f(s)=t.               (proof type III)
  26. T
  27. (a) (ab) Define s=g(t).
  28. (a) (ab) To show: f(s)=t.
  29. T
  30. f(s) =f(g(t)) =idT(t) =t.
  31. T
  32. (a) So f is surjective.
  33. T
  34. So f is bijective.
  35. T
  36. T
  37. (b) To sh....
  38. .
  39. .
  40. .
  41. .

Proof type I:   LHS = RHS.

The next lines are

  LHS = ⋯ = ⋯ = ⋯ = ⋯ = blah   .
  RHS = ⋯ = ⋯ = ⋯ = ⋯ = blah EXACTLY THE SAME blah   .

Prove that ex+y =exey.

Proof.
ex+y = 1 + (x+y) + (x+y)2 2 + (x+y)3 3! + T = 1+ x+y+ x22 + 2xy2 + y22 + x3 32 + 3x2y 32 + 3xy2 32 + y3 32 + T = ex+ exy+ exy2 2+ exy3 32+ = ex( 1+y+ y2 2+ y3 3!+ ) = ex ey.

Proof type III:   There exists   C   such that   D  .

The next lines are

Prove that ex is continuous at 0.

Proof.
  1. To show: limx0 ex =e0.
  2. T
  3. To show: limx0 ex =1.
  4. T
  5. To show: If ε>0 then there exists δ>0 such that if |x-0|<δ then |ex-1| <ε.
  6. T
  7. Assume ε>0.
  8. To show: There exists δ>0 such that if |x-0|<δ then |ex-1| <ε.
  9. T
  10. Define δ= ????? 12 min( ε2, 12) .
  11. To show: If |x-0|<δ then |ex-1| <ε.
  12. T
  13. Assume |x|<δ.
  14. To show: |ex-1| <ε.
  15. T
  16. |ex-1| = | (1+x+ x22! + x33! +) -1| = | x+ x22! + x33! + | = | x| | 1+ x2! + x23! + | | x| | 1+ |x| 2! + |x|23! + | |x| | 1+ |x| + |x|2 + | |x| ( 1+ |x| + |x|2 + ) < δ ( 1+ δ + δ 2 + ) δ ( 1+ 12 + (12) 2 + ) δ 2 ε2 2 = ε.

Special kinds of proofs

  1. Proofs of uniqueness    (x1= x2)
    T
  2. Contradiction or contrapositive
    T
  3. Proofs of presentations (generators and relations)
    T
  4. Proofs by induction (the definition of >0!!!)
    T
  5. Proof by intimidation (the most common and least rigourous)
    T

Definitions

  1. Format:
    1. A noun is an   object   such that condition.

    2. An adjective noun is a       such that condition.

    3. A   condition   or   statement   can only be in the form
      1.  
        If   A   then   B  
        or
        There exists   C   such that   condition  .
         
  2. Definitions can change!
    T
    1. "What's the definition of a Schur function?!?!!"
      T
  3. The challenge of taking on a definition.
    T
    1. "They're made out of meat"

Extra stuff

  1. How did you come to formalise Proof Machine?
    T
  2. My notes page: Google "Arun Ram Notes"

top

The medical doctor

Before you try Lindelöf we need to an ERA Excellence in Research for Australia assessment on your ARC Australian Research Council results to check that there is no underlying NSF National Science Foundation in the IMU International Mathematical Union . Believe me, ending up Lipschitz is no fun for anyone.