6
$\begingroup$

I'm trying to implement proofs of concepts for Equational Proofs on some basic number theory theorems.

One such example is:

"let a and b be positive integers and let d = gcd (a, b). If t divides both a and b, prove that t divides d."

Implemented in Mathematica-12 as 

ClearAll["Global`*"] axioms = {d == GCD[a, b] && Mod[a, t] == 0 && Mod[b, t] == 0} FindEquationalProof[ForAll[{d, t}, Mod[d, t] == 0], axioms]

Upon evaluation, Mathematica returns:

Failure["PropositionFalse", Association["MessageTemplate" -> TemplateObject[{"The proposition could not be reduced to True."}, InsertionFunction -> TextString, CombinerFunction -> StringJoin],"MessageParameters" -> Association[]]]

I've tried including logic in the "axioms" object for the variables' status as integers, but I end up with mathematica telling me my axioms are improper.

Any insight to this would be appreciated, as I'm quite sure this theorem is in fact true.

Improve this question
$\endgroup$
1
  • $\begingroup$ One insight might be that d must divide t but not necessarily vice versa. $\endgroup$ Commented Jun 14, 2019 at 17:30

1 Answer 1

Reset to default
5
$\begingroup$

This is more a draft answer to your question than a full answer. Two observations: first, while I'm hardly any expert on evaluation in Mathematica, Mathematica seems to try to evaluate the terms given to it as arguments in FindEquationalProof. So Mathematica probably crashed when presented with unbound variables. Second, FindEquationalProof requires a full statement of the axioms to be used in a proof; there are no background axioms that come in by default.

So here's a draft of an answer; a little more work would need to be done to include Mod. The GCD axioms came from this article on Wikipedia.

axiom1 = {ForAll[{a}, gcd[a, a] == a]} axiom2 = {ForAll[{a, b}, gcd[a, b] == gcd[b, a]]} axiom3 = {ForAll[{a, b, c}, gcd[a, gcd[b, c]] == gcd[gcd[a, b], c]]} hyp1 = {d == gcd[a, b]} hyp2 = {gcd[a, t] == t} hyp3 = {gcd[b, t] == t} axioms = Union[axiom1, axiom2, axiom3] hypotheses = Union[hyp1, hyp2, hyp3] FindEquationalProof[gcd[d, t] == t, Union[axioms, hypotheses]]
Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ Nice answer. Note that axiom1 should say gcd[a, a] == a. $\endgroup$ Commented Mar 30, 2020 at 22:58
  • $\begingroup$ @Jose: Nice catch! I've included your correction... which shortened the proof, by the way. $\endgroup$ Commented Mar 31, 2020 at 2:45
  • 1
    $\begingroup$ +1. In fact, axioms 4,5, and 6 are not axioms, but the hypotheses of the theorem. I suggest hyp1, hyp 2, and hyp 3 would be exacter notations. $\endgroup$ Commented Mar 31, 2020 at 8:52
  • $\begingroup$ @user64494: Thanks for your clarifying comment. I've attempted to incorporate your suggestions. $\endgroup$ Commented Mar 31, 2020 at 17:40

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.