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

DOI: 10.4236/apm.2013.33053   PDF   HTML   XML   2,907 Downloads   5,097 Views   Citations

Abstract

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

Share and Cite:

J. Foukzon and E. Men’kova, "Generalized Löb’s Theorem. Strong Reflection Principles and Large Cardinal Axioms," Advances in Pure Mathematics, Vol. 3 No. 3, 2013, pp. 368-373. doi: 10.4236/apm.2013.33053.

1. Introduction

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

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

If T h x Prov T h ( x , n ) ϕ n where x is the Gödel number of the proof of the formula with Gödel number n, and n is the numeral of the Gödel number of the formula φ n , then T h ϕ n . Taking into account the second Gödel theorem it is easy to be able to prove x Prov T h ( x , n ) φ n , for disprovable (refutable) and undecidable formulas φ n . 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 M ω T h 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

[ T h Pr T h ( [ Φ ] c ) ] & [ M ω T h Φ ]

implies T h # Φ .

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 T h of the Th: Ded ( T h # ) Ded ( T h ) implies Ded ( T h # ) = Ded ( T h ) .

Theorem 2. (Generalized Löb’s Theorem). Assume that 1) Con(Th) and 2) Th has an ω -model M ω T h . 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 0 ¯ , 1 ¯ , ) S will also have certain function symbols to be described shortly. To each formula, Φ , of the language of Th is assigned a closed term, [ Φ ] c , called the code of Φ . [N. B. If Φ ( x ) is a formula with a free variable x, then [ Φ ( x ) ] c is a closed term encoding the formula Φ ( x ) with x viewed as a syntactic object and not as a parameter.] Corresponding to the logical connectives and quantifiers are function symbols, neg ( ) , imp ( ) , etc., such that, for all formulae

Φ , Ψ : S | neg ( [ Φ ] c ) = [ ¬ Φ ] c , S | imp ( [ Φ ] c , [ Ψ ] c ) = [ Φ Ψ ] c etc.

Of particular importance is the substitution operator, represented by the function symbol sub ( , ) . For formulae Φ ( x ) , terms t with codes [ t ] c :

S | sub ( [ Φ ( x ) ] c , [ t ] c ) = [ Φ ( t ) ] c . (2.1)

Iteration of the substitution operator sub allows one to define function symbols sub 3 , sub 4 , , sub n such that

S | sub n ( [ Φ ( x 1 , x 2 , , x n ) ] c , [ t 1 ] c , [ t 2 ] c , , [ t n ] c ) = [ Φ ( t 1 , t 2 , , t n ) ] c (2.2)

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

T h Φ S Prov T h ( t , [ Φ ] c ) (2.3)

for some closed term t. Thus one can define predicate Pr T h ( y ) :

Pr T h ( y ) x Prov T h ( x , y ) , (2.4)

and therefore one obtain a predicate asserting provability.

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

T h Φ i S Pr T h ( [ Φ ] c ) . (2.5)

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

D 1. T h Φ implies S Pr T h ( [ Φ ] c ) , D 2. S Pr T h ( [ Φ ] c ) Pr T h ( [ Pr T h ( [ Φ ] c ) ] c ) , D 3. S Pr T h ( [ Φ ] c ) Pr T h ( [ Φ Ψ ] c ) Pr T h ( [ Ψ ] c ) . (2.6)

Conditions D 1 , D 2 and D 3 are called the Derivability Conditions.

Assumption 2.1. We assume now that:

1) the language of Th consists of:

numerals 0 ¯ , 1 ¯ ,

countable set of the numerical variables: { ν 0 , ν 1 , }

countable set Fof the set variables: F = { x , y , z , X , Y , Z , , }

countable set of the n-ary function symbols: f 0 n , f 1 n ,

countable set of the n-ary relation symbols: R 0 n , R 1 n ,

connectives: ¬ ,

quantifier: .

2) Th contains ZFC

3) Th has an ω -model M ω T h .

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

T h Pr T h ( [ ϕ ] c ) ϕ iff T h ϕ . (2.7)

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

