Advances in Pure Mathematics
Vol.3 No.3(2013), Article ID:31413,6 pages DOI:10.4236/apm.2013.33053

Generalized Löb’s Theorem. Strong Reflection Principles and Large Cardinal Axioms

J. Foukzon1, E. R. Men’kova2

1Israel Institute of Technology, Haifa, Israel

2Lomonosov Moscow State University, Moscow, Russia

Email: jaykovfoukzon@list.ru, E_Menkova@mail.ru

Copyright © 2013 J. Foukzon, E. R. Men’kova. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

Received February 9, 2013; revised March 13, 2013; accepted April 14, 2013

Keywords: Löb’s Theorem; Second Godel Theorem; Consistency; Formal System; Uniform Reflection Principles; ω-Model of ZFC; Standard Model of ZFC; Inaccessible Cardinal

ABSTRACT

In this article, a possible generalization of the Löb’s theorem is considered. Main result is: let κ be an inaccessible cardinal, then

1. Introduction

Let Th be some fixed, but unspecified, consistent formal theory.

Theorem 1 [1]. (Löb’s Theorem).

If where x is the Gödel number of the proof of the formula with Gödel number n, and is the numeral of the Gödel number of the formula, then. Taking into account the second Gödel theorem it is easy to be able to prove , for disprovable (refutable) and undecidable formulas. Thus summarized, Löb’s theorem says that for refutable or undecidable formula, the intuition “if exists proof of then” is fails.

Definition 1. Let be an -model of the Th. We said that, Th# is a nice theory over Th or a nice extension of the Th iff:

1) Th# contains Th;

2) Let be any closed formula, then

implies.

Definition 2. We said that, Th# is a maximally nice theory over Th or a maximally nice extension of the Th iff Th# is consistent and for any consistent nice extension

of the Th: implies

.

Theorem 2. (Generalized Löb’s Theorem). Assume that 1) Con(Th) and 2) Th has an -model. Then theory Th can be extended to a maximally consistent nice theory Th#.

2. Preliminaries

Let Th be some fixed, but unspecified, consistent formal theory. For later convenience, we assume that the encoding is done in some fixed formal theory S and that Th contains S. We do not specify S—it is usually taken to be a formal system of arithmetic, although a weak set theory is often more convenient. The sense in which S is contained in Th is better exemplified than explained: If S is a formal system of arithmetic and Th is, say, ZFC, then Th contains S in the sense that there is a well-known embedding, or interpretation, of S in Th. Since encoding is to take place in S, it will have to have a large supply of constants and closed terms to be used as codes. (e.g. in formal arithmetic, one has) will also have certain function symbols to be described shortly. To each formula, , of the language of Th is assigned a closed term, , called the code of. [N. B. If is a formula with a free variable x, then is a closed term encoding the formula with x viewed as a syntactic object and not as a parameter.] Corresponding to the logical connectives and quantifiers are function symbols, , etc., such that, for all formulae

etc.

Of particular importance is the substitution operator, represented by the function symbol. For formulae, terms t with codes:

. (2.1)

Iteration of the substitution operator sub allows one to define function symbols such that

(2.2)

It well known [2,3] that one can also encode derivations and have a binary relation (read “x proves y” or “x is a proof of y”) such that for closed iff is the code of a derivation in Th of the formula with code. It follows that

(2.3)

for some closed term t. Thus one can define predicate:

, (2.4)

and therefore one obtain a predicate asserting provability.

Remark 2.1. We note that is not always the case that [2,3]:

. (2.5)

It well known [3] that the above encoding can be carried out in such a way that the following important conditions and are met for all sentences [2,3]:

(2.6)

Conditions and are called the Derivability Conditions.

Assumption 2.1. We assume now that:

1) the language of Th consists of:

numerals

countable set of the numerical variables:

countable set F of the set variables:

countable set of the n-ary function symbols:

countable set of the n-ary relation symbols:

connectives:

quantifier:.

2) Th contains

3) Th has an -model.

Theorem 2.1. (Löb’s Theorem). Let be 1) and 2) be closed. Then

. (2.7)

It well known that replacing the induction scheme in Peano arithmetic PA by the -rule with the meaning “if the formula is provable for all n, then the formula is provable”:

(2.8)

leads to complete and sound system where each true arithmetical statement is provable. S. Feferman showed that an equivalent formal system can be obtained by erecting on a transfinite progression of formal systems according to the following scheme

(2.9)

where is a formula with one free variable and

is a limit ordinal. Then being Kleene’s system of ordinal notations, is equivalent to. It is easy to see that, i.e. is a maximally nice extension of the PA.

3. Generalized Löb’s Theorem

Definition 3.1. An (well-formed formula) is closed i.e., is a Th-sentence iff it has no free variables; a wff Ψ is open if it has free variables. We’ll use the slang “k-place open wff” to mean a wff with k distinct free variables. Given a model of the Th and a Th-sentence, we assume known the meaning of—i.e. is true in, (see for example [4-6]).

