Systematic brute-force searches for counterexamples

Question

This is getting nowhere on math.stackexchange.com, so I'm putting it here.

Gödel's completeness theorem says that for every statement in first-order predicate calculus with equality, there is either a proof that it holds in all structures, or a counterexample --- a structure in which it does not hold. What seems often insufficiently emphasized is the connection with computability: there is an efficient proof-checking algorithm. Without that, the conclusion would be of far less interest than it is! (Especially since one could just declare every universally valid formula to be a proof of itself. Then one would have absolutely no way of knowing what's a valid proof and what's not, but the conclusion of the theorem would still be true.)

Another theorem discovered in the '30s is that although there's a proof-checking algorithm for this situation, there's only half of a proof-finding algorithm:

• One can search systematically for a proof in such a manner that if one exists, then one will find it.
• But after a trillion years of searching without success, there's no way to know that it won't show up ten minutes later, nor that it will.

Both of the bulleted points were proved in the '30s. (Is "Church's theorem" the conventional name for the conjunction of the two bulleted items, or only the second one, or what? Right now I'm not sure.)

I think there's a vast literature on the computational efficiency (or lack of efficiency?) of these searches for proofs. Is there a literature on systematic brute-force searches for counterexamples? Such counterexamples would be structures in which a proposed first-order sentence is false.

Answer 1

Alg enumerates finite models of single-sorted first-order theories. It can find counter-examples, obviously, as we can just add the negation of the statement we wish to violate. My experience with this sort of thing is that it basically amounts to solving a satisfiability problem, so all the theory about SAT solvers might be relevant here.

For the general problem of finding a (possibly infinite) counter-model I have nothing intelligent to say. Well, I do. In order to talk about computability, we need to first specify what it means for a computer to "find" an infinite model. This leads to the question on how to represent infinite models, and at that point you're doing effective model theory.

Answer 2

Proofs are finite objects, so you can search for proofs systematically.

Counterexamples may be infinite models, so you can't search for them in the same way.

Thus a complete positive result seems unlikely.

Example 1: Are the axioms of Peano arithmetic consistent with the infinite set of sentences $\exists x. n=Sx, \exists x. n=SSx, \exists x. n=SSSx, \ldots$? You can't derive a contradiction from them, but you also won't find a counterexample by search because non-standard models of Peano arithmetic are non-recursive.

Example 2: Lerman and Schmerl came up with a sentence $\phi$ in the theory of trees with no recursive models. So counterexamples to $\phi\rightarrow\psi$ also won't show up in any ordinary type of search.

Answer 3

This is somewhat tangential to your specific query, but perhaps not entirely irrelevant. There has been considerable progress in the subdomain of geometry theorems, some of whose provers proceed by searching for and eliminating possible counterexamples. I am no expert, but permit me to cite three references, separated by about a decade each, to indicate the continued progress in this subarea:

1988: Chou, Shang-Ching. Mechanical geometry theorem proving. Vol. 41. Springer, 1988. (Springer link)
   
   _{p.109: Five Gauss lines are concurrent: A "possibly new theorem" [in 1988].}

2001: Jacques Fleuriot. "Geometry Theorem Proving." 2001, pp 11-30. A survey. (Springer link)

2011: Stojanović, Sana, Vesna Pavlović, and Predrag Janičić. "A coherent logic based geometry theorem prover capable of producing formal and readable proofs." Automated Deduction in Geometry. Springer Berlin Heidelberg, 2011. 201-220. (Springer link)

   
      _{Ulrik Buchholtz talk slides PDF download, 2010.}