MathDB

Let us consider a first-order language

L

with a ternary predicate

\operatorname{Plus}

. Hence (well-formed) formulas of

L

are built of symbols for variables, logical connectives, quantifiers, brackets, and the predicate symbol

\operatorname{Plus}

(\exists x_1)(\forall x_2):\operatorname{Plus}(x_2,x_1,x_2)\wedge(\forall x_3):\neg\operatorname{Plus}(x_1,x_3,x_3)

is an example of such a formula. Recall that a formula is closed iff each variable symbol occurs within the scope of a quantifier. Show that there exists an algorithm which decides whether or not a given closed formula of

L

is true for the set

\mathbb N

of natural numbers (

\{0,1,2,\ldots\}

) where

\operatorname{Plus}(x,y,z)

is interpreted as

x+y=z

Problem Statement