Axiomatising classical mechanics to arrive at the principle of stationary action - what are the fundamental definitions of momentum, etc.? $\newcommand{\d}{\mathrm{d}}\newcommand{\l}{\mathcal{L}}$Throughout all my study of physics, it has never been clear what is a definition, what is an axiom, what is a law and what is a proof in physics. There are many major results, like Newton's laws, Maxwell's equations, the focus of this question - stationary action, conservation of energy, conservation of momentum, potential energy, etc. and all my research on these concepts has lead me slightly in circles. The existence of relativity theory doesn't help, either: when Einstein wrote $E^2=m^2c^4+p^2c^2$, at the end of a presumably lengthy derivation, what definition of $p$ did he use? A photon has momentum but not mass; the top answer on this site that I saw referenced the above equation and derived that the momentum of a photon is "simply $p=E/c$", but to students without the right background, such as myself, this is very circular! Clearly the definition $p=mv$ does not suffice, but what else did Einstein take as his fundamental definition?
Onto the main question:
I will make what I consider to be the most fundamental definitions, not because I've been taught it this way but because this is what I've pieced together, and I'll try to proceed from there. My question to the users on this site is to correct me on my "fundamental" definitions, such as which definition of $p$ did Einstein use, as a formal ground-up construction of physics is not something I have ever seen, which is a shame to me as a mostly mathematical student - in my eyes, without given axioms and definitions, nothing can be shown. I have also not studied relativity and will be working in classical mechanics here, but I would like to have definitions consistent with relativity and quantum theory too. The goal is to arrive at the principle of stationary action, and yes, this has been discussed on this site before but all the answers invoked definitions I am not comfortable with, hence this question. I am confident that my outline of definitions below will be somehow in the wrong order, or wrong in some way, since the definitions are my own in the sense that they are the result of my attempt to make everything non-circular.

Axioms based on observation: every body of a physical system has some mass $m$, a resistance to motion, a position in $3D$ space, $s$, and events occur with respect to some order given by time $t$. Bodies in a system also have an energy $E$, a quantity representing their capacity to act on other bodies in the system, and bodies oppose the transfer of energy. All such properties are observed as, and are assumed to always be, mathematically continuous, differentiable and integrable quantities with respect to time. More definitions:

*

*The velocity $v$ of a body is the time derivative of its position $s$, and the acceleration $a$ is the time derivative of $v$.

*The momentum of the body, $p$, is the partial derivative of the body's energy $E$ with respect to the body's velocity.

*The net force acting on a body, $F(t)$, at some given time $t$ is the partial time derivative of $p$: $$F=\frac{\partial p}{\partial t}=\frac{\partial^2 E}{\partial tv}$$

*The kinetic energy, $T$, transferred over some time interval $[t_0,t_1]$ to a body is the integral of external forces with respect to the position measure: $$T=\int_{t_0}^{t_1}F(t)\cdot\d s(t)=\int_{t_0}^{t_1}F(t)\cdot v(t)\,\d t$$

*When a body is acted upon and it is moved along a path $L$, by an external force $F(s)$ at every $s$ along the path $L$, to it is also transferred a potential energy $U$: $$U=-\oint_LF(s)\cdot\d s$$Where the negative sign represents that body's opposition to the change in position, which exists by axiomatic assumption.


I believe these definitions make sense since if one naively takes $E=\frac{1}{2}mv^2$, then we get the familiar $p=\partial_vE=mv$, and if $m$ is constant then $F=\partial_tp=ma$ is the familiar definition of force. I am unsure if they are consistent with more general theories like relativity. It is important for me to have fundamental definitions of these quantities that are consistent with all of physics, so that I don't get confused when I study those topics later on. The energetic definitions I have seen floating around and I think what I've written is non-circular there, and correct. However, the clause "by axiomatic assumption" at the end there is dubious! Moreover, I have never seen $F=\partial_{vt}E$ written anywhere, so there is probably something awry with that definition. Another problem is that it isn't clear that the definitions of $T$ and $U$ are consistent with each other, in that it isn't clear that they both represent the energy $E$ (which I defined very vaguely...)
Note that $3$ is just Newton’s law, but I’ve always felt it is not really a law (I.e. a logical consequence of something else) but more just a definition (otherwise what is the meaning of force?) If I am mistaken in this belief please correct it!
Onto the Lagrangian mechanics:

