Motivation

The numbers of pure mathematics never appear naked and unadorned in practice. They appear with units attached to them - feet, meters, inches, centimeters, miles, yards, .... Therefore a practical mathematical notation must provide a meaingful way for this to be done. This set of notes set up a suitable system loosely inspired by the ISP notation of Gordon, Bell and ??? combined with "Dimensional Analysis" as used in Applied Mathematics and/or Physics[Crank ??].

Also see

Novak93, Conversion of Units of Measurement, IEEE Trans Sofware Engineering SE-21n8(pp651-661).

Metrology

1. Metrology::=the science of all aspects of measurement including the theory and practice in all fields of science and technology -- however uncertain.

   A standardized quantitive measurement is based on an underlying attribute, a defined unit, a primary reference of example of the unit, some secondary references used in practice and some methods of measurement used to get these measurements. For example the idea of "the inertia of an object" is experienced when we try to move a heavy and light object, or compare the effort to brake a truck with that of a child's toycar. This idea is refined into the concept of inertial mass with a unit like the kilogram and standard ways of measuring it.

   In America the National Institute of Standards (NIS) is in charge of these things [ http://www.nist.gov/ ] Their Information Technology Laboratory has been working on deriving the metrology of Information technology [ http://www.itl.nist.gov/ ]

   The SI Units are described at [ units.html ] (with thanks to Vince Tilroe, February 17th 2005)

   Measurement Theory

   Some measures do not have the complete set of properties of numbers. The classification commonly used are: nominal, ordinal, interval, and ratio.

   [click here if you can fill this hole]

   Dimensions

   We don't add feet and pounds together. And yet we can add pounds to pounds and get pounds: Hence we have a large number of similar sets of arithmetic - one arithmetic for each dimension. Because we can also add ounces and pounds, each dimension has several sets of units associated with it. The numbers in different units are proportional, however ( 16.oz=1.lb).

   Now if we multiply two lengths then we get an area - not another length. So the different dimensions are also related. Dimensional Analysis expresses all dimensions ( length, mass, weight, velocity, force, magnetic flux,...) in terms of a small number of fundamental dimensions - length, mass, time, and a few others.

2. DIMENSION::=
   Net{

   1. BASIS::=
      Net{

      1. Dimension::@Field(archimedian). Actually, each dimension is isomorphic to the real numbers.

         
         

      2. |- (partioned): For all D1,D2:Dimension, D1=D2 iff some D1&D2.

      3. Numbers::Dimension.

         
         

      4. |- (dgroup): GROUP(Dimension, (*), Numbers, (/)). Given two Diemnsions we can multiply them (*) to get another Dimension. Pure Numbers act like 1 in this multiplication and we have some kind of division as well.

         A unit gives a mapping of numbers into dimensions. For instance using 'inch' as a unit of length means that 1.inch is a measure of length,... A set of units works exactly like a set of numbers under addition. If Length is a dimension and inch a unit of length Length./inch indicates numbers which represent the numbers of inches of length.

         In general then a unit is map from abstract numbers into diemensions that preserves the operation of addition and the value of zero:

      5. For Dimension D, Units(D)::=(+,0)Numbers---D. [ Structure Preserving Maps in math_11_STANDARD ]

      
      }=::BASIS.

      
      

   2. |- (D0): BASIS. This just asserts the assumptions named BASIS above.

   3. MECHANICAL_UNITS::=
      Net{

      There are three basic physical dimensions - length, time, and mass. A more abstract one is that of information. We can also include angles from geometry. We assume that every possible dimension is expressible in terms of these 5 component dimensions:
      1. dim::Net{L,T,M,I,A:Rational}---Dimension,
      2. Number::= dim(L=>0,T=>0,M=>0,I=>0,A=>0).

      3. Length::= dim(L=>1,T=>0,M=>0,I=>0,A=>0),
      4. Mass::= dim(M=>1,L=>0,T=>0,I=>0,A=>0),
      5. Time::= dim(T=>1,M=>0,L=>0,I=>0,A=>0),
      6. Angle::= dim(T=>0,M=>0,L=>0,I=>0,A=>1),
      7. Information::= dim(I=>1,T=>0,M=>0,L=>0,A=>0).

         Next define product and quotient of two dimensions.

      8. For a:D1, b:D2, a/b::=dim(a./dim-b./dim),
      9. For a:D1, b:D2, a*b::=dim(a./dim+b./dim).
         
      10. (above)|- (ex1): Length*Length/Time=dim(L=>2,T=>-1,M=>0,I=>0, A=0).
          
      11. (above)|- (ex2): For Dimension D, D/D=Number.

      12. For Dimension D, a:D, dim(a)::=D.

          
          

      13. |- (D1): Number=Real.
          
      14. (above)|- (D1.0): For Dimension D, a:D, n:Number, dim(a*n)=dim(a).

          
          

      15. |- (D2): For Dimension D1, D2, u1:Units(D1), u2:Units(D2), a,b:Numbers, c:Numbers-{0}, a.u1/b.u2=(a*c).u1/(b*c).u2 and a.u1*b.u2=(a*c).u1*(b/c).u2=(a/c).u1*(b*c).u2.

          
          

      16. |- (D3): For Dimensions D1, D2, u1:Units(D1), u2:Units(U2), u1/u2::Units(dim(u1./dim-u2./dim)=((_).u1/1.u2).
          
      17. |- (D4): For Dimension D1,D2, u1:Units(U1), u2:Units(U2),
      18. u1*u2::Units(dim(u1./dim+u2./dim)=((_).u1*1.u2).
          
      19. |- (D5): For all D:Dimension, u1,u2,u3:Units(D), a,b:Numbers, if a.u1=1.u2 and b.u2=1.u3 then (a*b).u1=1.u3.
          For example, (D5)|-60*1000.ms=1.hr.

          
          

      20. |- (D6): For all Dimension D, u1,u2:Units(D), a,b,c:Numbers, if a.u1=b.u2 then (a*c).u1=(b*c).u2.
          For example, (D6)|-30.s=0.5.hr.

          Notice that if n is a number and u a unit the n.u is the measure. But if c is some constant measure (say the speed of light or the acceleration due to gravity) then c./u is the number in units u.

          
          

      21. |- (D7): For all Dimension D, u:Units(D), a:number, a.u./u = a.

      
      }=::MECHANICAL_UNITS.

      Common Units

      
      

      1. |- (common_units): MECHANICAL_UNITS.

         Lengths

      2. km::Units(Length),
      3. mm::Units(Length),
      4. cm::Units(Length),
      5. m::Units(Length),
      6. ft::Units(Length),
      7. inch::Units(Length),
      8. yd::Units(Length),
      9. miles::Units(Length),
      10. ...
          
      11. |- (l1): 100.cm=1.m,
          
      12. |- (l2): 10.mm=1.cm,
          
      13. |- (l3): 1000.m=1.km,
          
      14. |- (l4): 12.inch=1.ft,

          
          

      15. |- (l5): 3.ft=1.yd,
          
      16. |- (l6): 1760.yd=1.mile.
      17. ...

          Area and Volume

      18. Area::=Length*Length,
      19. acre::Units(Area),
      20. hectare::Units(Area),
      21. ...
      22. Volume::=Length*Length*Length.
      23. gallon::Units(Area), varies in size depending on geography.
      24. pint::Units(Area), varies in size depending on geography.
          
      25. |- (pg): 8.pint = 1.gallon.
      26. litre::Units(Area),
      27. cc::Units(Area),
      28. ...
          
      29. (above)|- (VL): Volume=Length*Area=Area*Length.

      30. mpg::Units(dim(L=> -2))=miles/gallon.

          Times and Dates

      31. ns::Units(Time), nanosecond
      32. ms::Units(Time), millisecond
      33. sec::Units(Time), second
      34. min::Units(Time), minute
      35. hr::Units(Time), hour
      36. day::Units(Time),
      37. week::Units(Time),
      38. month::Units(Time),
      39. year::Units(Time).
          
      40. |- (t1): 1000.ms=1.s and 1000.ns=1.ms,
          
      41. |- (t2): 60.min=1.hr,
          
      42. |- (t3): 60.s=1.min,

          
          

      43. |- (t4): 24.hr=1.day,
          
      44. |- (t5): 7.day=1.week. .Dangerous_bend The relationship between days, months and years depends on the calendar adopted.

      45. DATE::=
          Net{

          1. day::Integer & Time./day.
          2. month::Integer & Time./month.
          3. year::Integer & Time./year.

          
          }=::DATE.
          
          
      46. |- (d1): Dates<--$ DATE. The precise elements of $ DATE that are valid is an interesting exercise in local trivia.

          
          

      47. |- (d2): loset(Dates, <=, <).

      48. loset::= See http://csci.csusb.edu/dick/maths/math_21_Order.html#loset, a linearly ordered set.

      49. +::Dates><Time->Dates.
      50. +::Time><Dates->Dates.
          
      51. |- (d5): For all d1:Time,t1:Dates ( d1+t1 = t1+d1 ).
      52. -::Dates><Dates->Time.
          
      53. |- (d3): For all d1,d2,d3:Dates( d1+(d2-d3) = (d1-d3)+d2).
          
      54. |- (d4): For all d1,d2(d1-d2= -(d2-d1))

      55. ...

          .Dangerous_Bend A common mistake is to think that a light-year is a measure of time. It is a measure of distance - the distance covered by light in one year. At the atomic level the light_second is a simlar useful unit of distance.

      56. light_year::Length, distnace covered by light in a vacuum in one year.
      57. light_second::Length, distance covered by light... in one second.

          [ Velocity and Acceleration ]

          Units of Mass

      58. oz::Units(Mass),
      59. lbs::Units(Mass),
      60. gm::Units(Mass),
      61. kg::Units(Mass).
          
      62. |- (m1): 16.oz=1.lb,
          
      63. |- (m2): 1000.gm=1.kg, ...

          Do not confuse these with the forces that they cause due to the gravity of earth.... [ Force and weight ]

          Angles

      64. deg::Units(Angle).
      65. rad::Units(Angle).
      66. turn::Units(Angle).
          
      67. |- (a1): 1.turn=360.deg=(2*π).rad.

          Angles are an abstraction form the ratios between the radius of a circular arc and ite length.

      68. CIRCULAR::=
          Net{

          1. radius::Length,
          2. diameter::Length=2*radius.
          3. circumference::Length,
          4. area::Length*Length, π:Number::=3.1415... .
             
          5. |- (circ1): circumference=2*π*radius,
             
          6. |- (circ2): area=π*radius^2.
          7. ARC::=
             Net{

             angle:Angle./rad, length:Length, length=angle*radius,area=angle*radius.}.

             
             }=::CIRCULAR.

          8. π::=CIRCULAR.π.

             Information

          9. bit:Units(Information),
          10. byte:Units(Information),
          11. Kb:Units(Information),
          12. KB:Units(Information),
          13. MB:Units(Information),
          14. GB:Units(Information).
              
          15. |- (i1): 1024.bit=1.kb,
              
          16. |- (i2): 8.bit=1.byte,
              
          17. |- (i3): 1024.byte=1.KB,
              
          18. |- (i4): 1024.KB=1.MB,

              
              

          19. |- (i4): 1024.MB=1.GB. |- (i5): baud::=bit/s. |- (i6): bpi::=bit/inch.

              Velocity and Acceleration

          20. Velocity::=dim(L=>1,T=>-1,M=>0,I=>0,A=>0),
              
          21. (above)|- (v1): for all l:Length, t:Times, l/t in Velocity.
          22. fps::Units(Velocity).

          23. mph::Units(Velocity).
              
          24. (above)|- (v2): 60.mile/2.hour=30.mile/1.hour=30.mph.

          25. mph=miles/hour.
              
          26. |- (v3): 1.mph=1.mile/1.hour.
              
          27. |- (v4): 1.fps=1.ft/1.s.
              
          28. (above)|- (v5): x.fps=((60*60)*x/(12*3*1760)).mph.
              
          29. (above)|- (v6): x.ft/s=x.ft/1.s.

              Physicists believe that the speed of light is a fundamental constant - a kind of universal speed limit for all matter. It is often symbolysed by the letter "c":

          30. c::Velocity.
              
          31. |- (c1): c./mph = 186000 (??).
              
          32. |- (c2): light_year=year/c.
              
          33. |- (c3): light_second=sec/c.

          34. Acceleration::=dim(M=>0, L=>1, T=>-2,I=>0,A=>0).
          35. fpss, ...:Units(Acceleration).
              
          36. |- (a1): 1.fpss=1.ft/1.s/1.s.

              Force and weight

          37. Force::=dim(M=>1, L=>1, T=>-2, I=>0,A=>0).
          38. dynes::Units(Force),
          39. newtons::Units(Force).

              
              

          40. |- (f1): dyne=gm*cm/(s*s),
              
          41. |- (f2): newton=kg*m/(s*s),
              
          42. |- (f3): poundal=lb*ft/(s*s)=lb*fps=ftlb/ss,
              
          43. |- (f4): ss=s*s,

              
              

          44. |- (f5): ftlb=ft*lb.

              If g is the acceleration due to gravity in units ug and m is a mass in units of um then the wieght of a mass is the force exerted by gravity, or g*m in the units of ug.um. To simplify some expressions there are special units that take this into account:

          45. lb_wieght::Units(Force),

          46. kg_wieght::Units(Force).
              
          47. |- (f6): 1.lb_wieght= g.poundals.
              
          48. |- (f7): 1.kg_wieght= g.newton.

          . . . . . . . . . ( end of section Common Units) <<Contents | End>>

          Example in Computing

          
          If a track on a hard disk has radius R.inch, turns once every n.s, and stores b.bpi then the transfer rate t.baud will be
      69. t= (2 * π * r / n).baud.
      70. (baud=bit/s=inch*bpi/s, 1.turn=2*π.rad, a disk_track:$ CIRCULAR)

      
      }=::DIMENSION.

   SI Units

   The SI ( System International ) Units are described at [ units.html ] , here is a quick summary.
   1. SI::=
      Net{

      1. SI_base_units::=
         Net{

         
         
         1. |- (SI0): DIMENSION.BASIS.
         2. Dimension_Unit_Abreviation::=Net{ 1st:Dimension, 2nd:units(first). 3rd:=2nd}.
         3. DUA::=Dimension_Unit_Abreviation.
            
         4. |- (SIl): DUA(length, meter, m).
            
         5. |- (SIt): DUA(time, second, s).
            
         6. |- (SIT): DUA(temperature, kelvin, K).
            
         7. |- (SIm): DUA(mass, kilogram, kg).
            
         8. |- (SIc): DUA(electric_current, ampere, A).
            
         9. |- (SIM): DUA(ammount_of_substance, mole, mol).
            
         10. |- (SIL): DUA(luminous_intensity, candela, cd).

             (with thanks to Vince Tilroe, February 17th 2005, who emailed me corrections)

         
         }=::SI_base_units.
      2. SI_derived_units::=
         Net{

         To Be Done...

         
         }=::SI_derived_units.

      
      }=::SI.

   . . . . . . . . . ( end of section SI Units) <<Contents | End>>

   Temperature

   Unlike most units, temperature scales have different zeroes:
   1. Kelvin - absolute zero
   2. Centigrade - melting ice under standard pressures etc.
   3. Fahrenheit - the lowest temperature Fahrenheit could get - mixture of ice and salt.

      This means that the definition of unit implies that temperature is not a unit! Instead we can use a weaker form:

   4. For Dimension D, Scale(D)::=(+)Numbers---D, and formally define:
   5. Temperature::Dimension.
   6. Centigrade::=C::Scale(Temperature).
   7. Fahrenheit::=F::Scale(Temperature).
   8. Kelvin::=K::Units(Temperature).

   9. For all t:Temperature, t./C = t./K + absolute_zero.

   10. absolute_zero::=that temperaturee at which all motion ceases, this is inaccessable as it takes more and more work to extract heat (motion) from something, the closer you get to absolute zero. Absolute zero is the the lowest possible temperature.

       In the centigrade scale:

   11. absolute_zero::= -273.15./C.

       There are well known formulas for converting Fahrenheit to Centigrade and Fahrenheit to Centigrade:

   12. For all t, t./C = (5/9)*(t./F - 32 ),
   13. For all t, t./F = 32 + (9/5)*t./C.

       For details see [ Temperature ] in the Wikipedia.

   . . . . . . . . . ( end of section Temperature) <<Contents | End>>

   Money

   1. money::Dimension.
   2. dollars::units(money).
   3. cents::=units(money).

      
      

   4. |- (usa1): 1.dollars = 100.cents.

      Please add the definitions for any oth currencies that you know about by clicking here: [click here if you can fill this hole]

   . . . . . . . . . ( end of section Money) <<Contents | End>>

. . . . . . . . . ( end of section Dimensioned Numbers) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see