Newton's second law
$$\mathbf{F} = m\mathbf{a}$$
where $\mathbf{F}$ is the force, $m$ the mass, and $\mathbf{a}$ the acceleration, seems at first blush to be a simple tautology, since $\mathbf{F}$ and $m$ are not defined anywhere else in the formalism. Of course we can use the more general formulation
$$\frac{d\mathbf{p}}{dt} = \frac{d(m\mathbf{v})}{dt}$$
with $\mathbf{p}$ the linear momentum and $\mathbf{v}$ the velocity, but given the usual elementary definition of linear momentum $$\mathbf{p} \equiv m\mathbf{v}$$
this seems hardly an improvement.
Have I missed something? Perhaps in the Lagrangian or Hamiltonian formulation one can use Noether's theorem etc. to give a less trivial definition of $\mathbf{p}$? Or is there something even more elementary than that which I've missed?
Now, the law is clearly not tautologous in concert with some kind of force law, such as Coulomb's law or the law of universal gravitation. In that case we know what force means independently of mechanics. I'm just wondering if mechanics can be viewed as logically self-contained without recourse to such an addition.