3
$\begingroup$

Trying to implement the naturals in Mathematica, I follow E. Mendelson, Introduction to Mathematical Logic, Ch. 3, Par. 1. Here is my code for the axioms (exept the induction axiom)

Naxioms = {ForAll[{x, y, z},   Implies[x == y, Implies[x == z, y == z]]], 
ForAll[{x, y}, Implies[x == y, next[x] == next[y]]], 
ForAll[x, zero != next[x]],  ForAll[{x, y}, Implies[next[x] == next[y], x == y]], 
ForAll[x, plus[x, zero] == x],ForAll[{x, y}, plus[x, next[y]] == next[plus[x, y]]], 
ForAll[x, mul[x, zero] == zero],ForAll[{x, y}, mul[x, next[y]] == plus[mul[x, y], next[x]]]};

However, I fail with it, proving a simple theorem

FindEquationalProof[ForAll[x, plus[zero, x] == x], Naxioms]

FindEquationalProof::invs: Invalid specification of propositions !(*SubscriptBox[([ForAll]), ({x})](plus[zero, x] == x)) and axioms {!(*SubscriptBox[([ForAll]), ({x, y, z})]((x == y [Implies] ((x == z [Implies] y == z))))),!(*SubscriptBox[([ForAll]), ({x, y})]((x == y [Implies] next[x] == next[y]))),<<5>>,!(*SubscriptBox[([ForAll]), ({x, y})](mul[x, next[y]] == plus[mul[x, y], next[x]]))}

and the returned input. The questions arise: what is the reason? how to fix it? how to formulate the induction axiom?

Improve this question
$\endgroup$
10
  • $\begingroup$ I would recommend starting from just two basic axioms and gradually introducing the others to find the bad ones: Naxioms = { ForAll[{x, y}, plus[x, y] == plus[y, x]], ForAll[x, plus[x, zero] == x] }; works. $\endgroup$
    – flinty
    Commented Nov 18, 2020 at 16:56
  • 2
    $\begingroup$ The problem appears to be that Mathematica doesn't think that the first 4 axioms are proper equations. You can check like this (I found this internal function via tracing) Language`EquationalProofDump`isEquationQ /@ Naxioms returns {False, False, False, False, True, True, True, True} $\endgroup$
    – flinty
    Commented Nov 18, 2020 at 17:03
  • 2
    $\begingroup$ I'm not sure, it seems to be quite fussy about what it thinks is a valid equation: see here: pastebin.com/LsrdCt3P Something must go wrong internally - I suspect FindEquationalProof is kind of broken for a lot of use cases like yours, unless there are subtle semantics of ForAll that I'm not aware of. $\endgroup$
    – flinty
    Commented Nov 18, 2020 at 17:32
  • 1
    $\begingroup$ I'm not certain enough to give a full answer as I've only used this feature a few times (and I've always had difficulty with anything non-trivial and not in the docs). Also there's probably no hope for the induction axiom as it's a second order axiom, and it appears FindEquationalProof seems to suit first-order logic only. For example you cannot do second-order problems quantified over propositions like: FindEquationalProof[Exists[X, X[0]], {P[0], Q[0]}] expecting to get P[0] or Q[0] unifying X with P or Q. You may want to try Prolog, TLA+, z3, Lean theorem prover, perhaps. $\endgroup$
    – flinty
    Commented Nov 18, 2020 at 17:49
  • 2
    $\begingroup$ @user64494 by the way, I have a feeling Mathematica might be using this theorem prover: webwaldmeister.waldmeister.org for proof finding in some places, because 'waldmeister' appears in the traces as Language`EquationalProofDump`waldmeister. Also check here: mpi-inf.mpg.de/departments/automation-of-logic/software/… ...Stephen Wolfram has employed our system to carry out investigations in the area of singleton axiom systems for Boolean algebra... . So it wouldn't surprise me if that's being used as part of FindEquationalProof. $\endgroup$
    – flinty
    Commented Nov 18, 2020 at 23:53

1 Answer 1

Reset to default
3
$\begingroup$

Here's a first draft of an answer.

Induction will be used as the proof technique. Since Mathematica uses an equational prover, there's no direct way to use induction. What will be ventured here are just two first-order proofs, one for the basis case and the other for the induction step.

axioms = {
  ForAll[x, plus[x, zero] == x],
  ForAll[{x, y}, plus[x, next[y]] == next[plus[x, y]]]}

Basis case:

FindEquationalProof[ForAll[x, plus[zero, zero] == zero], axioms]

Induction assumption:

assertion = {ForAll[x, plus[zero, x] == x]}

Induction step:

FindEquationalProof[ForAll[x, plus[zero, next[x]] == next[x]], 
 Union[axioms, assertion]]

EDIT: As requested in the comments, the following is a proof of $2+2=4$. The axioms are the same as above:

FindEquationalProof[
 plus[next[next[zero]], next[next[zero]]] == 
  next[next[next[next[zero]]]], axioms]
Improve this answer
$\endgroup$
3
  • $\begingroup$ Can you prove $2+2=4$ ( maybe, extending your axioms)? TIA. $\endgroup$
    – user64494
    Commented Apr 29, 2021 at 3:54
  • $\begingroup$ @user64494: The proof of $2+2=4$ has been added as an edit to the original answer. $\endgroup$
    – ShyPerson
    Commented Apr 30, 2021 at 3:38
  • $\begingroup$ ShyPerson(@ does not work.)^ Thank you. I need some time to think about it. $\endgroup$
    – user64494
    Commented Apr 30, 2021 at 4:54

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.