# 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. – Nasser Dec 20 '14 at 11:46
• @Nasser A really ambitious, impressive, interesting, and long blog article. – hengxin Dec 20 '14 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 – John McGee Dec 20 '14 at 15:38
• TautologyQ[([Not] (a [Or] b)) == ([Not] a [And] [Not] b), {a, b}] – Sjoerd C. de Vries Dec 20 '14 at 22:40
• Also, you could do something like this: Simplify[Equivalent[Not[Or[a, b]], And[Not[a], Not[b]]]]. – Jens Dec 20 '14 at 22:48