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

```

• 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