PhD Dissertation

Author Saeed Salehi
Title Herbrand Consistency in Arithmetics with Bounded Induction
Language English
Supervisor Professor Zofia Adamowicz
Reviewers (1) Professor Henryk Kotlarski
(2) Professor Marcin Mostowski
Date June 2002

Here is the PhD Thesis (in PDF format - 84 pages); and this is an outline of the thesis (PDF file; 4 pages).


Abstract

By Gödel's celebrated incompleteness theorems, Truth is not conservative over Provability in theories that contain sufficiently strong fragments of arithmetic. In other words, for any given reasonable arithmetical theory T, there exists a true arithmetical sentence GT which is not provable in T. Moreover, this formula GT can be chosen to be a Π1-formula; thus Truth is not even Π1-conservative over Provability in general arithmetics. Needless to say, this GT may be provable in a stronger theory (than T). Thus, Π1-conservativity of a theory over its sufficiently strong sub-theories is an interesting, and often difficult, question in mathematical logic.

A natural candidate for showing the Π1-unconservativity of T over its sub-theory S ⊆ T is the consistency statement of S, Con(S); i.e., one would wish to show that T |— Con(S), and then use Göodel's Second Incompleteness Theorem to infer that S |–/– Con(S). Let us recall that for Zermelo-Frankel set theory ZFC and Peano's Arithmetic PA we have ZFC |— Con(PA), though PA |–/– Con(PA). Also, if IΣm is the fragment of PA in which the induction schema is restricted to Σm–formulas, we have IΣn+1 |— Con(IΣn) and IΣn |–/– Con(IΣn) for any n>0. For weak arithmetics this candidate does not work for Π1-separating IΔ0+Exp over IΔ0: we have IΔ0+Exp |–/– Con(IΔ0) (and also IΔ0 |–/– Con(IΔ0)). In 1981, J. Paris and A. Wilkie proposed cut-free consistency statement for this purpose; though at that time it was not yet proved that IΔ0 |–/– CFCon(IΔ0) where CFCon stands for cut-free consistency. However, it was known that IΔ0+Exp |–– CFCon(IΔ0). We note that the cost of cut-elimination in proof theory is super-exponential, so in weak arithmetics cut-free provability is not equivalent to the usual (Hilbert style) provability. Indeed, in those theories CFCon is a stronger predicate than Con.

From another point of view, unprovability of cut-free consistency of weak arithmetics in themselves is an interesting generalization of Gödel's Second Incompleteness Theorem. The original proof of this theorem was presented for the usual (Hilbert) consistency predicate of theories that contain primitive recursive arithmetic. However, later on, the theorem was proved for all r.e. extensions of Robinson't Arithmetic Q. So, one direction of generalizing the theorem was investigating the boundary cases: finding the weakest possible theories whose r.e. extensions cannot prove their own consistency. Another direction could be weakening the consistency predicate in addition to weakening the underlying theory. By 1985, another IΔ0+Exp-provable Π1-sentence that is unprovable in IΔ0 had been found; however the question of the unprovability of cut-free consistency in theories weaker than IΔ0+Exp remained open (see Pudlák's paper where he mentions the problem explicitly for Herbrand consistency in 1985). Let us recall that Herbrand consistency of a theory is the propositional satisfiability of every (finite) set of its Skolem instances. Herbrand consistency of a theory T is denoted by HCon(T).

The first demonstration of the unprovability of cut-free consistency in weak arithmetics was made by Z. Adamowicz who proved in an unpublished manuscript in 1999 (later appeared as a technical report) that the Tableau-consistency of IΔ0 +Ω1 is not provable in itself. Later on with P. Zbierski (2001) she proved the theorem (Gödel's Second Incompleteness Theorem) for Herbrand consistency of IΔ0 +Ω2, and a bit later she gave a model theoretic proof of it (2002). Extending these results for IΔ0 was proposed to me as a topic for my PhD thesis by her.

By modifying the definition of Herbrand consistency, Z. Adamowicz's model-theoretic proof is generalized to IΔ0 +Ω1 in Chapter 5 of the thesis (the result is not published anywhere else). Also, it is shown in Chapter 3 that IΔ0 |–/– HCon(IΔ0) where the theory IΔ0 is axiomatized by a conventional axiomatization of IΔ0 augmented with two IΔ0-provable sentences. These results were presented in the Logic Colloquium 2001 Vienna, Austria, and in the student session of the European Summer School in Logic, Language, and Information, 2001 Helsinki, Finland; a paper is published in the proceedings of the summer school. Chapter 4 proves IΔ0+Ω |–/– HCon(IΔ0+Ω) where Ω expresses the totality of ω(x)=xlog log x; here the conventional axiomatization of IΔ0 is taken in the proof. The theory IΔ0+Ω lies between IΔ0 and IΔ0 +Ω1.
In the end of Z. Adamowicz & P. Zbierski's paper (2001) three questions were asked. In Chapter 5 the second question is answered negatively, by elaborating a concrete counter-example (introduced in Chapter 2).

Independently, D. Willard (2002) introduced an IΔ0-provable Π1-formula V and showed that any theory whose axioms contains Q+V cannot prove its own Tableaux consistency. He also showed that Tableaux consistency of IΔ0 is not provable in itself; this proved the conjecture of J. Paris & A. Wilkie mentioned above.

              Table of Contents

1 Introduction 1
2 Basic Definitions and Formalizations 6
   2.1 Basic Definitions 6
   2.2 Model-Theoretic Observations 13
   2.3 Formalizations 18
   2.4 Main Theorems 27
3 A Σ1−Completeness Theorem 31
   3.1 Base Theory 33
   3.2 Skolemization of x∈I 36
   3.3 The Proof 42
4 A Proper Subtheory of IΔ0 +Ω1 49
   4.1 Skolemizing IΔ0+Ω 50
   4.2 The Proof 55
5 Relations to Earlier Results 66
   5.1 A Solution to Adamowicz & Zbierski's Problem 66
   5.2 A Generalization of Adamowicz's Theorem 68
       5.2.1 Skolemizing x∈log3 70
       5.2.2 The Proof 72
References 75
Index 78


http://saeedsalehi.ir/