Definition 3.2. Let be an -model of the Th. We said that, is a nice theory over Th or a nice extension of the Th iff:

1) contains Th;

2) Let be any closed formula, then

implies.

Definition 3.3. We said that is a maximally nice theory over Th or a maximally nice extension of the Th iff is consistent and for any consistent nice extension of the Th: implies

.

Lemma 3.1. Assume that: 1); and 2)

, where is a closed formula. Then

.

Proof. Let be the formula

(3.1)

where is a closed term. We note that under canonical observation, one obtain

for any closed wff.

Suppose that, then assumption (ii) gives

. (3.2)

From (3.1) and (3.2) one obtain

. (3.3)

But the Formula (3.3) contradicts the Formula (3.1).

Therefore:.

Lemma 3.2. Assume that: 1); and 2)

, where is a closed formula. Then.

Theorem 3.1. [7,8]. (Generalized Löb’s Theorem). Assume that:. Then theory Th can be extended to a maximally consistent nice theory over Th.

Proof. Let be an enumeration of all wff’s of the theory Th (this can be achieved if the set of propositional variables can be enumerated). Define a chain

of consistent theories inductively as follows: assume that theory is defined.

1) Suppose that a statement (3.4) is satisfied

. (3.4)

Then we define theory as follows

.

2) Suppose that a statement (3.5) is satisfied

. (3.5)

Then we define theory as follows:

.

3) Suppose that a statement (3.6) is satisfied

and.     (3.6)

Then we define theory as follows:

.

4) Suppose that a statement (3.7) is satisfied

and.     (3.7)

Then we define theory as follows:

.

We define now theory as follows:

. (3.8)

First, notice that each is consistent. This is done by induction on i and by Lemmas 3.1-3.2. By assumption, the case is true when. Now, suppose is consistent. Then its deductive closure is also consistent. If a statement (3.6) is satisfied i.e.,

and, then clearly

is consistent since it is a subset of closure. If a statement (3.7) is satisfied, i.e.,

and, then clearly

is consistent since it is a subset of closure.

Otherwise:

1) if a statement (3.4) is satisfied, i.e.

and, then clearly

is consistent by Lemma 3.1 and by one of the standard properties of consistency: is consistent iff;

2) if a statement (3.5) is satisfied, i.e.

and, then clearly

is consistent by Lemma 3.2 and by one of the standard properties of consistency: is consistent iff.

Next, notice is a maximally consistent nice extension of the set. A set is consistent because, by the standard Lemma 3.3 below, it is the union of a chain of consistent sets. To see that is maximal, pick any wff. Then is some in the enumerated list of all wff’s. Therefore for any such that or

either or

Since we have

or, which implies that

is maximally consistent nice extension of the

.

Lemma 3.3. The union of a chain of the consistent sets, ordered by, is consistent.

Definition 3.4. (a) Assume that a theory Th has an -model and is a Th-sentence. Let be a Th-sentence with all quantifiers relativized to -model [9];

(b) Assume that a theory Th has a standard model

And Φ is a Th-sentence. Let be a Th-sentence Φ with all quantifiers relativized to the model [9].

Definition 3.5. (a) Assume that Th has an -model

. Let be a theory Th relativized to a model

—i.e., any -sentence has a form for some Th-sentence [9];

(b) Assume that Th has an standard model. Let be a theory Th relativized to a model—i.e., any -sentence has a form for some Th-sentence Φ [9].

Definition 3.6. (a) For a given -model of the Th and for any -sentence, we define

such that the equivalence:

(3.9a)

where is satisfied;

(b) For a given standard model of the Th and for any -sentence, we define

such that the equivalence:

(3.9b)

where is satisfied.

Theorem 3.2. (Strong Reflection Principle). Assume that: 1), 2) Th has an -model and 3). Then

. (3.10)

Proof. The one direction is obvious. For the other, assume that

, (3.11)

and. Then

. (3.12)

Note that 1) + 2) implies.

Let be the formula

(3.13)

where is a closed term. Note that in any model by the canonical observation one obtain the equivalence: But the Formulae (3.11)-(3.12) contradicts the Formula (3.13). Therefore

and

Then theory is consistent and from the above observation one obtain that:

, where

(3.14)

On the other hand one obtain

. (3.15)

But the Formula (3.15), contradicts the Formula (3.14). This contradiction completed the proof.

Definition 3.7. (a) Assume that: (i) Th has an - model and (ii). Then we said that is a strong -model of the Th and denote such

-model of the Th as.

(b) Assume that: (i) Th has an standard model and (ii). Then we said that is a strong standard model of the Th and denote such standard model of the Th as.

Definition 3.8. (a) Assume that Th has a strong -model. Then we said that Th is a strongly consistent.

