5
$\begingroup$

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.

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

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.