A ( 0 ) , A ( 1 ) , , A ( n ) , x A ( x ) , (2.8)

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

P A 0 = P A P A α + 1 = P A α + { x Pr P A α ( [ A ( x ˙ ) ] c ) x A ( x ) } , P A λ = α < λ P A α (2.9)

where A ( x ) is a formula with one free variable and λ is a limit ordinal. Then T h = α O P A α , O being Kleene’s system of ordinal notations, is equivalent to T h # = P A . It is easy to see that T h # = P A # , i.e. T h # is a maximally nice extension of the PA.

3. Generalized Löb’s Theorem

Definition 3.1. An T h wff Φ (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 M T h of the Th and a Th-sentence Φ , we assume known the meaning of M Φ —i.e. Φ is true in M T h , (see for example [4-6]).

Definition 3.2. Let M ω T h be an ω -model of the Th. We shall say that, T h # is a nice theory over Th or a nice extension of the Th iff:

1) T h # contains Th;

2) Let Φ be any closed formula, then

[ T h Pr T h ( [ Φ ] c ) ] & [ M ω T h Φ ]

implies T h # Φ .

Definition 3.3. We shall say that T h # is a maximally nice theory over Th or a maximally nice extension of the Th iff T h # is consistent and for any consistent nice extension T h of the Th: Ded ( T h # ) Ded ( T h ) implies Ded ( T h # ) = Ded ( T h ) .

Lemma 3.1. Assume that: 1) Con ( T h ) ; and 2) T h Pr T h ( [ Φ ] c ) , where Φ is a closed formula. Then T h Pr T h ( [ ¬ Φ ] c ) .

Proof. Let Con T h ( Φ ) be the formula

Con T h ( Φ ) t 1 t 2 ¬ [ Prov T h ( t 1 , [ Φ ] c ) Prov T h ( t 2 , neg ( [ Φ ] c ) ) ] ¬ t 1 ¬ t 2 [ Prov T h ( t 1 , [ Φ ] c ) Prov T h ( t 2 , neg ( [ Φ ] c ) ) ] (3.1)

where t 1 , t 2 is a closed term. We note that under canonical observation, one obtains T h + Con ( T h ) Con T h ( Φ ) for any closed wff Φ .

Suppose that T h Pr T h ( [ ¬ Φ ] c ) , then assumption (ii) gives

T h Pr T h ( [ Φ ] c ) Pr T h ( [ ¬ Φ ] c ) . (3.2)

From (3.1) and (3.2) one obtain

t 1 t 2 [ Prov T h ( t 1 , [ Φ ] c ) Prov T h ( t 2 , neg ( [ Φ ] c ) ) ] . (3.3)

But the Formula (3.3) contradicts the Formula (3.1). Therefore: T h Pr T h ( [ ¬ Φ ] c ) .

Lemma 3.2. Assume that: 1) Con ( T h ) ; and 2) T h Pr T h ( [ ¬ Φ ] c ) , where Φ is a closed formula. Then T h Pr T h ( [ Φ ] c ) .

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

Proof. Let Φ 1 Φ i 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

= { T h i | i } , T h 1 = T h of consistent theories inductively as follows: assume that theory T h i is defined.

1) Suppose that a statement (3.4) is satisfied

T h Pr T h ( [ Φ i ] c ) and [ T h i Φ i ] & [ M ω T h Φ i ] . (3.4)

Then we define theory T h i + 1 as follows

T h i + 1 T h i { Φ i } .

2) Suppose that a statement (3.5) is satisfied

T h Pr T h ( [ ¬ Φ i ] c ) and [ T h i ¬ Φ i ] & [ M ω T h ¬ Φ i ] . (3.5)

Then we define theory T h i + 1 as follows:

T h i + 1 T h i { ¬ Φ i } .

3) Suppose that a statement (3.6) is satisfied

T h Pr T h ( [ Φ i ] c ) and T h i Φ i . (3.6)

Then we define theory T h i + 1 as follows:

T h i + 1 T h i { Φ i } .

4) Suppose that a statement (3.7) is satisfied