(b) Assume that Th has a strong standard model

Then we said that Th is a strongly SM-consistent Definition 3.9. (a) Assume that Th has a strong - model and is a Th-sentence. Let be a Th-sentence with all quantifiers relativized to a strong -model.

(b) Assume that Th has a strong standard model and Φ is a Th-sentence. Let be a Thsentence Φ with all quantifiers relativized to.

Definition 3.10. Assume that Th has a strong - model. Let be a theory Th relativised to i.e., any -sentence has the form for some Th-sentence.

Let Th be a theory such that Assumption 1.1 is satisfied. Let be a sentence in Th asserting that Th has a strong -model. Let Th* be a theory:.

Let be a sentence in Th* asserting that Th* has a strong -model. We assume throughout that Th is a strongly consistent, i.e. a sentence

is true in any ω-model of the Th.

Note that:

, (3.16)

where a sentence is refutable in and

, (3.17)

where a sentence is refutable in.

Lemma 3.4. Th* is a strongly consistent.

Proof. Assume that Th* is no strongly consistent, that is, has no any strong -model. This means that there is no any -model of the Th in which

is true and therefore from Formula (3.16)

one obtain, that a formula is true in any

-model of the Th. So from Formula (3.16) by using a Strong Reflection Principle (Theorem 3.2) one obtain that a sentence is provable in

, i.e.. But a sentence

contrary to the assumption that Th is a strongly consistent. This contradiction completed the proof.

Theorem 3.3. Th has no any strong -model. Proof. By Lemma 3.4 and Formula (3.17) one obtain that

. But Godel’s Second Incompleteness Theorem applied to asserts that is unprovable in. This contradiction completed the proof.

Theorem 3.4. ZFC has no any strong ω-model.

Proof. Immediately follows from Theorem 3.3 and definitions.

Theorem 3.5. ZFC has no any strong standard model..

Proof. Immediately follows from Theorem 3.4 and definitions.

Theorem 3.6. is incompatible with all the usual large cardinal axioms [10,11] which imply the existence of a strong standard model of ZFC.

Proof. Theorem 3.6 immediately follows from Theorem 3.5.

Theorem 3.7. Let κ be an inaccessible cardinal. Then.

Proof. Let be a set of all sets having hereditary size less then κ. It easy to see that forms a strong standard model of ZFC. Therefore Theorem 3.7 immediately follows from Theorem 3.6.

4. Conclusion

In this paper we proved so-called strong reflection principles corresponding to formal theories Th which has ω-models and in particular to formal theories Th, which has a standard models. The assumption that there exists a standard model of Th is stronger than the assumption that there exists a model of Th. This paper examined some specified classes of the standard models of ZFC so-called strong standard models of ZFC. Such models correspond to large cardinals axioms. In particular we proved that theory is incompatible with existence of any inaccessible cardinal κ. Note that the statement: (some inaccessible cardinal κ) is. Thus Theorem 3.6 asserts there exist numerical counterexample which would imply that a specific polynomial equation has at least one integer root.

REFERENCES

  1. M. H. Löb, “Solution of a Problem of Leon Henkin,” The Journal of Symbolic Logic, Vol. 20, No. 2, 1955, pp. 115-118. doi:10.2307/2266895
  2. J. Barwise, “Handbook of Mathematical Logic,” NorthHolland Publishing Company, New York, 1977, p. 1151.
  3. T. Drucker, “Perspectives on the History of Mathematical Logic,” Birkhauser, Boston, 2008, p. 191.
  4. A. Marcja and C. Toffalori, “A Guide to Classical and Modern Model Theory (Series: Trends in Logic),” Springer, Berlin, 2003, p. 371.
  5. F. W. Lawvere, C. Maurer and G. C. Wraith, “Model Theory and Topoi,” Springer, Berlin, 1975.
  6. D. Marker, “Model Theory: An Introduction (Graduate Texts in Mathematics),” Springer, Berlin, 2002.
  7. J. Foukzon, “Generalized Löb’s Theorem,” 2013. http://arxiv.org/abs/1301.5340
  8. J. Foukzon, “An Possible Generalization of the Löb’s Theorem,” AMS Sectional Meeting AMS Special Session. Spring Western Sectional Meeting University of Colorado Boulder, Boulder, 13-14 April 2013. http://www.ams.org/amsmtgs/2210_abstracts/1089-03-60.pdf
  9. P. Lindstrom, “First Order Predicate Logic with Generalized Quantifiers,” Theoria, Vol. 32, No. 3, 1966, pp. 186-195.
  10. F. R. Drake, “Set Theory: An Introduction to Large Cardinal (Studies in Logic and the Foundations of Mathematics, Vol. 76),” North-Holland, New York, 1974.
  11. A. Kanamori, “The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings,” 2nd Edition, Springer, Berlin, 2003.