There Is No Standard Model of ZFC and ZFC₂ with Henkin Semantics

Jaykov Foukzon¹, Elena Men’kova²

¹Department of Mathematics, Israel Institute of Technology, Haifa, Israel.
²Lomonosov Moscow State University, Moscow, Russia.

DOI: 10.4236/apm.2019.99034                

Abstract

In this article we proved so-called strong reflection principles corresponding to formal theories Th which has omega-models or nonstandard model with standard part. A possible generalization of Löb’s theorem is considered. Main results are: 1) , 2) , 3) , 4) , 5) let k be inaccessible cardinal then .

Keywords

Gödel Encoding, Completion of ZFC, Russell’s Paradox, ω-Model, Henkin Semantics, Full Second-Order Semantic, Strongly Inaccessible Cardinal

1. Introduction

Main Results

Let us remind that accordingly to naive set theory, any definable collection is a set. Let R be the set of all sets that are not members of themselves. If R qualifies as a member of itself, it would contradict its own definition as a set containing all sets that are not members of themselves. On the other hand, if such a set is not a member of itself, it would qualify as a member of itself by the same definition. This contradiction is Russell’s paradox. In 1908, two ways of avoiding the paradox were proposed, Russell’s type theory and Zermelo set theory, the first constructed axiomatic set theory. Zermelo’s axioms went well beyond Frege’s axioms of extensionality and unlimited set abstraction, and evolved into the now-canonical Zermelo-Fraenkel set theory ZFC. “But how do we know that ZFC is a consistent theory, free of contradictions? The short answer is that we don’t; it is a matter of faith (or of skepticism)”—E. Nelson wrote in his paper [1] . However, it is deemed unlikely that even ZFC₂ which is significantly stronger than ZFC harbors an unsuspected contradiction; it is widely believed that if ZFC and ZFC₂ were consistent, that fact would have been uncovered by now. This much is certain—ZFC and ZFC₂ are immune to the classic paradoxes of naive set theory: Russell’s paradox, the Burali-Forti paradox, and Cantor’s paradox.

Remark 1.1.1. The inconsistency of the second-order set theory ZFC2082 originally have been uncovered in [2] and officially announced in [3] , see also ref. [4] [5] [6] .

Remark 1.1.2. In order to derive a contradiction in second-order set theory ZFC₂ with the Henkin semantics [7] , we remind the definition given in P. Cohen handbook [8] (see [8] Ch. III, sec. 1, p. 87). P. Cohen wrote: “A set which can be obtained as the result of a transfinite sequence of predicative definitions Godel called ‘constructible’”. His result then is that the constructible sets are a model for ZF and that in this model GCH and AC hold. The notion of a predicative construction must be made more precise, of course, but there is essentially only one way to proceed. Another way to explain constructibility is to remark that the constructible sets are those sets which just occur in any model in which one admits all ordinals. The definition we now give is the one used in [9] .

Definition 1.1.1. [8] . Let X be a set. The set $X^{\prime }$ is defined as the union of X and the set Y of all sets y for which there is a formula $A\left(z\mathrm{,}{t}_1\mathrm{,}\cdots \mathrm{,}{t}_k\right)$ in ZF such that if $A_X$ denotes A with all bound variables restricted to X, then for some ${\bar{t}}_i,i=1,\cdots ,k$, in X,

$y=\left\{z\in X|A_X\left(z,{\bar{t}}_1,\cdots ,{\bar{t}}_k\right)\right\}.$ (1)

Observe $X^{\prime }\subseteq P\left(x\right)\cup X$, ${\overline{\stackrel{¯}{X}}}^{\prime }=\overline{\stackrel{¯}{X}}$ if X is infinite (and we assume AC). It should be clear to the reader that the definition of $X^{\prime }$, as we have given it, can be done entirely within ZF and that $Y=X^{\prime }$ is a single formula $A\left(X\mathrm{,}Y\right)$ in ZF. In general, one’s intuition is that all normal definitions can be expressed in ZF, except possibly those which involve discussing the truth or falsity of an infinite sequence of statements. Since this is a very important point we shall give a rigorous proof in a later section that the construction of $X^{\prime }$ is expressible in ZF.”

Remark 1.1.3. We will say that a set y is definable by the formula $A\left(z\mathrm{,}{t}_1\mathrm{,}\cdots \mathrm{,}{t}_k\right)$ relative to a given set X.

Remark 1.1.4. Note that a simple generalisation of the notion of the definability which has been by Definition 1.1.1 immediately gives Russell’s paradox in second order set theory ZFC₂ with the Henkin semantics [7] .

Definition 1.1.2. [6] . i) We will say that a set y is definable relative to a given set X iff there is a formula $A\left(z\mathrm{,}{t}_1\mathrm{,}\cdots \mathrm{,}{t}_k\right)$ in ZFC then for some ${\bar{t}}_i\in X,i=1,\cdots ,k$, in X there exists a set z such that the condition $A\left(z\mathrm{,}{\bar{t}}_1\mathrm{,}\cdots \mathrm{,}{\bar{t}}_k\right)$ is satisfied and $y=z$ or symbolically

$\exists z\left[A\left(z,{\bar{t}}_1,\cdots ,{\bar{t}}_k\right)\wedge y=z\right].$ (2)

It should be clear to the reader that the definition of $X^{\prime }$, as we have given it, can be done entirely within second order set theory ZFC₂ with the Henkin semantics [7] denoted by $ZF{C}_2^{Hs}$ and that $Y=X^{\prime }$ is a single formula $A\left(X\mathrm{,}Y\right)$ in $ZF{C}_2^{Hs}$.

ii) We will denote the set Y of all sets y definable relative to a given set X by $Y\triangleq {\Im }_2^{Hs}$.

Definition 1.1.3. Let ${\Re }_2^{Hs}$ be a set of the all sets definable relative to a given set X by the first order 1-place open wff’s and such that

$\forall x\left(x\in {\Im }_2^{Hs}\right)\left[x\in {\Re }_2^{Hs}\iff x\notin x\right]\mathrm{.}$ (3)

Remark 1.1.5. (a) Note that ${\Re }_2^{Hs}\in {\Im }_2^{Hs}$ since ${\Re }_2^{Hs}$ is a set definable by the first order 1-place open wff $\Psi \left(Z\mathrm{,}{\Im }_2^{Hs}\right)$ :

$\Psi \left(Z\mathrm{,}{\Im }_2^{Hs}\right)\triangleq \forall x\left(x\in {\Im }_2^{Hs}\right)\left[x\in Z\iff x\notin x\right]\mathrm{,}$ (4)

Theorem 1.1.1. [6] . Set theory $ZF{C}_2^{Hs}$ is inconsistent.

Proof. From (3) and Remark 1.1.2 one obtains

${\Re }_2^{Hs}\in {\Re }_2^{Hs}\iff {\Re }_2^{Hs}\notin {\Re }_2^{Hs}\mathrm{.}$ (5)

From (5) one obtains a contradiction

$\left({\Re }_2^{Hs}\in {\Re }_2^{Hs}\right)\wedge \left({\Re }_2^{Hs}\notin {\Re }_2^{Hs}\right)\mathrm{.}$ (6)

Remark 1.1.6. Note that in paper [6] we dealing by using following definability condition: a set y is definable if there is a formula $A\left(z\right)$ in ZFC such that

$\exists z\left[A\left(z\right)\wedge y=z\right].$ (7)

Obviously in this case a set $Y={\Re }_2^{Hs}$ is a countable set.

Definition 1.1.4. Let ${\Re }_2^{Hs}$ be the countable set of the all sets definable by the first order 1-place open wff’s and such that

$\forall x\left(x\in {\Im }_2^{Hs}\right)\left[x\in {\Re }_2^{Hs}\iff x\notin x\right]\mathrm{.}$ (8)

Remark 1.1.7. (a) Note that ${\Re }_2^{Hs}\in {\Im }_2^{Hs}$ since ${\Re }_2^{Hs}$ is a set definable by the first order 1-place open wff $\Psi \left(Z\mathrm{,}{\Im }_2^{Hs}\right)$ :

$\Psi \left(Z\mathrm{,}{\Im }_2^{Hs}\right)\triangleq \forall x\left(x\in {\Im }_2^{Hs}\right)\left[x\in Z\iff x\notin x\right]\mathrm{,}$ (9)

one obtains a contradiction $\left({\Re }_2^{Hs}\in {\Re }_2^{Hs}\right)\wedge \left({\Re }_2^{Hs}\notin {\Re }_2^{Hs}\right)$.

In this paper we dealing by using following definability condition.

Definition 1.1.5. i) Let $M_{st}=M_{st}^{ZFC}$ be a standard model of ZFC. We will say that a set y is definable relative to a given standard model $M_{st}$ of ZFC if there is a formula $A\left(z\mathrm{,}{t}_1\mathrm{,}\cdots \mathrm{,}{t}_k\right)$ in ZFC such that if $A_{M_{st}}$ denotes A with all bound variables restricted to $M_{st}$, then for some ${\bar{t}}_i\in M_{st},i=1,\cdots ,k$, in $M_{st}$ there exists a set z such that the condition $A_{M_{st}}\left(z\mathrm{,}{\bar{t}}_1\mathrm{,}\cdots \mathrm{,}{\bar{t}}_k\right)$ is satisfied and $y=z$ or symbolically

$\exists z\left[A_{M_{st}}\left(z\mathrm{,}{\bar{t}}_1\mathrm{,}\cdots \mathrm{,}{\bar{t}}_k\right)\wedge y=z\right].$ (10)

It should be clear to the reader that the definition of ${M^{\prime }}_{st}$, as we have given it, can be done entirely within second order set theory ZFC₂ with the Henkin semantics.

ii) In this paper we assume for simplicity but without loss of generality that

$A_{M_{st}}\left(z,{\bar{t}}_1,\cdots ,{\bar{t}}_k\right)=A_{M_{st}}\left(z\right).$ (11)

Remark 1.1.8. Note that in this paper we view i) the first order set theory ZFC under the canonical first order semantics ii) the second order set theory ZFC₂ under the Henkin semantics [7] and iii) the second order set theory ZFC₂ under the full second-order semantics [8] [9] [10] [11] [12] but also with a proof theory based on formal Urlogic [13] .

Remark 1.1.9. Second-order logic essentially differs from the usual first-order predicate calculus in that it has variables and quantifiers not only for individuals but also for subsets of the universe and variables for n-ary relations as well [7] - [13] . The deductive calculus $DE{D}_2$ of second order logic is based on rules and axioms which guarantee that the quantifiers range at least over definable subsets [7] . As to the semantics, there are two types of models: i) Suppose $U$ is an ordinary first-order structure and $S$ is a set of subsets of the domain A of $U$. The main idea is that the set-variables range over $S$, i.e.

$\langle U,S\rangle \models \exists X\Phi \left(X\right)\iff \exists S\left(S\in S\right)\left[\langle U,S\rangle \models \Phi \left(S\right)\right]$.

We call $\langle U,S\rangle$ a Henkin model, if $\langle U,S\rangle$ satisfies the axioms of $DE{D}_2$ and truth in $\langle U,S\rangle$ is preserved by the rules of $DE{D}_2$. We call this semantics of second-order logic the Henkin semantics and second-order logic with the Henkin semantics the Henkin second-order logic. There is a special class of Henkin models, namely those $\langle U,S\rangle$ where $S$ is the set of all subsets of A.

We call these full models. We call this semantics of second-order logic the full semantics and second-order logic with the full semantics the full second-order logic.

Remark 1.1.10. We emphasize that the following facts are the main features of second-order logic:

1) The Completeness Theorem: A sentence is provable in $DE{D}_2$ if and only if it holds in all Henkin models [7] - [13] .

2) The Löwenheim-Skolem Theorem: A sentence with an infinite Henkin model has a countable Henkin model.

3) The Compactness Theorem: A set of sentences, every finite subset of which has a Henkin model, has itself a Henkin model.

4) The Incompleteness Theorem: Neither $DE{D}_2$ nor any other effectively given deductive calculus is complete for full models, that is, there are always sentences which are true in all full models but which are unprovable.

5) Failure of the Compactness Theorem for full models.

6) Failure of the Löwenheim-Skolem Theorem for full models.

7) There is a finite second-order axiom system ${\mathbb{Z}}_2$ such that the semiring $\mathbb{N}$ of natural numbers is the only full model of ${\mathbb{Z}}_2$ up to isomorphism.

8) There is a finite second-order axiom system RCF₂ such that the field $ℝ$ of the real numbers is the only full model of RCF₂ up to isomorphism.

Remark 1.1.11. For let second-order ZFC be, as usual, the theory that results obtained from ZFC when the axiom schema of replacement is replaced by its second-order universal closure, i.e.

$\forall X\left[Func\left(X\right)\Rightarrow \forall u\exists \nu \forall r\left[r\in \nu \iff \exists s\left(s\in u\wedge \left(s,r\right)\in X\right)\right]\right],$ (12)

where X is a second-order variable, and where $Func\left(X\right)$ abbreviates “X is a functional relation”, see [12] .

Thus we interpret the wff’s of ZFC₂ language with the full second-order semantics as required in [12] [13] but also with a proof theory based on formal urlogic [13] .

Designation 1.1.1. We will denote: i) by $ZF{C}_2^{Hs}$ set theory $ZF{C}_2$ with the Henkin semantics,

ii) by $ZF{C}_2^{fss}$ set theory $ZF{C}_2$ with the full second-order semantics,

iii) by $\overline{ZFC}{}_2^{Hs}$ set theory $ZF{C}_2^{Hs}+\exists M_{st}^{ZF{C}_2^{Hs}}$ and

iv) by $ZF{C}_{st}$ set theory $ZFC+\exists M_{st}^{ZFC}$, where $M_{st}^{Th}$ is a standard model of the theory $Th$.

Remark 1.1.12. There is no completeness theorem for second-order logic with the full second-order semantics. Nor do the axioms of $ZF{C}_2^{fss}$ imply a reflection principle which ensures that if a sentence Z of second-order set theory is true, then it is true in some model $M^{ZF{C}_2^{fss}}$ of $ZF{C}_2^{fss}$ [11] .

Let Z be the conjunction of all the axioms of $ZF{C}_2^{fss}$. We assume now that: Z is true, i.e. $Con\left(ZF{C}_2^{fss}\right)$. It is known that the existence of a model for Z requires the existence of strongly inaccessible cardinals, i.e. under ZFC it can be shown that $\kappa$ is a strongly inaccessible if and only if $\left(H_{\kappa }\mathrm{,}\in \right)$ is a model of $ZF{C}_2^{fss}$. Thus

$\neg Con\left(ZF{C}_2^{fss}\right)\Rightarrow \neg Con\left(ZFC+\exists \kappa \right)\mathrm{.}$ (13)

In this paper we prove that:

i) $ZF{C}_{st}\triangleq ZFC+\exists M_{st}^{ZFC}$ ii) $\overline{ZFC}{}_2^{Hs}\triangleq ZF{C}_2^{Hs}+\exists M_{st}^{ZF{C}_2^{Hs}}$ and iii) $ZF{C}_2^{fss}$ is inconsistent, where $M_{st}^{Th}$ is a standard model of the theory $Th$.

Axiom $\exists M^{ZFC}$ [8] . There is a set $M^{ZFC}$ and a binary relation $\epsilon \subseteq M^{ZFC}\times M^{ZFC}$ which makes $M^{ZFC}$ a model for ZFC.

Remark 1.1.13. i) We emphasize that it is well known that axiom $\exists M^{ZFC}$ a single statement in ZFC see [8] , Ch. II, Section 7. We denote this statement thought all this paper by symbol $Con\left(ZFC;M^{ZFC}\right)$. The completeness theorem says that $\exists M^{ZFC}\iff Con\left(ZFC\right)$.

ii) Obviously there exists a single statement in $ZF{C}_2^{Hs}$ such that $\exists M^{ZF{C}_2^{Hs}}\iff Con\left(ZF{C}_2^{Hs}\right)$.

We denote this statement through all this paper by symbol $Con\left(ZF{C}_2^{Hs};M^{ZF{C}_2^{Hs}}\right)$ and there exists a single statement $\exists M^{Z_2^{Hs}}$ in $Z_2^{Hs}$. We denote this statement through all this paper by symbol $Con\left(Z_2^{Hs};M^{Z_2^{Hs}}\right)$.

Axiom $\exists M_{st}^{ZFC}$ [8] . There is a set $M_{st}^{ZFC}$ such that if R is $\left\{\langle x,y\rangle |x\in y\wedge x\in M_{st}^{ZFC}\wedge y\in M_{st}^{ZFC}\right\}$ then $M_{st}^{ZFC}$ is a model for ZFC under the relation R.

Definition 1.1.6. [8] . The model $M_{st}^{ZFC}$ is called a standard model since the relation $\in$ used is merely the standard $\in$ -relation.

Remark 1.1.14. Note that axiom $\exists M^{ZFC}$ doesn’t imply axiom $\exists M_{st}^{ZFC}$, see ref. [8] .

Remark 1.1.15. We remind that in Henkin semantics, each sort of second-order variable has a particular domain of its own to range over, which may be a proper subset of all sets or functions of that sort. Leon Henkin (1950) defined these semantics and proved that Gödel’s completeness theorem and compactness theorem, which hold for first-order logic, carry over to second-order logic with Henkin semantics. This is because Henkin semantics are almost identical to many-sorted first-order semantics, where additional sorts of variables are added to simulate the new variables of second-order logic. Second-order logic with Henkin semantics is not more expressive than first-order logic. Henkin semantics are commonly used in the study of second-order arithmetic. Väänänen [13] argued that the choice between Henkin models and full models for second-order logic is analogous to the choice between ZFC and $V$ ( $V$ is von Neumann universe), as a basis for set theory: “As with second-order logic, we cannot really choose whether we axiomatize mathematics using $V$ or ZFC. The result is the same in both cases, as ZFC is the best attempt so far to use $V$ as an axiomatization of mathematics”.

Remark 1.1.16. Note that in order to deduce: i) $~Con\left(ZF{C}_2^{Hs}\right)$ from $Con\left(ZF{C}_2^{Hs}\right)$,

