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

J. Foukzon, E. R. Men’kova

Israel Institute of Technology, Haifa, Israel.
Lomonosov Moscow State University, Moscow, Russia.

DOI: 10.4236/apm.2013.33053                

Abstract

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

Keywords

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

1. Introduction

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

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

If $Th⊢\exists x{\mathrm{Prov}}_{Th}\left(x,\stackrel{⌣}{n}\right)\to {\varphi }_n$ where x is the Gödel number of the proof of the formula with Gödel number n, and $\stackrel{⌣}{n}$ is the numeral of the Gödel number of the formula ${\phi }_n$ , then $Th⊢{\varphi }_n$ . Taking into account the second Gödel theorem it is easy to be able to prove $\exists x{\mathrm{Prov}}_{Th}\left(x,\stackrel{⌣}{n}\right)\to {\phi }_n$ , for disprovable (refutable) and undecidable formulas ${\phi }_n$ . Thus summarized, Löb’s theorem says that for refutable or undecidable formula $\phi$ , the intuition “if exists proof of $\phi$ then $\phi$ ” is fails.

Definition 1. Let $M_{\omega }^{Th}$ be an $\omega$ -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 $\Phi$ be any closed formula, then

$\left[Th⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)\right]\&\left[M_{\omega }^{Th}\models \Phi \right]$

implies $T{h}^{\#}⊢\Phi$ .

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}^{\prime }$ of the Th: $\mathrm{Ded}\left(T{h}^{\#}\right)\subseteq \mathrm{Ded}\left(T{h}^{\prime }\right)$ implies $\text{Ded}\left(T{h}^{\#}\right)=\text{Ded}\left(T{h}^{\prime }\right)$ .

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

$\begin{array}{l}\Phi ,\Psi :S|-\mathrm{neg}\left({\left[\Phi \right]}^c\right)\\ ={\left[\neg \Phi \right]}^c,S|-\mathrm{imp}\left({\left[\Phi \right]}^c,{\left[\Psi \right]}^c\right)={\left[\Phi \to \Psi \right]}^c\end{array}$ etc.

Of particular importance is the substitution operator, represented by the function symbol $\mathrm{sub}\left(\cdot ,\cdot \right)$ . For formulae $\Phi \left(x\right)$ , terms t with codes ${\left[t\right]}^c$ :

$S|-\mathrm{sub}\left({\left[\Phi \left(x\right)\right]}^c,{\left[t\right]}^c\right)={\left[\Phi \left(t\right)\right]}^c$ . (2.1)

Iteration of the substitution operator sub allows one to define function symbols ${\mathrm{sub}}_3,{\mathrm{sub}}_4,\cdots ,{\mathrm{sub}}_n$ such that

$\begin{array}{l}S|-{\mathrm{sub}}_n\left({\left[\Phi \left(x_1,x_2,\cdots ,x_n\right)\right]}^c,{\left[t_1\right]}^c,{\left[t_2\right]}^c,\cdots ,{\left[t_n\right]}^c\right)\\ ={\left[\Phi \left(t_1,t_2,\cdots ,t_n\right)\right]}^c\end{array}$ (2.2)

It well known [2,3] that one can also encode derivations and have a binary relation ${\mathrm{Prov}}_{Th}\left(x,y\right)$ (read “x proves y” or “x is a proof of y”) such that for closed $t_1,t_2:S|-{\mathrm{Prov}}_{Th}\left(t_1,t_2\right)$ iff $t_1$ is the code of a derivation in Th of the formula with code $t_2$ . It follows that

$Th⊢\Phi \leftrightarrow S⊢{\mathrm{Prov}}_{Th}\left(t,{\left[\Phi \right]}^c\right)$ (2.3)

for some closed term t. Thus one can define predicate ${\mathrm{Pr}}_{Th}\left(y\right)$ :

${\mathrm{Pr}}_{Th}\left(y\right)\leftrightarrow \exists x{\mathrm{Prov}}_{Th}\left(x,y\right)$ , (2.4)

and therefore one obtain a predicate asserting provability.

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

$Th⊢\Phi i\leftrightarrow S⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)$ . (2.5)

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

$\begin{array}{l}D1.Th⊢\Phi \text{implies}S⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right),\\ D2.S⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)\to {\mathrm{Pr}}_{Th}\left({\left[{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)\right]}^c\right),\\ D3.S⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)\wedge {\mathrm{Pr}}_{Th}\left({\left[\Phi \to \Psi \right]}^c\right)\\ \to {\mathrm{Pr}}_{Th}\left({\left[\Psi \right]}^c\right).\end{array}$ (2.6)

