A sentence of number theory (for our purposes) is a sequence of the following symbols:
0
and'
(successor) - successor means+1
, so0'''' = 0 + 1 + 1 + 1 + 1 = 4
+
(addition) and*
(multiplication)=
(equal to)(
and)
(parentheses)the logical operator
nand
(a nand b
isnot (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 code-golf, so try to make your program as short as possible!
v number
? \$\endgroup\$var number
, or even just1 + number
(so1
would bev0
,2
would bev1
, etc.) \$\endgroup\$'v number
instead ofv number'
if we choose the prefix-syntax option? \$\endgroup\$