ii) $~Con\left(ZFC\right)$ from $Con\left(ZFC\right)$, by using Gödel encoding, one needs something more than the consistency of $ZF{C}_2^{Hs}$, e.g., that $ZF{C}_2^{Hs}$ has an omega-model $M_{\omega }^{ZF{C}_2^{Hs}}$ or an standard model $M_{st}^{ZF{C}_2^{Hs}}$ i.e., a model in which the integers are the standard integers and the all wff of $ZF{C}_2^{Hs}$, ZFC, etc. represented by standard objects. To put it another way, why should we believe a statement just because there’s a $ZF{C}_2^{Hs}$ -proof of it? It’s clear that if $ZF{C}_2^{Hs}$ is inconsistent, then we won’t believe $ZF{C}_2^{Hs}$ -proofs. What’s slightly more subtle is that the mere consistency of $ZF{C}_2$ isn’t quite enough to get us to believe arithmetical theorems of $ZF{C}_2^{Hs}$ ; we must also believe that these arithmetical theorems are asserting something about the standard naturals. It is “conceivable” that $ZF{C}_2^{Hs}$ might be consistent but that the only nonstandard models $M_{Nst}^{ZF{C}_2^{Hs}}$ it has are those in which the integers are nonstandard, in which case we might not “believe” an arithmetical statement such as “ $ZF{C}_2^{Hs}$ is inconsistent” even if there is a $ZF{C}_2^{Hs}$ -proof of it.

Remark 1.1.17. Note that assumption $\exists M_{st}^{ZF{C}_2^{Hs}}$ is not necessary if nonstandard model $M_{Nst}^{ZF{C}_2^{Hs}}$ is a transitive or has a standard part $M_{st}^{Z_2^{Hs}}\subset M_{Nst}^{Z_2^{Hs}}$, see [14] [15] .

Remark 1.1.18. Remind that if M is a transitive model, then ${\omega }^M$ is the standard $\omega$. This implies that the natural numbers, integers, and rational numbers of the model are also the same as their standard counterparts. Each real number in a transitive model is a standard real number, although not all standard reals need be included in a particular transitive model. Note that in any nonstandard model $M_{Nst}^{Z_2^{Hs}}$ of the second-order arithmetic $Z_2^{Hs}$ the terms $\bar{0},S\bar{0}=\bar{1}\mathrm{,}SS\bar{0}=\bar{2}\mathrm{,}\cdots$ comprise the initial segment isomorphic to $M_{st}^{Z_2^{Hs}}\subset M_{Nst}^{Z_2^{Hs}}$. This initial segment is called the standard cut of the $M_{Nst}^{Z_2^{Hs}}$. The order type of any nonstandard model of $M_{Nst}^{Z_2^{Hs}}$ is equal to $\mathbb{N}+A\times \mathbb{Z}$, see ref. [16] , for some linear order A.

Thus one can choose Gödel encoding inside the standard model $M_{st}^{Z_2^{Hs}}$.

Remark 1.1.19. However there is no any problem as mentioned above in second order set theory $ZF{C}_2$ with the full second-order semantics because corresponding second order arithmetic $Z_2^{fss}$ is categorical.

Remark 1.1.20. Note if we view second-order arithmetic $Z_2$ as a theory in first-order predicate calculus. Thus a model $M^{Z_2}$ of the language of second-order arithmetic $Z_2$ consists of a set M (which forms the range of individual variables) together with a constant 0 (an element of M), a function S from M to M, two binary operations + and × on M, a binary relation < on M, and a collection D of subsets of M, which is the range of the set variables. When D is the full power set of M, the model $M^{Z_2}$ is called a full model. The use of full second-order semantics is equivalent to limiting the models of second-order arithmetic to the full models. In fact, the axioms of second-order arithmetic have only one full model. This follows from the fact that the axioms of Peano arithmetic with the second-order induction axiom have only one model under second-order semantics, i.e. $Z_2$, with the full semantics, is categorical by Dedekind’s argument, so has only one model up to isomorphism. When M is the usual set of natural numbers with its usual operations, $M^{Z_2}$ is called an ω-model. In this case we may identify the model with D, its collection of sets of naturals, because this set is enough to completely determine an ω-model. The unique full omega-model $M_{\omega }^{Z_2^{fss}}$, which is the usual set of natural numbers with its usual structure and all its subsets, is called the intended or standard model of second-order arithmetic.

2. Generalized Löb’s Theorem. Remarks on the Tarski’s Undefinability Theorem

2.1. Remarks on the Tarski’s Undefinability Theorem

Remark 2.1.1. In paper [2] under the following assumption

$Con\left(ZFC+\exists M_{st}^{ZFC}\right)$ (14)

it has been proved that there exists countable Russell’s set ${\Re }_{\omega }$ such that the following statement is satisfied:

$\begin{array}{l}ZFC+\exists M_{st}^{ZFC}⊢\exists {\Re }_{\omega }\left({\Re }_{\omega }\in M_{st}^{ZFC}\right)\wedge \left(card\left({\Re }_{\omega }\right)={\aleph }_0\right)\\ \wedge \left[{\models }_{M_{st}^{ZFC}}\forall x\left(x\in {\Re }_{\omega }\iff x\notin x\right)\right]\mathrm{.}\end{array}$ (15)

From (15) it immediately follows a contradiction

${\models }_{M_{st}^{ZFC}}\left({\Re }_{\omega }\in {\Re }_{\omega }\right)\wedge \left({\Re }_{\omega }\notin {\Re }_{\omega }\right)\mathrm{.}$ (16)

From (16) and (14) by reductio and absurdum it follows

$\neg Con\left(ZFC+\exists M_{st}^{ZFC}\right)$ (17)

Theorem 2.1.1. [17] [18] [19] . (Tarski’s undefinability theorem). Let $T{h}_L$ be first order theory with formal language $L$, which includes negation and has a Gödel numbering $g(\circ )$ such that for every $L$ -formula $A\left(x\right)$ there is a formula B such that $B\leftrightarrow A\left(g\left(B\right)\right)$ holds. Assume that $T{h}_L$ has a standard model $M_{st}^{T{h}_L}$ and $Con\left(T{h}_{L\mathrm{,}st}\right)$ where

$T{h}_{L\mathrm{,}st}\triangleq T{h}_L+\exists M_{st}^{T{h}_L}\mathrm{.}$ (18)

Let $T^{\ast }$ be the set of Gödel numbers of $L$ -sentences true in $M_{st}^{T{h}_L}$. Then there is no $L$ -formula $True\left(n\right)$ (truth predicate) which defines $T^{\ast }$. That is, there is no $L$ -formula $True\left(n\right)$ such that for every $L$ -formula A,

$True\left(g\left(A\right)\right)\iff {\left[A\right]}_{M_{st}^{T{h}_L}}\mathrm{,}$ (19)

where the abbreviation ${\left[A\right]}_{M_{st}^{T{h}_L}}$ means that A holds in standard model $M_{st}^{T{h}_L}$, i.e. ${\left[A\right]}_{M_{st}^{T{h}_L}}\iff {\models }_{M_{st}^{T{h}_L}}A$. Therefore $Con\left(T{h}_{L\mathrm{,}st}\right)$ implies that

$\neg \exists True\left(x\right)\left(True\left(g\left(A\right)\right)\iff {\left[A\right]}_{M_{st}^{T{h}_L}}\right)$ (20)

Thus Tarski’s undefinability theorem reads

$Con\left(T{h}_{L\mathrm{,}st}\right)\Rightarrow \neg \exists True\left(x\right)\left(True\left(g\left(A\right)\right)\iff {\left[A\right]}_{M_{st}^{T{h}_L}}\right)\mathrm{.}$ (21)

Remark 2.1.2. i) By the other hand the Theorem 2.1.1 says that given some really consistent formal theory $T{h}_{L\mathrm{,}st}$ that contains formal arithmetic, the concept of truth in that formal theory $T{h}_{L\mathrm{,}st}$ is not definable using the expressive means that that arithmetic affords. This implies a major limitation on the scope of “self-representation”. It is possible to define a formula $True\left(n\right)$, but only by drawing on a metalanguage whose expressive power goes beyond that of $L$. To define a truth predicate for the metalanguage would require a still higher metametalanguage, and so on.

ii) However if formal theory $T{h}_{L\mathrm{,}st}$ is inconsistent this is not surprising if we define a formula $True\left(n\right)=True\left(n\mathrm{<mo>\; ;\; </mo>}T{h}_{L\mathrm{,}st}\right)$ by drawing only on a language $L$.

iii) Note that if under assumption $Con\left(T{h}_{L\mathrm{,}st}\right)$ we define a formula $True\left(n\mathrm{<mo>\; ;\; </mo>}T{h}_{L\mathrm{,}st}\right)$ by drawing only on a language $L$ by reductio ad absurdum it follows

$\neg Con\left(T{h}_{L\mathrm{,}st}\right)\mathrm{.}$ (22)

Remark 2.1.3. i) Let $ZF{C}_{st}$ be a theory $ZF{C}_{st}\triangleq ZFC+\exists M_{st}^{ZFC}$. In this paper under assumption $Con\left(ZF{C}_{st}\right)$ we define a formula $True\left(n\mathrm{<mo>\; ;\; </mo>}ZF{C}_{st}\right)$ by drawing only on a language $L_{ZF{C}_{st}}$ by using Generalized Löb’s theorem [4] [5] . Thus by reductio ad absurdum it follows

$\neg Con\left(ZFC+\exists M_{st}^{ZFC}\right)\mathrm{.}$ (23)

ii) However note that in this case we obtain $\neg Con\left(ZF{C}_{st}\right)$ by using approach that completely different in comparison with approach based on derivation of the countable Russell’s set ${\Re }_{\omega }$ with conditions (15).

2.2. Generalized Löb’s Theorem

Definition 2.2.1. Let $T{h}_L^{\mathrm{<mo>\; \#\; </mo>}}$ be first order theory and $Con\left(T{h}^{\mathrm{<mo>\; \#\; </mo>}}\right)$. A theory $T{h}_L^{\mathrm{<mo>\; \#\; </mo>}}$ is complete if, for every formula A in the theory’s language $L$, that formula A or its negation $\neg A$ is provable in $T{h}_L^{\mathrm{<mo>\; \#\; </mo>}}$, i.e., for any wff A, always $T{h}_L^{\mathrm{<mo>\; \#\; </mo>}}⊢A$ or $T{h}_L^{\mathrm{<mo>\; \#\; </mo>}}⊢\neg A$.

Definition 2.2.2. Let $T{h}_L$ be first order theory and $Con\left(T{h}_L\right)$. We will say that a theory $T{h}_L^{\mathrm{<mo>\; \#\; </mo>}}$ is completion of the theory $T{h}_L$ if i) $T{h}_L\subset T{h}_L^{\mathrm{<mo>\; \#\; </mo>}}$, ii) a theory $T{h}_L^{\mathrm{<mo>\; \#\; </mo>}}$ is complete.

Theorem 2.2.1. [4] [5] . Assume that: $Con\left(ZF{C}_{st}\right)$, where $ZF{C}_{st}\triangleq ZFC+\exists M_{st}^{ZFC}$. Then there exists completion $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}$ of the theory $ZF{C}_{st}$ such that the following conditions hold:

i) For every formula A in the language of ZFC that formula ${\left[A\right]}_{M_{st}^{ZFC}}$ or formula ${\left[\neg A\right]}_{M_{st}^{ZFC}}$ is provable in $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}$ i.e., for any wff A, always $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}⊢{\left[A\right]}_{M_{st}^{ZFC}}$ or $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}⊢{\left[\neg A\right]}_{M_{st}^{ZFC}}$.

ii) $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}={\displaystyle {\cup }_{m\in \mathbb{N}}T{h}_m}$, where for any m a theory $T{h}_{m+1}$ is finite extension of the theory $T{h}_m$.

iii) Let ${\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ be recursive relation such that: y is a Gödel number of a proof of the wff of the theory $T{h}_m$ and x is a Gödel number of this wff. Then the relation ${\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ is expressible in the theory $T{h}_m$ by canonical Gödel encoding and really asserts provability in $T{h}_m$.

iv) Let ${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ be relation such that: y is a Gödel number of a proof of the wff of the theory $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}$ and x is a Gödel number of this wff. Then the relation ${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ is expressible in the theory $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}$ by the following formula

${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)\iff \exists m\left(m\in \mathbb{N}\right){\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ (24)

v) The predicate ${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ really asserts provability in the set theory $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}$.

Remark 2.2.1. Note that the relation ${\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ is expressible in the theory $T{h}_m$ since a theory $T{h}_m$ is a finite extension of the recursively axiomatizable theory ZFC and therefore the predicate ${\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ exists since any theory $T{h}_m$ is recursively axiomatizable.

Remark 2.2.2. Note that a theory $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}$ obviously is not recursively axiomatizable nevertheless Gödel encoding holds by Remark 2.2.1.

Theorem 2.2.2. Assume that: $Con\left(ZF{C}_{st}\right)$, where $ZF{C}_{st}\triangleq ZFC+\exists M_{st}^{ZFC}$. Then truth predicate $True\left(n\right)$ is expressible by using only first order language by the following formula

$True\left(g\left(A\right)\right)\iff \exists y\left(y\in \mathbb{N}\right)\exists m\left(m\in \mathbb{N}\right){\mathrm{Pr}}_m^{st}\left(y\mathrm{,}g\left(A\right)\right)\mathrm{.}$ (25)

Proof. Assume that:

$ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}⊢{\left[A\right]}_{M_{st}^{ZFC}}\mathrm{.}$ (26)

It follows from (26) there exists $m^{\ast }=m^{\ast }\left(g\left(A\right)\right)$ such that $T{h}_{m^{\ast }}⊢{\left[A\right]}_{M_{st}^{ZFC}}$ and therefore by (24) we obtain

${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}g\left(A\right)\right)\iff {\mathrm{Pr}}_{m^{\ast }}^{st}\left(y\mathrm{,}g\left(A\right)\right)\mathrm{.}$ (27)

From (24) immediately by definitions one obtains (25).

Remark 2.2.3. Note that Theorem 2.1.1 in this case reads

$Con\left(ZF{C}_{st}\right)\Rightarrow \neg \exists True\left(x\right)\left(True\left(g\left(A\right)\right)\iff {\left[A\right]}_{M_{st}^{ZFC}}\right)\mathrm{.}$ (28)

Theorem 2.2.3. $\neg Con\left(ZF{C}_{st}\right)$.

Proof. Assume that: $Con\left(ZF{C}_{st}\right)$. From (25) and (28) one obtains a contradiction $Con\left(ZF{C}_{st}\right)\wedge \neg Con\left(ZF{C}_{st}\right)$ (see Remark 2.1.3) and therefore by reductio ad absurdum it follows $\neg Con\left(ZF{C}_{st}\right)$.

Theorem 2.2.4. [4] [5] . Let $M_{Nst}^{ZFC}$ be a nonstandard model of ZFC and let $M_{st}^{PA}$ be a standard model of PA.

We assume now that $M_{st}^{PA}\subset M_{Nst}^{ZFC}$ and denote such nonstandard model of the set theory ZFC by $M_{Nst}^{ZFC}=M_{Nst}^{ZFC}\left[PA\right]$. Let $ZF{C}_{Nst}$ be the theory $ZF{C}_{Nst}=ZFC+M_{Nst}^{ZFC}\left[PA\right]$. Assume that: $Con\left(ZF{C}_{Nst}\right)$, where $ZF{C}_{st}\triangleq ZFC+\exists M_{Nst}^{ZFC}$. Then there exists completion $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ of the theory $ZF{C}_{Nst}$ such that the following conditions hold:

i) For every formula A in the language of ZFC that formula ${\left[A\right]}_{M_{Nst}^{ZFC}}$ or formula ${\left[\neg A\right]}_{M_{Nst}^{ZFC}}$ is provable in $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ i.e., for any wff A, always $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}⊢{\left[A\right]}_{M_{Nst}^{ZFC}}$ or $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}⊢{\left[\neg A\right]}_{M_{Nst}^{ZFC}}$.

ii) $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}={\displaystyle {\cup }_{m\in \mathbb{N}}T{h}_m}$, where for any m a theory $T{h}_{m+1}$ is finite extension of the theory $T{h}_m$.

iii) Let ${\mathrm{Pr}}_m^{Nst}\left(y\mathrm{,}x\right)$ be recursive relation such that: y is a Gödel number of a proof of the wff of the theory $T{h}_m$ and x is a Gödel number of this wff. Then the relation ${\mathrm{Pr}}_m^{Nst}\left(y\mathrm{,}x\right)$ is expressible in the theory $T{h}_m$ by canonical Gödel encoding and really asserts provability in $T{h}_m$.

iv) Let ${\mathrm{Pr}}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ be relation such that: y is a Gödel number of a proof of the wff of the theory $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ and x is a Gödel number of this wff. Then the relation ${\mathrm{Pr}}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ is expressible in the theory $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ by the following formula

${\mathrm{Pr}}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)\iff \exists m\left(m\in M_{st}^{PA}\right){\mathrm{Pr}}_m^{Nst}\left(y\mathrm{,}x\right)$ (29)

v) The predicate ${\mathrm{Pr}}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ really asserts provability in the set theory $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}$.

Remark 2.2.4. Note that the relation ${\mathrm{Pr}}_m^{Nst}\left(y\mathrm{,}x\right)$ is expressible in the theory $T{h}_m$ since a theory $T{h}_m$ is a finite extension of the recursively axiomatizable theory ZFC and therefore the predicate ${\mathrm{Pr}}_m^{Nst}\left(y\mathrm{,}x\right)$ exists since any theory $T{h}_m$ is recursively axiomatizable.

Remark 2.2.5. Note that a theory $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ obviously is not recursively axiomatizable nevertheless Gödel encoding holds by Remark 2.2.1.

Theorem 2.2.5. Assume that: $Con\left(ZF{C}_{Nst}\right)$, where $ZF{C}_{Nst}\triangleq ZFC+\exists M_{Nst}^{ZFC}$, $M_{st}^{PA}\subset M_{Nst}^{ZFC}$.

Then truth predicate $True\left(n\right)$ is expressible by using first order language by the following formula

$True\left(g\left(A\right)\right)\iff \exists y\left(y\in M_{st}^{PA}\right)\exists m\left(m\in M_{st}^{PA}\right){\mathrm{Pr}}_m^{Nst}\left(y\mathrm{,}g\left(A\right)\right)\mathrm{.}$ (30)

Proof. Assume that:

$ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}⊢{\left[A\right]}_{M_{Nst}^{ZFC}}\mathrm{.}$ (31)

It follows from (29) there exists $m^{\ast }=m^{\ast }\left(g\left(A\right)\right)$ such that $T{h}_{m^{\ast }}⊢{\left[A\right]}_{M_{Nst}^{ZFC}}$ and therefore by (31) we obtain

${\mathrm{Pr}}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}g\left(A\right)\right)\iff {\mathrm{Pr}}_{m^{\ast }}^{Nst}\left(y\mathrm{,}g\left(A\right)\right)\mathrm{.}$ (32)

