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.
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.
- Inconsistent theories, which have no models;
- 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;
- 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;
- 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;
- And lastly, the self-verifying systems described above.
- 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.