Conditions $D1,D2$ and $D3$ are called the Derivability Conditions.

Assumption 2.1. We assume now that:

1) the language of Th consists of:

numerals $\bar{0},\bar{1},\cdots$

countable set of the numerical variables: $\left\{{\nu }_0,{\nu }_1,\cdots \right\}$

countable set Fof the set variables: $F=\left\{x,y,z,X,Y,Z,\Re ,\cdots \right\}$

countable set of the n-ary function symbols: $f_0^n,f_1^n,\cdots$

countable set of the n-ary relation symbols: $R_0^n,R_1^n,\cdots$

connectives: $\neg ,\to$

quantifier: $\forall$ .

2) Th contains ZFC

3) Th has an $\omega$ -model $M_{\omega }^{Th}$ .

Theorem 2.1. (Löb’s Theorem). Let be 1) $\mathrm{Con}\left(Th\right)$ and 2) $\varphi$ be closed. Then

$Th⊢{\mathrm{Pr}}_{Th}\left({\left[\varphi \right]}^c\right)\to \varphi \text{iff}Th⊢\varphi$ . (2.7)

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

$\frac{A\left(0\right),A\left(1\right),\cdots ,A\left(n\right),\cdots }{\forall xA\left(x\right)},$ (2.8)

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

$\begin{array}{l}P{A}_0=PA\\ P{A}_{\alpha +1}=P{A}_{\alpha }+\left\{\forall x{\mathrm{Pr}}_{PA{}_{\alpha }}\left({\left[A\left(\stackrel{\dot{}}{x}\right)\right]}^c\right)\to \forall xA\left(x\right)\right\},\\ P{A}_{\lambda }={\displaystyle \underset{\alpha <\lambda }{\cup }P{A}_{\alpha }}\end{array}$ (2.9)

where $A\left(x\right)$ is a formula with one free variable and $\lambda$ is a limit ordinal. Then $Th={\displaystyle {\cup }_{\alpha \in O}P{A}_{\alpha },O}$ being Kleene’s system of ordinal notations, is equivalent to $T{h}^{\#}=P{A}_{\infty }$ . 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 $Th-\mathrm{wff}\Phi$ (well-formed formula $\Phi$ ) is closed i.e., $\Phi$ 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^{Th}$ of the Th and a Th-sentence $\Phi$ , we assume known the meaning of $M\models \Phi$ —i.e. $\Phi$ is true in $M^{Th}$ , (see for example [4-6]).

Definition 3.2. Let $M_{\omega }^{Th}$ be an $\omega$ -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 $\Phi$ be any closed formula, then

$\left[Th⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)\right]\&\left[M_{\omega }^{Th}\models \Phi \right]$

implies $T{h}^{\#}⊢\Phi$ .

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}^{\prime }$ of the Th: $\mathrm{Ded}\left(T{h}^{\#}\right)\subseteq \text{Ded}\left(T{h}^{\prime }\right)$ implies $\text{Ded}\left(T{h}^{\#}\right)=\text{Ded}\left(T{h}^{\prime }\right)$ .

Lemma 3.1. Assume that: 1) $\text{Con}\left(Th\right)$ ; and 2) $Th⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)$ , where $\Phi$ is a closed formula. Then $Th⊬{\mathrm{Pr}}_{Th}\left({\left[\neg \Phi \right]}^c\right)$ .

Proof. Let ${\mathrm{Con}}_{Th}\left(\Phi \right)$ be the formula