From (32) immediately by definitions one obtains (30).

Remark 2.2.6. Note that Theorem 2.1.1 in this case reads

$Con\left(ZF{C}_{Nst}\right)\Rightarrow \neg \exists True\left(x\right)\left(True\left(g\left(A\right)\right)\iff {\left[A\right]}_{M_{Nst}^{ZFC}}\right)\mathrm{.}$ (33)

Theorem 2.2.6. $\neg Con\left(ZF{C}_{Nst}\right)$.

Proof. Assume that: $Con\left(ZF{C}_{Nst}\right)$. From (30) and (33) one obtains a contradiction $Con\left(ZF{C}_{Nst}\right)\wedge \neg Con\left(ZF{C}_{Nst}\right)$ and therefore by reductio ad absurdum it follows $\neg Con\left(ZF{C}_{Nst}\right)$.

Theorem 2.2.7. Assume that: $Con\left(\overline{ZFC}{}_2^{Hs}\right)$, where $\overline{ZFC}{}_2^{Hs}\triangleq ZF{C}_2^{Hs}+\exists M_{st}^{ZF{C}_2^{Hs}}$. Then there exists completion $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}$ of the theory $\overline{ZFC}{}_2^{Hs}$ such that the following conditions hold:

i) For every first order wff formula A (wff₁ A) in the language of $ZF{C}_2^{Hs}$ that formula ${\left[A\right]}_{M_{st}^{ZF{C}_2^{Hs}}}$ or formula ${\left[\neg A\right]}_{M_{st}^{ZF{C}_2^{Hs}}}$ is provable in $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}$ i.e., for any wff₁ A, always $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}⊢{\left[A\right]}_{M_{st}^{ZF{C}_2^{Hs}}}$ or $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}⊢{\left[\neg A\right]}_{M_{st}^{ZF{C}_2^{Hs}}}$.

ii) $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}={\displaystyle {\cup }_{m\in \mathbb{N}}T{h}_m}$, where for any m a theory $T{h}_{m+1}$ is finite extension of the theory $T{h}_m$.

iii) Let ${\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ be recursive relation such that: y is a Gödel number of a proof of the wff₁ of the theory $T{h}_m$ and x is a Gödel number of this wff₁. Then the relation ${\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ is expressible in the theory $T{h}_m$ by canonical Gödel encoding and really asserts provability in $T{h}_m$.

iv) Let ${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ be relation such that: y is a Gödel number of a proof of the wff of the set theory $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}$ and x is a Gödel number of this wff₁. Then the relation ${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ is expressible in the set theory $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}$ by the following formula

${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)\iff \exists m\left(m\in \mathbb{N}\right){\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ (34)

v) The predicate ${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}x\right)$ really asserts provability in the set theory $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}$.

Remark 2.2.7. Note that the relation ${\mathrm{Pr}}_m^{st}\left(y\mathrm{,}x\right)$ is expressible in the theory $T{h}_m$ since a theory $T{h}_m$ is a finite extension of the finite axiomatizable theory $ZF{C}_2^{Hs}$ and therefore the predicate ${\mathrm{Pr}}_m^{Nst}\left(y\mathrm{,}x\right)$ exists since any theory $T{h}_m$ is recursively axiomatizable.

Remark 2.2.8. Note that a theory $ZF{C}_{Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ obviously is not recursively axiomatizable nevertheless Gödel encoding holds by Remark 2.2.1.

Theorem 2.2.8. Assume that: $Con\left(\overline{ZFC}{}_2^{Hs}\right)$, where

$\overline{ZFC}{}_2^{Hs}\triangleq ZF{C}_2^{Hs}+\exists M_{st}^{ZF{C}_2^{Hs}}$.

Then truth predicate $True\left(n\right)$ is expressible by using first order language by the following formula

$True\left(g\left(A\right)\right)\iff \exists y\left(y\in \mathbb{N}\right)\exists m\left(m\in \mathbb{N}\right){\mathrm{Pr}}_m^{st}\left(y\mathrm{,}g\left(A\right)\right)\mathrm{,}$ (35)

where A is wff₁.

Proof. Assume that:

$\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}⊢{\left[A\right]}_{M_{st}^{ZF{C}_2^{Hs}}}\mathrm{.}$ (36)

It follows from (34) there exists $m^{\ast }=m^{\ast }\left(g\left(A\right)\right)$ such that $T{h}_{m^{\ast }}⊢{\left[A\right]}_{M_{st}^{ZF{C}_2^{Hs}}}$ and therefore by (36) we obtain

${\mathrm{Pr}}_{st}^{\mathrm{<mo>\; \#\; </mo>}}\left(y\mathrm{,}g\left(A\right)\right)\iff {\mathrm{Pr}}_{m^{\ast }}^{st}\left(y\mathrm{,}g\left(A\right)\right)\mathrm{.}$ (37)

From (37) immediately by definitions one obtains (35).

Remark 2.2.9. Note that in considered case Tarski’s undefinability theorem (2.1.1) reads

$Con\left(\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}\right)\Rightarrow \neg \exists True\left(x\right)\left(True\left(g\left(A\right)\right)\iff {\left[A\right]}_{M_{st}^{ZF{C}_2^{Hs}}}\right)\mathrm{,}$ (38)

where A is wff₁.

Theorem 2.2.9. $\neg Con\left(\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}\right)$.

Proof. Assume that: $Con\left(\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}\right)$. From (35) and (38) one obtains a contradiction $Con\left(\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}\right)\wedge \neg Con\left(\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}\right)$ and therefore by reductio ad absurdum it follows $\neg Con\left(\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}\right)$.

3. Derivation of the Inconsistent Provably Definable Set in Set Theory $\overline{ZFC}{}_2^{Hs}$, $ZF{C}_{st}$ and $ZF{C}_{Nst}$

3.1. Derivation of the Inconsistent Provably Definable Set in Set Theory $\overline{ZFC}{}_2^{Hs}$

Definition 3.1.1. i) Let $\Phi$ be a wff of $\overline{ZFC}{}_2^{Hs}$. We will say that $\Phi$ is a first order n-place open wff if $\Phi$ contains free occurrences of the first order individual variables $X_1\mathrm{,}\cdots \mathrm{,}{X}_n$ and quantifiers only over any first order individual variables $Y_1\mathrm{,}\cdots \mathrm{,}{Y}_m$.

ii) Let ${\tilde{\Im }}_2^{Hs}$ be the countable set of the all first order provable definable sets X, i.e. sets such that $\overline{ZFC}{}_2^{Hs}⊢\exists \mathrm{<mo>\; !\; </mo>}X\Psi \left(X\right)$, where $\Psi \left(X\right)={\Psi }_{M_{st}}\left(X\right)$ is a first order 1-place open wff that contains only first order variables (we will denote such wff for short by wff₁), with all bound variables restricted to standard model $M_{st}=M_{st}^{ZF{C}_2^{Hs}}$, i.e.

$\begin{array}{l}\forall Y\{Y\in {\tilde{\Im }}_2^{Hs}\iff \overline{ZFC}{}_2^{Hs}⊢\exists {\Psi }_{M_{st}}\left(X\right)[\left(\left[{\Psi }_{M_{st}}\left(X\right)\right]\in {\Gamma }_{X\mathrm{,}{M}_{st}}^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\\ \wedge \left[\exists \mathrm{<mo>\; !\; </mo>}X\left[{\Psi }_{M_{st}}\left(X\right)\wedge Y=X\right]\right]]\}\mathrm{,}\end{array}$ (39)

or in a short notation

$\begin{array}{l}\forall Y\{Y\in {\tilde{\Im }}_2^{Hs}\iff \overline{ZFC}{}_2^{Hs}⊢\exists \Psi \left(X\right)[\left(\left[\Psi \left(X\right)\right]\in {\Gamma }_X^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\\ \wedge \left[\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right]]\}\mathrm{.}\end{array}$ (40)

Notation 3.1.1. In this subsection we often write for short $\Psi \left(X\right)\mathrm{,}{F}_X^{Hs}\mathrm{,}{\Gamma }_X^{Hs}$ instead ${\Psi }_{M_{st}}\left(X\right)\mathrm{,}{F}_{X\mathrm{,}{M}_{st}}^{Hs}\mathrm{,}{\Gamma }_{X\mathrm{,}{M}_{st}}^{Hs}$ but this should not lead to a confusion.

Assumption 3.1.1. We assume now for simplicity but without loss of generality that

$F_{X\mathrm{,}{M}_{st}}^{Hs}\in M_{st}$ (41)

and therefore by definition of model $M_{st}=M_{st}^{ZF{C}_2^{Hs}}$ one obtains ${\Gamma }_{X\mathrm{,}{M}_{st}}^{Hs}\in M_{st}^{ZF{C}_2^{Hs}}$.

Let $X{\notin }_{{⊢}_{\overline{ZFC}{}_2^{Hs}}}Y$ be a predicate such that $X{\notin }_{{⊢}_{{\overline{ZFC}}_2^{Hs}}}Y\leftrightarrow \overline{ZFC}{}_2^{Hs}⊢X\notin Y$. Let ${\tilde{\Re }}_2^{Hs}$ be the countable set of the all sets such that

$\forall X\left(X\in {\tilde{\Im }}_2^{Hs}\right)\left[X\in {\tilde{\Re }}_2^{Hs}\leftrightarrow X{\notin }_{{⊢}_{{\overline{ZFC}}_2^{Hs}}}X\right]\mathrm{.}$ (42)

From (42) one obtains

${\tilde{\Re }}_2^{Hs}\in {\tilde{\Re }}_2^{Hs}\leftrightarrow {\tilde{\Re }}_2^{Hs}{\notin }_{{⊢}_{{\overline{ZFC}}_2^{Hs}}}{\tilde{\Re }}_2^{Hs}\mathrm{.}$ (43)

But obviously (43) immediately gives a contradiction

$\left({\tilde{\Re }}_2^{Hs}\in {\tilde{\Re }}_2^{Hs}\right)\wedge \left({\tilde{\Re }}_2^{Hs}{\notin }_{{⊢}_{{\overline{ZFC}}_2^{Hs}}}{\tilde{\Re }}_2^{Hs}\right)\mathrm{.}$ (44)

Remark 3.1.1. Note that a contradiction (44) in fact is a contradiction inside $\overline{ZFC}{}_2^{Hs}$ for the reason that predicate $X{\notin }_{{⊢}_{{\overline{ZFC}}_2^{Hs}}}Y$ is expressible by first order

language as predicate of $\overline{ZFC}{}_2^{Hs}$ (see subsection 1.2, Theorem 1.2.8 (ii)-(iii)) and therefore countable sets ${\tilde{\Im }}_2^{Hs}$ and ${\tilde{\Re }}_2^{Hs}$ are sets in the sense of the set theory $\overline{ZFC}{}_2^{Hs}$.

Remark 3.1.2. Note that by using Gödel encoding the above stated contradiction can be shipped in special completion $\overline{ZFC}{}_2^{Hs\mathrm{<mo>\; \#\; </mo>}}$ of $\overline{ZFC}{}_2^{Hs}$, see subsection 1.2, Theorem 1.2.8.

Remark 3.1.3. i) Note that Tarski’s undefinability theorem cannot block the equivalence (43) since this theorem is no longer holds by Proposition 2.2.1. (Generalized Löbs Theorem).

ii) In additional note that: since Tarski’s undefinability theorem has been proved under the same assumption $\exists M_{st}^{ZF{C}_2^{Hs}}$ by reductio ad absurdum it follows again $\neg Con\left(ZF{C}_{Nst}\right)$, see Theorem 1.2.10.

Remark 3.1.4. More formally we can to explain the gist of the contradictions derived in this paper (see Section 4) as follows.

Let M be Henkin model of $ZF{C}_2^{Hs}$. Let ${\tilde{\Re }}_2^{Hs}$ be the set of the all sets of M provably definable in $\overline{ZFC}{}_2^{Hs}$, and let ${\tilde{\Re }}_2^{Hs}=\left\{x\in {\tilde{\Im }}_2^{Hs}:\square \left(x\notin x\right)\right\}$ where $\square A$ means “sentence A derivable in $\overline{ZFC}{}_2^{Hs}$ ”, or some appropriate modification thereof. We replace now formula (39) by the following formula

$\forall Y\left\{Y\in {\tilde{\Im }}_2^{Hs}\leftrightarrow \exists \Psi \left(X\right)\left[\left(\left[\Psi \left(X\right)\right]\in {\Gamma }_X^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\wedge \square \exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right]\right\}\mathrm{.}$ (45)

and we replace formula (42) by the following formula

$\forall X\left(X\in {\tilde{\Im }}_2^{Hs}\right)\left[X\in {\tilde{\Re }}_2^{Hs}\iff \square \left(X\notin X\right)\right]\mathrm{.}$ (46)

Definition 3.1.2. We rewrite now (45) in the following equivalent form

$\forall Y\left\{Y\in {\tilde{\Im }}_2^{Hs}\iff \exists \Psi \left(X\right)\left[\left({\left[\Psi \left(X\right)\right]}_{Hs}\in {\Gamma }_X^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\wedge \left(Y=X\right)\right]\right\}\mathrm{,}$ (47)

where the countable set ${\Gamma }_X^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X$ is defined by the following formula

$\forall \Psi \left(X\right)\left\{\left[\Psi \left(X\right)\right]\in {\Gamma }_X^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\iff \left[\left({\left[\Psi \left(X\right)\right]}_{Hs}\in {\Gamma }_X^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\wedge \square \exists !X\Psi \left(X\right)\right]\right\}$ (48)

Definition 3.1.3. Let ${\tilde{\Re }}_2^{Hs}$ be the countable set of the all sets such that

$\forall X\left(X\in {\tilde{\Im }}_2^{Hs}\right)\left[X\in {\tilde{\Re }}_2^{Hs}\iff \square X\notin X\right]\mathrm{.}$ (49)

Remark 3.1.5. Note that ${\tilde{\Re }}_2^{Hs}\in {\tilde{\Im }}_2^{Hs}$ since ${\tilde{\Re }}_2^{Hs}$ is a set definable by the first order 1-place open wff₁:

$\Psi \left(Z\mathrm{,}{\tilde{\Re }}_2^{Hs}\right)\triangleq \forall X\left(X\in {\tilde{\Im }}_2^{Hs}\right)\left[X\in Z\iff \square \left(X\notin X\right)\right]\mathrm{.}$ (50)

From (49) and Remark 3.1.4 one obtains

${\tilde{\Re }}_2^{Hs}\in {\tilde{\Re }}_2^{Hs}\iff \square \left({\tilde{\Re }}_2^{Hs}\notin {\tilde{\Re }}_2^{Hs}\right)\mathrm{.}$ (51)

But (51) immediately gives a contradiction

$\overline{ZFC}{}_2^{Hs}⊢\left({\tilde{\Re }}_2^{Hs}\in {\tilde{\Re }}_2^{Hs}\right)\wedge \left({\tilde{\Re }}_2^{Hs}\notin {\tilde{\Re }}_2^{Hs}\right)\mathrm{.}$ (52)

Remark 3.1.6. Note that contradiction (52) is a contradiction inside $\overline{ZFC}{}_2^{Hs}$ for the reason that the countable set ${\tilde{\Im }}_2^{Hs}$ is a set in the sense of the set theory $\overline{ZFC}{}_2^{Hs}$.

In order to obtain a contradiction inside $\overline{ZFC}{}_2^{Hs}$ without any reference to Assumption 3.1.1 we introduce the following definitions.

Definition 3.1.4. We define now the countable set ${\Gamma }_{\nu }^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }$ by the following formula

${\left[y\right]}_{Hs}\in {\Gamma }_{\nu }^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\iff \left({\left[y\right]}_{Hs}\in {\Gamma }_{\nu }^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\right)\wedge \widehat{Fr}{}_2^{Hs}\left(y\mathrm{,}v\right)\wedge \left[\square \exists !X{\Psi }_{y\mathrm{,}\nu }\left(X\right)\right]$ (53)

Definition 3.1.5. We choose now $\square A$ in the following form

$\square A\triangleq Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\mathrm{.}$ (54)

Here $Be{w}_{\overline{ZFC}{}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)$ is a canonical Gödel formula which says to us that there exists proof in $\overline{ZFC}{}_2^{Hs}$ of the formula A with Gödel number $\mathrm{<mo>\; \#\; </mo>}A$.

Remark 3.1.7. Note that the Definition 3.1.5 holds as definition of predicate really asserting provability of the first order sentence A in $\overline{ZFC}{}_2^{Hs}$.

Definition 3.1.6. Using Definition 3.1.5, we replace now formula (48) by the following formula

$\begin{array}{l}\forall \Psi \left(X\right)\{\left[\Psi \left(X\right)\right]\in {\Gamma }_X^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\iff \exists \Psi \left(X\right)\left(\left[\Psi \left(X\right)\right]\in {\Gamma }_X^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\\ \wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right)\right)\right]\\ \wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right)\right)\Rightarrow \exists !X\left[\Psi \left(X\right)\wedge Y=X\right]\right]\}\mathrm{.}\end{array}$ (55)

Definition 3.1.7. Using Definition 3.1.5, we replace now formula (49) by the following formula

$\begin{array}{l}\forall X\left(X\in {\tilde{\Im }}_2^{Hs}\right)[X\in {\tilde{\Re }}_2^{Hs}\iff \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\\ \wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\Rightarrow X\notin X\right]\mathrm{.}\end{array}$ (56)

Definition 3.1.8. Using Proposition 2.1.1 and Remark 2.1.10 [6] , we replace now formula (53) by the following formula

$\begin{array}{l}\forall y\{{\left[y\right]}_{Hs}\in {\Gamma }_{\nu }^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\iff \left({\left[y\right]}_{Hs}\in {\Gamma }_{\nu }^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\right)\\ \wedge \widehat{F{r}_2^{Hs}}\left(y\mathrm{,}v\right)\wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\exists \mathrm{<mo>\; !\; </mo>}X\left[{\Psi }_{y\mathrm{,}\nu }\left(X\right)\wedge Y=X\right]\right)\right]\\ \wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\exists \mathrm{<mo>\; !\; </mo>}X\left[{\Psi }_{y\mathrm{,}\nu }\left(X\right)\wedge Y=X\right]\right)\Rightarrow \exists \mathrm{<mo>\; !\; </mo>}X\left[{\Psi }_{y\mathrm{,}\nu }\left(X\right)\wedge Y=X\right]\right]\}\mathrm{.}\end{array}$ (57)

Definition 3.1.9. Using Definitions 3.1.4-3.1.6, we define now the countable set ${\tilde{\Im }}_2^{\star Hs}$ by formula

