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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.