$\begin{array}{l}{\mathrm{Con}}_{Th}\left(\Phi \right)\\ \triangleq \forall t_1\forall t_2\neg \left[{\mathrm{Prov}}_{Th}\left(t_1,{\left[\Phi \right]}^c\right)\wedge {\mathrm{Prov}}_{Th}\left(t_2,\mathrm{neg}\left({\left[\Phi \right]}^c\right)\right)\right]\\ \leftrightarrow \neg \exists t_1\neg \exists t_2\left[{\mathrm{Prov}}_{Th}\left(t_1,{\left[\Phi \right]}^c\right)\wedge {\mathrm{Prov}}_{Th}\left(t_2,\mathrm{neg}\left({\left[\Phi \right]}^c\right)\right)\right]\end{array}$ (3.1)

where $t_1,t_2$ is a closed term. We note that under canonical observation, one obtains $Th+\mathrm{Con}\left(Th\right)⊢{\mathrm{Con}}_{Th}\left(\Phi \right)$ for any closed wff $\Phi$ .

Suppose that $Th⊢{\mathrm{Pr}}_{Th}\left({\left[\neg \Phi \right]}^c\right)$ , then assumption (ii) gives

$Th⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)\wedge {\mathrm{Pr}}_{Th}\left({\left[\neg \Phi \right]}^c\right)$ . (3.2)

From (3.1) and (3.2) one obtain

$\exists t_1\exists t_2\left[{\mathrm{Prov}}_{Th}\left(t_1,{\left[\Phi \right]}^c\right)\wedge {\mathrm{Prov}}_{Th}\left(t_2,\mathrm{neg}\left({\left[\Phi \right]}^c\right)\right)\right]$ . (3.3)

But the Formula (3.3) contradicts the Formula (3.1). Therefore: $Th⊬{\mathrm{Pr}}_{Th}\left({\left[\neg \Phi \right]}^c\right)$ .

Lemma 3.2. Assume that: 1) $\mathrm{Con}\left(Th\right)$ ; and 2) $Th⊢{\mathrm{Pr}}_{Th}\left({\left[\neg \Phi \right]}^c\right)$ , where $\Phi$ is a closed formula. Then $Th⊬{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)$ .

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

Proof. Let ${\Phi }_1\cdots {\Phi }_i\cdots$ 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

$\wp =\left\{T{h}_i|i\in \mathbb{N}\right\},T{h}_1=Th$ of consistent theories inductively as follows: assume that theory $T{h}_i$ is defined.

1) Suppose that a statement (3.4) is satisfied

$\begin{array}{l}Th⊢{\mathrm{Pr}}_{Th}\left({\left[{\Phi }_i\right]}^c\right)\text{and}\\ \left[T{h}_i⊬{\Phi }_i\right]\&\left[M_{\omega }^{Th}\models {\Phi }_i\right]\end{array}$ . (3.4)

Then we define theory $T{h}_{i+1}$ as follows

$T{h}_{i+1}\triangleq T{h}_i\cup \left\{{\Phi }_i\right\}$ .

2) Suppose that a statement (3.5) is satisfied

$\begin{array}{l}Th⊢{\mathrm{Pr}}_{Th}\left({\left[\neg {\Phi }_i\right]}^c\right)\text{and}\\ \left[T{h}_i⊬\neg {\Phi }_i\right]\&\left[M_{\omega }^{Th}\models \neg {\Phi }_i\right]\end{array}$ . (3.5)

Then we define theory $T{h}_{i+1}$ as follows:

$T{h}_{i+1}\triangleq T{h}_i\cup \left\{\neg {\Phi }_i\right\}$ .

3) Suppose that a statement (3.6) is satisfied

$Th⊢{\mathrm{Pr}}_{Th}\left({\left[{\Phi }_i\right]}^c\right)$ and $T{h}_i⊢{\Phi }_i$ . (3.6)

Then we define theory $T{h}_{i+1}$ as follows:

$T{h}_{i+1}\triangleq T{h}_i\cup \left\{{\Phi }_i\right\}$ .

4) Suppose that a statement (3.7) is satisfied

$Th⊢{\mathrm{Pr}}_{Th}\left({\left[\neg {\Phi }_i\right]}^c\right)$ and $Th⊢\neg {\Phi }_i$ . (3.7)

Then we define theory $T{h}_{i+1}$ as follows:

$T{h}_{i+1}\triangleq T{h}_i$ .