$\forall Y\left\{Y\in {\tilde{\Im }}_2^{\star Hs}\iff \exists y\left[\left(\left[y\right]\in {\Gamma }_{\nu }^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\right)\wedge \left(g_{{\overline{ZFC}}_2^{Hs}}\left(X\right)=\nu \right)\right]\right\}\mathrm{.}$ (58)

Remark 3.1.8. Note that from the second order axiom schema of replacement (12) it follows directly that ${\tilde{\Im }}_2^{\star Hs}$ is a set in the sense of the set theory $\overline{ZFC}{}_2^{Hs}$.

Definition 3.1.10. Using Definition 3.1.8 we replace now formula (56) by the following formula

$\begin{array}{l}\forall X\left(X\in {\tilde{\Im }}_2^{\star Hs}\right)[X\in {\tilde{\Re }}_2^{\star Hs}\iff \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\\ \wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\Rightarrow X\notin X\right]].\end{array}$ (59)

Remark 3.1.9. Notice that the expression (60)

$\left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\Rightarrow X\notin X\right]$ (60)

obviously is a well formed formula of $\overline{ZFC}{}_2^{Hs}$ and therefore a set ${\tilde{\Re }}_2^{\star Hs}$ is a set in the sense of $\overline{ZFC}{}_2^{Hs}$.

Remark 3.1.10. Note that ${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Im }}_2^{\star Hs}$ since ${\tilde{\Re }}_2^{\star Hs}$ is a set definable by 1-place open wff

$\begin{array}{l}\Psi \left(Z\mathrm{,}{\tilde{\Re }}_2^{\star Hs}\right)\triangleq \forall X\left(X\in {\tilde{\Im }}_2^{Hs}\right)[X\in Z\iff \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\\ \wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\Rightarrow X\notin X\right]]\mathrm{.}\end{array}$ (61)

Theorem 3.1.1. Set theory $\overline{ZFC}{}_2^{Hs}\triangleq ZF{C}_2^{Hs}+\exists M_{st}^{ZF{C}_2^{Hs}}$ is inconsistent.

Proof. From (59) we obtain

$\begin{array}{l}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\iff \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)\right]\\ \wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)\Rightarrow {\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right]\mathrm{.}\end{array}$ (62)

a) Assume now that:

${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\mathrm{.}$ (63)

Then from (62) we obtain ${⊢}_{{\overline{ZFC}}_2^{Hs}}Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)$ and

${⊢}_{{\overline{ZFC}}_2^{Hs}}Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)\Rightarrow {\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$,

therefore ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$ and so

${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\Rightarrow {\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\mathrm{.}$ (64)

From (63)-(64) we obtain

${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\mathrm{,}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\Rightarrow {\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}⊢{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$

and thus ${⊢}_{\overline{ZFC}{}_2^{Hs}}\left({\tilde{\Re }}_2^{Hs}\in {\tilde{\Re }}_2^{Hs}\right)\wedge \left({\tilde{\Re }}_2^{Hs}\notin {\tilde{\Re }}_2^{Hs}\right)$.

b) Assume now that

$\left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)\right]\wedge \left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)\Rightarrow {\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right]\mathrm{.}$ (65)

Then from (65) we obtain $⊢{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$. From (65) and (62) we obtain ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}$, so ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$, ${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}$ which immediately gives us a contradiction ${⊢}_{{\overline{ZFC}}_2^{Hs}}\left({\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\right)\wedge \left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)$.

Definition 3.1.11. We choose now $\square A$ in the following form

$\square A\triangleq \overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\mathrm{,}$ (66)

or in the following equivalent form

$\square A\triangleq \overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]$ (67)

similar to (46). Here $\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)$ is a Gödel formula which really asserts provability in $\overline{ZFC}{}_2^{Hs}$ of the formula A with Gödel number $\mathrm{<mo>\; \#\; </mo>}A$.

Remark 3.1.11. Notice that the Definition 3.1.12 with formula (66) holds as definition of predicate really asserting provability in $\overline{ZFC}{}_2^{Hs}$.

Definition 3.1.12. Using Definition 3.1.11 with formula (66), we replace now formula (48) by the following formula

$\begin{array}{l}\forall \Psi \left(X\right)\{\left[\Psi \left(X\right)\right]\in {\bar{\Gamma }}_X^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\iff \exists \Psi \left(X\right)\left(\left[\Psi \left(X\right)\right]\in {\Gamma }_X^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\\ \wedge \left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(\exists !X\left[\Psi \left(X\right)\wedge Y=X\right]\right)\right)\right]\}\mathrm{.}\end{array}$ (68)

Definition 3.1.13. Using Definition 3.1.11 with formula (66), we replace now formula (49) by the following formula

$\forall X\left(X\in {\tilde{\Im }}_2^{Hs}\right)\left[X\in {\tilde{\Re }}_2^{Hs}\iff \left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\right]$ (69)

Definition 3.1.14. Using Definition 3.1.11 with formula (66), we replace now formula (53) by the following formula

$\begin{array}{l}\forall y\{{\left[y\right]}_{Hs}\in {\Gamma }_{\nu }^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\iff \left({\left[y\right]}_{Hs}\in {\Gamma }_{\nu }^{Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\right)\wedge \widehat{Fr}{}_2^{Hs}\left(y\mathrm{,}v\right)\\ \wedge \left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\exists !X\left[{\Psi }_{y\mathrm{,}\nu }\left(X\right)\wedge Y=X\right]\right)\right]\}\mathrm{.}\end{array}$ (70)

Definition 3.1.15. Using Definitions 3.1.12-3.1.16, we define now the countable set ${\tilde{\Im }}_2^{\star Hs}$ by formula

$\forall Y\left\{Y\in {\tilde{\Im }}_2^{\star Hs}\iff \exists y\left[\left(\left[y\right]\in {\Gamma }_{\nu }^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\right)\wedge \left(g_{{\overline{ZFC}}_2^{Hs}}\left(X\right)=\nu \right)\right]\right\}\mathrm{.}$ (71)

Remark 3.1.12. Note that from the axiom schema of replacement (12) it follows directly that ${\tilde{\Im }}_2^{\star Hs}$ is a set in the sense of the set theory $\overline{ZFC}{}_2^{Hs}$.

Definition 3.1.16. Using Definition 3.1.15 we replace now formula (69) by the following formula

$\forall X\left(X\in {\tilde{\Im }}_2^{\star Hs}\right)\left[X\in {\tilde{\Re }}_2^{\star Hs}\iff \left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\right]\mathrm{.}$ (72)

Remark 3.1.13. Notice that the expressions (73)

$\begin{array}{l}\left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\text{and}\\ \left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\wedge \left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\Rightarrow X\notin X\right]\end{array}$ (73)

obviously are a well formed formula of $\overline{ZFC}{}_2^{Hs}$ and therefore collection ${\tilde{\Re }}_2^{\star Hs}$ is a set in the sense of $\overline{ZFC}{}_2^{Hs}$.

Remark 3.1.14. Note that ${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Im }}_2^{\star Hs}$ since ${\tilde{\Re }}_2^{\star Hs}$ is a set definable by 1-place open wff₁

$\Psi \left(Z\mathrm{,}{\tilde{\Re }}_2^{\star Hs}\right)\triangleq \forall X\left(X\in {\tilde{\Im }}_2^{\star Hs}\right)\left[X\in Z\iff \overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\mathrm{.}$ (74)

Theorem 3.1.2. Set theory $\overline{ZFC}{}_2^{Hs}\triangleq ZF{C}_2^{Hs}+\exists M_{st}^{ZF{C}_2^{Hs}}$ is inconsistent.

Proof. From (72) we obtain

${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\iff \left[\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)\right]\mathrm{.}$ (75)

a) Assume now that:

${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\mathrm{.}$ (76)

Then from (75) we obtain ${⊢}_{{\overline{ZFC}}_2^{Hs}}\overline{Bew}{}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)$ and therefore ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$, thus we obtain

${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\Rightarrow {\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\mathrm{.}$ (77)

From (76)-(77) we obtain ${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}$ and ${\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\Rightarrow {\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$, thus ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$ and finally we obtain ${⊢}_{{\overline{ZFC}}_2^{Hs}}\left({\tilde{\Re }}_2^{Hs}\in {\tilde{\Re }}_2^{Hs}\right)\wedge \left({\tilde{\Re }}_2^{Hs}\notin {\tilde{\Re }}_2^{Hs}\right)$.

b) Assume now that

$\left[Be{w}_{{\overline{ZFC}}_2^{Hs}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)\right)\right]\mathrm{.}$ (78)

Then from (78) we obtain ${⊢}_{\overline{ZFC}{}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$. From (78) and (75) we obtain ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}$, thus ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$ and ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}$ which immediately gives us a contradiction ${⊢}_{{\overline{ZFC}}_2^{Hs}}\left({\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\right)\wedge \left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)$.

3.2. Derivation of the Inconsistent Provably Definable Set in Set Theory ZFC_st

Let ${\Im }_{st}$ be the countable set of all sets X such that $ZF{C}_{st}⊢\exists \mathrm{<mo>\; !\; </mo>}X\Psi \left(X\right)$, where $\Psi \left(X\right)$ is a 1-place open wff of ZFC i.e.,

$\begin{array}{l}\forall Y\{Y\in {\Im }_{st}\iff ZF{C}_{st}⊢\exists \Psi \left(X\right)[\left(\left[\Psi \left(X\right)\right]\in {\Gamma }_X^{st}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\\ \wedge \exists !X\left[\Psi \left(X\right)\wedge Y=X\right]]\}\mathrm{.}\end{array}$ (79)

Let $X{\notin }_{{⊢}_{ZF{C}_{st}}}Y$ be a predicate such that $X{\notin }_{{⊢}_{ZF{C}_{st}}}Y\iff ZF{C}_{st}⊢X\notin Y$. Let $\Re$ be the countable set of the all sets such that

$\forall X\left[X\in {\Re }_{st}\iff \left(X\in {\Im }_{st}\right)\wedge \left(X{\notin }_{{⊢}_{ZF{C}_{st}}}X\right)\right]\mathrm{.}$ (80)

From (80) one obtains

${\Re }_{st}\in {\Re }_{st}\iff {\Re }_{st}{\notin }_{{⊢}_{ZF{C}_{st}}}{\Re }_{st}\mathrm{.}$ (81)

But (81) immediately gives a contradiction

$\left({\Re }_{st}\in {\Re }_{st}\right)\wedge \left({\Re }_{st}\notin {\Re }_{st}\right)\mathrm{.}$ (82)

Remark 3.2.1. Note that a contradiction (82) is a contradiction inside $ZF{C}_{st}$

for the reason that predicate $X{\notin }_{{⊢}_{ZF{C}_{st}}}Y$ is expressible by using first order

language as predicate of $ZF{C}_{st}$ (see subsection 4.1) and therefore countable sets ${\Im }_{st}$ and ${\Re }_{st}$ are sets in the sense of the set theory $ZF{C}_{st}$.

Remark 3.2.2. Note that by using Gödel encoding the above stated contradiction can be shipped in special completion $ZF{C}_{st}^{\mathrm{<mo>\; \#\; </mo>}}$ of $ZF{C}_{st}$, see subsection 1.2, Theorem 1.2.2 (i).

Designation 3.2.1. i) Let $M_{st}^{ZFC}$ be a standard model of ZFC and

ii) let $ZF{C}_{st}$ be the theory $ZF{C}_{st}=ZFC+\exists M_{st}^{ZFC}$,

iii) let ${\Im }_{st}$ be the set of the all sets of $M_{st}^{ZFC}$ provably definable in $ZF{C}_{st}$, and let ${\Re }_{st}=\left\{X\in {\Im }_{st}\mathrm{<mo>\; :\; </mo>}{\square }_{st}\left(X\notin X\right)\right\}$, where ${\square }_{st}A$ means: “sentence A derivable in $ZF{C}_{st}$ ”, or some appropriate modification thereof.

We replace now (79) by formula

$\forall Y\left\{Y\in {\Im }_{st}\leftrightarrow {\square }_{st}\left[\exists \Psi (\cdot )\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right]\right\}\mathrm{,}$ (83)

and we replace (80) by formula

$\forall X\left[X\in {\Re }_{st}\leftrightarrow \left(X\in {\Im }_{st}\right)\wedge {\square }_{st}\left(X\notin X\right)\right]\mathrm{.}$ (84)

Assume that $ZF{C}_{st}⊢{\Re }_{st}\in {\Im }_{st}$. Then, we have that: ${\Re }_{st}\in {\Re }_{st}$ iff ${\square }_{st}\left({\Re }_{st}\notin {\Re }_{st}\right)$, which immediately gives us ${\Re }_{st}\in {\Re }_{st}$ iff ${\Re }_{st}\notin {\Re }_{st}$. But this is a contradiction, i.e., $ZF{C}_{st}⊢\left({\Re }_{st}\in {\Re }_{st}\right)\wedge \left({\Re }_{st}\notin {\Re }_{st}\right)$. We choose now ${\square }_{st}A$ in the following form

${\square }_{st}A\triangleq Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\mathrm{.}$ (85)

Here $Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)$ is a canonical Gödel formula which says to us that there exists proof in $ZF{C}_{st}$ of the formula A with Gödel number $\mathrm{<mo>\; \#\; </mo>}A\in M_{st}^{PA}$.

Remark 3.2.3. Notice that Definition 3.2.6 holds as definition of predicate really asserting provability in $ZF{C}_{st}$.

Definition 3.2.1. We rewrite now (83) in the following equivalent form

$\forall Y\left\{Y\in {\tilde{\Im }}_{st}\iff \exists \Psi \left(X\right)\left[\left({\left[\Psi \left(X\right)\right]}_{st}\in {\Gamma }_X^{\star st}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\wedge \left(Y=X\right)\right]\right\}\mathrm{,}$ (86)

where the countable collection ${\Gamma }_X^{\star Hs}\mathrm{<mo>\; /\; </mo>}{\sim }_X$ is defined by the following formula

$\forall \Psi \left(X\right)\left\{{\left[\Psi \left(X\right)\right]}_{st}\in {\Gamma }_X^{\star st}\mathrm{<mo>\; /\; </mo>}{\sim }_X\iff \left[\left({\left[\Psi \left(X\right)\right]}_{st}\in {\Gamma }_X^{st}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\wedge {\square }_{st}\exists \mathrm{<mo>\; !\; </mo>}X\Psi \left(X\right)\right]\right\}$ (87)

Definition 3.2.2. Let ${\tilde{\Re }}_{st}$ be the countable collection of the all sets such that

$\forall X\left(X\in {\tilde{\Im }}_{st}\right)\left[X\in {\tilde{\Re }}_{st}\iff {\square }_{st}\left(X\notin X\right)\right]\mathrm{.}$ (88)

Remark 3.2.4. Note that ${\tilde{\Re }}_2^{Hs}\in {\tilde{\Im }}_2^{Hs}$ since ${\tilde{\Re }}_2^{Hs}$ is a collection definable by 1-place open wff

$\Psi \left(Z\mathrm{,}{\tilde{\Re }}_{st}\right)\triangleq \forall X\left(X\in {\tilde{\Im }}_{st}\right)\left[X\in Z\iff {\square }_{st}\left(X\notin X\right)\right]\mathrm{.}$ (89)

Definition 3.2.3. By using formula (85) we rewrite now (86) in the following equivalent form

$\forall Y\left\{Y\in {\tilde{\Im }}_{st}\iff \exists \Psi \left(X\right)\left[\left({\left[\Psi \left(X\right)\right]}_{st}\in {\Gamma }_X^{\star st}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\wedge \left(Y=X\right)\right]\right\}\mathrm{,}$ (90)

where the countable collection ${\Gamma }_X^{\star Hs}/{\sim }_X$ is defined by the following formula

$\begin{array}{l}\forall \Psi \left(X\right)\{{\left[\Psi \left(X\right)\right]}_{st}\in {\Gamma }_X^{\star st}\mathrm{<mo>\; /\; </mo>}{\sim }_X\iff \\ \left[\left({\left[\Psi \left(X\right)\right]}_{st}\in {\Gamma }_X^{st}\mathrm{<mo>\; /\; </mo>}{\sim }_X\right)\wedge Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\exists \mathrm{<mo>\; !\; </mo>}X\Psi \left(X\right)\right)\right]\\ \wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\exists \mathrm{<mo>\; !\; </mo>}X\Psi \left(X\right)\right)\Rightarrow \exists \mathrm{<mo>\; !\; </mo>}X\Psi \left(X\right)\right]\}\end{array}$ (91)

Definition 3.2.4. Using formula (85), we replace now formula (88) by the following formula

$\forall X\left(X\in {\tilde{\Im }}_{st}\right)[X\in {\tilde{\Re }}_{st}\iff \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\mathrm{.}$ (92)

Definition 3.2.5. Using Proposition 2.1.1 and Remark 2.2.2 [6] , we replace now formula (89) by the following formula

$\begin{array}{l}\forall y\{{\left[y\right]}_{st}\in {\Gamma }_{\nu }^{\star st}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\iff \left({\left[y\right]}_{st}\in {\Gamma }_{\nu }^{st}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\right)\wedge \widehat{Fr}{}_{st}\left(y\mathrm{,}v\right)\\ \wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\exists \mathrm{<mo>\; !\; </mo>}X\left[{\Psi }_{y\mathrm{,}\nu }\left(X\right)\wedge Y=X\right]\right)\right]\\ \wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\exists \mathrm{<mo>\; !\; </mo>}X\left[{\Psi }_{y\mathrm{,}\nu }\left(X\right)\wedge Y=X\right]\right)\Rightarrow \exists \mathrm{<mo>\; !\; </mo>}X\left[{\Psi }_{y\mathrm{,}\nu }\left(X\right)\wedge Y=X\right]\right]\}\mathrm{.}\end{array}$ (93)

Definition 3.2.6. Using Definitions 3.2.3-3.2.5, we define now the countable set ${\tilde{\Im }}_{st}^{\star }$ by formula

$\forall Y\left\{Y\in {\tilde{\Im }}_{st}^{\star }\iff \exists y\left[\left({\left[y\right]}_{st}\in {\Gamma }_{\nu }^{\star st}\mathrm{<mo>\; /\; </mo>}{\sim }_{\nu }\right)\wedge \left(g_{ZF{C}_{st}}\left(X\right)=\nu \right)\right]\right\}\mathrm{.}$ (94)

Remark 3.2.5. Note that from the axiom schema of replacement it follows directly that ${\tilde{\Im }}_{st}^{\star }$ is a set in the sense of the set theory $ZF{C}_{st}$.

Definition 3.2.7. Using Definition 3.2.6 we replace now formula (92) by the following formula

