You may have heard about the Tarski-Seidenberg theorem, which says that the first-order theory of the reals is decidable, that the first-order theory of the complex numbers is similarly decidable, or that the first order theory of the integers without multiplication is decidable.

In the course of John Harrison‘s logic textbook Handbook of Practical Logic and Automated Reasoning, all three of these algorithms (and many more) are implemented.  Furthermore, you can download and play with them for free.  (However, I still recommend checking out the book: especially if you are looking for a good textbook for a course on logic with a concrete, computational bent.)

Below, I’ll describe how to install the programs and try them out.  There are many more interesting functions in this suite that I haven’t described.

Installation:

The software is written in OCaml and can be run interactively in an OCaml toplevel (don’t worry, you won’t actually need to know any OCaml).  Download and install OCaml as well as its preprocessor Camlp5 (which is used for formatting formulas nicely).

Then, download the code from here (under “All the code together”) and unzip it somewhere.

To run it, go to wherever you unzipped it and type make interactive in a shell.

(At least, that’s what worked for me on a Mac OSX.  Other systems may be different.)

The Tarski-Seidenberg Theorem.

The Tarski-Seidenberg theorem implies that there is a decision procedure which, given a first-order sentence over using plus, times, 0, and 1, will tell you if it’s true or not.  The function real_qelim implements this.  Let’s try it out.  (The symbol # indicates the beginning of the prompt; don’t type that, just type in what’s after it.)

This function knows that not all quadratic polynomials have roots, but all cubics do.

# real_qelim <<forall b c. exists x. x^2 + b*x + c = 0>>;;
- : fol formula = <<false>>
# real_qelim <<forall b c d. exists x. x^3 + b*x^2 + c*x + d = 0>>
  ;;
- : fol formula = <<true>>

Many geometric puzzles can, in theory, be solved automatically by this function.  Unfortunately, it is too slow for most interesting ones.  Harrison notes that there are open problems about kissing numbers of high-dimensional spheres which could be solved in theory by this algorithm, although in practice it is an unworkable approach.

This algorithm actually does something stronger than decide the truth of first-order sentences: it does quantifier-elimination, which means that if you give it a formula with free variables, it will give you a quantifier-free formula in those same free variables (in the case of a sentence, which has no free variables, that means either the formula “true” or the formula “false”).

For example, if you’ve forgotten the quadratic formula and want to know what the condition is for a quadratic polynomial to have a root:

# real_qelim <<exists x. x^2 + b*x + c = 0>>;;
- : fol formula =
<<(0 + c * 4) + b * (0 + b * -1) = 0 \/
 ~(0 + c * 4) + b * (0 + b * -1) = 0 /\
 ~(0 + c * 4) + b * (0 + b * -1) > 0>>

Note that there is no claim that the formula it gives you will be completely simplified, only that it will be correct.

Deciding Sentences over the Complex Numbers

We can similarly use the function complex_qelim to do quantifier elimination over the complexes. The fact that this possible is easier to prove than the corresponding fact for the reals, and the algorithm is similarly faster.

# complex_qelim <<forall x. x^3 = 1 ==> x = 1>>;;
- : fol formula = <<false>>

The following sentence is also true over the reals (although for a different reason than why it’s true over the complexes), but it takes significantly longer for the real quantifier elimination algorithm to decide it.

# complex_qelim <<forall x1 x2 x3. (x1^3 = 1 /\ x2^3 = 1 /\
  x3^3 = 1 /\ ~(x1 = x2) /\ ~(x1 = x3) /\ ~(x2 = x3))
  ==> x1 + x2 + x3 = 0>>;;
- : fol formula = <<true>>

Suppose we read on wikipedia that the translation of the limaçon to rectangular coordinates is . We can verify this (I’ve used s to represent and c to represent ):

# complex_qelim << forall r s c x y. (x^2 + y^2 = r^2
  /\ r * c = x /\ r * s = y ==>
  forall a b. (r = b + a * c ==>
  (x^2 + y^2 - a * x)^2 = b^2 * (x^2 + y^2)))>>;;
- : fol formula = <<true>>

Presburger Arithmetic

Finally, first-order sentences with plus and less-than over the integers and over the natural numbers are decidable. The relevant functions are integer_qelim and natural_qelim. Even though multiplication of variables is prohibited, we can still multiply by constants (since for example, instead of we could have written anyway).

An example Harrison gives is: There is an old (easy) puzzle which is to show that, with 3- and 5-cent stamps, you can make an -cent stamp for any .

# natural_qelim <<forall n. n >= 8 ==>
  exists x y. 3 * x + 5 * y = n>>;;
- : fol formula = <<true>>