# How to do predicate logic in Mathematica

I'm trying to formalize and analyze the following reasoning:

1. All equilateral triangles are isosceles triangles.
2. Some triangles are not equilateral triangles.
3. Therefore some triangles are not isosceles triangles.

The reasoning is obviously not valid. But I tried to find that out with Mathematica. So I typed what I would type in my math notebook:

Resolve[Implies[
SubsetEqual[equilateralTriangles, isoscelesTriangles] &&
Exists[triangle, NotElement[triangle, equilateralTriangles]]
, Exists[triangle, NotElement[triangle, equilateralTriangles]]]]


and I got:

Resolve::elemc: Unable to resolve the domain or region membership condition triangle ∉ equilateralTriangles. >>

Resolve[equilateralTriangles \[SubsetEqual] isoscelesTriangles && \!$$\*SubscriptBox[\(\[Exists]$$, $$triangle$$]$$triangle \[NotElement] equilateralTriangles$$\) \[Implies] \!$$\*SubscriptBox[\(\[Exists]$$, $$triangle$$]$$triangle \[NotElement] equilateralTriangles$$\)]


Am I doing this the right way? Can one solve problems like this with Mathematica?

• SubsetEqual has no meaning, for starters. It's there for output convenience, or can be overloaded with user-written functionality... – ciao Mar 7 '15 at 8:45

Resolve[
Implies[
ForAll[triangle,
Implies[
Element[triangle, equilateralTriangles],
Element[triangle, isoscelesTriangles]]] &&
Exists[triangle, NotElement[triangle, equilateralTriangles]],
Exists[triangle, NotElement[triangle, isoscelesTriangles]]]]


but that still produces the Resolve::elemc message.

To answer your second question: I don't think so. Mathematica can only apply the predicate calculus to points in geometric regions or numerical domains, not totally abstract sets, and that is what the message Resolve::elemc is trying to tell you. See the documentation forExists