$\begin{array}{l}\forall X\left(X\in {\tilde{\Im }}_{st}^{\star }\right)[X\in {\tilde{\Re }}_{st}^{\star }\iff \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\\ \wedge \left[Be{w}_{{\overline{ZFC}}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\Rightarrow X\notin X\right]].\end{array}$ (95)

Remark 3.2.6. Notice that the expression (96)

$\left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\Rightarrow X\notin X\right]$ (96)

obviously is a well formed formula of $ZF{C}_{st}$ and therefore collection ${\tilde{\Re }}_{st}^{\star }$ is a set in the sense of $\overline{ZFC}{}_2^{Hs}$.

Remark 3.2.7. Note that ${\tilde{\Re }}_{st}^{\star }\in {\tilde{\Im }}_{st}^{\star }$ since ${\tilde{\Re }}_{st}^{\star }$ is a collection definable by 1-place open wff

$\begin{array}{l}\Psi \left(Z\mathrm{,}{\tilde{\Re }}_{st}^{\star }\right)\triangleq \forall X\left(X\in {\tilde{\Im }}_{st}^{\star }\right)[X\in Z\iff \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\right]\\ \wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left(X\notin X\right)\right)\Rightarrow X\notin X\right]]\mathrm{.}\end{array}$ (97)

Theorem 3.2.1. Set theory $ZF{C}_{st}\triangleq ZFC+\exists M_{st}^{ZFC}$ is inconsistent.

Proof. From (95) we obtain

$\begin{array}{l}{\tilde{\Re }}_{st}^{\star }\in {\tilde{\Re }}_{st}^{\star }\iff \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right)\right)\right]\\ \wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right)\right)\Rightarrow {\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right]\mathrm{.}\end{array}$ (98)

a) Assume now that:

${\tilde{\Re }}_{st}^{\star }\in {\tilde{\Re }}_{st}^{\star }\mathrm{.}$ (99)

Then from (98) we obtain $⊢Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right)\right)$ and $⊢Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right)\right)\Rightarrow {\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }$, therefore $⊢{\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }$ and so

${⊢}_{ZF{C}_{st}}{\tilde{\Re }}_{st}^{\star }\in {\tilde{\Re }}_{st}^{\star }\Rightarrow {\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\mathrm{.}$ (100)

From (99)-(100) we obtain ${\tilde{\Re }}_{st}^{\star }\in {\tilde{\Re }}_{st}^{\star }\mathrm{,}{\tilde{\Re }}_{st}^{\star }\in {\tilde{\Re }}_{st}^{\star }\Rightarrow {\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }⊢{\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }$ and therefore ${⊢}_{ZF{C}_{st}}\left({\tilde{\Re }}_{st}^{\star }\in {\tilde{\Re }}_{st}^{\star }\right)\wedge \left({\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right)$.

b) Assume now that

$\left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right)\right)\right]\wedge \left[Be{w}_{ZF{C}_{st}}\left(\mathrm{<mo>\; \#\; </mo>}\left({\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right)\right)\Rightarrow {\tilde{\Re }}_{st}^{\star }\notin {\tilde{\Re }}_{st}^{\star }\right]\mathrm{.}$ (101)

Then from (101) we obtain $⊢{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}$. From (101) and (98) we obtain ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}$, so ${⊢}_{{\overline{ZFC}}_2^{Hs}}{\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\mathrm{,}{\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}$ which immediately gives us a contradiction ${⊢}_{{\overline{ZFC}}_2^{Hs}}\left({\tilde{\Re }}_2^{\star Hs}\in {\tilde{\Re }}_2^{\star Hs}\right)\wedge \left({\tilde{\Re }}_2^{\star Hs}\notin {\tilde{\Re }}_2^{\star Hs}\right)$.

3.3. Derivation of the Inconsistent Provably Definable Set in ZFC_Nst

Designation 3.3.1. i) Let $\overline{PA}$ be a first order theory which contain usual postulates of Peano arithmetic [8] and recursive defining equations for every primitive recursive function as desired.

ii) Let $M_{Nst}^{ZFC}$ be a nonstandard model of ZFC and let $M_{st}^{\overline{PA}}$ be a standard model of $\overline{PA}$. We assume now that $M_{st}^{\overline{PA}}\subset M_{Nst}^{ZFC}$ and denote such nonstandard model of ZFC by $M_{Nst}^{ZFC}\left[\overline{PA}\right]$.

iii) Let $ZF{C}_{Nst}$ be the theory $ZF{C}_{Nst}=ZFC+M_{Nst}^{ZFC}\left[\overline{PA}\right]$.

iv) Let ${\Im }_{Nst}$ be the set of the all sets of $M_{st}^{ZFC}\left[\overline{PA}\right]$ provably definable in $ZF{C}_{Nst}$, and let ${\Re }_{Nst}=\left\{X\in {\Im }_{Nst}\mathrm{<mo>\; :\; </mo>}{\square }_{Nst}\left(X\notin X\right)\right\}$ where ${\square }_{Nst}A$ means “sentence A derivable in $ZF{C}_{Nst}$ ”, or some appropriate modification thereof. We replace now (45) by formula

$\forall Y\left\{Y\in {\Im }_{Nst}\leftrightarrow {\square }_{Nst}\left[\exists \Psi (\cdot )\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right]\right\}\mathrm{,}$ (102)

and we replace (46) by formula

$\forall X\left[X\in {\Re }_{Nst}\leftrightarrow \left(X\in {\Im }_{Nst}\right)\wedge {\square }_{Nst}\left(X\notin X\right)\right]\mathrm{.}$ (103)

Assume that $ZF{C}_{Nst}⊢{\Re }_{Nst}\in {\Im }_{Nst}$. Then, we have that: ${\Re }_{Nst}\in {\Re }_{Nst}$ iff ${\square }_{Nst}\left({\Re }_{Nst}\notin {\Re }_{Nst}\right)$, which immediately gives us ${\Re }_{Nst}\in {\Re }_{Nst}$ iff ${\Re }_{Nst}\notin {\Re }_{Nst}$. But this is a contradiction, i.e., $ZF{C}_{Nst}⊢\left({\Re }_{Nst}\in {\Re }_{Nst}\right)\wedge \left({\Re }_{Nst}\notin {\Re }_{Nst}\right)$. We choose now ${\square }_{Nst}A$ in the following form

${\square }_{Nst}A\triangleq Be{w}_{ZF{C}_{Nst}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{ZF{C}_{Nst}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)A\right]\mathrm{.}$ (104)

Here $Be{w}_{ZF{C}_{Nst}}\left(\mathrm{<mo>\; \#\; </mo>}A\right)$ is a canonical Gödel formula which says to us that there exists proof in $ZF{C}_{Nst}$ of the formula A with Gödel number $\mathrm{<mo>\; \#\; </mo>}A\in M_{st}^{PA}$.

Remark 3.3.1. Notice that definition (104) holds as definition of predicate really asserting provability in $ZF{C}_{Nst}$.

Designation 3.3.2. i) Let $g_{ZF{C}_{Nst}}\left(u\right)$ be a Gödel number of given an expression u of $ZF{C}_{Nst}$.

ii) Let $F{r}_{Nst}\left(y\mathrm{,}v\right)$ be the relation: y is the Gödel number of a wff of $ZF{C}_{Nst}$ that contains free occurrences of the variable with Gödel number v [6] [10] .

iii) Let ${\wp }_{Nst}\left(y\mathrm{,}v\mathrm{,}{\nu }_1\right)$ be a Gödel number of the following wff: $\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]$, where $g_{ZF{C}_{Nst}}\left(\Psi \left(X\right)\right)=y$, $g_{ZF{C}_{Nst}}\left(X\right)=\nu$, $g_{ZF{C}_{Nst}}\left(Y\right)={\nu }_1$.

iv) Let ${\mathrm{Pr}}_{ZF{C}_{Nst}}\left(z\right)$ be a predicate asserting provability in $ZF{C}_{Nst}$.

Remark 3.3.2. Let ${\Im }_{Nst}$ be the countable collection of all sets X such that $ZF{C}_{Nst}⊢\exists \mathrm{<mo>\; !\; </mo>}X\Psi \left(X\right)$, where $\Psi \left(X\right)$ is a 1-place open wff i.e.,

$\forall Y\left\{Y\in {\Im }_{Nst}\iff ZF{C}_{Nst}⊢\exists \Psi \left(X\right)\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right\}\mathrm{.}$ (105)

We rewrite now (105) in the following form

$\begin{array}{l}\forall Y\{Y\in {\Im }_{Nst}^{\star }\iff \left(g_{ZF{C}_{Nst}}\left(Y\right)={\nu }_1\right)\wedge \exists y\widehat{Fr}{}_{Nst}\left(y\mathrm{,}v\right)\\ \wedge \left(g_{ZF{C}_{Nst}}\left(X\right)=\nu \right)\wedge [{\mathrm{Pr}}_{ZF{C}_{Nst}}\left({\wp }_{Nst}\left(y\mathrm{,}v\mathrm{,}{\nu }_1\right)\right)\\ \wedge \left[{\mathrm{Pr}}_{ZF{C}_{Nst}}\left({\wp }_{Nst}\left(y\mathrm{,}v\mathrm{,}{\nu }_1\right)\right)\Rightarrow \exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right]]\}\end{array}$ (106)

Designation 3.3.3. Let ${\wp }_{Nst}\left(z\right)$ be a Gödel number of the following wff: $Z\notin Z$, where $g_{ZF{C}_{Nst}}\left(Z\right)=z$.

Remark 3.3.3. Let ${\Re }_{Nst}$ above by formula (103), i.e.,

$\forall Z\left[Z\in {\Re }_{Nst}\leftrightarrow \left(Z\in {\Im }_{Nst}\right)\wedge {\square }_{Nst}\left(Z\notin Z\right)\right]\mathrm{.}$ (107)

We rewrite now (107) in the following form

$\begin{array}{l}\forall Z\left[Z\in {\Re }_{Nst}^{\star }\leftrightarrow \left(Z\in {\Im }_{Nst}^{\star }\right)\wedge g_{ZF{C}_{Nst}}\left(Z\right)=z\wedge {\mathrm{Pr}}_{ZF{C}_{Nst}}\left({\wp }_{Nst}\left(z\right)\right)\right]\\ \wedge \left[{\mathrm{Pr}}_{ZF{C}_{Nst}}\left({\wp }_{Nst}\left(z\right)\right)\Rightarrow Z\notin Z\right]\mathrm{.}\end{array}$ (108)

Theorem 3.3.1. $ZF{C}_{Nst}⊢{\Re }_{Nst}^{\star }\in {\Re }_{Nst}^{\star }\wedge {\Re }_{Nst}^{\star }\notin {\Re }_{Nst}^{\star }$.

3.4. Generalized Tarski’s Undefinability Lemma

Remark 3.4.1. Remind that: i) if $Th$ is a theory, let $T_{Th}$ be the set of Godel numbers of theorems of $Th$ [10] , ii) the property $x\in T_{Th}$ is said to be is expressible in $Th$ by wff $True\left(x_1\right)$ if the following properties are satisfied [10] :

a) if $n\in T_{Th}$ then $Th⊢True\left(\bar{n}\right)$, b) if $n\notin T_{Th}$ then $Th⊢\neg True\left(\bar{n}\right)$.

Remark 3.4.2. Notice it follows from (a) $\wedge$ (b) that

$\neg \left[\left(Th⊬True\left(\bar{n}\right)\right)\wedge \left(Th⊬\neg True\left(\bar{n}\right)\right)\right]$.

Theorem 3.4.1. (Tarski’s undefinability Lemma) [10] . Let $Th$ be a consistent theory with equality in the language $L$ in which the diagonal function D is representable and let $g_{Th}\left(u\right)$ be a Gödel number of given an expression u of $Th$. Then the property $x\in T_{Th}$ is not expressible in $Th$.

Proof. By the diagonalization lemma applied to $\neg True\left(x_1\right)$ there is a sentence $F$ such that: c) $Th⊢F\iff \neg True\left(\bar{q}\right)$, where q is the Godel number of $F$, i.e. $g_{Th}\left(F\right)=q$.

Case 1. Suppose that $Th⊢F$, then $q\in T_{Th}$. By (a), $Th⊢True\left(\bar{q}\right)$. But, from $Th⊢F$ and (c), by biconditional elimination, one obtains $Th⊢\neg True\left(\bar{q}\right)$. Hence $Th$ is inconsistent, contradicting our hypothesis.

Case 2. Suppose that $Th⊬F$, then $q\notin T_{Th}$. By (b), $Th⊢\neg True\left(\bar{q}\right)$. Hence, by (c) and biconditional elimination, $Th⊢F$. Thus, in either case a contradiction is reached.

Definition 3.4.1. If $Th$ is a theory, let $T_{Th}$ be the set of Godel numbers of theorems of $Th$ and let $g_{Th}\left(u\right)$ be a Gödel number of given an expression u of $Th$. The property $x\in T_{Th}$ is said to be is a strongly expressible in $Th$ by wff $Tru{e}^{\ast }\left(x_1\right)$ if the following properties are satisfied:

a) if $n\in T_{Th}$ then $Th⊢Tru{e}^{\ast }\left(\bar{n}\right)\wedge \left(Tru{e}^{\ast }\left(\bar{n}\right)\Rightarrow g_{Th}^{-1}\left(n\right)\right)$,

b) if $n\notin T_{Th}$ then $Th⊢\neg Tru{e}^{\ast }\left(\bar{n}\right)$.

Theorem 3.4.2. (Generalized Tarski’s undefinability Lemma). Let $Th$ be a consistent theory with equality in the language $L$ in which the diagonal function D is representable and let $g_{Th}\left(u\right)$ be a Gödel number of given an expression u of $Th$. Then the property $x\in T_{Th}$ is not strongly expressible in $Th$.

Proof. By the diagonalization lemma applied to $\neg Tru{e}^{\ast }\left(x_1\right)$ there is a sentence $F^{\ast }$ such that: c) $Th⊢F^{\ast }\iff \neg Tru{e}^{\ast }\left(\bar{q}\right)$, where q is the Godel number of $F^{\ast }$, i.e. $g_{Th}\left(F^{\ast }\right)=q$.

Case 1. Suppose that $Th⊢F^{\ast }$, then $q\in T_{Th}$. By (a), $Th⊢Tru{e}^{\ast }\left(\bar{q}\right)$. But, from $Th⊢F^{\ast }$ and (c), by biconditional elimination, one obtains $Th⊢\neg Tru{e}^{\ast }\left(\bar{q}\right)$. Hence $Th$ is inconsistent, contradicting our hypothesis.

Case 2. Suppose that $Th⊬F^{\ast }$, then $q\notin T_{Th}$. By (b), $Th⊢\neg Tru{e}^{\ast }\left(\bar{q}\right)$. Hence, by (c) and biconditional elimination, $Th⊢F^{\ast }$. Thus, in either case a contradiction is reached.

Remark 3.4.3. Notice that Tarski’s undefinability theorem cannot blocking the biconditionals

$\begin{array}{l}\Re \in \Re \iff \Re \notin \Re \mathrm{,}{\Re }_{st}\in {\Re }_{st}\iff {\Re }_{st}\notin {\Re }_{st}\mathrm{,}\\ {\Re }_{Nst}\in {\Re }_{Nst}\iff {\Re }_{Nst}\notin {\Re }_{Nst}\mathrm{,}\end{array}$ (109)

see Subsection 2.2.

3.5. Generalized Tarski’s Undefinability Theorem

Remark 3.5.1. I) Let $T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}$ be the theory $T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}\triangleq \overline{ZFC}{}_2^{Hs}$.

In addition under assumption $\widetilde{Con}\left(T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}\right)$, we establish a countable sequence of the consistent extensions of the theory $T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}$ such that:

i) $T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}⊊\cdots ⊊T{h}_i^{\mathrm{<mo>\; \#\; </mo>}}⊊T{h}_{i+1}^{\mathrm{<mo>\; \#\; </mo>}}⊊\cdots ⊊T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}$, where

ii) $T{h}_{i+1}^{\mathrm{<mo>\; \#\; </mo>}}$ is a finite consistent extension of $T{h}_i^{\mathrm{<mo>\; \#\; </mo>}}$,

iii) $T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}={\displaystyle {\cup }_{i\in \mathbb{N}}T{h}_i^{\mathrm{<mo>\; \#\; </mo>}}}$,

iv) $T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}$ proves the all sentences of $T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}$, which is valid in M, i.e., $M\models A\Rightarrow T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}⊢A$, see see Subsection 4.1, Proposition 4.1.1.

II) Let $T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ be $T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}\triangleq ZF{C}_{st}$.

In addition under assumption $\widetilde{Con}\left(T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}\right)$, we establish a countable sequence of the consistent extensions of the theory $T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}$ such that:

i) $T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}⊊\cdots ⊊T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}⊊T{h}_{i+\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}⊊\cdots ⊊T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$, where

ii) $T{h}_{i+\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ is a finite consistent extension of $T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$,

iii) $T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}={\displaystyle {\cup }_{i\in \mathbb{N}}T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}}$,

iv) $T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ proves the all sentences of $T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}$, which valid in $M_{st}^{ZFC}$, i.e., $M_{st}^{ZFC}\models A\Rightarrow T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}⊢A$, see Subsection 4.1, Proposition 4.1.1.

III) Let $T{h}_{\mathrm{1,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ be $T{h}_{\mathrm{1,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}\triangleq ZF{C}_{Nst}$.

In addition under assumption $\widetilde{Con}\left(T{h}_{\mathrm{1,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}\right)$, we establish a countable sequence of the consistent extensions of the theory $T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}$ such that:

i) $T{h}_{\mathrm{1,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}⊊\cdots ⊊T{h}_{i\mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}⊊T{h}_{i+\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}⊊\cdots ⊊T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$, where

ii) $T{h}_{i+\mathrm{1,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ is a finite consistent extension of $T{h}_{i\mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$,

iii) $T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}={\displaystyle {\cup }_{i\in \mathbb{N}}T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}}$

iv) $T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ proves the all sentences of $T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}$, which valid in $M_{Nst}^{ZFC}\left[PA\right]$, i.e., $M_{Nst}^{ZFC}\left[PA\right]\models A\Rightarrow T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}⊢A$, see Subsection 4.1, Proposition 4.1.1.