We define now theory $T{h}^{\#}$ as follows:

$T{h}^{\#}\triangleq {\displaystyle \underset{i\in \mathbb{N}}{\cup }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 $\text{Ded}\left(T{h}_i\right)$ is also consistent. If a statement (3.6) is satisfied i.e., $Th⊢{\text{Pr}}_{Th}\left({\left[{\Phi }_i\right]}^c\right)$ and $Th⊢{\Phi }_i$ , then clearly $T{h}_{i+1}\triangleq T{h}_i\cup \left\{{\Phi }_i\right\}$ is consistent since it is a subset of closure $\text{Ded}\left(T{h}_i\right)$ . If a statement (3.7) is satisfied, i.e., $Th⊢{\mathrm{Pr}}_{Th}\left({\left[\neg {\Phi }_i\right]}^c\right)$ and $T{h}_i⊢\neg {\Phi }_i$ , then clearly $T{h}_{i+1}\triangleq T{h}_i\cup \left\{\neg {\Phi }_i\right\}$ is consistent since it is a subset of closure $\text{Ded}\left(T{h}_i\right)$ .

Otherwise:

1) if a statement (3.4) is satisfied, i.e. $T{h}_i⊢{\mathrm{Pr}}_{{\text{Th}}_i}\left({\left[{\Phi }_i\right]}^c\right)$ and $T{h}_i⊬{\Phi }_i$ , then clearly $T{h}_{i+1}\triangleq T{h}_i\cup \left\{{\Phi }_i\right\}$ is consistent by Lemma 3.1 and by one of the standard properties of consistency: $\Delta \cup \left\{A\right\}$ is consistent iff $\Delta ⊬\neg A$ ;

2) if a statement (3.5) is satisfied, i.e. $Th⊢{\mathrm{Pr}}_{Th}\left({\left[\neg {\Phi }_i\right]}^c\right)$ and $T{h}_i⊬\neg {\Phi }_i$ , then clearly $T{h}_{i+1}\triangleq T{h}_i\cup \left\{\neg {\Phi }_i\right\}$ is consistent by Lemma 3.2 and by one of the standard properties of consistency: $\Delta \cup \left\{\neg A\right\}$ is consistent iff $\Delta ⊬A$ .

