next up previous
Next: Expressing the creative ideas Up: CREATIVE SOLUTIONS TO Previous: Pinning down the ideas

Elementary first order formulations

 

The impossibility statement is readily formulated as a sentence of the predicate calculus, but I don't see how the parity and counting argument can be translated into a guide to the method of semantic tableaus, into a resolution argument, or into a standard proof.

The word ``elementary'' is used in the sense that the quantifiers range over numbers and not over sets.

The formulas are here for completeness. If you don't like reading them, the rest of this section may be skipped.

We number the rows and columns from 1 to 8 and we introduce predicates S(x,y), L(x,y), E(x,y), tex2html_wrap_inline204 , tex2html_wrap_inline206 , tex2html_wrap_inline208 , tex2html_wrap_inline210 , and tex2html_wrap_inline212 with the following intended interpretations:

S(x,y) means y = x + 1.

L(x,y) means x < y.

E(x,y) means x = y.

tex2html_wrap_inline204 means the square (x,y) and the square (x+1,y) are covered by a domino.

tex2html_wrap_inline206 means the square (x,y) and the square (x,y+1) are covered by a domino.

tex2html_wrap_inline208 means the square (x,y) and the square (x-1,y) are covered by a domino.

tex2html_wrap_inline210 means the square (x,y) and the square (x,y-1) are covered by a domino.

tex2html_wrap_inline212 means the square (x,y) is not covered.

We shall axiomatize only as much of the properties of the numbers from 1 to 8 as we shall need.

  1. tex2html_wrap_inline240
  2. tex2html_wrap_inline242 .
  3. tex2html_wrap_inline244 .
  4. tex2html_wrap_inline246 .
  5. E(x,x).

    These axioms insure that all eight numbers are different and determine the values of S(x,y), L(x,y), and E(x,y) for tex2html_wrap_inline256 .

  6. tex2html_wrap_inline258
  7. tex2html_wrap_inline260
  8. tex2html_wrap_inline262
  9. tex2html_wrap_inline264
  10. tex2html_wrap_inline266

    These axioms insure that every square (x,y) satisfies exactly one tex2html_wrap_inline268 .

  11. tex2html_wrap_inline270 .
  12. tex2html_wrap_inline272 These axioms insure that the uncovered squares are precisely (1,1) and (8,8).
  13. tex2html_wrap_inline274
  14. tex2html_wrap_inline276 These axioms state the conditions that a pair of adjacent squares be covered by a domino.
  15. tex2html_wrap_inline278

These axioms state that the dominoes don't stick out over the edge of the board.

Suppose we had a model of these 15 sentences (in Robinson's clausal formalism, there would be 31 clauses). There would have to be eight individuals tex2html_wrap_inline280 satisfying the relations asserted for tex2html_wrap_inline282 in the axioms. They would have to be distinct since axioms 1,2, and 3 allow us to prove L(x,y) whenever this is so and axioms 4 and 5 then allow us to show that L(x,y) holds only for distinct x and y.

We then label the squares of a checkboard and place a domino on each square (x,y) that satisfies tex2html_wrap_inline204 or tex2html_wrap_inline206 sticking to the right or up as the case may be. Axioms 13 and 14 insure that the dominoes don't overlap, axioms 6-12 insure that all squares but the corner squares are covered and axiom 15 insures that no dominoes stick out over the edge.

Since there is no such covering the sentences have no model and are inconsistent.

In a formalism that allows functions and equality we have a briefer inconsistent set of sentences involving

s(x)the successor of x

g(x,y) has value of 1 to 5 according to whether tex2html_wrap_inline204 or tex2html_wrap_inline304 or tex2html_wrap_inline212

The sentences are

  1. s(s(s(s(s(s(s(s(8)))))))) = 8.
  2. tex2html_wrap_inline310

    The sentences insure the existence of 8 distinct individuals using a cyclic successor function.

  3. tex2html_wrap_inline312

    Insures that exactly the corner squares (1,1) and (8,8) are uncovered.

  4. tex2html_wrap_inline314
  5. tex2html_wrap_inline316

    Each domino covers two adjacent squares

  6. tex2html_wrap_inline318

    Dominoes don't stick out

  7. tex2html_wrap_inline320 .
  8. tex2html_wrap_inline322 .

This identifies the numbers used and ties down the values of g(x,y).

Not only is this language incapable of expressing the colors of the squares. It is also incapable of expressing the counts of the numbers of squares with a given property, the latter being required for expressing the Minsky, Winograd and Stefanuk proofs.


next up previous
Next: Expressing the creative ideas Up: CREATIVE SOLUTIONS TO Previous: Pinning down the ideas

John McCarthy
Mon Mar 29 15:20:19 PST 1999