Remark 3.5.2. I) Let ${\Im }_i\mathrm{,}i=\mathrm{1,2,}\cdots$ be the set of the all sets of M provably definable in $T{h}_i^{\mathrm{<mo>\; \#\; </mo>}}$,

$\forall Y\left\{Y\in {\Im }_i\leftrightarrow {\square }_i\exists \Psi (\cdot )\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right\}\mathrm{.}$ (110)

and let ${\Re }_i=\left\{x\in {\Im }_i\mathrm{<mo>\; :\; </mo>}{\square }_i\left(x\notin x\right)\right\}$ where ${\square }_{i}A$ means sentence A derivable in $T{h}_i^{\mathrm{<mo>\; \#\; </mo>}}$. Then we have that ${\Re }_i\in {\Re }_i$ iff ${\square }_i\left({\Re }_i\notin {\Re }_i\right)$, which immediately gives us ${\Re }_i\in {\Re }_i$ iff ${\Re }_i\notin {\Re }_i$. We choose now ${\square }_{i}A\mathrm{,}i=\mathrm{1,2,}\cdots$ in the following form

${\square }_{i}A\triangleq Be{w}_i\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_i\left(\mathrm{<mo>\; \#\; </mo>}A\right)A\right]\mathrm{.}$ (111)

Here $Be{w}_i\left(\mathrm{<mo>\; \#\; </mo>}A\right)\mathrm{,}i=\mathrm{1,2,}\cdots$ is a canonical Gödel formulae which says to us that there exists proof in $T{h}_i^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}i=\mathrm{1,2,}\cdots$ of the formula A with Gödel number $\mathrm{<mo>\; \#\; </mo>}A$.

II) Let ${\Im }_{i\mathrm{,}st}\mathrm{,}i=\mathrm{1,2,}\cdots$ be the set of the all sets of $M_{st}^{ZFC}$ provably definable in $T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$,

$\forall Y\left\{Y\in {\Im }_{i\mathrm{,}st}\leftrightarrow {\square }_{i\mathrm{,}st}\exists \Psi (\cdot )\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right\}\mathrm{.}$ (112)

and let ${\Re }_{i\mathrm{,}st}=\left\{x\in {\Im }_{i\mathrm{,}st}\mathrm{<mo>\; :\; </mo>}{\square }_{i\mathrm{,}st}\left(x\notin x\right)\right\}$ where ${\square }_{i\mathrm{,}st}A$ means sentence A derivable in $T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$.

Then we have that ${\Re }_{i\mathrm{,}st}\in {\Re }_{i\mathrm{,}st}$ iff ${\square }_{i\mathrm{,}st}\left({\Re }_{i\mathrm{,}st}\notin {\Re }_{i\mathrm{,}st}\right)$, which immediately gives us ${\Re }_{i\mathrm{,}st}\in {\Re }_{i\mathrm{,}st}$ iff ${\Re }_{i\mathrm{,}st}\notin {\Re }_{i\mathrm{,}st}$. We choose now ${\square }_{i\mathrm{,}st}A\mathrm{,}i=\mathrm{1,2,}\cdots$ in the following form

${\square }_{i\mathrm{,}st}A\triangleq Be{w}_{i\mathrm{,}st}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{i\mathrm{,}st}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\mathrm{.}$ (113)

Here $Be{w}_{i\mathrm{,}st}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\mathrm{,}i=\mathrm{1,2,}\cdots$ is a canonical Gödel formulae which says to us that there exists proof in $T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}i=\mathrm{1,2,}\cdots$ of the formula A with Gödel number $\mathrm{<mo>\; \#\; </mo>}A$.

III) Let ${\Im }_{i\mathrm{,}Nst}\mathrm{,}i=\mathrm{1,2,}\cdots$ be the set of the all sets of $M_{Nst}^{ZFC}\left[PA\right]$ provably definable in $T{h}_{i\mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$,

$\forall Y\left\{Y\in {\Im }_{i\mathrm{,}Nst}\leftrightarrow {\square }_{i\mathrm{,}Nst}\exists \Psi (\cdot )\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right\}\mathrm{.}$ (114)

and let ${\Re }_{i\mathrm{,}Nst}=\left\{x\in {\Im }_{i\mathrm{,}Nst}\mathrm{<mo>\; :\; </mo>}{\square }_{i\mathrm{,}Nst}\left(x\notin x\right)\right\}$ where ${\square }_{i\mathrm{,}Nst}A$ means sentence A derivable in $T{h}_{i\mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$. Then we have that ${\Re }_{i\mathrm{,}Nst}\in {\Re }_{i\mathrm{,}Nst}$ iff ${\square }_{i\mathrm{,}Nst}\left({\Re }_{i\mathrm{,}Nst}\notin {\Re }_{i\mathrm{,}Nst}\right)$, which immediately gives us ${\Re }_{i\mathrm{,}Nst}\in {\Re }_{i\mathrm{,}Nst}$ iff ${\Re }_{i\mathrm{,}Nst}\notin {\Re }_{i\mathrm{,}Nst}$.

We choose now ${\square }_{i\mathrm{,}Nst}A\mathrm{,}i=\mathrm{1,2,}\cdots$ in the following form

${\square }_{i\mathrm{,}Nst}A\triangleq Be{w}_{i\mathrm{,}Nst}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{i\mathrm{,}Nst}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\mathrm{.}$ (115)

Here $Be{w}_{i\mathrm{,}Nst}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\mathrm{,}i=\mathrm{1,2,}\cdots$ is a canonical Gödel formulae which says to us that there exists proof in $T{h}_{i\mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}i=\mathrm{1,2,}\cdots$ of the formula A with Gödel number $\mathrm{<mo>\; \#\; </mo>}A$.

Remark 3.5.3. Notice that definitions (111), (113) and (115) hold as definitions of predicates really asserting provability in $T{h}_i^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ and $T{h}_{i\mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}i=\mathrm{1,2,}\cdots$ correspondingly.

Remark 3.5.4. Of course the all theories $T{h}_i^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}T{h}_{i\mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}T{h}_{i\mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}i=\mathrm{1,2,}\cdots$ are inconsistent, see subsection 4.1.

Remark 3.5.5. I) Let ${\Im }_{\infty }$ be the set of the all sets of M provably definable in $T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}$,

$\forall Y\left\{Y\in {\Im }_{\infty }\leftrightarrow {\square }_{\infty }\exists \Psi (\cdot )\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right\}\mathrm{.}$ (116)

and let ${\Re }_{\infty }=\left\{x\in {\Im }_{\infty }\mathrm{<mo>\; :\; </mo>}{\square }_{\infty }\left(x\notin x\right)\right\}$, where ${\square }_{\infty }A$ means “sentence A derivable in $T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}$ ”. Then, we have that ${\Re }_{\infty }\in {\Re }_{\infty }$ iff ${\square }_{\infty }\left({\Re }_{\infty }\notin {\Re }_{\infty }\right)$, which immediately gives us ${\Re }_{\infty }\in {\Re }_{\infty }$ iff ${\Re }_{\infty }\notin {\Re }_{\infty }$. We choose now ${\square }_{\infty }A\mathrm{,}i=\mathrm{1,2,}\cdots$ in the following form

${\square }_{\infty }A\triangleq \exists i\left[Be{w}_i\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_i\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\right]\mathrm{.}$ (117)

II) Let ${\Im }_{\infty \mathrm{,}st}$ be the set of the all sets of $M_{st}^{ZFC}$ provably definable in $T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$,

$\forall Y\left\{Y\in {\Im }_{\infty \mathrm{,}st}\leftrightarrow {\square }_{\infty \mathrm{,}st}\exists \Psi (\cdot )\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right\}\mathrm{.}$ (118)

and let ${\Re }_{\infty \mathrm{,}st}$ be the set ${\Re }_{\infty \mathrm{,}st}=\left\{x\in {\Im }_{\infty \mathrm{,}st}\mathrm{<mo>\; :\; </mo>}{\square }_{\infty \mathrm{,}st}\left(x\notin x\right)\right\}$, where ${\square }_{\infty \mathrm{,}st}A$ means “sentence A derivable in $T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ ”. Then, we have that ${\Re }_{\infty \mathrm{,}st}\in {\Re }_{\infty \mathrm{,}st}$ iff ${\square }_{\infty \mathrm{,}st}\left({\Re }_{\infty \mathrm{,}st}\notin {\Re }_{\infty \mathrm{,}st}\right)$, which immediately gives us ${\Re }_{\infty \mathrm{,}st}\in {\Re }_{\infty \mathrm{,}st}$ iff ${\Re }_{\infty \mathrm{,}st}\notin {\Re }_{\infty \mathrm{,}st}$. We choose now ${\square }_{\infty \mathrm{,}st}A\mathrm{,}i=\mathrm{1,2,}\cdots$ in the following form

${\square }_{\infty \mathrm{,}st}A\triangleq \exists i\left[Be{w}_{i\mathrm{,}st}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{i\mathrm{,}st}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\right]\mathrm{.}$ (119)

III) Let ${\Im }_{\infty \mathrm{,}Nst}$ be the set of the all sets of $M_{Nst}^{ZFC}\left[PA\right]$ provably definable in $T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$,

$\forall Y\left\{Y\in {\Im }_{\infty \mathrm{,}Nst}\leftrightarrow {\square }_{\infty \mathrm{,}Nst}\exists \Psi (\cdot )\exists \mathrm{<mo>\; !\; </mo>}X\left[\Psi \left(X\right)\wedge Y=X\right]\right\}\mathrm{.}$ (120)

and let ${\Re }_{\infty \mathrm{,}Nst}$ be the set ${\Re }_{\infty \mathrm{,}Nst}=\left\{x\in {\Im }_{\infty \mathrm{,}Nst}\mathrm{<mo>\; :\; </mo>}{\square }_{\infty \mathrm{,}Nst}\left(x\notin x\right)\right\}$ where ${\square }_{\infty \mathrm{,}Nst}A$ means “sentence A derivable in $T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ ”. Then, we have that ${\Re }_{\infty \mathrm{,}Nst}\in {\Re }_{\infty \mathrm{,}Nst}$ iff ${\square }_{\infty \mathrm{,}Nst}\left({\Re }_{\infty \mathrm{,}Nst}\notin {\Re }_{\infty \mathrm{,}Nst}\right)$, which immediately gives us ${\Re }_{\infty \mathrm{,}Nst}\in {\Re }_{\infty \mathrm{,}Nst}$ iff ${\Re }_{\infty \mathrm{,}Nst}\notin {\Re }_{\infty \mathrm{,}Nst}$. We choose now ${\square }_{\infty \mathrm{,}Nst}A\mathrm{,}i=\mathrm{1,2,}\cdots$ in the following form

${\square }_{\infty \mathrm{,}Nst}A\triangleq \exists i\left[Be{w}_{i\mathrm{,}Nst}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{i\mathrm{,}Nst}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\right]\mathrm{.}$ (121)

Remark 3.5.6. Notice that definitions (117), (119) and (121) hold as definitions of a predicate really asserting provability in $T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ and $T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ correspondingly.

Remark 3.5.7. Of course all the theories $T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}\mathrm{,}T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ and $T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ are inconsistent, see subsection 4.1.

Remark 3.5.8. Notice that under naive consideration the set ${\Im }_{\infty }$ and ${\Re }_{\infty }$ can be defined directly using a truth predicate, which of course is not available in the language of $ZF{C}_2^{Hs}$ (but iff $ZF{C}_2^{Hs}$ is consistent) by well-known Tarski’s undefinability theorem [10] .

Theorem 3.5.1. Tarski’s undefinability theorem: I) Let $T{h}_L$ be first order theory with formal language $L$, which includes negation and has a Gödel numbering $g(\circ )$ such that for every $L$ -formula $A\left(x\right)$ there is a formula B such that $B\leftrightarrow A\left(g\left(B\right)\right)$ holds. Assume that $T{h}_L$ has a standard model $M_{st}^{T{h}_L}$ and $Con\left(T{h}_{L\mathrm{,}st}\right)$ where

$T{h}_{L\mathrm{,}st}\triangleq T{h}_L+\exists M_{st}^{T{h}_L}\mathrm{.}$ (122)

Let $T^{\ast }$ be the set of Gödel numbers of $L$ -sentences true in $M_{st}^{T{h}_L}$. Then there is no $L$ -formula $True\left(n\right)$ (truth predicate) which defines $T^{\ast }$. That is, there is no $L$ -formula $True\left(n\right)$ such that for every $L$ -formula A,

$True\left(g\left(A\right)\right)\iff A$ (123)

holds.

II) Let $T{h}^{Hs}$ be second order theory with Henkin semantics and formal language $L$, which includes negation and has a Gödel numbering $g(\circ )$ such that for every $L$ -formula $A\left(x\right)$ there is a formula B such that $B\leftrightarrow A\left(g\left(B\right)\right)$ holds.

Assume that $T{h}^{Hs}$ has a standard model $M_{st}^{T{h}_L^{Hs}}$ and $Con\left(T{h}_{L\mathrm{,}st}^{Hs}\right)$, where

$T{h}_{\mathrm{,}st}^{Hs}\triangleq T{h}^{Hs}+\exists M_{st}^{T{h}_L^{Hs}}$ (124)

Let $T^{\ast }$ be the set of Gödel numbers of the all $L$ -sentences true in M. Then there is no $L$ -formula $True\left(n\right)$ (truth predicate) which defines $T^{\ast }$. That is, there is no $L$ -formula $True\left(n\right)$ such that for every $L$ -formula A,

$True\left(g\left(A\right)\right)\iff A$ (125)

holds.

Remark 3.5.9. Notice that the proof of Tarski’s undefinability theorem in this form is again by simple reductio ad absurdum. Suppose that an $L$ -formula True(n) defines $T^{\ast }$. In particular, if A is a sentence of $T{h}_L$ then $True\left(g\left(A\right)\right)$ holds in $\mathbb{N}$ iff A is true in $M_{st}^{T{h}_L}$. Hence for all A, the Tarski T-sentence $True\left(g\left(A\right)\right)\iff A$ is true in $M_{st}^{T{h}_L}$. But the diagonal lemma yields a counterexample to this equivalence, by giving a “Liar” sentence S such that $S\iff \neg True\left(g\left(S\right)\right)$ holds in $M_{st}^{T{h}_L}$. Thus no $L$ -formula $True\left(n\right)$ can define $T^{\ast }$.

Remark 3.5.10. Notice that the formal machinery of this proof is wholly elementary except for the diagonalization that the diagonal lemma requires. The proof of the diagonal lemma is likewise surprisingly simple; for example, it does not invoke recursive functions in any way. The proof does assume that every $L$ -formula has a Gödel number, but the specifics of a coding method are not required.

Remark 3.5.11. The undefinability theorem does not prevent truth in one consistent theory from being defined in a stronger theory. For example, the set of (codes for) formulas of first-order Peano arithmetic that are true in $\mathbb{N}$ is definable by a formula in second order arithmetic. Similarly, the set of true formulas of the standard model of second order arithmetic (or n-th order arithmetic for any n) can be defined by a formula in first-order ZFC.

Remark1.3.5.12. Notice that Tarski’s undefinability theorem cannot blocking the biconditionals

$\begin{array}{l}{\Re }_i\in {\Re }_i\iff {\Re }_i\notin {\Re }_i\mathrm{,}i\in \mathbb{N}\mathrm{,}\\ {\Re }_{\infty }\in {\Re }_{\infty }\iff {\Re }_{\infty }\notin {\Re }_{\infty }\mathrm{,}\text{etc}\text{.,}\end{array}$ (126)

see Remark 3.5.14 below.

Remark 3.5.13. I) We define again the set ${\Im }_{\infty }$ but now by using generalized truth predicate $Tru{e}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}\left(g\left(A\right)\mathrm{,}A\right)$ such that

$\begin{array}{l}Tru{e}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}\left(g\left(A\right)\mathrm{,}A\right)\iff \exists i\left[Be{w}_i\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_i\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\right]\iff \\ Tru{e}_{\infty }\left(g\left(A\right)\right)\wedge \left[Tru{e}_{\infty }\left(g\left(A\right)\right)\Rightarrow A\right]\iff A\mathrm{,}\\ Tru{e}_{\infty }\left(g\left(A\right)\right)\iff \exists iBe{w}_i\left(\mathrm{<mo>\; \#\; </mo>}A\right)\mathrm{.}\end{array}$ (127)

holds.

II) We define the set ${\Im }_{\infty \mathrm{,}st}$ using generalized truth predicate $Tru{e}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}\left(g\left(A\right)\mathrm{,}A\right)$ such that

$\begin{array}{l}Tru{e}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}\left(g\left(A\right)\mathrm{,}A\right)\iff \exists i\left[Be{w}_{i\mathrm{,}st}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{i\mathrm{,}st}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\right]\iff \\ Tru{e}_{\infty \mathrm{,}st}\left(g\left(A\right)\right)\wedge \left[Tru{e}_{\infty \mathrm{,}st}\left(g\left(A\right)\right)\Rightarrow A\right]\iff A\mathrm{,}\\ Tru{e}_{\infty \mathrm{,}st}\left(g\left(A\right)\right)\iff \exists iBe{w}_{i\mathrm{,}st}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\end{array}$ (128)

holds. Thus in contrast with naive definition of the sets ${\Im }_{\infty }$ and ${\Re }_{\infty }$ there is no any problem which arises from Tarski’s undefinability theorem.

III) We define a set ${\Im }_{\infty \mathrm{,}Nst}$ using generalized truth predicate $Tru{e}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}\left(g\left(A\right)\mathrm{,}A\right)$ such that

$\begin{array}{l}Tru{e}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}\left(g\left(A\right)\mathrm{,}A\right)\iff \exists i\left[Be{w}_{i\mathrm{,}Nst}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\wedge \left[Be{w}_{i\mathrm{,}Nst}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\Rightarrow A\right]\right]\iff \\ Tru{e}_{\infty \mathrm{,}Nst}\left(g\left(A\right)\right)\wedge \left[Tru{e}_{\infty \mathrm{,}Nst}\left(g\left(A\right)\right)\Rightarrow A\right]\iff A\mathrm{,}\\ Tru{e}_{\infty \mathrm{,}Nst}\left(g\left(A\right)\right)\iff \exists iBe{w}_{i\mathrm{,}Nst}\left(\mathrm{<mo>\; \#\; </mo>}A\right)\mathrm{.}\end{array}$ (129)

holds. Thus in contrast with naive definition of the sets ${\Im }_{\infty \mathrm{,}Nst}$ and ${\Re }_{\infty \mathrm{,}Nst}$ there is no any problem which arises from Tarski’s undefinability theorem.

Remark 3.5.14. In order to prove that set theory $ZF{C}_2^{Hs}+\exists M^{ZF{C}_2^{Hs}}$ is inconsistent without any reference to the set ${\Im }_{\infty }$, notice that by the properties of the extension $T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}$ it follows that definition given by formula (127) is correct, i.e., for every $ZF{C}_2^{Hs}$ -formula $\Phi$ such that $M^{ZF{C}_2^{Hs}}\models \Phi$ the following equivalence $\Phi \iff Tru{e}_{\infty }\left(g\left(\Phi \right)\mathrm{,}\Phi \right)$ holds.

Theorem 3.5.2. (Generalized Tarski’s undefinability theorem) (see subsection 4.2, Proposition 4.2.1). Let $T{h}_L$ be a first order theory or the second order theory with Henkin semantics and with formal language $L$, which includes negation and has a Gödel encoding $g(\cdot )$ such that for every $L$ -formula $A\left(x\right)$ there is a formula B such that the equivalence $B\iff A\left(g\left(B\right)\right)$ holds. Assume that $T{h}_L$ has a standard Model $M_{st}^{Th}$. Then there is no $L$ -formula $True\left(n\right)\mathrm{,}n\in \mathbb{N}$, such that for every $L$ -formula A such that $M\models A$, the following equivalence holds

$A\iff True\left(g\left(A\right)\mathrm{,}A\right)\mathrm{.}$ (130)

Theorem 3.5.3. i) Set theory $T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}=ZF{C}_2^{Hs}+\exists M^{ZF{C}_2^{Hs}}$ is inconsistent;

