Group Abstract Group Abstract

Message Boards Message Boards

1
|
10.4K Views
|
12 Replies
|
4 Total Likes
View groups...
Share
Share this post:

Fundamental question about symbolic capabilities of Wolfram Language

Posted 11 years ago

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.

POSTED BY: Atriya Sen
12 Replies

Did anyone hear of Coq?

POSTED BY: Sam Carrettie
Posted 11 years ago
POSTED BY: Atriya Sen
Posted 11 years ago

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!

POSTED BY: Atriya Sen
Posted 11 years ago
POSTED BY: Atriya Sen
Posted 11 years ago

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.

POSTED BY: Atriya Sen

What do you mean:

... the kind of things I'm trying to do are indeed the ones Wolfram states (in the blog entry) that Mathematica cannot presently do.

A direct quote from the blog would be nice to support your statement, could you please post it?

I think the blog gives you examples of exactly what you looking for, for instance:

So what happens when we generate a proof automatically? I had an interesting example about 15 years ago, when I was working on A New Kind of Science, and ended up finding the simplest axiom system for Boolean algebra (just the single axiom ((p?q)?r)?(p?((p?r)?p))==r, as it turned out). I used equational-logic automated theorem-proving (now built into FullSimplify) to prove the correctness of the axiom system. And I printed the proof that I generated in the book:

enter image description here

POSTED BY: Sam Carrettie
Posted 11 years ago
POSTED BY: Atriya Sen

Take a look at the The Theorema System package.

POSTED BY: Frank Kampas
Posted 11 years ago

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.

POSTED BY: Atriya Sen
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
Attachments
Remove
or Discard