Generalized Löb’s Theorem. Strong Reflection Principles and Large Cardinal Axioms ()
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 Fof the set variables:
countable set of the n-ary function symbols:
countable set of the n-ary relation symbols:
connectives:
quantifier:
.
2) Th contains ZFC
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 shall say 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 shall say 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 obtains
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 relativised to
-model
;
(b) Assume that a theory Th has a standard model
and
is an Th-sentence. Let
be a Th-sentence
with all quantifiers relativized to a model
[9].
Remark 3.1. In some special cases we denote a sentence
by a symbol
and we denote a sentence
by symbol
correspondingly.
Definition 3.5. (a) Assume that Th has an
-model
. Let
be a theory Th relativized to a model
, that is, 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
, that is, any
-sentence has a form
for some Th-sentence Φ [9].
Remark 3.2. In some special cases we denote a theory
by symbol
and we denote a theory
by symbol
correspondingly.
Theorem 3.2. (Strong Reflection Principle).
(i) Assume that: Th has an
-model
. Then for any
-sentence
(3.9)
(ii) Assume that: Th has model
. Then for any
-sentence
(3.10)
Proof. (i) The one direction is obvious. For the other, assume that
, (3.11)
and
. Then
. (3.12)
Note that
holds since
. Let
be the formula
(3.13)
where
is a closed term. Note that for any
-model
by the canonical observation one obtains the equivalence
(see [2]). But the Formulae (3.11)-(3.12) contradicts the Formula (3.13). Therefore
Then theory
is consistent and from the above observation one obtains that:
, where
(3.14)
On the other hand one obtains
. (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
be a sentence in Th asserting that Th has
-model
.
(b) Let
be a sentence in Th asserting that Th has standard model
.
Assumption 3.1. We assume that (i) a sentence
is expressible in Th, i.e., a sentence
is expressible by using the lenguage
of the Th; (ii) a sentence
is expressible in Th, i.e., a sentence
is expressible by using the lenguage
of the Th.
Remark 3.3. Note that (i) for any
-model
of the Th by the canonical observation (see [2]) one obtains the equivalence
, (3.16)
(see remark 3.1) and the equivalence
(3.17)
(see remark 3.2), where
is a closed formula refutable in Th.
(ii) for any standard model
of the Th by the canonical observation (see [2] chapter), one obtains the equivalence
(3.18)
(see remark 3.1) and the equivalence
(3.19)
(see remark 3.2), where
is a closed formula refutable in Th.
Lemma 3.4. (I) Assume that Th has
-model
.
Let
be a theory
. Then
is consistent.
(II) Assume that Th has standard model
.
Let
be a theory
. Then
is consistent.
Proof. (I) Assume that a theory
is inconsistent:
. This means that there is no any model
of Th in which
is true and in particular that is Th has no any
-model
of Th in which
is true, i.e.,
and therefore one obtains for any
-model
of Th that
(3. 20)
and in particular
(3. 21)
From (3.21) using (3.16)-(3.17) and one obtains
(3. 22)
From (3.22) and Theorem 3.2(I) one obtains
(3. 23)
Obviously (3.23) contradicts to the assumption that Th has an
-model
. This contradiction completed the proof.
Theorem 3.3. (I) Th has no any
-model
.
(II) Th has no any standard model
.
Proof. (I) By Lemma 3.4(I) one obtains that
But Godel’s Second Incompleteness Theorem applied to
asserts that
is unprovable in
. This contradiction completed the proof.
Proof. (II) Similarly as above.
Remark 3.4. We emphasize that it is well known that axiom
a single statement in ZFC see [10], Ch. II, section 7. We denote this statement through all this paper by symbol
.
Theorem 3.4. ZFC has no anyω-model
.
Proof. Immediately follows from Theorem 3.3 (I) and Remark 3.4.
Theorem 3.5. ZFC has no any standard model.
.
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
.
Proof. Let
be a set of all sets having hereditary size less then κ. It easy to see that
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
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.