ii) Set theory $T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}=ZFC+\exists M_{st}^{ZFC}$ is inconsistent; iii) Set theory $T{h}_{\mathrm{1,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}=ZFC+\exists M_{Nst}^{ZFC}$ is inconsistent; (see subsection 4.2, Proposition 4.2.2).

Proof. i) Notice that by the properties of the extension $T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}$ of the theory $ZF{C}_2^{Hs}+\exists M^{ZF{C}_2^{Hs}}=T{h}_1^{\mathrm{<mo>\; \#\; </mo>}}$ it follows that

$M^{ZF{C}_2^{Hs}}\models \Phi \Rightarrow T{h}_{\infty }^{\mathrm{<mo>\; \#\; </mo>}}⊢\Phi \mathrm{.}$ (131)

Therefore formula (127) gives generalized “truth predicate” for the set theory $T{h}_1^{\#}$. By Theorem 3.5.2 one obtains a contradiction.

ii) Notice that by the properties of the extension $T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ of the theory $ZFC+\exists M_{st}^{ZFC}=T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ it follows that

$M_{st}^{ZFC}\models \Phi \Rightarrow T{h}_{\infty \mathrm{,}st}^{\mathrm{<mo>\; \#\; </mo>}}⊢\Phi \mathrm{.}$ (132)

Therefore formula (128) gives generalized “truth predicate” for the set theory $T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}$. By Theorem 3.5.2 one obtains a contradiction.

iii) Notice that by the properties of the extension $T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$ of the theory $ZFC+\exists M_{Nst}^{ZFC}=T{h}_{\mathrm{1,}st}^{\mathrm{<mo>\; \#\; </mo>}}$ it follows that

$M_{Nst}^{ZFC}\models \Phi \Rightarrow T{h}_{\infty \mathrm{,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}⊢\Phi \mathrm{.}$ (133)

Therefore (129) gives generalized “truth predicate” for the set theory $T{h}_{\mathrm{1,}Nst}^{\mathrm{<mo>\; \#\; </mo>}}$. By Theorem 3.5.2 one obtains a contradiction.

3.6. Avoiding the Contradictions from Set Theory $\overline{ZFC}{}_2^{Hs}$, $ZF{C}_{st}$ and Set Theory $ZF{C}_{Nst}$ Using Quinean Approach

In order to avoid difficulties mentioned above we use well known Quinean approach [19] .

3.6.1. Quinean Set Theory NF

Remind that the primitive predicates of Russellian unramified typed set theory (TST), a streamlined version of the theory of types, are equality = and membership $\in$. TST has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed. For each (meta-) natural number n, type $n+1$ objects are sets of type n objects; sets of type n have members of type $n-1$. Objects connected by identity must have the same type. The following two atomic formulas succinctly describe the typing rules: $x^n=y^n$ and $x^n\in y^{n+1}$.

The axioms of TST are:

Extensionality: sets of the same (positive) type with the same members are equal;

Axiom schema of comprehension:

If $\Phi \left(x^n\right)$ is a formula, then the set ${\left\{x^n|\Phi \left(x^n\right)\right\}}^{n+1}$ exists i.e., given any formula $\Phi \left(x^n\right)$, the formula

$\exists A^{n+1}\forall x^n\left[x^n\in A^{n+1}\leftrightarrow \Phi \left(x^n\right)\right]$ (134)

is an axiom where $A^{n+1}$ represents the set ${\left\{x^n|\Phi \left(x^n\right)\right\}}^{n+1}$ and is not free in $\Phi \left(x^n\right)$.

Quinean set theory. (New Foundations) seeks to eliminate the need for such superscripts.

New Foundations has a universal set, so it is a non-well founded set theory. That is to say, it is a logical theory that allows infinite descending chains of membership such as $x_n\in x_{n-1}\in \cdots \in x_3\in x_2\in x_1$. It avoids Russell’s paradox by only allowing stratifiable formulas in the axiom of comprehension. For instance $x\in y$ is a stratifiable formula, but $x\in x$ is not (for details of how this works see below).

Definition 3.6.1. In New Foundations (NF) and related set theories, a formula $\Phi$ in the language of first-order logic with equality and membership is said to be stratified iff there is a function 3c3 which sends each variable appearing in $\Phi$ [considered as an item of syntax] to a natural number (this works equally well if all integers are used) in such a way that any atomic formula $x\in y$ appearing in $\Phi$ satisfies $\sigma \left(x\right)+1=\sigma \left(y\right)$ and any atomic formula $x=y$ appearing in $\Phi$ satisfies $\sigma \left(x\right)=\sigma \left(y\right)$.

Quinean Set Theory NF

Axioms and stratification are:

The well-formed formulas of New Foundations (NF) are the same as the well-formed formulas of TST, but with the type annotations erased. The axioms of NF are [19] .

Extensionality: Two objects with the same elements are the same object.

A comprehension schema: All instances of TST Comprehension but with type indices dropped (and without introducing new identifications between variables).

By convention, NF’s Comprehension schema is stated using the concept of stratified formula and making no direct reference to types. Comprehension then becomes.

Stratified Axiom schema of comprehension:

$\left\{x|{\Phi }^s\right\}$ exists for each stratified formula ${\Phi }^s$.

Even the indirect reference to types implicit in the notion of stratification can be eliminated. Theodore Hailperin showed in 1944 that Comprehension is equivalent to a finite conjunction of its instances, so that NF can be finitely axiomatized without any reference to the notion of type [20] . Comprehension may seem to run afoul of problems similar to those in naive set theory, but this is not the case. For example, the existence of the impossible Russell class $\left\{x|x\notin x\right\}$ is not an axiom of NF, because $x\notin x$ cannot be stratified.

3.6.2. SET Theory $\overline{ZFC}{}_2^{Hs}$, $ZF{C}_{st}$ and Set Theory $ZF{C}_{Nst}$ with Stratified Axiom Schema of Replacement

The stratified axiom schema of replacement asserts that the image of a set under any function definable by stratified formula of the theory $ZF{C}_{st}$ will also fall inside a set.

Stratified Axiom schema of replacement:

Let ${\Phi }^s\left(x\mathrm{,}y\mathrm{,}{w}_1\mathrm{,}{w}_2\mathrm{,}\cdots \mathrm{,}{w}_n\right)$ be any stratified formula in the language of $ZF{C}_{st}$ whose free variables are among $x\mathrm{,}y\mathrm{,}A\mathrm{,}{w}_1\mathrm{,}{w}_2\mathrm{,}\cdots \mathrm{,}{w}_n$, so that in particular B is not free in ${\Phi }^s$. Then

$\begin{array}{l}\forall A\forall w_1\forall w_2\cdots \forall w_n[\forall x\left(x\in A\Rightarrow \exists \mathrm{<mo>\; !\; </mo>}y{\Phi }^s\left(x\mathrm{,}y\mathrm{,}{w}_1\mathrm{,}{w}_2\mathrm{,}\cdots \mathrm{,}{w}_n\right)\right)\\ \Rightarrow \exists B\forall x\left(x\in A\Rightarrow \exists y\left(y\in B\wedge {\Phi }^s\left(x\mathrm{,}y\mathrm{,}{w}_1\mathrm{,}{w}_2\mathrm{,}\cdots \mathrm{,}{w}_n\right)\right)\right)]\mathrm{,}\end{array}$ (135)

i.e., if the relation ${\Phi }^s\left(x\mathrm{,}y\mathrm{,}\cdots \right)$ represents a definable function f, A represents its domain, and $f\left(x\right)$ is a set for every $x\in A$, then the range of f is a subset of some set B.

Stratified Axiom schema of separation:

Let ${\Phi }^s\left(x\mathrm{,}{w}_1\mathrm{,}{w}_2\mathrm{,}\cdots \mathrm{,}{w}_n\right)$ be any stratified formula in the language of $ZF{C}_{st}$ whose free variables are among $x\mathrm{,}A\mathrm{,}{w}_1\mathrm{,}{w}_2\mathrm{,}\cdots \mathrm{,}{w}_n$, so that in particular B is not free in ${\Phi }^s$. Then

$\forall w_1\forall w_2\cdots \forall w_n\forall A\exists B\forall x\left[x\in B\iff \left(x\in A\wedge {\Phi }^s\left(x\mathrm{,}{w}_1\mathrm{,}{w}_2\mathrm{,}\cdots \mathrm{,}{w}_n\right)\right)\right]\mathrm{,}$ (136)

Remark 3.6.1. Notice that the stratified axiom schema of separation follows from the stratified axiom schema of replacement together with the axiom of empty set.

Remark 3.6.2. Notice that the stratified axiom schema of replacement (separation) obviously violated any contradictions (82), (126), etc. mentioned above. The existence of the countable Russell sets ${\Re }_2^{\ast Hs}\mathrm{,}{\Re }_{st}^{\ast }$ and ${\Re }_{Nst}^{\ast }$ is impossible, because $x\notin x$ cannot be stratified.

4. Generalized Löbs Theorem

4.1. Generalized Löbs Theorem. Second-Order Theories with Henkin Semantics

Remark 4.1.1. In this section we use second-order arithmetic $Z_2^{Hs}$ with Henkin semantics. Notice that any standard model $M_{st}^{Z_2^{Hs}}$ of second-order arithmetic $Z_2^{Hs}$ consisting of a set $\mathbb{N}$ of unusual natural numbers (which forms the range of individual variables) together with a constant 0 (an element of $\mathbb{N}$ ), a function S from $\mathbb{N}$ to $\mathbb{N}$, two binary operations + and $\cdot$ on $\mathbb{N}$, a binary relation < on $\mathbb{N}$, and a collection $D\subseteq 2^{\mathbb{N}}$ of subsets of $\mathbb{N}$, which is the range of the set variables. Omitting D produces a model of the first order Peano arithmetic.

When $D=2^{\mathbb{N}}$ is the full power set of $\mathbb{N}$, the model $M_{st}^{Z_2}$ is called a full model. The use of full second-order semantics is equivalent to limiting the models of second-order arithmetic to the full models. In fact, the axioms of second-order arithmetic $Z_2^{fss}$ have only one full model. This follows from the fact that the axioms of Peano arithmetic with the second-order induction axiom have only one model under second-order semantics, see Section 3.

Let $Th$ be some fixed, but unspecified, consistent formal theory. For later convenience, we assume that the encoding is done in some fixed formal second order theory $S$ and that $Th$ contains $S$. We assume throughout this paper that formal second order theory $S$ has an ω-model $M_{\omega }^S$. The sense in which $S$ is contained in $Th$ is better exemplified than explained: if $S$ is a formal system of a second order arithmetic $Z_2^{Hs}$ and $Th$ is, say, $ZF{C}_2^{Hs}$, 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 $M_{\omega }^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}\mathrm{,}\bar{1}\mathrm{,}\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$ [19] . We note that if $\Phi \left(x\right)$ is a formula with 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 the function symbols, $neg(\cdot )$, $imp(\cdot )$, etc., such that for all first order formulae $\Phi \mathrm{,}\Psi \mathrm{<mo>\; :\; </mo>}S⊢neg\left({\left[\Phi \right]}^c\right)={\left[\neg \Phi \right]}^c$, $S⊢imp\left({\left[\Phi \right]}^c\mathrm{,}{\left[\Psi \right]}^c\right)={\left[\Phi \to \Psi \right]}^c$ etc. Of particular importance is the substitution operator, represented by the function symbol $sub\left(\cdot \mathrm{,}\cdot \right)$. For formulae $\Phi \left(x\right)$, terms t with codes ${\left[t\right]}^c$ :

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

It well known that one can also encode derivations and have a binary relation $Pro{v}_{Th}\left(x\mathrm{,}y\right)$ (read “x proves y” or “x is a proof of y”) such that for closed $t_1\mathrm{,}{t}_2\mathrm{<mo>\; :\; </mo>}S⊢Pro{v}_{Th}\left(t_1\mathrm{,}{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 \text{iff}S⊢Pro{v}_{Th}\left(t\mathrm{,}{\left[\Phi \right]}^c\right)$ (138)

for some closed term t. Thus we can define

$P{r}_{Th}\left(y\right)\leftrightarrow \exists xPro{v}_{Th}\left(x\mathrm{,}y\right)\mathrm{,}$ (139)

and therefore we obtain a predicate asserting provability.

Remark 4.1.2. I) We note that it is not always the case that:

$Th⊢\Phi \text{iff}S⊢P{r}_{Th}\left({\left[\Phi \right]}^c\right)\mathrm{,}$ (140)

unless $S$ is fairly sound, e.g. this is the case when $S$ and $Th$ replaced by $S_{\omega }=S\upharpoonright M_{\omega }^{Th}$ and $T{h}_{\omega }=Th\upharpoonright M_{\omega }^{Th}$ correspondingly (see Designation 4.1.1 below).

II) Notice that it is always the case that:

$T{h}_{\omega }⊢{\Phi }_{\omega }\text{iff}{S}_{\omega }⊢P{r}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right)\mathrm{,}$ (141)

i.e. that is the case when predicate $P{r}_{T{h}_{\omega }}\left(y\right)\mathrm{,}y\in M_{\omega }^{Th}$ :

$P{r}_{T{h}_{\omega }}\left(y\right)\leftrightarrow \exists x\left(x\in M_{\omega }^{Th}\right)Pro{v}_{T{h}_{\omega }}\left(x\mathrm{,}y\right)$ (142)

really asserting provability.

It well known that the above encoding can be carried out in such a way that the following important conditions $D\mathrm{1,}D2$ and $D3$ are meeting for all sentences:

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

Conditions $D\mathrm{1,}D2$ and $D3$ are called the Derivability Conditions.

Remark 4.1.3. From (141)-(142) it follows that

$\begin{array}{l}D4.T{h}_{\omega }⊢\Phi \text{iff}{S}_{\omega }⊢P{r}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right)\mathrm{,}\\ D5.S_{\omega }⊢P{r}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right)\leftrightarrow P{r}_{T{h}_{\omega }}\left({\left[P{r}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right)\right]}^c\right)\mathrm{,}\\ D6.S_{\omega }⊢P{r}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right)\wedge P{r}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\to \Psi \right]}^c\right)\to P{r}_{T{h}_{\omega }}\left({\left[{\Psi }_{\omega }\right]}^c\right)\mathrm{.}\end{array}$ (144)

Conditions $D\mathrm{4,}D5$ and $D6$ are called a Strong Derivability Conditions.

Definition 4.1.1. Let $\Phi$ be well formed formula (wff) of $Th$. Then wff $\Phi$ is called $Th$ -sentence iff it has no free variables.

Designation 4.1.1 i) Assume that a theory $Th$ has an ω-model $M_{\omega }^{Th}$ and $\Phi$

is a $Th$ -sentence, then: ${\Phi }_{M_{\omega }^{Th}}\triangleq \Phi \upharpoonright M_{\omega }^{Th}$ (we will write ${\Phi }_{\omega }$ instead ${\Phi }_{M_{\omega }^{Th}}$ )

is a $Th$ -sentence $\Phi$ with all quantifiers relativized to ω-model $M_{\omega }^{Th}$ [11] and $T{h}_{\omega }\triangleq Th\upharpoonright M_{\omega }^{Th}$ is a theory $Th$ relativized to model $M_{\omega }^{Th}$, i.e., any $T{h}_{\omega }$ -sentence has the form ${\Phi }_{\omega }$ for some $Th$ -sentence $\Phi$.

ii) Assume that a theory $Th$ has a standard model $M_{st}^{Th}$ and $\Phi$ is a $Th$ -sentence, then:

${\Phi }_{M_{st}^{Th}}\triangleq \Phi \upharpoonright M_{st}^{Th}$ (we will write ${\Phi }_{st}$ instead ${\Phi }_{M_{st}^{Th}}$ ) is a $Th$ -sentence with

all quantifiers relativized to a standard model $M_{st}^{Th}$, and $T{h}_{st}\triangleq Th\upharpoonright M_{st}^{Th}$ is a theory $Th$ relativized to model $M_{st}^{Th}$, i.e., any $T{h}_{st}$ -sentence has a form ${\Phi }_{st}$ for some $Th$ -sentence $\Phi$.

iii) Assume that a theory $Th$ has a non-standard model $M_{Nst}^{Th}$ and $\Phi$ is a $Th$ -sentence, then:

${\Phi }_{M_{Nst}^{Th}}\triangleq \Phi \upharpoonright M_{Nst}^{Th}$ (we will write ${\Phi }_{Nst}$ instead ${\Phi }_{M_{Nst}^{Th}}$ ) is a $Th$ -sentence with

all quantifiers relativized to non-standard model $M_{Nst}^{Th}$, and $T{h}_{Nst}\triangleq Th\upharpoonright M_{Nst}^{Th}$ is a theory $Th$ relativized to model $M_{Nst}^{Th}$, i.e., any $T{h}_{Nst}$ -sentence has a form ${\Phi }_{Nst}$ for some $Th$ -sentence $\Phi$.

iv) Assume that a theory $Th$ has a model $M=M^{Th}$ and $\Phi$ is a $Th$ -sentence, then: ${\Phi }_{M^{Th}}$ is a $Th$ -sentence with all quantifiers relativized to model $M^{Th}$, and $T{h}_M$ is a theory $Th$ relativized to model $M^{Th}$, i.e. any $T{h}_M$ -sentence has a form ${\Phi }_M$ for some $Th$ -sentence $\Phi$.

