Fundamental question about symbolic capabilities of Wolfram Language

Posted 8 years ago
7949 Views
|
12 Replies
|
3 Total Likes
|
 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): Let $M^3$ be a 3-dimensional metric space with metric tensor $g$. Every $U_{\gamma }\in \left\{U_{\gamma }\right\}$ and it's first order derivatives are smooth on $M^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$. 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: 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. 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.) If not representable, is there any third-party package for Mathematica, free or commercial, which would make the goal possible? If still not possible, is there any other computer algebra system currently existing, free or proprietary, which would make the goal possible (Magma, maybe?)? 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.
12 Replies
Sort By:
Posted 8 years ago
 Did anyone hear of Coq?
Posted 8 years ago
 I have. I understand that it's partly a theorem prover. From what I understand, theorem provers can, in principle, prove (or try to prove, given limited time resources) any theorem in mathematics, no matter how abstract, since all of mathematics is apparently reducible to FOL. In practice, however, this would require thousands of axioms, and impossible amounts of time for any non-trivial theorem.That's why it may be beneficial for a theorem prover to integrate/communicate with Mathematica. However, no such link exists with Coq. The only theorem prover I know of which does integrate with modern versions of Mathematica is Theorema 2, which is in too early a stage of development to be useful for non-trivial proofs. (There's also Analytica, which is old, and doesn't work on Mathematica versions after 4 or so.)
Posted 8 years ago
 I don't know if this qualifies for your first case but this is how a three dimensional space could be set up in GrassmannCalculus. The following declares a 3-dimensional point space with coordinates x, y and z, and establishes it with a vector basis. The other choice is an exterior form basis. This also establishes a, b, c, d and subscripted g's as scalar symbols in the system. The symbols p, q, r and s are established as symbolic vector symbols. A Grassmann point space is one that has an origin as well as free vectors. You can declare spaces with and without an origin and with and without a metric. (The FivePointedStar character doesn't display nicely in a posting. )You now have a space with all the facilities of Grassmann algebra built in. << GrassmannCalculus SetGrassmannNSpace[3, {x, y, z}, "Vector"] \[FivePointedStar]S[a, b, c, d, Subscript[g, _, _]]; \[FivePointedStar]V[p, q, r, s] The following shows a basis palette that is established for all grades of the algebra. These are buttons that will paste to the notebook. You can switch to a form basis with: SwitchBasis["Form"] The new Basis palette is:The following declares a specific symbolic metric. DeclareMetric[ DiagonalMatrix[{Subscript[g, 1, 1], Subscript[g, 2, 2], Subscript[g, 3, 3]}]] The following is the metric palette that shows the induced metrics associated with each sub-algebra of various grades. The following is a palette with Mathematica Rules for exterior products. These are rules for Regressive products. Again, these can be pasted into a notebook.These Rules are built into most of the symbolic operations, but they do give some ability to do detailed manipulation.I hope this is some help. It does give a taste for what can be done with Mathematica. John Browne's book on Grassmann Algebra is available at: Grassmann Algebra Book I'm currently implementing the use of Mathematica 10 Associations. These are quite nice because everything is retrieved by keys and the particular order of things in the Association is not important. So a user could create an Association for his particular problem that contained the core data for Grassmann algebra, but then add other items such as charts for a manifold and transition functions between them - or whatever pertained to the particular project.
Posted 8 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 8 years ago
 This is an interesting question and discussion. If Atriya is asking if Mathematica can or could know all of mathematics and find, or prove on the fly, the necessary theorems for every question that might be asked, then I'm certain the answer is no. But if something more modest is asked for, say representation of the structures and axioms of a specific field, then I think Mathematica can do a fairly good job. I've been working with John Browne on his Grassmann algebra and Grassmann calculus application. This is built up on an axiom system and the axioms are represented either in definitions or often in rules that are available and can be applied to symbolic expressions. Its applications are certainly limited to a specific area but that area is extremely broad, extending from simple exterior algebra to the generation of hyper-complex algebras including symbolic quaternions and octonions. Going back to the simple end, it's easy to use the algebra to prove Euclidean theorems. And, of course, it's useful in practical calculations.So yes, the symbolic capabilities of Mathematica are very good - but you can't expect to start from zero, or encompass all possible mathematics.
Posted 8 years ago
 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!
Posted 8 years ago
 This blog entry may be relevant: Computational Knowledge and the Future of Pure Mathematics
Posted 8 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 8 years ago
 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:
Posted 8 years ago