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>
- Mathematica logic capabilities