MathGroup Archive 2008

[Date Index] [Thread Index] [Author Index]

Search the Archive

Re: Mathematica logic capabilities

  • To: mathgroup at
  • Subject: [mg86418] Re: [mg86400] Mathematica logic capabilities
  • From: Andrzej Kozlowski <akoz at>
  • Date: Tue, 11 Mar 2008 02:56:09 -0500 (EST)
  • References: <>

On 10 Mar 2008, at 08:05, magma wrote:

> Mathematica is supposed to have an automated theorem prover.
> I see that I can write an expression in propositional calculus and use
> Reduce to determine whether it is a tautology (valid expression) or
> not.
> For example
> Implies[Not[Not[p] \[And] Not[q]], p \[Or] q] // Reduce
> gives True   (De Morgan law)
> However it does not seem to be able to do the same with predicate
> calculus.
> For example:
> Implies[ForAll[x, f[x]], Exists[x, f[x]]] // Reduce
> returns an error, complaining that the expression is not quantized,
> instead of returning true as it should.
> So the question is: can Mathematica be used to do predicate calculus,
> without extra packages?
> If yes how?

Mathematica's ForAll and Exists are only implemented in the context of  
so called "first order formulas of the language of ordered fields with  
parameters in R". What this roughly means is that your f[x] has to be  
an explicit equation, inequation or inequality or a logical  
combination of these, involving algebraic functions of x. For example:

f[a_] := (a^3 + a^2 - a + 1)/(a^5 - 3*a^2 + 2) > a^11

Resolve[Implies[ForAll[x, f[x]], Exists[x, f[x]]]]


Andrzej Kozlowski

  • Prev by Date: Re: FindFit issue
  • Next by Date: Re: A question regarding a hyperbolic geometric function
  • Previous by thread: Mathematica logic capabilities
  • Next by thread: FindFit issue