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

Re: Mathematica logic capabilities

• To: mathgroup at smc.vnet.net
• Subject: [mg86418] Re: [mg86400] Mathematica logic capabilities
• From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
• Date: Tue, 11 Mar 2008 02:56:09 -0500 (EST)
• References: <200803100705.CAA24814@smc.vnet.net>

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]]]]

True


Andrzej Kozlowski

• References:
  • Mathematica logic capabilities
    • From: magma <maderri2@gmail.com>