22 Sep 2004 chalst   » (Master)

Self-Verifying Theories
I've been meaning to put something together about consistent theories that can prove their own consistency; a few weeks ago I got drawn into working on the logic pages at Wikipedia (and a few others), and have finally written something.

A bit of context: I discovered about such theories from a talk Dan Willard gave at the FOL75 conference last autumn, and its taken me a while to figure out what to make of them. The most obvious consequence is that it shows the usually described dichotomy between theories not strong enough to talk about themselves, and theories that can't prove their own consistency to be a false one: but we knew that anyway because of the existence of theories with axioms equivalent to claiming that they are inconsistent.

What follows is adapted from material at the Self-verifying theories and Consistency proof entries I created today.

Dan Willard showed a few years back that there are a family of consistent systems over the language of first-order arithmetic that are capable of proving their own consistency (in what follows, all formal theories are assumed to be first-order theories with decidable axiom schemes)

  • In outline, the key is to formalise enough of the Goedel machinery to talk about provability internally without being able to formalise diagonalisation.
  • Diagonalisation depends upon not being able to prove multiplication total (and in the earlier versions of the result, addition also); addition and multiplication are not function symbols of the language, instead subtraction and division are, with the addition and multiplication predicates being defined in terms of these.
  • Then we can't prove:
    (All x,y)(Exists z) multiply(x,y,z).
    Now totality of muliplication is a Pi-0-2 sentence, and the theory is organiused so that we can prove only the Pi-0-1 results we need; and provability can be expressed in terms of a tableau search algorithm.
  • Provability of consistency can then simply be added as a Pi-0-1 axiom. The resulting system can be proven consistent by means of a relative consistency argument with respect to regular arithmetic.
  • As an aside: it is the Pi-0-2 sentences, such as the totalility of multiplication, that are dangerous; it is safe to add any Pi-0-1 truth of arithmetic to the theory; the self-verifying systems can be quite strong in a ceratin sense.
As a result we can divide theories into (at least) five kinds, depending on the relationship of their completeness, and their possibility of expressing (or easily being extended to express) their own provability predicate:
  1. Inconsistent theories, which have no models;
  2. Theories which cannot talk about their own provability relation, such as Tarski's axiomatisation of point and line geometry, and Presburger arithmetic. These theories are satisfactorily described by the model we obtain from the completeness theorem; we can say such systems are complete;
  3. Theories which can talk about their own consistency, and which include the negation of the sentence asserting their own consistency. Such theories are complete with respect to the model one obtains from the completeness theorem, but contain as a theorem the derivability of a contradiction, in contradition to the fact that they are consistent;
  4. Essentially incomplete theories, that is, theories capable of expressing their own provability relation and can carry out a diagonal argument. In other words, the theories that Goedel's incompleteness theorem treats;
  5. And lastly, the self-verifying systems described above.
Is that all? It's the taxonomy I so far understand, but I also had another revelation regarding the incompleteness theorems, through attending a short lecture course by Stephen Simpson on mass problems, a formalism in recursion theory aimed at expressing fine distinctions in degrees of solvability; they also happen to be express the notion of maximal consistent extensions of arithmetic theories nicely. I plan to summarise this idea in the near future (no promises about how long exactly), but the point I want to make now is that the theory gives a nice twist on the usual hierarchy of provability strengths:
  • An immediate and well-known consequence of the incompleteness theorems is that one can organise formal theories in a partial order according to relative consistency (A is higher than B if A can prove B consistent); the partial order the extends upwards endlessly;
  • A less well-known fact, rendered crystal-clear on Simpson's account, is that all essentially incomplete theories have the same potential to be extended to stronger theories; that is, among the essentially incomplete theories, it is always possible to extend weaker theories so that they fully describe the consequences of the stronger theory. One doesn't need the recursion theoretic machinery to see this; one can see this using the usual Goedelian machinery, but I find the expression using mass problems much more forceful.

Latex for Logicians
Via Richard Zach, Peter Smith's LaTeX for Logicians page, an annotated set of links to LaTeX resources for typestting tree/tableau proofs, logic symbols, and class files for logic journals.

Postscript: A minor correction in the above thanks to Robert Solovay. I added a little bit more, but much more should be said.
Postscript #2: wo was there too...

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!