T h Pr T h ( [ ¬ Φ i ] c ) and T h ¬ Φ i . (3.7)

Then we define theory T h i + 1 as follows:

T h i + 1 T h i .

We define now theory T h # as follows:

T h # i T h i . (3.8)

First, notice that each T h i is consistent. This is done by induction on i and by Lemmas 3.1-3.2. By assumption, the case is true when i = 1 . Now, suppose T h i is consistent. Then its deductive closure Ded ( T h i ) is also consistent. If a statement (3.6) is satisfied i.e., T h Pr T h ( [ Φ i ] c ) and T h Φ i , then clearly T h i + 1 T h i { Φ i } is consistent since it is a subset of closure Ded ( T h i ) . If a statement (3.7) is satisfied, i.e., T h Pr T h ( [ ¬ Φ i ] c ) and T h i ¬ Φ i , then clearly T h i + 1 T h i { ¬ Φ i } is consistent since it is a subset of closure Ded ( T h i ) .

Otherwise:

1) if a statement (3.4) is satisfied, i.e. T h i Pr Th i ( [ Φ i ] c ) and T h i Φ i , then clearly T h i + 1 T h i { Φ i } is consistent by Lemma 3.1 and by one of the standard properties of consistency: Δ { A } is consistent iff Δ ¬ A ;

2) if a statement (3.5) is satisfied, i.e. T h Pr T h ( [ ¬ Φ i ] c ) and T h i ¬ Φ i , then clearly T h i + 1 T h i { ¬ Φ i } is consistent by Lemma 3.2 and by one of the standard properties of consistency: Δ { ¬ A } is consistent iff Δ A .

