How can I semi-automate mathematical proofs using Mathematica or other tools?

[jordi]

I am looking for a method to semi-automate mathematical proofs. Precisely, what I would like is that, if for example I define (sorry, I have never used latex in this forum, and I still do not know how to do it yet):

f[A] := {y|\existsx\inA (y=f(x))}

then, if I have

f[A\cupB]

what I would like is to make a call to the definition above (something like F[f=f,A=A$$\cup$$B]) and that the math editor (maybe Mathematica) just writes

f[A\cupB] = {y|\existsx\inA\cupB (y=f(x))}

where the = has a link (hyperlink) to the initial definition (ie, if I click on it, I go to the original definition).

How can I do that?

1. Is there in Mathematica functionality for that?
2. Is there a package that does that, not Mathematica?
3. If not, can I program in a programming language, using latex symbols?

 

[EnumaElish]

You should be able to do this by using either of the Module or Block functions in Math'ca.

 

[jordi]

You should be able to do this by using either of the Module or Block functions in Math'ca.

Let us say I want to proof something very simple, eg, A U (B U C) = (A U B) U C.

If I define:

UnionToSet=Function[{A,B},body={x|x\inA||x\inB}]

I start the proof with:

UnionToSet[C,UnionToSet[F,G]]

that gives me:

{x|x\inC||x\in{x|x\inF||x\inG}}

Now I need to apply the axiom:

x\in{x|P(x)} iff P(x)

I find then a problem:

In my definition of UnionToSet, the body is only a string of characters. What I would like is to be able to define an object, Set(P), which is a functional on the set of “acceptable logic statements”, that is equivalent to {x|P(x)}. This object should have methods, like Belongs(x,Set(P)), and Property(x,Set(P))=P(x).

I have googled a bit, but I cannot find anything like this. It is strange, because I think a mathematical package should have an object for defining sets, for belonging, for logic statements... and I think quite natural that mathematicians working with Mathematica would want to state their axioms and let the package to automate the proofs.

Note: for the record, the above proof should be ( means belongs to)\in

CU(FUG)={x|x\inC||x\inFUG}}={x|x\inC||x\in{y|y\inF||y\inG}} = {x|x\inC||(x\inF||x\inG)} = {x|(x\inC||x\inF)||x\inG} = {x|x\in{y|y\inC||y\inF}||x\inG}={x|x\inCUF||x\inG}}=(CUF)UG.

What I would like is that every time I write “=” and I refer to it a given theorem/axiom/whatever, the program automatically applies this theorem/axiom/whatever and writes the corresponding right hand side.

CU(FUG)=Set(P = *\inC||*\inFUG)=Set(P = *\inC||*\inSet(P=**\inF||**\inG ))=Set(P = *\inC||(*\inF||*\inG ))
=Set(P = (*\inC||*\inF)||*\inG )=Set(P = (*\inSet(P=**\inC ||**\inF ))||*\inG)=Set(P = *\inCUF||*\inG )=(CUF)UG.

 

[jordi]

You should be able to do this by using either of the Module or Block functions in Math'ca.

I have seen that there is a package in Mathematica called SetTheory.m. Apparently, it automates the proofs in set theory and logic. Has anybody used it? Is it possible to use it for proofs not only in set theory and logic, but in all other areas of mathematics?