Can multiplication be defined in terms of divisibility? Peano Arithmetic has two axioms which use the multiplication symbol: ∀x:x*0=0 and ∀x:∀y:x*Sy=x+x*y.  The 2-term relation "x divides y" can be expressed as D(x,y) := ∃z:z*x=y.  Multiplication is a function and divisibility is a relation, so in order to compare apples and apples, consider the 3-term relation M(x,y,z) := x*y=z and the axioms ∀x:M(x,0,0) and ∀x:∀y:∃u:∃v:M(x,Sy,u)∧M(x,y,v)∧v+x=u and also the fact that M is a function ∀x:∀y:∀u:∀v:(M(x,y,u)∧M(x,y,v))→u=v.  Now D can be defined in terms of M by D(x,y) := ∃z:M(z,x,y).  I wonder if it is possible to do the reverse, and define multiplication in terms of divisibility.  If the M axioms are replaced by some D axioms (maybe ∀x:D(x,x), ∀x:D(x,0), and others), can M be expressed in terms of D?  Prime, GCD, LCM can all be defined in terms of D alone, but I don't know how to define M in terms of D, nor do I know how to axiomatize D without reference to M.  If it is possible, what axioms are required for the divisibility relation, and how is the multiplication relation defined?  If not, why not?

No, not in general.  You can define the multiplication relation in terms of the division function, but this only gives you a truth condition M(x,y,z) that tells you if z is the product of x and y.  It does not give you a mechanism for generating the z from the x and y: for that you need to be able to prove that the multiplication relation specifies a total function.  
And this is not always possible:


*

*There are weak theories of arithmetic for which division is total, but where, although the multiplication relation exists, and specifies the expected triples, the relation cannot prove the multiplication is total (and so admits nonstandard models in which there are multiplication relations but all have "holes" at nonstandard number parameters and so are not functions);

*Even worse, there are such weak theories which would be rendered inconsistent by the addition of an axiom asserting that multiplication was a total function.   All self-verifying theories are of this sort.

