# 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 "reasonable" format. Here are some example of reasonable formats for the sentence forall v0 (v0 * v0 * v0 = v0) in number theory modulo 3:

("forall v0 (v0 * v0 * v0 = v0)", 3)
"3:forall v0 (((v0 * v0) * v0) = v0)"
"(forall v0)(((v0 * v0) * v0) = v0) mod 3"
[3, "forall", "v0", "(", "(", "(", "v0", "*", "v0", ")", "*", "v0", ")", "=", "v0", ")"]
(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)
"f v0 = * * v0 v0 v0 v0"
[3, ["forall", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]
"3.v0((v0 * (v0 * v0)) = v0)"


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 "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 , so try to make your program as short as possible!

• Are variable names always in the format v number? – Jo King Aug 15 at 1:20
• @JoKing They can if you want them to be- you can use var number, or even just 1 + number (so 1 would be v0, 2 would be v1, etc.) – Leo Tenenbaum Aug 15 at 1:21
• @JoKing You should allow for (theoretically) an infinite number of variables. It's okay if the maximum number of variables is bounded by the maximum size of an integer, but you shouldn't have such a low limit. You can choose one of the other input formats if this is a problem for you. – Leo Tenenbaum Aug 15 at 1:29
• @UnrelatedString Sure, so long as they can be arbitrarily long. – Leo Tenenbaum Aug 15 at 3:51
• Can one use 'v number instead of v number' if we choose the prefix-syntax option? – Mr. Xcoder Aug 15 at 10:40

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

• Right now it's outputting Python code, but it should have two distinct outputs for if the sentence is true or false. You can use print(eval(g(*input()))). – Leo Tenenbaum Aug 15 at 12:09
• @LeoTenenbaum Yeah, I had that on the first version, but forgot to add it back in after golfing – TFeld Aug 15 at 13:31