Fundamental question about capabilities of Mathematica to represent abstract mathematics [closed]

I have an fundamental question about what Mathematica can and cannot do.

I have a book which presents a certain physical theory in an axiomatic manner. The axioms make heavy use of mathematics.

Some representative examples of the axioms it contains are as follows (this is certainly not the complete set of axioms provided):

1. Let $M^3$ be a 3-dimensional metric space with metric tensor $g$.
2. Every $U_{\gamma }\in \left\{U_{\gamma }\right\}$ and it's first order derivatives are smooth on $M^3$.
3. Every $\rho \in \{\rho \}$ is a function from $B M^3 T$ to a set of nonnegative reals, Lebasgue integrable over any finite region of $M^3$.
4. For every $\gamma \in \Gamma$, every ..., there exists at least one $k \in K$ such that $\rho \ddot{X}=\text{divT}-\rho \nabla U$.

Where the symbols have their usual meanings in mathematical physics. Then, after many more axioms and definitions in this vein, several 'theorems' are stated and proved from the axioms and definitions.

My questions are as follows:

1. It is somehow possible to represent these mathematical statements in Mathematica? The focus here is not on the specific axiom system I chose, but axiom systems of this general nature. For example, this particular axiom system uses tensors, which may or may not be representable in Mathematica, but that is not the point. Even if tensors are not representable, axioms systems of this nature which happen not to use tensors may be representable (or not). Whether or not they (likely) are, is the question I'm asking.
2. If representable, is it then possible to use FullSimplify (or any other feature of Mathematica) to check if other statements follow from using these as assumptions, which is my main goal, or otherwise manipulate these statements in any manner? (For example, I know how to use FullSimplify to determine whether or not the square root of 2 is rational, but of course, that is trivial compared to anything involving these axioms.)
3. If not representable, is there any third-party package for Mathematica, free or commercial, which would make the goal possible?
4. If still not possible, is there any other computer algebra system currently existing, free or proprietary, which would make the goal possible (Magma, maybe?)?
5. If still not possible, why do you think that is the case? Is it somehow fundamentally impossible (which I doubt) or difficult to do this using a computer? Is this technology we (as in the human race) are on the verge of achieving, or something which might happen decades later, or not at all?

In asking this question, am I fundamentally misunderstanding the nature and purpose of Mathematica and what it can do? If so, why? I had the impression that Mathematica specializes in symbolic manipulation, as opposed to something like MATLAB, which specializes in numerical computation. My example certainly seems to be of symbolic manipulation, though of an abstract nature.

Note:

I am aware that the main goal is, in principle, achievable using an automated theorem prover like Prover9, but in practice, impractically difficult, requiring axioms of all the mathematics involved - sets, numbers, analysis, geometry, etc, all built on top of each other and ultimately on first order logic - possibly thousands of axioms, causing a combinatorial explosion in any proof that is attempted.

closed as too broad by Jens, bbgodfrey, m_goldberg, Dr. belisarius, Bob HanlonMay 8 '15 at 12:13

Please edit the question to limit it to a specific problem with enough detail to identify an adequate answer. Avoid asking multiple distinct questions at once. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• Have you looked at the documentation for Resolve and Reduce? You can certainly derive other statements from given expressions. So the answer to question 2. seems to be yes, and that makes the other points of the question moot. But as to your first points, you'll have to do some work to bring your statements into the form of Mathematica expressions. It would certainly be appropriate as a question, but I think you would need to show some example of what you have already tried to make this question less ambiguous. As is, it's not easy to parse by a human, let alone a program. – Jens May 7 '15 at 22:03
• Thank you for your response, which gives me some hope. The trouble is, the axioms I have stated are exactly as provided to me, and that's all I have to go by. I do not already know how to translate them to Mathematica - if I did I would not have posted this question. So, if there is a direct Mathematica Language translation for the sentence 'M3 is a 3-dimensional metric space with metric tensor g', I would need someone to provide me with it, or at least point me in the right direction, from where I may be able to find out on my own. – Atriya May 7 '15 at 22:11
• PS There is some strong evidence that perhaps the translation cannot be done (contrary to what you say), such as a blog post from Wolfram which states that Mathematica needs major work before it's useful to pure mathematicians. I'm not sure if the kind of pure mathematics Wolfram is talking about applies directly to the situation I have at hand, which would be depressing. That's why I asked the question. Here's the blog post: blog.stephenwolfram.com/2014/08/…. – Atriya May 7 '15 at 22:18
• For what it's worth, I disagree with the decision to close this question because it's too broad and that there are many possible answers. I am clearly asking for translations to Wolfram Language of 3 precise mathematical statements, the first being 'M3 is a 3-dimensional metric space with metric tensor g'. This statement is not vague or ambiguous, and it is possible that someone might be able to provide a translation for it (if that can be done at all). – Atriya May 8 '15 at 12:28
• – Michael E2 May 9 '15 at 11:30

Mathematica has logical symbols such as $\exists$, $\forall$, $\in$, $\wedge$, and so forth and can be used in statements such as ForAll[{a, b}, a > 0 && b > 0, (a + b)/2 >= Sqrt[a b]]. One performs simple logical resolution by Resolve[] applied to such an expression. I suspect Mathematica can simplify or resolve such logical and existential statements, and test whether two such statements are equivalent (through statement1 == statement2), but not make inferences to find new such statements.

As for statements such as $M^3$ being a metric space: I think you would have to do something along the following lines (meant as a pointer in the right direction, not a full solution):

myTriangleInequality =
a > 0 && b > 0 && c > 0 && a + b > c && a + c > b && b + c > a;
myTest = ForAll[{a, b, c}, myTriangleInequality,
a b c (a^2/b^2 + b^2/c^2 + c^2/a^2) >=
a^3 + b^3 + c^3 + a b (b - a) + a c (a - c) + b c (c - b)];
Resolve[myTest]

(* True *)

For your case, you'd have to incorporate a metric tensor $g$ and so forth.

In short, I think you'd have to be pretty specific about defining the properties of your abstract structures in logical expressions.

• Yes, I am well aware that Mathematica can represent logical connectives and quantifiers and perform operations on them. For example, to prove that Sqrt is irrational, I used FullSimplify[Exists[{a, b}, Element[a,Integers] && Element[b, Integers] && a^2/b^2 == 2 ]]. However, that does not answer my question, which was about Mathematica's ability to represent abstract mathematical structures and perform (abstract) operations on them. The 'axioms' provided are examples of the kind of statements I need to represent. – Atriya May 7 '15 at 21:39
• Thank you for your updated answer, with the code provided. However, I think we are still in disagreement over the level of abstraction required. I realize that if I have a particular metric space in mind, with a particular metric tensor, I would perhaps be able to represent this in Mathematica. However, that is not the point. The point is whether I can represent the statement that M3 is A metric space - ANY metric space - and that g is A metric tensor - ANY metric tensor. – Atriya May 7 '15 at 23:03
• If such a translation were possible, manipulating that in Mathematica would be equivalent to the level of abstraction of a mathematician proving things about metric spaces and tensors themselves, not things about a specific metric space and tensor they might happen to be interested in. Your code seems to suggest a test of whether a particular space is or is not a metric space, which would be a lower level of abstraction. In a treatise written by the above mathematician, such endeavors would feature in examples, but not in proofs. – Atriya May 7 '15 at 23:03
• I apologize if the above is a misunderstanding of your code. I am not a mathematician, but a philosopher (rather a student of philosophy). – Atriya May 7 '15 at 23:12