# Can I define an axiomatic (Boolean algebra) system and prove theorems using Mathematica?

The general question is

Can I define an axiomatic system and prove theorems using Mathematica?

The more concrete one is about Boolean algebra.

I consider this axiomatic Boolean algebra system (wiki).

How can I

1. define the six (or twelve) axioms there in Mathematica and

2. then let Mathematica prove theorems in the user-defined axiomatic system, instead of the built-in system in Mathematica?

(Theorems like: De Morgan's law ($$\lnot(a \lor b) \equiv \lnot a \land \lnot b$$) or the easier (maybe harder) ones such as $$\lnot(\lnot a) \equiv a$$ and $$\lnot 0 \equiv 1$$.

You are not limited to Boolean algebra. You can show your skills in any fields you are good at.

• Wolfram is working on adding pure math to Mathematica, here is his blog on this computational-knowledge-and-the-future-of-pure-mathematics/ the idea is that one should be able to proof things and do more pure math using Mathematica. Proofs can be generated or checked. But this is for future versions. Commented Dec 20, 2014 at 11:46
• @Nasser A really ambitious, impressive, interesting, and long blog article. Commented Dec 20, 2014 at 12:40
• Theorema is a Mathematica package for proving theorems. Version 2 was presented at the Wolfram Conference in Fall 2014. risc.jku.at/research/theorema/software/?page=Download Commented Dec 20, 2014 at 15:38
• TautologyQ[([Not] (a [Or] b)) == ([Not] a [And] [Not] b), {a, b}] Commented Dec 20, 2014 at 22:40
• Also, you could do something like this: Simplify[Equivalent[Not[Or[a, b]], And[Not[a], Not[b]]]].
– Jens
Commented Dec 20, 2014 at 22:48