Define $\l(s(t),s'(t))=T(s'(t))-U(s(t))$ the Lagrangian of a body. The body will take a (possibly zero) path $\gamma$ in the system as time goes on, from positions $s_0$ to $s_1$. Define $A(\gamma)=\oint_\gamma\l(t)\d t$ the action of the body. It will be shown that the path taken by the body, $\gamma$, is that for which $A(\gamma)$ has a stationary point with respect to the space of smooth paths in the system.

The usual variational calculus derivation occurs, and one arrives at:

$$\frac{\partial\l}{\partial s}=\frac{\d}{\d t}\frac{\partial\l}{\partial s'}$$

Being a necessary condition for $s$ on the path $\gamma$. From the definitions $2,3$ I used, which follow Newton, we have that:
$$\frac{\partial\l}{\partial s}=-\frac{\partial}{\partial s}U(s)=F(t),\quad\frac{\d}{\d t}\frac{\partial\l}{\partial s'}=\frac{\d}{\d t}\frac{\partial}{\partial s'}T(s'(t))=\frac{\d}{\d t}p(t)=F(t)$$
Which is consistent with definition $5$ by the fundamental theorem of calculus. "Therefore" the principle of stationary action is correct and Lagrangian mechanics is consistent with Newtonian mechanics.
Is this correct? I assume my definitions are wobbly... I'd greatly appreciate help on the fundamental construction of mechanics theory. The “therefore” is feels quite weak; is it an actual conclusion?
 A: Both Marsden & Arnold's description of an axiomatisation of classical mechanics uses the apparatus of symplectic manifolds. These are the 'odd' version of Riemannian manifold where the metric is not symmetric but anti-symmetric.
A simple model of classical model begins with a manifold $M$ of configurations. Velocities are then identified with the tangent manifold $TM$ (which is always paracomplex) and momentum with the cotangent manifold $T^*M$ (which is always symplectic). Inertia is identified with a linear isomorphism between the two as in the equation:

$p=mv$.

An autonomous Lagrangian or action density is given by
$L: TM \rightarrow \mathbb{R}$
With the action given by
$S[c] := \int_c L = \int_I c^*L$
Where $c$ is a path

$c: I \rightarrow M$

through configuration space.
Hence velocity should be thought of as a tangent vector and momentum as a cotangent covector.
A: Others have gotten into the weeds, so I'll step back a bit. Sorry to break out a mix of maths, philosophy & physics here, but:

it has never been clear what is a definition, what is an axiom, what is a law and what is a proof

Even in pure mathematics, attempting an axiom/definition distinction overlooks the role of axioms as implicit definitions. The axioms of Euclidean geometry, PA and ZFC respectively discuss "points", "natural numbers" and "sets". They don't explicitly define these, but they characterize them by the axioms they satisfy, to the point their names are only of historical relevance, in that these axioms attempt to capture older intuitive notions tied to natural languages' words. Hilbert made a famous comment about this.
A law is presumably a theorem, or stylized variant thereof, satisfying additional criteria I won't try to summarize. It's certainly not a matter of being fundamental, at least not long after a law is named. As for proofs, the real challenge is in choosing what to assume, not in identifying what was assumed or how it has specific consequences. In the empirical sciences, we have an "it works" criterion; the closest parallel in mathematics is consistency, which is much less selective. That's not to say other criteria aren't used for further selection, though.

all my research on these concepts has lead [sic] me slightly in circles.

There are many equivalent formulations of (for example) mechanics that have different domains of easiest usage, which is why they're all worth learning. If you ask "which is fundamental?", none are. One might be the oldest, but "they're all right, because they're all one theory, which is right" is all the justification physics needs. Why are they right? Mathematics can't prove they are, but evidence kinda sorta can (see also Sec. 7.1 here).

I will make what I consider to be the most fundamental definitions... correct me on my "fundamental" definitions... a formal ground-up construction of physics is not something I have ever seen

For the above reasons, this may be the wrong aim.

without given axioms and definitions, nothing can be shown

Not a priori, no. But that's not how science works. Philosophical subtleties aside, it at least occasionally glances at the world to discover its contingent truths.

The goal is to arrive at the principle of stationary action

I realize you have specific goals I've so far overlooked. If you want something deeper that that principle, this will interest you. The basic idea is quantum amplitudes interfere constructively and destructively, and the mean effect is... basically what the classical version of the aforementioned principle says.

they are the result of my attempt to make everything non-circular

One delicious consequence of empirical knowledge is you don't need to worry about whether you're circular . A "concise" characterization of your theory that doesn't repeat itself the way a circular theory might doesn't have any predictive advantages over one that's open to such an accusation. We know we're (probably approximately) correct because the world tells us so.

Axioms based on observation: every body of a physical system has some mass $m$, a resistance to motion, a position in $3D$ space, $s$, and events occur with respect to some order given by time $t$.

It's one thing to say observation warrants such claims; it's another to take them as axioms, or as unique axioms. Ultimately the entire theory is equally corroborated by the evidence, as a whole; data doesn't say which parts to treat as axioms. The role of proofs (putting aside for the moment how deep we have to go to hit "axioms", whose choice may not be unique) is to help us organize the explanation of many observations as the consequences of a few ideas so that (i) if we discover we're wrong (as sometimes happens!) we have a shortlist of what might "have to give and (ii) motivate unifying efforts so we're not just stamp-collecting.

It is important for me to have fundamental definitions of these quantities that are consistent with all of physics, so that I don't get confused when I study those topics later on.

Sadly, we sometimes revise attempts at such axioms when "all" of physics expands. If it works, it works. My main advice for you, however, is to focus on Lagrangian formulations, if only because they've typically had the least trouble adapting in this manner. For example, Lagrangian mechanics accommodates relativity by becoming a field theory, which accommodates quantum effects with operators. Perhaps the biggest upset this will cause your apple cart is the need to focus on canonical, not kinetic, momenta.

the clause "by axiomatic assumption" at the end there is dubious

Why? An axiom can assume whatever it wants. As long as the final theory is neither inconsistent nor at odds with observation, you're fine.

it isn't clear that the definitions of $T$ and $U$ are consistent with each other, in that it isn't clear that they both represent the energy $E$ (which I defined very vaguely...)

If by vaguely you mean implicitly, sure, but that's fine. And if two quantities aren't "clearly" equal, an axiom can say they are, and hopefully that's never false. As I said, I'm leaving other answers to comment on the general validity of your axioms.

it is not really a law (I.e. [sic] a logical consequence of something else) but more just a definition (otherwise what is the meaning of force?)

Oh, you're definitely wrong about that.
A: You should read  books on mechanics meant for mathematicians:
For example the old classic: A Treatise on the Analytical Dynamics of Particles and Rigid Bodies: With an Introduction to the Problem of Three Bodies by E. T. Whittaker (1944). More  modern is V. I. Arnold Mathematical Methods of Classical Mechanics (Graduate Texts in Mathematics, Vol. 60), or at a more advanced level of diferential geometry there is Foundations of Mechanics
by Ralph Abraham and  Jerrold E. Marsden.
All these treat mechanics axiomatically, and the latter two have treatments that work for relativistic systems.
A: I cannot give a fully comprehensive answer, but some remarks may be complementary, although I am not sure if they are evident to you already:
i) Postulate of Energy is not really needed, since this quantity just amounts to an integral of the motion. Starting from Newoton 3rd law: $F = \frac{dp}{dt} $ (disregarding what $F$ even may be, and for $p$ only postulating, that for single point particles being $m\dot{x}$, where $m$ is just some real proportionality constant) you can modify:
\begin{equation}
\vec{F} \cdot \vec{p} = \frac{d\vec{p}}{dt} \cdot \vec{p} = \frac{1}{2} \frac{d}{dt}\vec{p}^2 \implies  \tilde{E} = \frac{1}{2}\vec{p}^2 - \int \vec{F}\cdot \vec{p} dt 
\end{equation}
For point particles, if $\vec{F} = -\nabla U$, you see that $\tilde{E}$ is not explicitly time dependent. This quantity $\tilde{E}$ is then really convenient if one wants to solve trajectories etc., thus it is given its importance in physics. (ii) I think you mention it, but the process of arriving at the Lagrange equation of the second kind is "simply" to introduce general coordinates $q_k$ which describe the system fully and are not obliged to any constraint. Then one just cleverly manipulates $ F= \dot{p} $ (expressed in $q_k$) until naturally one arrives at $\frac{d}{dt}\frac{\partial L}{\partial \dot{q}} = \frac{\partial L}{\partial q} $ (only for conservative forces of course). One can now recognise, that these equations are exactly the same as the Euler-Lagrange equations in variational problems for $\int L dt$, by which time you can postulate, that the action principle is the more "fundamental" one.
A: The question you raise has been addressed in the most thorough way in the book Gravitation by Misner, Thorne, and Wheeler.
I will first give several quotes, and then I will proceed to phrase my own specific thoughts.
Gravitation, Misner, Thorne, Wheeler
Paragraph 12.3

Point of principle: how can one write down the laws of gravity and properties of spacetime in Galilean coordinates first (par. 12.1), and only afterwards (here) com to grip with the nature of the coordinate system and its nonuniqueness? Answer: (a quotation from par. 3.1, slightly modified): "Here and elsewhere in science, as emphasized not least by Henri Poincaré, that view is out of date which used to say 'Define your terms before you proceed.' All the laws and theories of physics, including Newton's laws of gravity, have this deep and subtle character, that they both define the concepts they use (here Galilean coordinates) and make statements about these concepts."

The discussion in section 3.1 of the book goes as follows:

All the laws and theories of physics, including the Lorentz force law, have this deep and subtle character, that they both define the concepts they use (here B and E) and make statements about these  concepts. Contrariwise, the absence of some body of theory, law, and principle deprives one of the means properly to define or even use concepts.
Any forward step in human knowledge is creative in this sense: that theory, concept, law, and method of measurement - forever inseparable - are born into the world in union.


The following quote is from an answer by physics.SE contributor Kevin Zhou. In an answer on how to introduce the Schrödinger equation Kevin proceeds to put things in a wider perspective:

There is often confusion here because derivations in physics work very differently than proofs in mathematics.


For example, in physics, you can often run derivations in both directions: you can use X to derive Y, and also Y to derive X. That isn't circular reasoning, because the real support for X (or Y) isn't that it can be derived from Y (or X), but that it is supported by some experimental data D. This two-way derivation then tells you that if you have data D supporting X (or Y), then it also supports Y (or X).


Once you finish putting high school math on a rigorous foundation, undergraduate math generally builds upward. For example, you can't use Stokes' theorem to prove the fundamental theorem of calculus, even though it technically subsumes it as a special case, because its proof depends on the fundamental theorem of calculus in the first place. In other words, as long as your classes are being rigorous at all, it would be very strange to hear "we can't derive this important result now, but we'll derive it next year" -- that would be in danger of logical circularity.


This isn't the case in physics: undergraduate physics generally builds downward. Every year, you learn a new theory that subsumes everything you previously learned as a special case, which is completely logically independent of those earlier theories. You don't actually need any results from classical mechanics to completely define quantum mechanics: it is a new layer constructed below classical mechanics rather than above it. That's why definitions now can turn into derived things later, once you learn the lower level. And it means that in practice, physicists have to guess the lower level given only access to the higher level; that's the fundamental reason why science is hard!



History
A defining moment in the history of science was the recognition of non-Euclidean geometries. Up until that point Euclidean geometry was in effect treated as a physical theory of what space is.
We have that hyperbolic geometry and spherical geometry are self-consistent, and just as expressive and just as rich as Euclidean geometry.
A mathematical framework (such as geometry) exists in and of itself. It can correspond to something in the real world, but it doesn't have to. In that sense a mathematical framework is pure abstraction.
In order for a framework of thought to count as a mathematical framework satisfying one specific condition is sufficient: it must be free of self-contradiction. (Of course, that is a very, very demanding condition.)
The idea of axiomatization is that it enforces unification. The scholars of ancient Greece had obtained a lot of geometric results, but how to be sure that that body of knowledge is free from self-contradiction?
Euclid recognized/expected: by formulating axioms of geometry and subsequently deriving all theorems from those axioms: absence of self-contradiction is assured.


Logic and axiomatization
In any logical system there is great freedom to exchange axiom and theorem without changing the contents of the system.
Axiomatization of a mathematical framework is not unique. Things do get narrowed down, of course, but generally there will be multiple equivalent permutations.


Theories of physics
Attempting to axiomatize a theory of physics is not a good idea. If you do try you are only bogging yourself down.
Specifically, If you would try and attempt to impose a fundamental separation of definition, axiom, law, result, etc. you are only bogging yourself down.
Technology is where the rubber meets the road. Do we have a good understanding of celestial motion? Well, our theory of celestial motion is applied in planning the course of space probes, such as the Voyager space probes. Each flyby was a gravity assist onto a course towards the next goal. The fact that the technology works as designed is evidence beyond reasonable doubt that the theory the technology is based on isn't circular reasoning.


Kepler problem without the fixed stars
To illustrate my point let me discuss the following thought experiment of doing astronomy without the benefit of fixed stars:
Let's say that one galaxy swept close by another galaxy, and a tidal tail is ripped out, resulting in a runaway star. Let's say this lone star has a planetary system exactly like our solar system. Let's say that after billons of years life has evolved on the counterpart of the Earth, an intelligent species has evolved, and the counterpart of our Kepler is trying to work out laws of planetary motion. From here on I will refer to this counterpart Kepler with the same name: Kepler.
The distance to the surrounding galaxies is so large that none of them are visible with the naked eye. Under those circumstances: is it still possible for Kepler to find laws of celestial motion?
Our historical Kepler had the benefit of astronomy being able to use the fixed stars as reference of planetary motion. So what is still possible without fixed stars?
Kepler does have that the motions of the planets are roughly co-planar. The rotation rate of the Earth can be inferred by charting the motion of that plane; the period of the rotation of the planetary plane is the counterpart of the sidereal day. The plane of the Earth's orbit and the equatorial plane are at an angle to each other. In our astronomy that line marks the equinoxes. That intersection line can be put into service as a reference of motion.
What that shows that that celestial motion itself can provide reference of motion.
The celestial motion can serve as a reference of motion because that motion has strong regularities; the motion results from a mathematically expressible property; the inverse square law of gravity.
Kepler's laws of motion obtain if and only if the motion of the celestial bodies is referenced with respect to an inertial coordinate system.
The equinoxes provide a jumping off point. Kepler can use the equinoxes as the fixed point to reference the positions of the planets. This illustrates that even without the benifit of the fixed stars as reference it is still possible to solve the Kepler problem
(There is the precession of the equinoxes, but that precession is slow enough to not prevent Kepler from figuring out laws of celestial motion. Over time the precession of the equinoxes will be recognized, and it will be accounted for.)


Process of mutual reinforcement
In the Principia Isaac Newton proceeded to show that Jupiter is so heavy that our Sun is orbiting the center of mass of our Solar system at a distance slightly larger than the Sun's radius.
Here is why that is significant:
The position of the center of mass of the Solar system is inferred from the motion of the celestial bodies.
There is no such thing as first defining the center of mass of the solar system, and then proceed to figure out the law of universal gravity.
The process of homing in on ever more accurate assessment is a process of steps of mutual reinforcement.
This process of homing in on ever more accurate assessment in steps of mutual reinforcement is everywhere in science. It is fundamentally how science makes progress.
That is the significance of the quote from Misner, Thorne, Wheeler.
It is inherently impossible to first define concepts and only then start finding out laws of physics. The laws of physics are the definitions of the concept you are using.

That is why implementation of theories in design of machines is essential. If the machine works according to the specification then the theory that informed that design is corroborated.
