Interpreter for number theory, modulo n A sentence of number theory (for our purposes) is a sequence of the following symbols:

0 and ' (successor) - successor means +1, so 0'''' = 0 + 1 + 1 + 1 + 1 = 4

+ (addition) and * (multiplication)

= (equal to)

( and ) (parentheses)

the logical operator nand (a nand b is not (a and b))

forall (the universal quantifier)

v0, v1, v2, etc. (variables)
Here is an example of a sentence:


forall v1 (forall v2 (forall v3 (not (v1*v1*v1 + v2*v2*v2 = v3*v3*v3))))

Here not x is shorthand for x nand x -- the actual sentence would use (v1*v1*v1 + v2*v2*v2 = v3*v3*v3) nand (v1*v1*v1 + v2*v2*v2 = v3*v3*v3), because x nand x = not (x and x) = not x.
This states that for every combination of three natural numbers v1, v2, and v3, it is not the case that v13 + v23 = v33 (which would be true because of Fermat's Last Theorem, except for the fact that it would get 0^3+0^3=0^3).
Unfortunately, as proved by Gödel, it is not possible to determine whether or not a sentence in number theory is true.
It is possible, however, if we restrict the set of natural numbers to a finite set.
So, this challenge is to determine whether or not a sentence of number theory is true, when taken modulo n, for some positive integer n. For example, the sentence
forall v0 (v0 * v0 * v0 = v0)

(the statement that for all numbers x, x3 = x)
Is not true for ordinary arithmetic (e.g. 23 = 8 ≠ 2), but is true when taken modulo 3:
0 * 0 * 0 ≡ 0 (mod 3)
1 * 1 * 1 ≡ 1 (mod 3)
2 * 2 * 2 ≡ 8 ≡ 2 (mod 3)

Input and output format
The input is a sentence and positive integer n in any &quot;reasonable&quot; format. Here are some example of reasonable formats for the sentence forall v0 (v0 * v0 * v0 = v0) in number theory modulo 3:
(&quot;forall v0 (v0 * v0 * v0 = v0)&quot;, 3)
&quot;3:forall v0 (((v0 * v0) * v0) = v0)&quot;
&quot;(forall v0)(((v0 * v0) * v0) = v0) mod 3&quot; 
[3, &quot;forall&quot;, &quot;v0&quot;, &quot;(&quot;, &quot;(&quot;, &quot;(&quot;, &quot;v0&quot;, &quot;*&quot;, &quot;v0&quot;, &quot;)&quot;, &quot;*&quot;, &quot;v0&quot;, &quot;)&quot;, &quot;=&quot;, &quot;v0&quot;, &quot;)&quot;]
(3, [8, 9, 5, 5, 5, 9, 3, 9, 6, 3, 9, 6, 4, 9, 6]) (the sentence above, but with each symbol replaced with a unique number)
&quot;f v0 = * * v0 v0 v0 v0&quot;
[3, [&quot;forall&quot;, &quot;v0&quot;, [&quot;=&quot;, [&quot;*&quot;, &quot;v0&quot;, [&quot;*&quot;, &quot;v0&quot;, &quot;v0&quot;]], &quot;v0&quot;]]]
&quot;3.v0((v0 * (v0 * v0)) = v0)&quot;

Input can be from stdin, a command line argument, a file, etc.
The program can have any two distinct outputs for whether the sentence is true or not, e.g. it could output yes if it's true and no if it's not.
You do not need to support one variable being the subject of a forall twice, e.g. (forall v0 (v0 = 0)) nand (forall v0 (v0 = 0)). You can assume that your input has valid syntax.
Test cases
forall v0 (v0 * v0 * v0 = v0) mod 3
true

forall v0 (v0 * v0 * v0 = v0) mod 4
false (2 * 2 * 2 = 8 ≡ 0 mod 4)

forall v0 (v0 = 0) mod 1
true (all numbers are 0 modulo 1)

0 = 0 mod 8
true

0''' = 0 mod 3
true

0''' = 0 mod 4
false

forall v0 (v0' = v0') mod 1428374
true

forall v0 (v0 = 0) nand forall v1 (v1 = 0) mod 2
true (this is False nand False, which is true)

forall v0 ((v0 = 0 nand v0 = 0) nand ((forall v1 (v0 * v1 = 0' nand v0 * v1 = 0') nand forall v2 (v0 * v2 = 0' nand v0 * v2 = 0')) nand (forall v3 (v0 * v3 = 0' nand v0 * v3 = 0') nand forall v4 (v0 * v4 = 0' nand v0 * v4 = 0')))) mod 7
true
(equivalent to &quot;forall v0 (v0 =/= 0 implies exists v1 (v0 * v1 = 0)), which states that every number has a multiplicative inverse modulo n, which is only true if n is 1 or prime)

forall v0 ((v0 = 0 nand v0 = 0) nand ((forall v1 (v0 * v1 = 0' nand v0 * v1 = 0') nand forall v2 (v0 * v2 = 0' nand v0 * v2 = 0')) nand (forall v3 (v0 * v3 = 0' nand v0 * v3 = 0') nand forall v4 (v0 * v4 = 0' nand v0 * v4 = 0')))) mod 4
false


This is code-golf, so try to make your program as short as possible!
Python 2, 252 236 bytes



def g(n,s):
 if str(s)==s:return s.replace("'","+1")
 o,l,r=map(g,[n]*3,s);return['all((%s)for %s in range(%d))'%(r,l,n),'not((%s)*(%s))'%(l,r),'(%s)%%%d==(%s)%%%d'%(l,n,r,n),'(%s)%s(%s)'%(l,o,r)]['fn=+'.find(o)]
print eval(g(*input()))


Try it online!

Takes input as the nested prefix-syntax, with f instead of forall and n instead of nand:

[3, ["f", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]