Designation 4.1.2. i) Assume that a theory $Th$ with a language $L$ has an ω-model $M_{\omega }^{Th}$ and there exists $Th$ -sentence $S_L$ such that: a) $S_L$ expressible by language $L$ and

b) $S_L$ asserts that $Th$ has a model $M_{\omega }^{Th}$ ; we denote such $Th$ -sentence $S_L$ by $Con\left(Th;M_{\omega }^{Th}\right)$.

ii) Assume that a theory $Th$ with a language $L$ has a non-standard model $M_{Nst}^{Th}$ and there exists $Th$ -sentence $S_L$ such that: a) $S_L$ expressible by language $L$ and

b) $S_L$ asserts that $Th$ has a non-standard model $M_{Nst}^{Th}$ ; we denote such $Th$ -sentence $S_L$ by $Con\left(Th;M_{Nst}^{Th}\right)$.

iii) Assume that a theory $Th$ with a language $L$ has an model $M^{Th}$ and there exists $Th$ -sentence $S_L$ such that: a) $S_L$ expressible by language $L$ and

b) $S_L$ asserts that $Th$ has a model $M^{Th}$ ; we denote such $Th$ -sentence $S_L$ by $Con\left(Th;M^{Th}\right)$.

Remark 4.1.4. We emphasize that: i) it is well known that there exists a ZFC-sentence $Con\left(ZFC;M^{ZFC}\right)$ [8] ,

ii) obviously there exists a $ZF{C}_2^{Hs}$ -sentence $Con\left(ZF{C}_2^{Hs};M^{ZF{C}_2^{Hs}}\right)$ and there exists a $Z_2^{Hs}$ -sentence $Con\left(Z_2^{Hs};M^{Z_2^{Hs}}\right)$.

Designation 4.1.3. Assume that $Con\left(Th;M^{Th}\right)$. Let $\widetilde{Con}\left(Th;M^{Th}\right)$ be the formula:

$\begin{array}{l}\widetilde{Con}\left(Th\mathrm{<mo>\; ;\; </mo>}{M}^{Th}\right)\triangleq \forall t_1\left(t_1\in M_{\omega }^{Th}\right)\forall {t^{\prime }}_1\left({t^{\prime }}_1\in M_{\omega }^{Th}\right)\forall t_2\left(t_2\in M_{\omega }^{Th}\right)\\ \forall {t^{\prime }}_2\left({t^{\prime }}_2\in M_{\omega }^{Th}\right)\neg \left[Pro{v}_{Th}\left(t_1\mathrm{,}{\left[\Phi \right]}^c\right)\wedge Pro{v}_{Th}\left(t_2\mathrm{,}neg\left({\left[\Phi \right]}^c\right)\right)\right],\\ \text{where}{t^{\prime }}_1={\left[\Phi \right]}^c\mathrm{,}{t^{\prime }}_2=neg\left({\left[\Phi \right]}^c\right)\\ \text{or}\widetilde{Con}\left(Th\mathrm{<mo>\; ;\; </mo>}{M}_{\omega }^{Th}\right)\triangleq \forall \Phi \forall t_1\left(t_1\in M_{\omega }^{Th}\right)\forall t_2\left(t_2\in M_{\omega }^{Th}\right)\\ \neg \left[Pro{v}_{Th}\left(t_1\mathrm{,}{\left[\Phi \right]}^c\right)\wedge Pro{v}_{Th}\left(t_2\mathrm{,}neg\left({\left[\Phi \right]}^c\right)\right)\right]\end{array}$ (145)

and where $t_1\mathrm{,}{t^{\prime }}_1\mathrm{,}{t}_2\mathrm{,}{t^{\prime }}_2$ is a closed term.

Lemma 4.1.1. I) Assume that: i) a theory $Th$ is recursively axiomatizable.

ii) $Con\left(Th;M^{Th}\right)$,

iii) $M^{Th}\models \widetilde{Con}\left(Th\mathrm{<mo>\; ;\; </mo>}{M}^{Th}\right)$ and

iv) $Th⊢P{r}_{Th}\left({\left[\Phi \right]}^c\right)$, where $\Phi$ is a closed formula.

Then $Th⊬P{r}_{Th}\left({\left[\neg \Phi \right]}^c\right)$.

II) Assume that: i) a theory $Th$ is recursively axiomatizable.

ii) $Con\left(Th;M_{\omega }^{Th}\right)$

iii) $M_{\omega }^{Th}\models \widetilde{Con}\left(Th\mathrm{<mo>\; ;\; </mo>}{M}^{Th}\right)$ and

iv) $T{h}_{\omega }⊢P{r}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right)$, where ${\Phi }_{\omega }$ is a closed formula.

Then $T{h}_{\omega }⊬P{r}_{T{h}_{\omega }}\left({\left[\neg {\Phi }_{\omega }\right]}^c\right)$.

Proof. I) Let $\widetilde{Con}{}_{Th}\left(\Phi \mathrm{<mo>\; ;\; </mo>}{M}^{Th}\right)$ be the formula:

$\begin{array}{l}\widetilde{Con}\left(\Phi \mathrm{<mo>\; ;\; </mo>}{M}^{Th}\right)\triangleq \forall t_1\left(t_1\in M^{Th}\right)\forall t_2\left(t_2\in M^{Th}\right)\\ \neg \left[Pro{v}_{Th}\left(t_1\mathrm{,}{\left[\Phi \right]}^c\right)\wedge Pro{v}_{Th}\left(t_2\mathrm{,}neg\left({\left[\Phi \right]}^c\right)\right)\right],\\ \text{i}\text{.e}\text{.}\forall t_1\left(t_1\in M^{Th}\right)\forall t_2\left(t_2\in M^{Th}\right)\\ \neg \left[Pro{v}_{Th}\left(t_1\mathrm{,}{\left[\Phi \right]}^c\right)\wedge Pro{v}_{Th}\left(t_2\mathrm{,}neg\left({\left[\Phi \right]}^c\right)\right)\right]\leftrightarrow \\ \left\{\neg \exists t_1\left(t_1\in M^{Th}\right)\neg \exists t_2\left(t_2\in M^{Th}\right)\left[Pro{v}_{Th}\left(t_1\mathrm{,}{\left[\Phi \right]}^c\right)\wedge Pro{v}_{Th}\left(t_2\mathrm{,}neg\left({\left[\Phi \right]}^c\right)\right)\right]\right\}\mathrm{.}\end{array}$ (146)

where $t_1\mathrm{,}{t}_2$ is a closed term. From (i)-(ii) it follows that theory $Th+\widetilde{Con}\left(Th\mathrm{<mo>\; ;\; </mo>}{M}^{Th}\right)$ is consistent. We note that $Th+\widetilde{Con}\left(Th\mathrm{<mo>\; ;\; </mo>}{M}^{Th}\right)⊢\widetilde{Con}{}_{Th}\left(\Phi \mathrm{<mo>\; ;\; </mo>}{M}^{Th}\right)$ for any closed $\Phi$. Suppose that $Th⊢P{r}_{Th}\left({\left[\neg \Phi \right]}^c\right)$, then (iii) gives

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

From (139) and (147) we obtain

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

But the formula (146) contradicts the formula (148). Therefore $Th⊬P{r}_{Th}\left({\left[\neg \Phi \right]}^c\right)$.

Remark 4.1.5. In additional note that under the following conditions:

i) a theory $Th$ is recursively axiomatizable,

ii) $Con\left(Th;M_{st}^{Th}\right)$, and

iii) $M_{st}^{Th}\models \widetilde{Con}\left(Th;M_{st}^{Th}\right)$ predicate $P{r}_{Th}\left({\left[\Psi \right]}^c\right)$ really asserts provability, one obtains

$Th⊢\Phi \wedge \neg \Phi$ (149)

and therefore by reductio ad absurdum again one obtains $Th⊬P{r}_{Th}\left({\left[\neg \Phi \right]}^c\right)$.

II) Let $\widetilde{Con}{}_{Th}\left(\Phi \mathrm{<mo>\; ;\; </mo>}{M}_{\omega }^{Th}\right)$ be the formula:

$\begin{array}{l}\widetilde{Con}{}_{Th}\left(\Phi \mathrm{<mo>\; ;\; </mo>}{M}_{\omega }^{Th}\right)\triangleq \forall t_1\left(t_1\in M_{\omega }^{Th}\right)\forall t_2\left(t_2\in M_{\omega }^{Th}\right)\\ \neg \left[Pro{v}_{Th}\left(t_1\mathrm{,}{\left[\Phi \right]}^c\right)\wedge Pro{v}_{Th}\left(t_2\mathrm{,}neg\left({\left[\Phi \right]}^c\right)\right)\right],\\ i.e.\forall t_1\left(t_1\in M_{\omega }^{Th}\right)\forall t_2\left(t_2\in M_{\omega }^{Th}\right)\\ \neg \left[Pro{v}_{Th}\left(t_1\mathrm{,}{\left[\Phi \right]}^c\right)\wedge Pro{v}_{Th}\left(t_2\mathrm{,}neg\left({\left[\Phi \right]}^c\right)\right)\right]\leftrightarrow \\ \left\{\neg \exists t_1\left(t_1\in M_{\omega }^{Th}\right)\neg \exists t_2\left(t_2\in M_{\omega }^{Th}\right)\left[Pro{v}_{Th}\left(t_1\mathrm{,}{\left[\Phi \right]}^c\right)\wedge Pro{v}_{Th}\left(t_2\mathrm{,}neg\left({\left[\Phi \right]}^c\right)\right)\right]\right\}\mathrm{.}\end{array}$ (150)

This case is trivial because formula $P{r}_{T{h}_{\omega }}\left({\left[\neg \Phi \right]}^c\right)$ by the Strong Derivability Condition $D4$, see formulae (144), really asserts provability of the $T{h}_{\omega }$ -sentence $\neg {\Phi }_{\omega }$. But this is a contradiction.

Lemma 4.1.2. I) Assume that: i) a theory $Th$ is recursively axiomatizable.

ii) $Con\left(Th;M^{Th}\right)$,

iii) $M^{Th}\models \widetilde{Con}\left(Th\right)$ and

iv) $Th⊢P{r}_{Th}\left({\left[\neg \Phi \right]}^c\right)$, where $\Phi$ is a closed formula. Then $Th⊬P{r}_{Th}\left({\left[\Phi \right]}^c\right)$,

II) Assume that: i) a theory $Th$ is recursively axiomatizable.

ii) $Con\left(Th;M_{\omega }^{Th}\right)$

iii) $M_{\omega }^{Th}\models \widetilde{Con}\left(Th\right)$ and

iv) $T{h}_{\omega }⊢P{r}_{T{h}_{\omega }}\left({\left[\neg {\Phi }_{\omega }\right]}^c\right)$,

where ${\Phi }_{\omega }$ is a closed formula. Then $T{h}_{\omega }⊬P{r}_{T{h}_{\omega }}\left({\left[{\Phi }_{\omega }\right]}^c\right)$.

Proof. Similarly as Lemma 4.1.1 above.

Example 4.1.1. i) Let $Th=PA$ be Peano arithmetic and $\Phi \iff 0=1$.

Assume that: i) $Con\left(PA;M^{PA}\right)$

ii) $M^{PA}\models \widetilde{Con}\left(PA;M^{PA}\right)$ where $M^{PA}$ is a model of $PA$.

Then obviously $PA⊢P{r}_{PA}\left(0\ne 1\right)$ since $PA⊢0\ne 1$ and therefore by Lemma 4.1.1 $PA⊬P{r}_{PA}\left(0=1\right)$.

ii) Let $Con\left(PA;M^{PA}\right)\mathrm{,}{M}^{PA}\models \neg \widetilde{Con}\left(PA;M^{PA}\right)$ and let $P{A}^{♣}$ be a theory $P{A}^{♣}=PA+\neg \widetilde{Con}\left(PA;M^{PA}\right)$ and $\Phi \iff 0=1$. Then obviously

$P{A}^{♣}⊢\left[P{r}_{PA}\left(0\ne 1\right)\right]\wedge \left[P{r}_{PA}\left(0=1\right)\right]\mathrm{.}$ (151)

and therefore

$P{A}^{♣}⊢P{r}_{PA}\left(0\ne 1\right)\mathrm{,}$ (152)

and

$P{A}^{♣}⊢P{r}_{PA}\left(0=1\right)\mathrm{.}$ (153)

However by Löbs theorem

$P{A}^{♣}⊬0=1.$ (154)

iii) Let $Con\left(P{A}^{♣};M^{P{A}^{♣}}\right)\mathrm{,}{M}^{P{A}^{♣}}\models \widetilde{Con}\left(P{A}^{♣};M^{P{A}^{♣}}\right)$ and $\Phi \iff 0=1$. Then obviously $P{A}^{♣}⊢P{r}_{P{A}^{♣}}\left(0\ne 1\right)$ since $P{A}^{♣}⊢0\ne 1$ and therefore by Lemma 4.1.1 we obtain. $P{A}^{♣}⊬P{r}_{P{A}^{♣}}($

Conflicts of Interest

The authors declare no conflicts of interest regarding the publication of this paper.

References

[1]	Nelson, E. (2011) Warning Signs of a Possible Collapse of Contemporary Mathematics. In: Heller, M. and Hugh Woodin, W., Ed., Infinity: New Research Frontiers, Cambridge University Press, Cambridge, 75-85. https://books.google.co.il/books?hl=en&lr=&id=PVNbIGS37wMC&oi=fnd&pg=PA76&ots=-aw1XHf3Xf&sig=fgKPoccDIFUtFYTCgz1XVaO8_hg&redir_esc=y#v=onepage&q&f=false
[2]	Foukzon, J. (2013) Generalized Lob’s Theorem. Strong Reflection Principles and Large Cardinal Axioms. Consistency Results in Topology. ArXiv: 1301.5340. https://arxiv.org/abs/1301.5340
[3]	Lemhoff, R. (2016) 2016 European Summer Meeting of the Association for Symbolic Logic. Logic COLLOQUIUM’16, Leeds, UK, July 31-August 6, 2016. The Bulletin of Symbolic Logic, 23, 213-216. https://www.jstor.org/stable/44259451?seq=1#page_scan_tab_contents
[4]	Foukzon, J. and Men’kova, E.R. (2013) Generalized Löb’s Theorem. Strong Reflection Principles and Large Cardinal Axioms. Advances in Pure Mathematics, 3, 368-373. https://doi.org/10.4236/apm.2013.33053
[5]	Foukzon, J. (2015) Inconsistent Countable Set in Second Order ZFC and Nonexistence of the Strongly Inaccessible Cardinals. British Journal of Mathematics & Computer Science, 9, 380-393. https://doi.org/10.9734/BJMCS/2015/16849 http://www.sciencedomain.org/abstract/9622
[6]	Foukzon, J. and Men’kova, E.R. (2019) There Is No Standard Model of ZFC and ZFC2. In: Advances in Mathematics and Computer Science, Volume 1, Book Publisher International. http://bp.bookpi.org/index.php/bpi/catalog/view/46/221/408-1
[7]	Henkin, L. (1950) Completeness in the Theory of Types. Journal of Symbolic Logic, 15, 81-91. https://doi.org/10.2307/2266967
[8]	Cohen, P. (1966) Set Theory and the Continuum Hypothesis. W. A. Benjamin, Inc., New York.
[9]	Gödel, K. (1968) Consistency of the Continuum Hypothesis. In: Annals of Mathematics Studies, Princeton University Press, Princeton, NJ, 69 p.
[10]	Rossberg, M. (2004) First-Order Logic, Second-Order Logic, and Completeness. In: Hendricks, V., et al., Eds., First-Order Logic Revisited, Logos-Verlag, Berlin, 303-321. http://logic.amu.edu.pl/images/4/46/Completenessrossberg.pdf
[11]	Shapiro, S. (2000) Foundations without Foundationalism: A Case for Second-Order Logic. Oxford University Press, Oxford.
[12]	Rayo, A. and Uzquiano, G. (1999) Toward a Theory of Second-Order Consequence. Notre Dame Journal of Formal Logic, 40, 315-325. https://doi.org/10.1305/ndjfl/1022615612
[13]	Vaananen, J. (2001) Second-Order Logic and Foundations of Mathematics. Bulletin of Symbolic Logic, 7, 504-520. https://doi.org/10.2307/2687796
[14]	Friedman, H. (1973) Countable Models of Set Theories. In: Mathias, A.R.D. and Rogers, H., Eds., Cambridge Summer School in Mathematical Logic. Lecture Notes in Mathematics, Springer, Berlin, Heidelberg, 539-573. https://doi.org/10.1007/BFb0066789
[15]	Magidor, M., Shelah, S. and Stavi, J. (1983) On the Standard Part of Nonstandard Models of Set Theory. The Journal of Symbolic Logic, 48, 33-38. https://doi.org/10.2307/2273317
[16]	Bovykin, A. (2000) On Order-Types of Models of Arithmetic. In: Logic and Algebra, Contemporary Mathematics Series of the AMS, Volume 302, American Mathematical Society, Providence, RI, 275-285. https://doi.org/10.1090/conm/302/05055
[17]	Mendelson, E. (1997) Introduction to Mathematical Logic. Springer, New York.
[18]	Takeuti, G. (2013) Proof Theory. 2nd Edition. Dover Publications, New York.
[19]	Quine, W.V. (1937) New Foundations for Mathematical Logic. The American Mathematical Monthly, 44, 70-80. https://doi.org/10.2307/2300564
[20]	Hailperin, T. (1944) A Set of Axioms for Logic. Journal of Symbolic Logic, 9, 1-19. https://doi.org/10.2307/2267307
[21]	Montague, R. (1965) Set Theory and Higher-Order Logic. Studies in Logic and the Foundations of Mathematics, 40, 131-148. https://doi.org/10.1016/S0049-237X(08)71686-0
[22]	Foukzon, J. (2015) Non-Archimedean Analysis on the Extended Hyperreal Line and the Solution of Some Very Old Transcendence Conjectures over the Field . Advances in Pure Mathematics, 5, 587-628. https://arxiv.org/abs/0907.0467 https://doi.org/10.4236/apm.2015.510056
[23]	Foukzon, J. (2013) An Possible Generalization of the Löb’s Theorem. AMS Sectional Meeting AMS Special Session, Spring Western Sectional Meeting University of Colorado Boulder, Boulder, CO, 13-14 April 2013. http://www.ams.org/amsmtgs/2210_abstracts/1089-03-60.pdf
[24]	Foukzon, J. (2013) Strong Reflection Principles and Large Cardinal Axioms. Fall Southeastern Sectional Meeting University of Louisville, Louisville, KY, 5-6 October 2013.