Gareth’s blog

Sunday, May 08, 2005

"Project1" virus (pictures.templates4friends.com MSN messages)

Having just sorted this I thought I should write something about it. Ben received a message over MSN similar to this earlier this evening:

Username: rofl is this you?
Username: http://pictures.templates4friends.com/ pictures.php?email=emailaddress@hotmail.com

He clicked the link and ended up installing a program "Project1" running the process spool.exe in C:\Documents and Settings\[User name]\. Installation and a quick scan with Microsoft Windows AntiSpyware (Beta) detected it and a few other bits of spyware and seems to have sorted it out. Microsoft's Antispyware had some initial problems, detecting Firefox as spyware, for example but the software was easy to use. The interface didn't seem too bad either, though the menus at the top seemed to operate rather strangely, the scroll bars don't seem to resize according to content and nothing else can be done while the software is scanning.

A reinstallation apparently also works, but it's probably worth installing Antispyware to catch anything else which has been inadvertently clicked.

Read more at Symantec Security Response and McAfee.

Saturday, May 07, 2005

Notes on "Mathematics to Logic: It's Evolution from Logic to Mathematics"

Earlier this evening Chris, Cai and I went to a talk. Cai and I had a bit of a competition taking notes, and here are mine (now with additions by Cai to). I understand this is likely to be of very minority interest, but having typed it up I thought I might as well post it.

G.C. STEWARD LECTURES (1 of 3) at the Bateman auditorium, Gonville and Caius College, Cambridge, Friday 6th May 2005 17:00 to 18:00 by Angus Macintyre

(Lectures 2 and 3 rescheduled to 3:45 on Monday 9th May and Friday 13th May 2005 in MR3 at CMS, Clarkson Road, Cambridge.)

1. Dedekind to Turing c.1950 to c.1940: The Mathematics of 1850

  • Quality at least as high as that of today (Contributions from the likes of Gauss, Abel, Galois, Jacobi, Riemann etc.)
  • Turmoil in geometry, non-Euclidean geometries, Riemann's foundations, generalisation of space, beginnings of Topology.
  • Elliptic functions and marvelous formulas, but often without the rigour one (usually) demands later.
  • Systematic development of algebraic number theory.
  • Groups everywhere
  • "Impossibility results" in theory of equations or transcendence theory or integration in finite terms or geometry.

2. "Flaws"

  • In analysis, concerning various processes like sums and integrals.
  • In geometry, concerning continuity assumption.
  • Vagueness of notion of a function.
  • Absence of notion of formal proof (and no need for it).
  • Sporadic use of infinitesimals.
  • Inability to say what one was talking about (infact, rarely a barrier to doing important mathematics).
  • Only sporadic axiomatic activity (not always a flaw).

3. Subject matter

  • Geometrical conception.
  • Numerical conception (integers, rationals, complex numbers and functions).
  • The question if either/any are fundamental.
  • How to cope with the questions of philosophers like what is a point, an integer, a real number or an infinitesimal?
  • One may fruitfully change this to what are the properties of a point, integer, real number of infinitesimal and what properties Mathematics presupposes.

