Is there a way to restrict the domain to all positive integers when you're using Resolve[] on nested quantifiers in Wolfram Alpha? If so, how? If not but there is another tool which can do this, would one be able to point me to it?
For example, say I am determining the truth of the quantified expression $\forall_n \forall_m \exists_pP(n,m,p),\quad p = (m+n)/2 \quad$ where $n,m,p\in \Bbb R$
In Wolfram Alpha I could put: Resolve[ForAll[n, ForAll[m, Exists[p, p = (m+n)/2]]]] and it correctly comes back with True as a result since there is a real number $p$ for any real values $m,n$.
Suppose though I wanted the domain to be positive integers $\Bbb Z^+$. Now the answer to the same problem would be False. Is it possible to add the restriction to the domain in Wolfram Alpha or another software tool?
Best Answer
The Resolve command should allow restricting the domain as per Resolve Documentation. However, I could manage it by adding the domain restriction using $\in$ symbol as follows:
You may concat more conditions as you want, for example
&& p>0.