Tiling problems and logical unsolvability

Abstract

The goal of finding some universal language and method for stating and solving arbitrary scientific problems has been an ideal since Leibniz who envisioned a "characteristica universalis": a universal language in which any scientific fact could be expressed. In addition, a general method for deciding the truth or falsity of any statement in the language, was envisioned. Through the work of Frege, Russel & Whitehead, Tarski, Godel and others this goal of a universal language for formalising mathematical facts, found expression in the development of what is now known as first order logic. The Completeness Theorem of Godel which states that all valid formulas are deducible, was seen as a justification for the ideals for the universality of the language and method. According to Hilbert and his school, the only justifiable foundation for the practice of mathematics was a logical system encompassing all of mathematical reasoning which further, was complete and consistent, i.e. all meaningful statements expressible in the language are either provably true or provably false(completeness) and no contradiction can arise in the system(consistency). In 1931 Godel showed that in any consistent logical system of some minimal expressivity there are expressions within the language which are not provably true or provably false. An open question was whether there was some method of identifying such expressions. In 1935 Church and Turing showed that no general method can exist for deciding whether or not a formula is deducible and that first order logic is therefore undecidable, i.e. there is no algorithmic procedure which can always correctly decide whether a formula is valid, i.e. deducible from given axioms and inference rules, or not. Given that the predicate calculus as a whole is undecidable, one may ask which subclasses of the predicate calculus are decidable and which are not. Initially, the method which showed some particular class of formulas of first order logic to be undecidable or unsolvable was a presentation of an effective method by which any quantificational formula could be reduced to some formula in the particular class. Such classes are called reduction classes. The unsolvability of the class then follows from the unsolvability of quantificational theory as a whole. See Turing, (28). In the early 1960's Biichi and Wang showed how simple computational or combinatorial systems- Turing Machines or Dominoes- could be naturally described by simple quantificational formulas. The unsolvability of these extralogical problems -the dominoe problem or the Halting problem-then implied the unsolvability of certain logical classes, these classes not being reduction classes, that is the classes are actual 'subclasses' of the class of quantificational formulas. These results are much sharper than those obtained by the previous reduction methods. This work is concerned with proofs that certain classes are undecidable, the results are due to various different people (see chapter 6 for references) but were recast in a homogeneous form by Lewis, [20] which is the main source for this work. The first few chapters are concerned with proving the unsolvability of various combinatorial problems, these results are then used in later chapters to prove the unsolvability of the classes of formulas.