4. What was imminent?

  • Language of infinite set theory (already viewed with suspicion by Gauss).
  • Cantor's two kinds of transfinite arithmetic with immediate impact on analysis and the source of more suspicion.
  • The development of predicate calculus by Frege and Peirce.
  • Frege's analysis of the notion of natural numbers via 'higher-order notions' (concepts like sets).
  • Formal languages and deductive systems for all of mathematics.
  • Flaws in Frege's foundations (around notions he used to define numbers, discovered Cantor, though he didn't really care (was this because he wasn't much bothered about the formalisation of maths?). Bertie Russell was another of the people who found flaws, and he made a big fuss about it.)

5. A diagram

  Higher order notions
          /\
          ||
          ||
          ||
  Working mathematics
          ||
          ||
          ||
          \/
    Formal aspects
  • Mathematical logic would develop by confronting formal and higher order notions.

6. Dedekind's analyses of integers and real numbers

  • What is at issue is not what they are but what shape they are.
  Z+: 0  1  2  3  ....
         S0 S1 S2           (S = successor)
  • 0 is not a successor.
  • All other members of the natural numbers are successors of unique elements. [First order]
  • Every subset containing 0 and closed under successor is equal to the natural numbers. [Second order]
  • First order means quantification only over elements of N (S is given).

7. Isomorphism

  • If (N1,S1), (N2,S2) are models of these axioms there is a unique bijection f: N1 → N2 respecting successor.
  • Related definability: + and * are second order definable from 0 and S. If you allow function or relation quantifiers, but not first-order quantifiers [missing text] first order definable from them. It would eventually be proved that second order axioms are crucial in the above even if +, * are allowed as primitive notions (Skolem, 1934).

8. The shape of the real numbers

  --------------------------------------------
  -infinity                          +infinity
  • An ordering '<' exists, the real numbers are densely ordered and posess no end points. [First order]
  • They are complete, sets bounded above have least upper bounds and sets bounded below have greatest lower bounds. [Second order]
  • Still something is missing, there are various ways to close the gap depending on whether you allow more primitives.
    • Say that there is a countable dense subset.
  • Once again, isomorphism theory, which demand a second order setting and is false for any first order axioms, no matter what primitives are allowed, in particular gets models with infinitesimals as in the nonstandard analysis of Robinson (1960).

9. From natural numbers to real numbers

  • From natural numbers to real numbers to rational numbers is essentially formal, but from rationals to reals is essentially a higher order process and can be done in several ways.
    1. Elements of the set of real numbers as Dedekind cuts in the rationals.
    2. Elements of the set of real numbers as sets of convergent sequences from the rational numbers.
  • In either case one needs set theoretic principles to develop the mathematics of the real numbers.

10. Conceptual analysis of the natural numbers

  • Frege: The meaning of statements of arithmetic (including answering the question 'what is an integer?') can be analysed in terms of the high-order logic of concepts and extension. Though this proved to be logically flawed, key ideas survive allowing the development of much arithmetic in terms of set theory and so the development of much mathematics.

11. Unnatural

  • Various eminent mathematicians (Hilbert, Brouwer) denied the meaning of elementary combinatory arithmetic (i.e. irrationality of root(2)) could be dependent on the logic of higher order notions (logic should be proven like all other mathematical principles).
  • Brouwer: The concept of an integer is basic, but it is illegitimate to take classical logic as a basis for proof, it has to be established when valid. On the other hand, higher order notions have meaning, but not the classical one.

12. Hilbert and formalisation

  • Though his work on number is flawed and had an unfair effect on the reputation of cantor's transfinite arithmetig Frege's work on predicate calculus is beyond reproach and is the basis for all that ensued in mathematical logic.
  • Frege codified valid principles in both first order and higher order logic and corresponding principles of deduction. These were perfectly adapted to existing mathematic argument.

13. Metamathematics

  • This was the direction that the work was going after Frege.
  • This apparently allowed a precise formalisation of all existing mathematics turning proofs into formal deductions from formal axioms.
  • This subject matter is finite combinatorial virtually identical with formal arithmetic (obviously, even without any glamorous coding).
  • More over it now has prominent algorithmic aspects
    • Testing formula is mechanical (like testing for a prime).
    • Testing proof fro algorithmically given axioms is mechanical but...

14. Testing provability

  • Testing provability is not obviously mechanical, because of hidden quantification - 'there is a proof' (analogous to 'there are integers'). [Testing truth has a meaning in some cases, less clearly in others]
  • Frege systems can generate proofs nondeterministically just as one can generate solutions of equations in integers but waiting time is unknown.

15. Using analysis to prove theorems in number theory

  • One found many examples in the 19th century (e.g. on distribution of primes) and one naturally asks if there are mechanical ways of converting the higher order proof to a first order one. [The answer is not obvious but it 'usually, yes']

16. Various formal systems

  • These arose either form
    • Limited subject matters e.g. geometries, algebras, arithmetic;
    • Potentially universal subject matter e.g. Mathematica Principa or the axioms ZFC for set theory.
  • In all cases the axioms and rule are mechanically recognisable [You do not need tan exact definition of mechanical for this].
  • Hilbert had proved relative consistency between various geometric and algebraic systems and came to possibility of showing consistency of strong systems by weak methods and/or transforming higher order proof of first order conclusion into first order proofs of such conclusion and deciding algorithmically, validity or provability or truth. [Now you will need a definition of algorithmic if you want negative results]

17. The impossibility theorems

[Godel, Church, Turing in the 1930s]

  • Higher order method not eliminable for the standard systems of arithmetic.
  • Consistency usually not provable by elementary means.
  • Strong systems cannot prove their own consistency.
  • Predicate calculus is mechanically unpredictable.
  • Truth in arithmetic is mechanically undecidable.
  • It became a possibility that there is not algorithm for deciding if Diophantine equations have integer solutions.

18. Positive outcome

  • The precise models of idealised computers which Turing came up with. These so-called 'Turing machines' are computers which are not bounded by limits of processing power or memory, but must have only finite programs.
  • Deep understanding of recursive definitions.
  • Lambda calculus for later use in computer science.
  • Some novel ways of defining arithmetic functions from + and *.
  • Development of sophisticated proof theory, precursor of technique of extracting constructive information from overtly nonconsecutive proofs, so-called 'proof mining.'