Next, notice Ded ( T h # ) is a maximally consistent nice extension of the set Ded ( T h ) . A set Ded ( T h # ) is consistent because, by the standard Lemma 3.3 below, it is the union of a chain of consistent sets. To see that Ded ( T h # ) is maximal, pick any wff Φ . Then Φ is some Φ i in the enumerated list of all wff’s. Therefore for any Φ such that T h Pr T h ( [ Φ ] c ) or T h Pr T h ( [ ¬ Φ ] c ) , either Φ T h # or ¬ Φ T h # .

Since Ded ( T h i + 1 ) Ded ( T h # ) , we have Φ Ded ( T h # ) or ¬ Φ Ded ( T h # ) , which implies that Ded ( T h # ) is maximally consistent nice extension of the Ded ( T h ) .

Lemma 3.3. The union of a chain = { Γ i | i } of the consistent sets Γ i , ordered by , is consistent.

Definition 3.4. (a) Assume that a theory Th has an ω -model M ω T h and Φ is a Th-sentence. Let Φ ω be a Th-sentence Φ with all quantifiers relativised to ω -model M ω T h ;

(b) Assume that a theory Th has a standard model S M T h and Φ is an Th-sentence. Let Φ S M be a Th-sentence Φ with all quantifiers relativized to a model S M T h [9].

Remark 3.1. In some special cases we denote a sentence Φ ω by a symbol Φ [ M ω T h ] and we denote a sentence Φ S M by symbol Φ [ M T h ] correspondingly.

Definition 3.5. (a) Assume that Th has an ω -model M ω T h . Let T h ω be a theory Th relativized to a model M ω T h , that is, any T h ω -sentence has a form Φ ω for some Th-sentence Φ [9];

(b) Assume that Th has an standard model S M T h . Let T h S M be a theory Th relativized to a model S M T h , that is, any T h S M -sentence has a form Φ S M for some Th-sentence Φ [9].

Remark 3.2. In some special cases we denote a theory T h ω by symbol T h [ M ω T h ] and we denote a theory T h S M by symbol T h [ M T h ] correspondingly.

Theorem 3.2. (Strong Reflection Principle).

(i) Assume that: Th has an ω -model M ω T h . Then for any T h ω -sentence Φ ω

T h ω Pr T h ω ( [ Φ ω ] c ) iff T h ω Φ ω . (3.9)

(ii) Assume that: Th has model M S M T h . Then for any T h S M -sentence Φ S M

T h S M Pr T h S M ( [ Φ S M ] c ) iff T h S M Φ S M . (3.10)

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

T h ω Pr T h ω ( [ Φ ω ] c ) , T h ω Φ ω , (3.11)

and T h ω ¬ Φ ω . Then

T h ω Pr T h ω ( [ ¬ Φ ω ] c ) . (3.12)

Note that Con ( T h ω ) holds since M ω T h . Let Con T h ω be the formula

Con T h ω t 1 t 2 t 3 ( t 3 = [ Φ ω ] c ) ¬ [ Prov T h ω ( t 1 , [ Φ ω ] c ) Prov T h ω ( t 2 , neg ( [ Φ ω ] c ) ) ] ¬ t 1 ¬ t 2 ¬ t 3 ( t 3 = [ Φ ω ] c ) × [ Prov T h ω ( t 1 , [ Φ ω ] c ) Prov T h ω ( t 2 , neg ( [ Φ ω ] c ) ) ] . (3.13)

where t 1 , t 2 , t 3 is a closed term. Note that for any ω -model M ω T h by the canonical observation one obtains the equivalence Con ( T h ω ) Con T h ω (see [2]). But the Formulae (3.11)-(3.12) contradicts the Formula (3.13). Therefore

T h ω Φ ω , Pr T h ω ( [ ¬ Φ ω ] c ) and T h ω ¬ Φ ω .

Then theory T h ω = T h ω + ¬ Φ ω is consistent and from the above observation one obtains that:

Con ( T h ω ) Con T h ω , where

Con T h ω ¬ t 1 ¬ t 2 ¬ t 3 ( t 3 = [ Φ ω ] c ) × [ Prov T h ω ( t 1 , [ Φ ω ] c ) Prov T h ω ( t 2 , neg ( [ Φ ω ] c ) ) ] . (3.14)

On the other hand one obtains

T h ω Pr T h ω ( [ Φ ω ] c ) , T h ω Pr T h ω ( [ ¬ Φ ω ] c ) . (3.15)

But the Formulae (3.15) contradicts the Formula (3.14). This contradiction completed the proof. Proof (ii) similarly as the proof (i) above.

Definition 3.6.

Let Th be a theory such that the Assumption 1.1 is satisfied.

(a) Let Ξ T h ω C o n ( T h ; M ω T h ) be a sentence in Th asserting that Th has ω -model M ω T h .

(b) Let Ξ T h S M C o n ( T h ; M S M T h ) be a sentence in Th asserting that Th has standard model M S M T h .

Assumption 3.1. We assume that (i) a sentence Ξ T h ω is expressible in Th, i.e., a sentence Ξ T h ω is expressible by using the lenguage L T h of the Th; (ii) a sentence Ξ T h S M is expressible in Th, i.e., a sentence Ξ T h S M is expressible by using the lenguage L T h of the Th.

Remark 3.3. Note that (i) for any ω -model M ω T h of the Th by the canonical observation (see [2]) one obtains the equivalence

Con ( T h ; M ω T h ) Con ( T h [ M ω T h ] ) Con T h [ M ω T h ] , (3.16)

(see remark 3.1) and the equivalence

Con T h [ M ω T h ] ¬ Pr T h [ M ω T h ] ( [ Ϝ [ M ω T h ] ] c ) (3.17)

(see remark 3.2), where Ϝ is a closed formula refutable in Th.

(ii) for any standard model M ω T h of the Th by the canonical observation (see [2] chapter), one obtains the equivalence

Con ( T h ; M S M T h ) Con ( T h [ M S M T h ] ) Con T h [ M S M T h ] (3.18)

(see remark 3.1) and the equivalence

Con T h [ M S M T h ] ¬ Pr T h S M ( [ Ϝ [ M S M T h ] ] c ) (3.19)

(see remark 3.2), where Ϝ is a closed formula refutable in Th.

Lemma 3.4. (I) Assume that Th has ω -model M ω T h .

Let T h 1 be a theory T h 1 = T h + Ξ T h ω . Then T h 1 is consistent.

(II) Assume that Th has standard model S M T h .

Let T h 2 be a theory T h 2 = T h + Ξ T h S M . Then T h 2 is consistent.

Proof. (I) Assume that a theory T h 1 = T h + Ξ T h ω T h + C o n ( T h ; M ω T h ) is inconsistent: ¬ C o n ( T h 1 ) . This means that there is no any model M T h of Th in which C o n ( T h ; M ω T h ) is true and in particular that is Th has no any ω -model M 1 , ω T h of Th in which C o n ( T h ; M ω T h ) is true, i.e., M 1 , ω T h Ξ T h ω [ M 1 , ω T h ] C o n ( T h ; M ω T h ) [ M 1 , ω T h ] and therefore one obtains for any ω -model M 1 , ω T h of Th that

M 1 , ω T h ¬ Con ( T h ; M ω T h ) [ M 1 , ω T h ] , (3. 20)

and in particular

M 1 , ω T h ¬ Con ( T h ; M 1 , ω T h ) [ M 1 , ω T h ] , (3. 21)

From (3.21) using (3.16)-(3.17) and one obtains

M 1 , ω T h ¬ Con T h [ M 1 , ω T h ] [ M 1 , ω T h ] P r T h [ M 1 , ω T h ] ( [ Ϝ [ M 1 , ω T h ] ] c ) . (3. 22)

From (3.22) and Theorem 3.2(I) one obtains

M 1 , ω T h ( [ Ϝ [ M 1 , ω T h ] ] c ) . (3. 23)

Obviously (3.23) contradicts to the assumption that Th has an ω -model M ω T h . This contradiction completed the proof.

Theorem 3.3. (I) Th has no any ω -model M ω T h .

(II) Th has no any standard model S M T h .

Proof. (I) By Lemma 3.4(I) one obtains that T h 1 C o n ( T h 1 ) . But Godel’s Second Incompleteness Theorem applied to T h 1 asserts that C o n ( T h 1 ) is unprovable in T h 1 . This contradiction completed the proof.

Proof. (II) Similarly as above.

Remark 3.4. We emphasize that it is well known that axiom S M Z F C a single statement in ZFC see [10], Ch. II, section 7. We denote this statement through all this paper by symbol C o n ( Z F C ; S M Z F C ) .

Theorem 3.4. ZFC has no anyω-model M ω Z F C .

Proof. Immediately follows from Theorem 3.3 (I) and Remark 3.4.

Theorem 3.5. ZFC has no any standard model. S M Z F C .

Proof. Immediately follows from Theorem 3.3 (II) and Remark 3.4.

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

Proof. Theorem 3.6 immediately follows from Theorem 3.5.

Theorem 3.7. Let κ be an inaccessible cardinal. Then ¬ Con ( Z F C + κ ) .

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

4. Conclusion

In this paper we proved so-called strong reflection principles corresponding to formal theories Th which has ω-models M ω T h and in particular to formal theories Th, which has a standard models S M T h . 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 Z F C + Con ( Z F C ) is incompatible with existence of any inaccessible cardinal κ. Note that the statement: Con ( Z F C + some inaccessible cardinal κ) is Π 1 0 . Thus Theorem 3.6 asserts there exist numerical counterexample which would imply that a specific polynomial equation has at least one integer root.

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1] M. H. Lob, “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] C. Smorynski, “Handbook of Mathematical Logic,” North-Holland Publishing Company, 1977.
[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 Lob’s Theorem,” 2013. http://arxiv.org/abs/1301.5340
[8] J. Foukzon, “An Possible Generalization of the Lob’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] P. Cohen, “Set theory and the continuum hypothesis,” Reprint of the W. A. Benjamin, Inc., New York, 1966 edition; 1966. ISBN-13: 978-0486469218
[11] A. Kanamori, “The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings,” 2nd Edition, Springer, Berlin, 2003.

  
comments powered by Disqus

Copyright © 2020 by authors and Scientific Research Publishing Inc.

Creative Commons License

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.