Next, notice $\text{Ded}\left(T{h}^{\#}\right)$ is a maximally consistent nice extension of the set $\text{Ded}\left(Th\right)$ . A set $\text{Ded}\left(T{h}^{\#}\right)$ is consistent because, by the standard Lemma 3.3 below, it is the union of a chain of consistent sets. To see that $\text{Ded}\left(T{h}^{\#}\right)$ is maximal, pick any wff $\Phi$ . Then $\Phi$ is some ${\Phi }_i$ in the enumerated list of all wff’s. Therefore for any $\Phi$ such that $Th⊢{\mathrm{Pr}}_{Th}\left({\left[\Phi \right]}^c\right)$ or $Th⊢{\mathrm{Pr}}_{Th}\left({\left[\neg \Phi \right]}^c\right),$ either $\Phi \in T{h}^{\#}$ or $\neg \Phi \in T{h}^{\#}.$

Since $\text{Ded}\left(T{h}_{i+1}\right)\subseteq \text{Ded}\left(T{h}^{\#}\right),$ we have $\Phi \in \text{Ded}\left(T{h}^{\#}\right)$ or $\neg \Phi \in \text{Ded}\left(T{h}^{\#}\right)$ , which implies that $\text{Ded}\left(T{h}^{\#}\right)$ is maximally consistent nice extension of the $\text{Ded}\left(Th\right)$ .

Lemma 3.3. The union of a chain $\wp =\left\{{\Gamma }_i|i\in \mathbb{N}\right\}$ of the consistent sets ${\Gamma }_i$ , ordered by $\subseteq$ , is consistent.

Definition 3.4. (a) Assume that a theory Th has an $\omega$ -model $M_{\omega }^{Th}$ and $\Phi$ is a Th-sentence. Let ${\Phi }_{\omega }$ be a Th-sentence $\Phi$ with all quantifiers relativised to $\omega$ -model $M_{\omega }^{Th}$ ;

(b) Assume that a theory Th has a standard model $S{M}^{Th}$ and $\Phi$ is an Th-sentence. Let ${\Phi }_{SM}$ be a Th-sentence $\Phi$ with all quantifiers relativized to a model $S{M}^{Th}$ [9].

Remark 3.1. In some special cases we denote a sentence ${\Phi }_{\omega }$ by a symbol $\Phi \left[M_{\omega }^{Th}\right]$ and we denote a sentence ${\Phi }_{SM}$ by symbol $\Phi \left[M^{Th}\right]$ correspondingly.

Definition 3.5. (a) Assume that Th has an $\omega$ -model $M_{\omega }^{Th}$ . Let $T{h}_{\omega }$ be a theory Th relativized to a model $M_{\omega }^{Th}$ , that is, any $T{h}_{\omega }$ -sentence has a form ${\Phi }_{\omega }$ for some Th-sentence $\Phi$ [9];

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

Remark 3.2. In some special cases we denote a theory $T{h}_{\omega }$ by symbol $Th\left[M_{\omega }^{Th}\right]$ and we denote a theory $T{h}_{SM}$ by symbol $Th\left[M^{Th}\right]$ correspondingly.

Theorem 3.2. (Strong Reflection Principle).

(i) Assume that: Th has an $\omega$ -model $M_{\omega }^{Th}$ . Then for any $T{h}_{\omega }$ -sentence ${\Phi }_{\omega }$

$T{h}_{\omega }⊢{\mathrm{Pr}}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right)\text{iff}T{h}_{\omega }⊢{\Phi }_{\omega }.$ (3.9)

(ii) Assume that: Th has model $M_{SM}^{Th}$ . Then for any $T{h}_{SM}$ -sentence ${\Phi }_{SM}$

$T{h}_{SM}⊢\mathrm{Pr}T{h}_{SM}\left({\left[{\Phi }_{SM}\right]}^c\right)\text{iff}T{h}_{SM}⊢{\Phi }_{SM}.$ (3.10)

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

$T{h}_{\omega }⊢{\mathrm{Pr}}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right),T{h}_{\omega }⊬{\Phi }_{\omega }$ , (3.11)

and $T{h}_{\omega }⊢\neg {\Phi }_{\omega }$ . Then

$T{h}_{\omega }⊢{\mathrm{Pr}}_{T{h}_{\omega }}\left({\left[\neg {\Phi }_{\omega }\right]}^c\right)$ . (3.12)

Note that $\mathrm{Con}\left(T{h}_{\text{ω}}\right)$ holds since $\exists M_{\omega }^{Th}$ . Let ${\mathrm{Con}}_{T{h}_{\text{ω}}}$ be the formula

$\begin{array}{l}{\mathrm{Con}}_{T{h}_{\omega }}\leftrightarrow \forall t_1\forall t_2\forall t_3\left(t_3={\left[{\Phi }_{\omega }\right]}^c\right)\\ \neg \left[{\mathrm{Prov}}_{T{h}_{\omega }}\left(t_1,{\left[{\Phi }_{\omega }\right]}^c\right)\wedge {\mathrm{Prov}}_{T{h}_{\omega }}\left(t_2,\mathrm{neg}\left({\left[{\Phi }_{\omega }\right]}^c\right)\right)\right]\\ \leftrightarrow \neg \exists t_1\neg \exists t_2\neg \exists t_3\left(t_3={\left[{\Phi }_{\omega }\right]}^c\right)\\ \times \left[{\mathrm{Prov}}_{T{h}_{\omega }}\left(t_1,{\left[{\Phi }_{\omega }\right]}^c\right)\wedge {\mathrm{Prov}}_{T{h}_{\omega }}\left(t_2,\mathrm{neg}\left({\left[{\Phi }_{\omega }\right]}^c\right)\right)\right].\end{array}$ (3.13)

where $t_1,t_2,t_3$ is a closed term. Note that for any $\omega$ -model $M_{\omega }^{Th}$ by the canonical observation one obtains the equivalence $\mathrm{Con}\left(T{h}_{\omega }\right)\leftrightarrow {\mathrm{Con}}_{T{h}_{\omega }}$ (see [2]). But the Formulae (3.11)-(3.12) contradicts the Formula (3.13). Therefore

$T{h}_{\omega }⊬{\Phi }_{\omega },⊬{\mathrm{Pr}}_{T{h}_{\omega }}\left({\left[\neg {\Phi }_{\omega }\right]}^c\right)\text{and}T{h}_{\omega }⊬\neg {\Phi }_{\omega }.$

Then theory $T{h^{\prime }}_{\omega }=T{h}_{\omega }+\neg {\Phi }_{\omega }$ is consistent and from the above observation one obtains that:

$\mathrm{Con}\left(T{h^{\prime }}_{\omega }\right)\leftrightarrow {\mathrm{Con}}_{T{h^{\prime }}_{\omega }}$ , where

$\begin{array}{l}{\mathrm{Con}}_{T{h^{\prime }}_{\omega }}\leftrightarrow \neg \exists t_1\neg \exists t_2\neg \exists t_3\left(t_3={\left[{\Phi }_{\omega }\right]}^c\right)\\ \times \left[{\mathrm{Prov}}_{T{h^{\prime }}_{\omega }}\left(t_1,{\left[{\Phi }_{\omega }\right]}^c\right)\wedge {\mathrm{Prov}}_{T{h^{\prime }}_{\omega }}\left(t_2,\mathrm{neg}\left({\left[{\Phi }_{\omega }\right]}^c\right)\right)\right].\end{array}$ (3.14)

On the other hand one obtains

$T{h^{\prime }}_{\omega }⊢{\mathrm{Pr}}_{T{h^{\prime }}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right),T{h^{\prime }}_{\omega }⊢{\mathrm{Pr}}_{T{h^{\prime }}_{\omega }}\left({\left[\neg {\Phi }_{\omega }\right]}^c\right)$ . (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 ${\Xi }^{T{h}_{\omega }}\equiv Con\left(Th;M_{\omega }^{Th}\right)$ be a sentence in Th asserting that Th has $\omega$ -model $M_{\omega }^{Th}$ .

(b) Let ${\Xi }^{T{h}_{SM}}\equiv Con\left(Th;M_{SM}^{Th}\right)$ be a sentence in Th asserting that Th has standard model $M_{SM}^{Th}$ .

Assumption 3.1. We assume that (i) a sentence ${\Xi }^{T{h}_{\omega }}$ is expressible in Th, i.e., a sentence ${\Xi }^{T{h}_{\omega }}$ is expressible by using the lenguage ${\mathcal{L}}_{Th}$ of the Th; (ii) a sentence ${\Xi }^{T{h}_{SM}}$ is expressible in Th, i.e., a sentence ${\Xi }^{T{h}_{SM}}$ is expressible by using the lenguage ${\mathcal{L}}_{Th}$ of the Th.

Remark 3.3. Note that (i) for any $\omega$ -model $M_{\omega }^{Th}$ of the Th by the canonical observation (see [2]) one obtains the equivalence

$\begin{array}{l}\mathrm{Con}\left(Th;M_{\omega }^{Th}\right)\leftrightarrow \\ \mathrm{Con}\left(Th\left[M_{\omega }^{Th}\right]\right)\leftrightarrow {\mathrm{Con}}_{Th\left[M_{\omega }^{Th}\right]}\end{array}$ , (3.16)

(see remark 3.1) and the equivalence

${\mathrm{Con}}_{Th\left[M_{\omega }^{Th}\right]}\leftrightarrow \neg {\mathrm{Pr}}_{Th\left[M_{\omega }^{Th}\right]}\left({\left[Ϝ\left[M_{\omega }^{Th}\right]\right]}^c\right)$ (3.17)

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

(ii) for any standard model $M_{\omega }^{Th}$ of the Th by the canonical observation (see [2] chapter), one obtains the equivalence

$\mathrm{Con}\left(Th;M_{SM}^{Th}\right)\leftrightarrow \mathrm{Con}\left(Th\left[M_{SM}^{Th}\right]\right)\leftrightarrow {\mathrm{Con}}_{Th\left[M_{SM}^{Th}\right]}$ (3.18)

(see remark 3.1) and the equivalence

${\mathrm{Con}}_{Th\left[M_{SM}^{Th}\right]}\leftrightarrow \neg {\mathrm{Pr}}_{T{h}_{SM}}\left({\left[Ϝ\left[M_{SM}^{Th}\right]\right]}^c\right)$ (3.19)

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

Lemma 3.4. (I) Assume that Th has $\omega$ -model $M_{\omega }^{Th}$ .

Let $T{h}_1$ be a theory $T{h}_1=Th+{\Xi }^{T{h}_{\omega }}$ . Then $T{h}_1$ is consistent.

(II) Assume that Th has standard model $S{M}^{Th}$ .

Let $T{h}_2$ be a theory $T{h}_2=Th+{\Xi }^{T{h}_{SM}}$ . Then $T{h}_2$ is consistent.

Proof. (I) Assume that a theory $T{h}_1=Th+{\Xi }^{T{h}_{\omega }}\equiv Th+Con\left(Th;M_{\omega }^{Th}\right)$ is inconsistent: $\neg Con\left(T{h}_1\right)$ . This means that there is no any model $M^{Th}$ of Th in which $Con\left(Th;M_{\omega }^{Th}\right)$ is true and in particular that is Th has no any $\omega$ -model $M_{1,\omega }^{Th}$ of Th in which $Con\left(Th;M_{\omega }^{Th}\right)$ is true, i.e., $M_{1,\omega }^{Th}⊭{\Xi }^{T{h}_{\omega }}\left[M_{1,\omega }^{Th}\right]\equiv Con\left(Th;M_{\omega }^{Th}\right)\left[M_{1,\omega }^{Th}\right]$ and therefore one obtains for any $\omega$ -model $M_{1,\omega }^{Th}$ of Th that

$M_{1,\omega }^{Th}\models \neg \mathrm{Con}\left(Th;M_{\omega }^{Th}\right)\left[M_{1,\omega }^{Th}\right],$ (3. 20)

and in particular

$M_{1,\omega }^{Th}\models \neg \mathrm{Con}\left(Th;M_{1,\omega }^{Th}\right)\left[M_{1,\omega }^{Th}\right],$ (3. 21)

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

$M_{1,\omega }^{Th}\models \neg {\mathrm{Con}}_{Th\left[M_{1,\omega }^{Th}\right]}\left[M_{1,\omega }^{Th}\right]\leftrightarrow P{r}_{Th\left[M_{1,\omega }^{Th}\right]}\left({\left[Ϝ\left[M_{1,\omega }^{Th}\right]\right]}^c\right).$ (3. 22)

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

$M_{1,\omega }^{Th}\models \left({\left[Ϝ\left[M_{1,\omega }^{Th}\right]\right]}^c\right).$ (3. 23)

Obviously (3.23) contradicts to the assumption that Th has an $\omega$ -model $M_{\omega }^{Th}$ . This contradiction completed the proof.

Theorem 3.3. (I) Th has no any $\omega$ -model $M_{\omega }^{Th}$ .

(II) Th has no any standard model $S{M}^{Th}$ .

Proof. (I) By Lemma 3.4(I) one obtains that $T{h}_1⊢Con\left(T{h}_1\right).$ But Godel’s Second Incompleteness Theorem applied to $T{h}_1$ asserts that $Con\left(T{h}_1\right)$ 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 $\exists S{M}^{ZFC}$ a single statement in ZFC see [10], Ch. II, section 7. We denote this statement through all this paper by symbol $Con\left(ZFC;S{M}^{ZFC}\right)$ .

Theorem 3.4. ZFC has no anyω-model $M_{\omega }^{ZFC}$ .

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

Theorem 3.5. ZFC has no any standard model. $S{M}^{ZFC}$ .

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 $\neg \mathrm{Con}\left(ZFC+\exists \kappa \right)$ .

Proof. Let $H_{\kappa }$ be a set of all sets having hereditary size less then κ. It easy to see that $H_{\kappa }$ 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_{\omega }^{Th}$ and in particular to formal theories Th, which has a standard models $S{M}^{Th}$ . 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 $ZFC+\mathrm{Con}\left(ZFC\right)$ is incompatible with existence of any inaccessible cardinal κ. Note that the statement: $\mathrm{Con}$ ( $ZFC+\exists$ some inaccessible cardinal κ) is ${\Pi }_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.