Although I'm not sure if anything here applies to my case, it does seem to be a case of abstract mathematics represented in Mathematica. I will look into it further.

Thank you very much for taking the time to answer!

I do not know how it is possible, from my question, to conclude that I expect Mathematica to know all of mathematics, and prove the necessary theorems for every question that might be asked. It seems to me that I have presented 4 axioms, only 3 of which I have presented completely, and am asking if Mathematica can represent those 3, or even just one, of the axioms, in the Wolfram Language.

The obvious way to answer in the affirmative would be to provide a translation of one of those axioms. This would be very helpful to me, and I'd really appreciate it if someone could spare a few mins to do it (it probably wouldn't take more than a few mins for an expert).

Yes, I am asking if the Wolfram Language can represent the axioms of specific field (which is different from saying that I expect the axioms to be built into Mathematica - I am merely asking for the tools to program them in myself). The axioms I provided are 3 from about 20 axioms of the Newton-Poisson theory of gravitation, as formulated by Mario Bunge in his book "Philosophy of Physics" (1973).

I find it very interesting that the axiom system of Grassmann algebra can be represented in Mathematica, although that does necessarily mean that my axioms can. You also seem to suggest that you can deduce Euclidean theorems from the axioms. I like this idea a lot - could you please point me a publication where I can learn about it? Also, could you show me an axiom or two represented in the Wolfram Language, as illustrative examples?

Thanks!

Yes, it certainly seems to be. I was aware of it, but just wanted to confirm (by asking this question) that the kind of things I'm trying to do are indeed the ones Wolfram states (in the blog entry) that Mathematica cannot presently do.

In that case, my question is: is there any add-on to Mathematica, or an entirely different system (Magma, maybe?) which CAN do things like this? Theorema (mentioned above) might aspire to this end, but is in a very early stage of development, and not helpful to me as of now.

Thank you for your reply. However, I have already experimented with Theorema, and while its ultimate goal might be to handle cases like mine, it is nowhere to close to that right now. At this moment, it does not even have axioms for set theory built in, let alone metric spaces, tensors and integrals.