(with 
1 Introduction
Consistency statements have become an integral part of metamathematics. Intuitively speaking, a consistency statement is any statement that expresses some form of non-contradiction. Examples of statements satisfying that property are (
${\texttt {Pr}}_{\alpha }$
denotes the provability predicate for the numeration
$\alpha $
):
$\neg {\texttt {Pr}}_{\alpha }(\ulcorner \perp \urcorner )$
,
$\neg {\texttt {Pr}}_{\alpha }(\ulcorner {\texttt {Pr}}_{\alpha }(\ulcorner \cdots {\texttt {Pr}}_{\alpha }(\ulcorner \perp \urcorner )\cdots \urcorner )\urcorner )$
,
$\omega $
-consistency, and n-consistency of Kreisel. We recall that a theory T is
$\omega $
-inconsistent if there is a formula
$\varphi (x)$
such that
-
$\omega $
-inc.1: For all
$n\in \mathbb {N}$
,
$T\vdash \varphi (\overline {n})$
, and -
$\omega $
-inc.2:
$T\vdash \exists x.\neg \varphi (x)$
;
and
$\omega $
-consistent otherwise (see [Reference Boolos3] and [Reference Smorynski19, p. 851] for further details on
$\omega $
-consistency). Moreover, T is n-consistent if T is
$\omega $
-consistent for
$\Sigma _n$
-formulas; this notion was introduced by Kreisel in [Reference Kreisel13] (see, for instance, [Reference Kikuchi and Kurahashi12] and [Reference Salehi and Seraji18] for recent developments on n-consistency). Although the previous notions do not necessarily express that
$\perp $
is not derivable, they express some form of non-contradiction. In addition, slow consistency [Reference Friedman, Rathjen and Weiermann7] is another example of a statement expressing non-contradiction. All these notions, when formalized, depend on numerations
$\alpha $
of the axioms of the considered theory T in some base theory S. In a sense, they are statements of the form
$\mathcal {C}_{\alpha }:=\forall \mathcal {A}(x).\mathcal {C}_{\alpha }(x)$
that depend on
$\alpha $
(more details about this later).
Gödel’s Second Incompleteness Theorem (G2), see [Reference Hájek and Pudlák8, p. 164], states that 
, whenever
$\alpha $
includes some standard
$\Delta _0(S)$
-definition of S (the reader can find a lovely generalization of this fact in [Reference Visser23, theorem 5.1]). Clearly, any serious candidate to a consistency statement is expected to satisfy G2, i.e., 
for such an
$\alpha $
including a standard
$\Delta _0(S)$
-definition of S.
Feferman, in his groundbreaking paper [Reference Feferman6], proved, in Theorem 5.9, that, for T sufficiently strong, there is a numeration
$\tau $
of the axioms of T such that
$T\vdash {\texttt {Con}}_\tau $
.
In this paper, we aim at generalize the previously mentioned consistency statements while maintaining two important features: G2, and Feferman’s result. G2 guarantees that we are, in a sense, expressing some reasonable forms of consistency. Feferman’s result ensures the reader that we did not generalize too much, since the numerations of the considered theories still play a defining role. We take, in a sense, an axiomatic approach, since we isolate the main properties that are needed for these two results. There are important works in the literature in this direction. In [Reference Visser24], the reader can find a profound coordinate-free analysis of consistency; Visser characterizes consistoids, up to provable equivalence, using interpretations (see also [Reference Visser22] where the similar notion of a pro-consistency statement is introduced). In [Reference Visser21], the reader can find one of the first papers on the coordinate-free endeavour. It is worth mentioning that some known nonstandard notions of consistency—such as Mostowski’s, Rosser’s, and Artemov’s notions—do not satisfy G2.
As we just mentioned, there are some works on the literature in the direction we are aiming at, but our approach differs from the literature because we do not restrict our analysis to finitely axiomatizable theories, and, more importantly, since we want to explore the role played by different numerations; we want to present an analysis that does not aim at obtaining coordinate-free consistency, but rather at generalizing consistency statements that do depend on numeration; these are complementary approaches to the generalization of consistency statements. Visser in [Reference Visser23] gave an account of G2 in a similar setting to the one we desire to work with, namely the one considered by Feferman in [Reference Feferman6] where he studied in detail the role played by different numerations of the axioms, but our focus here is to extend the sort of account of [Reference Visser23] to include other consistency statements, such as
$\omega $
-consistency (the goal of [Reference Visser23] was to extend the approach of [Reference Feferman6] to allow the interpretation of number theory not to be fixed).
We also need to exclude in our analysis pathological cases, such as Rosser’s consistency: Rosser’s provability predicate is given by
where
${\texttt {Prf}}_{\alpha }(x,y)$
expresses that “y is a proof of x for the numeration
$\alpha $
”, and 
represents negation. We know that
$S\vdash \neg {\texttt {Pr}}_{\alpha }^R(\ulcorner \perp \urcorner )$
. This happens because, in fact,
$\neg {\texttt {Pr}}_{\alpha }^R(\ulcorner \perp \urcorner )$
is not expressing a standard form of consistency, on the contrary it only expresses that “if one is given a proof y of
$\perp $
, then one can find a smaller proof z of
$\top $
”, as the reader can seeFootnote
1
, no actual form of non-contradiction.
To convince the reader that our notions are natural ones, we create a notion of provability that arises from a given general notion of consistency and we study conditions on the general notion of consistency that entail derivability conditions on the notion of provability: the aim is not to obtain new results on provability predicates, but rather to show how transversal our analysis is. Moreover, we introduce the concept of a notion of interpretability. We end our paper by account for compatibility of theories in our general framework. These three examples—namely of provability, interpretability, and compatibility—confirm that our analysis is general enough to capture the usual properties of these domains.
The epistemological structure of the paper. We follow a quasi-empirical approach to consistency. Firstly, we develop a candidate notion of general consistency statement that we recognize to express a form on non-contradiction. Then, we confirm that the set of sufficiently distinct consistency statements we are considering is a particular case of that notion. From that fact, we establish our two goals for the notion we developed: G2 and Feferman’s result. Lastly, we account for slow consistency and we develop a notion of provability and a notion of interpretability for each general notion of consistency.
This approach is quasi-empirical in the sense that we start from a set of sufficiently diverse consistency statements and we try to generalize them, by confirming that they fit our definition: this is the empirical part, we have no proof that our definition accounts for any sentences we recognize as expressing consistency; on the contrary, we isolate important properties and work using only those properties we isolated, very much in a scientific (axiomatic) fashionFootnote 2 .
It is important to emphasize that, rather than working all the way with a fixed theory T, we assume a weak sub-theory S and we parametrize our results for these two theories. Some results, like Theorem 2, impose extra-conditions on the theories and on the interplay with the numerations; this extra-complexity is, for the most part, only apparent and a consequence of the splitting of the theories S and T, for the case
$S=T$
the conditions of the results are satisfied much more easily.
2 Preliminaries
Throughout this paper, S and T stand for consistentFootnote
3
theories that include
$\mathsf {EA}$
(this theory is
$\mathsf {I}\Delta _0+\mathsf {exp}$
, where
$\mathsf {exp}$
denotes the totality of exponentiation; see [Reference Beklemishev1] for details on this theory); we assume
$S\subseteq T$
, S is a potentially weak theory, and T a potentially strong theory (for example
${\mathsf {PA}}\subseteq T$
); we assume that S has a modicum of arithmetic required to state our results, we emphasize the requirements as we go: usually, the modicum is simply
$\mathsf {EA}$
extended by a function-symbol for each definable function in
$\mathsf {EA}$
. Whenever we consider a consistency statement in T, we assume it to be tacitly true for that theory; for example, when we study
$\omega $
-consistency, we assume that T is
$\omega $
-consistent. In the last section, we consider theories denoted by
$T_0$
and
$T_1$
that are also theories that extend
$\mathsf {EA}$
, but we do not necessarily wish that one of them is potentially weaker than the other; in this sense, they should be though as theories that do not need to coincide with either S or T. We obviously assume that all these theories share the same basis language. In our framework, whenever we speak about a theory we are in fact speaking about its set of axioms; in this sense, we might have two apparently different theories
$T_0$
and
$T_1$
(they are sets of axioms), but that have the same set of theorems.
As usual, we are considering the usual metamathematical notions, in particular we use
$\overline {n}$
to denote the (efficient [Reference Buss4, p. 29]) numeral of n; we also use
$\#\varphi $
to denote the code of a formula, and
$\ulcorner \varphi \urcorner $
to denote its numeral.
$\vec {Q}$
denotes an arbitrary array of quantifiers,
$\vec {x}$
an array of variables. For an array of quantifiers
$\vec {Q}:=Q_0\cdots Q_n$
and an array of variables
$\vec {x}:=x_0\cdots x_n$
, clearly
$\vec {Q}\vec {x}$
represents
$Q_0x_0.\cdots Q_nx_n$
.
Definition 1.
${\texttt {Formula}}(x)$
stands for a formula in S that identifies all formulas, scilicet such that
$S\vdash {\texttt {Formula}}(\overline {n})$
if, and only if, n is the code of a formula. Similarly,
$\mathsf {\Sigma }_n(x)$
is a formula that identifies all the one free variable
$\Sigma _n$
-formulas in S (see [Reference Hájek and Pudlák8, pp. 13–18, 62] for a definition of these classes), and
${\texttt {Sent}}(x)$
all sentences. We also consider that
$n{\texttt {-var}}(x)$
defines all formulas with exactly n free variables. As usual,
$\forall \Phi (x).\varphi (x)$
abbreviates
$\forall x. \Phi (x)\rightarrow \varphi (x)$
. In addition,
$\langle x_0,\ldots ,x_k\rangle $
denotes a sequence function such that
$S\vdash {(\langle x_0,\ldots ,x_k\rangle )}_i=x_i$
. We assume that S has function-symbols
${\texttt {sub}}$
and
$\texttt {numeral}$
such that:
$$ \begin{align*} &S\vdash {\texttt{sub}}(\ulcorner\varphi(x)\urcorner,\ulcorner t\urcorner)=\ulcorner\varphi(t)\urcorner; &S\vdash \texttt{numeral}(\overline{n})=\ulcorner\overline{n}\urcorner. \end{align*} $$
Feferman’s dot notation (see [Reference Smorynski19, p. 837] and [Reference Buss4, p. 135]) is defined in the following way: 
. We consider function-symbols 
, 
, 
, 
, 
, and 
in S satisfying:
We consider the previous definitions also for arrays of variables, namely 
and 
. In fact, for an array of variables
$T\vdash {\texttt {sub}}(\ulcorner \varphi (\vec {x})\urcorner ,\ulcorner \vec {t}\urcorner )=\ulcorner \varphi (\vec {t})\urcorner $
, where
$\ulcorner \vec {t}\urcorner :=\langle \ulcorner t_0\urcorner ,\ldots , \ulcorner t_n\urcorner \rangle $
. Likewise, we also define
${\texttt {s}}(y,\vec {x})={\texttt {s}}(y,x_0\cdots x_n):={\texttt {sub}}(y,\langle \texttt {numeral}(x_0),\ldots ,\texttt {numeral}(x_n)\rangle )$
(we are going to assume that
$x_0\cdots x_n$
is the order of occurrences of the variables in y). If
$\varphi $
is a sentence, we stipulate
$T\vdash {\texttt {sub}}(\ulcorner \varphi \urcorner ,\ulcorner x_0\urcorner )=\ulcorner \varphi \urcorner $
; if
$\varphi $
has more variables than the length n of a given array
$\vec {t}$
, we define that
${\texttt {sub}}$
applies to the first n variables of
$\varphi $
the array
$\vec {t}$
.
Definition 2. We say that
$\alpha $
numerates T (in S), or that
$\alpha $
is a numeration of T, if the set
$\{\varphi |S\vdash \alpha (\ulcorner \varphi \urcorner )\}$
coincides with the set of the codes of the axioms of T. If
$\alpha $
and
$\beta $
are numerations of T, we say that
$\alpha $
includes
$\beta $
if
$S\vdash \beta \rightarrow \alpha $
. Throughout the rest of the paper,
$\xi $
stands for a fixed
$\Delta _0(S)$
-numeration of the axioms of S. Given a numeration
$\alpha $
of T, we define
$(\alpha \upharpoonright x)(v):=\alpha (v)\land v\leq x$
and
$(\alpha +x)(v):=\alpha (v)\lor v=x$
. Moreover, we define
$S\upharpoonright \ell $
to be the theory numerated by
$\xi \upharpoonright \overline {\ell }$
.
Definition 3. Given a numeration
$\alpha $
of T, we consider the standard proof predicate for
$\alpha $
,
${\texttt {Prf}}_{\alpha }(x,y)$
that expresses “y is a proof of x using axioms numerated by
$\alpha $
”, as defined by Feferman in [Reference Feferman6] and we define the standard provability predicate for
$\alpha $
by
${\texttt {Pr}}_{\alpha }(x):=\exists y.{\texttt {Prf}}_{\alpha }(x,y)$
. Moreover,
${\texttt {Proof}}_{\alpha }(x)$
expresses “x is a proof with axioms in
$\alpha $
” (see [Reference Feferman6]). As usual,
${\texttt {Con}}_{\alpha }:=\neg {\texttt {Pr}}_{\alpha }(\ulcorner \perp \urcorner )$
. Clearly,
$S\vdash {\texttt {Prf}}_{\alpha }(x,y)\rightarrow {\texttt {Proof}}_{\alpha }(y)$
.
We now present some of the derivability conditions satisfied by
${\texttt {Pr}}_{\alpha }$
, for more details we recommend: [Reference Buss4, pp. 133–149], [Reference Buss5, pp. 117, 118], [Reference Feferman6], [Reference Lindström16, p. 14], [Reference Kurahashi14], [Reference Henk and Visser9], and [Reference Kurahashi15].
Fact 1. The following conditions hold when
$\alpha $
includes
$\xi $
and numerates T:
-
C1. If
$T\vdash \varphi (\vec {x})$
, then ; -
C2.
; -
C3. For all
${\Sigma _1}(S)$
-formulas
$\varphi (\vec {x})$
, ; -
C4.
$S \vdash \alpha (x)\rightarrow {\texttt {Pr}}_{\alpha }(x)$
; -
C5.
$S\vdash (\forall x. \alpha (x)\rightarrow \tau (x))\rightarrow (\forall x.{\texttt {Pr}}_{\alpha }(x)\rightarrow {\texttt {Pr}}_\tau (x))$
; -
C6.
; -
C7.
; -
C8.
.
;
;
;
;
;
. From G2, as
$\xi $
is
$\Delta _0(S)$
, we know 
, whenever
$\alpha $
includes
$\xi $
(see, for instance, [Reference Hájek and Pudlák8, p. 164] for further details). We now present several definitions of consistency statements.
Definition 4. We define:
In the previous definition,
$\omega \text {-}{\texttt {Con}}_{\alpha }$
and
$\omega \text {-}{\texttt {Con}}^\alpha $
stand for formalizations of
$\omega $
-consistency (the latter being a new form of
$\omega $
-consistency that relates numeral instances of the weak theory with existential formulas of the stronger);
$n\text {-}{\texttt {Con}}_{\alpha }$
represents n-consistency;
${\texttt {Con}}^{1;n}_{\alpha }$
and
${\texttt {Con}}^{n}_{\alpha }$
represent iterated consistency statements; and
${\texttt {RfC}}^n_{\alpha }$
denotes a consistency statement related to reflection principles, namely that they are not provably refutable (see [Reference Beklemishev2] for an overview of reflection principles).
3 General notion of consistency
Definition 5. We say that
$\mathcal {C}_{\alpha }:=\forall \mathcal {A}(x).\mathcal {C}_{\alpha }(x)$
, that is parametrized by numerations
$\alpha $
(for each
$\alpha $
we have such a formula, the
$\alpha $
occurs in
$\mathcal {C}_{\alpha }$
, just like it does in
${\texttt {Pr}}_{\alpha }$
and
${\texttt {Con}}_{\alpha }$
), is a general notion of consistency if there are terms
${\texttt {f}}$
and
${\texttt {h}}$
of S and a false sentence
$\mathcal {F}$
satisfying
$S\vdash \forall {\texttt {Proof}}_\xi (x).{\texttt {f}}({\texttt {h}}(x))=x$
,
$S\vdash \forall {\texttt {Proof}}_\xi (x). \mathcal {A}({\texttt {h}}(x))$
, and
$$ \begin{align} S\vdash \mathcal{C}_{\alpha}(x)\rightarrow\neg{\texttt{Prf}}_\xi(\ulcorner\mathcal{F}\urcorner,{\texttt{f}}(x)), \end{align} $$
whenever
$\alpha $
includes
$\xi $
. Moreover, they need to satisfy:
-
(i) For allFootnote 4 , Footnote 5
$\alpha $
and
$\beta $
,
$S\vdash (\mathcal {C}_{\alpha }\land. \alpha \leftrightarrow \beta )\rightarrow \mathcal {C}_\beta $
; -
(ii)
$\mathbb {N}\models \mathcal {C}_\xi $
.
If
$\mathcal {C}_{\alpha }$
satisfies all conditions with possible exception of (i) we call it a flat general notion of consistency.
In an intuitive wayFootnote
6
, a sentence
$\mathcal {C}_{\alpha }:=\forall \mathcal {A}(x).\mathcal {C}_{\alpha }(x)$
is a general notion of consistency if
$\mathcal {C}_{\alpha }(x)$
S-implies
$\neg {\texttt {Prf}}_\xi (\ulcorner \mathcal {F}\urcorner ,{\texttt {f}}(x))$
, a formula expressing that the provably surjective functionFootnote
7
${\texttt {f}}$
cannot output a proof of the false sentence
$\mathcal {F}$
. It is clear that
$\mathcal {C}_{\alpha }$
expresses, in a way, a form of consistency, since it entails that the false sentence
$\mathcal {F}$
cannot be instance-wise provable using the surjective
${\texttt {f}}$
; see also Observation 3 for a comment on (GenCon).
The previous conditions are satisfied by the usual consistency statement,
${\texttt {Con}}_{\alpha }$
, as we are going to see in the next proposition. (i) expresses the fact that numerations play a defining role in the notion of consistency; and (ii) says that the notion of consistency is true for
$\xi $
. The next result shows that our notion is adequate to account for the already introduced notions of consistency.
Proposition 1. The following are general notions of consistency:
-
1.
${\texttt {Con}}_{\alpha }$
; 2.
${\texttt {Con}}^{1;n}_{\alpha }$
; 3.
$\omega \text {-}{\texttt {Con}}_{\alpha }$
; -
4.
$\omega \text {-}{\texttt {Con}}^\alpha $
; 5.
$n\text {-}{\texttt {Con}}_{\alpha }$
; 6.
${\texttt {RfC}}^n_{\alpha }$
.
Moreover,
${\texttt {Con}}^n_{\alpha }$
is a flat general notion of consistencyFootnote
8
.
Proof.
-
1. Follows from the following fact by considering
$\mathcal {A}(x):=(x=x)$
,
$\mathcal {F}:=\perp $
, and
${\texttt {f}}:={\texttt {h}}:={\texttt {id}}$
(a term denoting the identity function): if
$\alpha $
includes
$\xi $
, then
$$ \begin{align*} S\vdash {\texttt{Prf}}_\xi(\ulcorner\mathcal{F}\urcorner,{\texttt{f}}(x))&\rightarrow {\texttt{Prf}}_\xi(\ulcorner\perp\urcorner,x)\\ &\rightarrow {\texttt{Prf}}_{\alpha}(\ulcorner\perp\urcorner,x). \end{align*} $$
-
2. For
$n\geq 2$
(we obtain the result for n from the result for
$n-1$
), follows from the following fact by considering
$\mathcal {F}:=\neg {\texttt {Con}}^{n-1}_\xi $
, and
${\texttt {f}}:={\texttt {h}}:={\texttt {id}}$
: if
$\alpha $
includes
$\xi $
, then
$$ \begin{align*} S\vdash {\texttt{Prf}}_\xi(\ulcorner\mathcal{F}\urcorner,{\texttt{f}}(x))&\rightarrow {\texttt{Prf}}_\xi(\ulcorner\neg {\texttt{Con}}^{n-1}_\xi\urcorner,x)\\ &\rightarrow {\texttt{Prf}}_{\alpha}(\ulcorner\neg {\texttt{Con}}^{n-1}_\xi\urcorner,x). \end{align*} $$
-
3. Let
$\mathcal {A}(x):=1{\texttt {-var}}(x)$
and
$\mathcal {F}:=\perp $
. Take
$f_0:\mathbb {N}\to one\text {-}var$
and
$f_1:\mathbb {N}\to \textit{Proof}_S$
elementary bijections whose inverses are also elementary (
$one\text {-}var$
denotes the set of the codes of one free variable formulas and
$\textit{Proof}_S$
the set of the codes of S-proofs). Then, they can be represented inside S using terms
${\texttt {f}}_0$
,
${\texttt {f}}_1$
for the functions, and
${\texttt {f}}_0^{-1}$
,
${\texttt {f}}_1^{-1}$
for the inverses. MoreoverFootnote
9
, S satisfies:
$S\vdash {\texttt {f}}_0^{-1}({\texttt {f}}_0(x))=x$
and
$S\vdash {\texttt {f}}_1({\texttt {f}}_1^{-1}(x))=x$
.Define
${\texttt {f}}(x):={\texttt {f}}_1({\texttt {f}}_0^{-1}(x))$
, and
${\texttt {h}}(x):={\texttt {f}}_0({\texttt {f}}_1^{-1}(x))$
. So,
$$ \begin{align*} S\vdash \forall {\texttt{Proof}}_\xi(x). {\texttt{f}}({\texttt{h}}(x))&={\texttt{f}}_1({\texttt{f}}_0^{-1}({\texttt{f}}_0({\texttt{f}}_1^{-1}(x))))={\texttt{f}}_1({\texttt{f}}_1^{-1}(x))=x. \end{align*} $$
Moreover,
$S\vdash \forall {\texttt {Proof}}_\xi (x).1{\texttt {-var}}({\texttt {h}}(x))$
. Observe thatFootnote
10
, when
$\alpha $
includes
$\xi $
, -
4. Similar to the previous case.
-
5. Let
$\mathcal {A}(x):=\mathsf {\Sigma }_n(x)$
. Consider
${\texttt {f}}_1$
as before. Take
$f_2:\mathbb {N}\to \Sigma _n$
an elementary bijection whose inverse is also elementary. Then, it can be represented inside S using terms
${\texttt {f}}_2$
,
${\texttt {f}}_2^{-1}$
for the inverses. We can require that S satisfies:
$S\vdash {\texttt {f}}_2^{-1}({\texttt {f}}_2(x))=x$
and
$S\vdash {\texttt {f}}_1({\texttt {f}}_1^{-1}(x))=x$
.Define
${\texttt {f}}(x):={\texttt {f}}_1({\texttt {f}}_2^{-1}(x))$
, and
${\texttt {h}}(x):={\texttt {f}}_2({\texttt {f}}_1^{-1}(x))$
. So, and
$$ \begin{align*} S\vdash \forall {\texttt{Proof}}_\xi(x). {\texttt{f}}({\texttt{h}}(x))&={\texttt{f}}_1({\texttt{f}}_2^{-1}({\texttt{f}}_2({\texttt{f}}_1^{-1}(x))))={\texttt{f}}_1({\texttt{f}}_1^{-1}(x))=x, \end{align*} $$
$S\vdash \forall {\texttt {Proof}}_\xi (x). \mathcal {A}({\texttt {h}}(x))$
. The rest of the proof is similar.
-
6. Follows from the following fact, where
${\texttt {f}}$
is as in item 5: when
$\alpha $
includes
$\xi $
,
Clearly, conditions (i) and (ii) are satisfied for all the considered consistency statements.
${\texttt {Con}}^n_{\alpha }$
has a proof similar to 2 and clearly satisfies (ii).
Observation 1. Clearly, if
$\mathcal {F}$
is any false sentence, then
$\neg {\texttt {Pr}}_{\alpha }(\ulcorner \mathcal {F}\urcorner )$
is a general notion of consistency; for example,
$\neg {\texttt {Pr}}_{\alpha }(\ulcorner \neg \mathcal {G}_{\alpha }\urcorner )$
is a general notion of consistency, with
$\mathcal {G}_{\alpha }$
a Gödel-sentence for
$\alpha $
with respect to S (i.e.,
$S\vdash \mathcal {G}_{\alpha }\leftrightarrow \neg {\texttt {Pr}}_{\alpha }(\ulcorner \mathcal {G}_{\alpha }\urcorner )$
). As the reader could observe, the surjectivity of
${\texttt {f}}$
was an important feature to guarantee a total connection with the usual consistency statement.
Observation 2. Given
$\mathcal {C}_{\alpha }$
a flat general notion of consistency, if it satisfies
$S\vdash (\mathcal {C}_{\alpha }\land. {\texttt {Pr}}_{\alpha }\leftrightarrow {\texttt {Pr}}_\beta )\rightarrow \mathcal {C}_\beta $
, then it is a general notion of consistency. Here is why: using C5,
$ S\vdash (\mathcal {C}_{\alpha }\land. \alpha \leftrightarrow \beta ) \rightarrow (\mathcal {C}_{\alpha }\land. {\texttt {Pr}}_{\alpha }\leftrightarrow {\texttt {Pr}}_\beta ) \rightarrow \mathcal {C}_\beta $
.
The next result resembles G2, our first goal.
Theorem 1. If
$\mathcal {C}_{\alpha }$
is a general notion of consistency and
$\alpha $
includes
$\xi $
, then 
.
Proof. Clearly,
$S\vdash \exists \mathcal {A}(x). {\texttt {Prf}}_\xi (\ulcorner \mathcal {F}\urcorner ,{\texttt {f}}(x))\rightarrow {\texttt {Pr}}_\xi (\ulcorner \mathcal {F}\urcorner )$
. Reason inside S for the converse direction. Assume
${\texttt {Pr}}_\xi (\ulcorner \mathcal {F}\urcorner )$
, i.e.,
$\exists x.{\texttt {Prf}}_\xi (\ulcorner \mathcal {F}\urcorner ,x)$
. Take such an x and consider
$y:={\texttt {h}}(x)$
. As
${\texttt {Proof}}_\xi (x)$
, it follows that
${\texttt {f}}(y)={\texttt {f}}({\texttt {h}}(x))=x$
and
$\mathcal {A}(y)$
. So,
${\texttt {Prf}}_\xi (\ulcorner \mathcal {F}\urcorner ,{\texttt {f}}(y))$
, and thus
$\exists \mathcal {A}(y).{\texttt {Prf}}_\xi (\ulcorner \mathcal {F}\urcorner ,{\texttt {f}}(y))$
. Going outside S, we can cumulatively conclude
$$ \begin{align} S\vdash \exists \mathcal{A}(y).{\texttt{Prf}}_\xi(\ulcorner\mathcal{F}\urcorner,{\texttt{f}}(y))\leftrightarrow {\texttt{Pr}}_\xi(\ulcorner\mathcal{F}\urcorner). \end{align} $$
Assume, by way of contradiction, that
$S\vdash \mathcal {C}_{\alpha }$
. So,
$S\vdash \forall \mathcal {A}(x).\mathcal {C}_{\alpha }(x)$
, hence, using (GenCon),
$S\vdash \forall \mathcal {A}(x).\neg {\texttt {Prf}}_\xi (\ulcorner \mathcal {F}\urcorner ,{\texttt {f}}(x))$
. Consequently, we can conclude
$S\vdash \neg \exists \mathcal {A}(x).{\texttt {Prf}}_\xi (\ulcorner \mathcal {F}\urcorner ,{\texttt {f}}(x))$
. Therefore, by (I) we obtain
$S\vdash \neg {\texttt {Pr}}_\xi (\ulcorner \mathcal {F}\urcorner )$
.
As
$S\vdash \perp \rightarrow \mathcal {F}$
, it follows that
$S\vdash {\texttt {Pr}}_\xi (\ulcorner \perp \urcorner )\rightarrow {\texttt {Pr}}_\xi (\ulcorner \mathcal {F}\urcorner )$
, and thus
$S\vdash \neg {\texttt {Pr}}_\xi (\ulcorner \mathcal {F}\urcorner)\rightarrow \neg {\texttt {Pr}}_\xi (\ulcorner \perp \urcorner )$
. From what was previously concluded, we get
$S\vdash \neg {\texttt {Pr}}_\xi (\ulcorner \perp \urcorner )$
, which contradicts the fact that 
.
Observation 3. From (I), we know that
$S\vdash \mathcal {C}_{\alpha }\rightarrow \neg {\texttt {Pr}}_\xi (\ulcorner \mathcal {F}\urcorner )$
, that is
$S\vdash \forall \mathcal {A}(x).\mathcal {C}_{\alpha }(x)\rightarrow \forall {\texttt {Proof}}_\xi (y). \neg {\texttt {Prf}}_\xi (\ulcorner \perp \urcorner ,y)$
; it is important to emphasize that (GenCon) requires moreFootnote
11
than simply the latter S-implication, it asks for a more uniform condition, namely one that relates y and x, making
$y={\texttt {f}}(x)$
:
$S\vdash \mathcal {C}_{\alpha }(x)\rightarrow \neg {\texttt {Prf}}_\xi (\ulcorner \mathcal {F}\urcorner ,{\texttt {f}}(x))$
. We decided to include this statement, namely (GenCon), instead of just
$S\vdash \mathcal {C}_{\alpha }\rightarrow \neg {\texttt {Pr}}_\xi (\ulcorner \mathcal {F}\urcorner )$
, because it is more constructive, in the sense that it gives a more concrete relation between
$\mathcal {C}_{\alpha }$
and
$\neg {\texttt {Pr}}_\xi (\ulcorner \mathcal {F}\urcorner )$
—something not only philosophically desirable but also desirable in the practical use of the statements—, and since this occurs in all our considered examples of consistency statements. Moreover, (GenCon) will allow a more fine grained analysis of slow consistency, cf. (GenCon
$^{{\texttt {g}}}$
) of Definition 9.
Now we confirm that the pathological Rosser’s version of consistency is excluded from our analysis.
Corollary 1. If
$\alpha $
includes
$\xi $
and numerates T, then
$\neg {\texttt {Pr}}_{\alpha }^R(\ulcorner \perp \urcorner )$
is not a general notion of consistency.
Proof. We know that
$S\vdash \neg {\texttt {Pr}}_{\alpha }^R(\ulcorner \perp \urcorner )$
, the result follows from the previous Theorem.
Corollary 2. If
$\alpha $
includes
$\xi $
, then 
.
Proof. The result follows from Theorem 1 and from Proposition 1.
Corollary 3. If S has a modicum of arithmetic and
$\alpha $
includes
$\xi $
, then 
.
Corollary 4. Given
$n\in \mathbb {N}$
, if S has a modicum of arithmetic, and
$\alpha $
includes
$\xi $
, then 
.
The next result generalizes Feferman’s Theorem 5.9 from [Reference Feferman6], our second goal.
Theorem 2. Suppose that
$\mathcal {C}_{\alpha }$
is a general notion of consistency defined for each numerationFootnote
12
$\alpha $
of S in
$T\supseteq S$
, with
${\mathsf {PA}}\subseteq T$
, and that (here, and in Theorem 3, we assume the more general case that the basis
$\xi $
does
$\Delta _0(T)$
-numerate S in T, and not necessarily in S, but in the rest of the paper we do not make this assumption):
-
(iii)
$S\vdash \mathcal {C}_\xi \leftrightarrow \forall x.\mathcal {C}_{\xi \upharpoonright x}$
;Footnote
13
-
(iv)
$S\vdash \mathcal {C}_{\xi \upharpoonright 0}$
; -
(v) For all
$\alpha $
and
$\beta $
,
$S\vdash (\alpha \rightarrow \beta )\rightarrow (\mathcal {C}_\beta \rightarrow \mathcal {C}_{\alpha })$
; -
(vi) For each
$n\in \mathbb {N}$
,
$T\vdash \mathcal {C}_{\xi \upharpoonright \overline {n}}$
.
Then, there is a numeration
$\tau $
of S in T such that
$T\vdash \mathcal {C}_\tau $
.
The previous result needs T because S might not be strong enough to prove the needed form of reflexivity (condition (vi)); clearly, the result also holds for
$S=T$
, the common situation. Again, the previous conditions are satisfied by the
${\texttt {Con}}_{\alpha }$
. (iii) and (iv) express usual properties of
$\xi \upharpoonright x$
, namely that if we have information about
$\xi \upharpoonright x$
for each value of x, then we also have information about
$\xi $
; (v) generalizes the derivability conditionFootnote
14
C5 from Fact 1; and (vi) expresses a form of reflexivity (see [Reference Hájek and Pudlák8, p. 168] for the definition and more information on reflexivity). The extra conditions we are requiring do not constitute a problem, since they are satisfied for the consistency statements of Definition 4, as long as they are represented in such a way that they respect the uniformity role of
$\xi $
; as we mentioned, all this plays no role for the usual case when
$S=T$
, since
$S\vdash \omega \text {-}{\texttt {Con}}_\xi \leftrightarrow \omega \text {-}{\texttt {Con}}^\xi ,{\texttt {Con}}^{n}_\xi \leftrightarrow {\texttt {Con}}^{1;n}_\xi $
. The properties of consistency we used are just part of the properties Feferman considered in [Reference Feferman6]: this is due to the fact that we aim at finding the most general framework possible, and consequently some properties—although being relevant—are not strictly necessary to be considered.
Proof of Theorem 2.
Consider
$\tau (v):=\xi (v)\land \forall x\leq v.\mathcal {C}_{\xi \upharpoonright x}$
. Let us see that
$\tau $
is a numeration of S in T. If
$T\vdash \tau (\overline {n})$
, then
$T\vdash \xi (\overline {n})$
, and so n is the code of an axiom of S. Now, suppose that n is the code of an axiom of S. Then,
$T\vdash \xi (\overline {n})$
. By (vi),
$T\vdash \forall x\leq \overline {n}.\mathcal {C}_{\xi \upharpoonright x}$
. In sum,
$T\vdash \xi (\overline {n})\land \forall x\leq \overline {n}.\mathcal {C}_{\xi \upharpoonright x}$
, i.e.,
$T\vdash \tau (\overline {n})$
. All this entails that
$\tau $
is a numeration of S in T.
As T includes
${\mathsf {PA}}$
, using condition (iii) and [Reference Hájek and Pudlák8, p. 63], we get
$T\vdash \neg \mathcal {C}_\xi \rightarrow \exists z. (\neg \mathcal {C}_{\xi \upharpoonright z}\land \forall y<z. \mathcal {C}_{\xi \upharpoonright y})$
. By (iv),
$T\vdash \mathcal {C}_{\xi \upharpoonright 0}$
, and so
$$ \begin{align} T\vdash \neg \mathcal{C}_\xi \rightarrow \exists z. (\neg \mathcal{C}_{\xi \upharpoonright {\texttt{S}}(z)}\land \forall y\leq z. \mathcal{C}_{\xi \upharpoonright y}). \end{align} $$
Reason inside T and assume, by hypothesis,
$\neg \mathcal {C}_\xi $
. Then, by (I), we conclude
$\exists z. \neg \mathcal {C}_{\xi \upharpoonright {\texttt {S}}(z)}\land \forall y\leq z. \mathcal {C}_{\xi \upharpoonright y}$
. Take such a z. Clearly,
$\mathcal {C}_{\xi \upharpoonright z}$
. Let us show that
$\forall x. (\tau (x)\leftrightarrow \xi (x)\land x\leq z)$
. Consider any x. Firstly, assume
$\xi (x)\land x\leq z$
. From before,
$\forall y\leq z. \mathcal {C}_{\xi \upharpoonright y}$
, in particular, as
$x\leq z$
,
$\forall y\leq x. \mathcal {C}_{\xi \upharpoonright y}$
; thus
$\xi (x)\land \forall y\leq x. \mathcal {C}_{\xi \upharpoonright y}$
, and so
$\tau (x)$
. Now, assume
$\tau (x)$
. Then,
$\xi (x)\land \forall y\leq x. \mathcal {C}_{\xi \upharpoonright y}$
. Let us show that
$x\leq z$
. Assume, by way of contradiction, that
$x>z$
. Then,
${\texttt {S}}(z)\leq x$
, and thus
$\mathcal {C}_{\xi \upharpoonright {\texttt {S}}(z)}$
, which contradicts (I). This proves the desired formula.
Stepping outside T and using what we have previously concluded, we obtain
$T\vdash \neg \mathcal {C}_\xi \rightarrow \exists z. (\mathcal {C}_{\xi \upharpoonright z}\land \forall x. \tau (x)\leftrightarrow \xi (x)\land x\leq z)$
, in other words,
$T\vdash \neg \mathcal {C}_\xi \rightarrow \exists z. (\mathcal {C}_{\xi \upharpoonright z}\land .\tau \leftrightarrow (\xi \upharpoonright z))$
. Consequently, by (i),
$T\vdash \neg \mathcal {C}_\xi \rightarrow \exists z.\mathcal {C}_\tau $
, and thus
$T\vdash \neg \mathcal {C}_\xi \rightarrow \mathcal {C}_\tau $
.
By definition,
$T\vdash \tau \rightarrow \xi $
, and so, using (v),
$T\vdash \mathcal {C}_\xi \rightarrow \mathcal {C}_\tau $
. In sum,
$T\vdash \mathcal {C}_\tau $
.
Definition 6. We say that
$\mathcal {C}_{\alpha }$
is a canonical general notion of consistency with respect to S and T if it is a general notion of consistency and satisfies the conditions of Theorem 2.
Observation 4. It is clear that (v) S-implies (i). We decided to maintain both, since they are used differently in different contexts; (i) is used in the more general context.
Canonical general notion of consistency (with respect to S and T) is the notion we looked for to satisfy G2 and Feferman’s result; this notion depends deeply on the underlying theories S and T, especially condition (vi) of Theorem 2: this last condition is more a feature of the theory T than actually a feature of
$\mathcal {C}_{\alpha }$
; this happens because we aim at a fine grain analysis, so we are separating S from T. For this reason, and since canonical general notions of consistency are a particular case of general notions of consistency, we will mainly focus our attention to the latter (nevertheless, the examples we consider in this paper are canonical, for a suitable theory T).
Corollary 5. If, for each
$m\in \mathbb {N}$
,
$T\vdash {\texttt {Con}}^{1;n}_{\xi \upharpoonright \overline {m}}$
, then there is a numeration
$\tau $
of S in T such that
$T\vdash {\texttt {Con}}^{1;n}_\tau $
.
Proof. We show the truth of the assumptions of Theorem 2.
-
(iii) This condition is a consequence of the fact that
$T\vdash {\texttt {Pr}}_\xi \leftrightarrow \exists x. {\texttt {Pr}}_{\xi \upharpoonright x}$
. -
(iv) This follows from the reflexivity of
${\mathsf {PA}}$
([Reference Hájek and Pudlák8, p. 168, theorem 2.35]). -
(v) This condition is immediately satisfied from the definition of
${\texttt {Con}}^{1;n}_{\alpha }$
. -
(vi) This is true by our initial assumptions on T and from the hypothesis.
Corollary 6. Suppose that
$T\supseteq S$
and for each
$n\in \mathbb {N}$
,
$T\vdash \omega \text {-}{\texttt {Con}}^{\xi \upharpoonright \overline {n}}$
. Then, there is a numeration
$\tau $
of S in T such that
$T\vdash \omega \text {-}{\texttt {Con}}^\tau $
.
Proof. As before, we verify the assumptions of Theorem 2:
-
(iii) This condition is a consequence of the fact that
$T\vdash {\texttt {Pr}}_\xi \leftrightarrow \exists x. {\texttt {Pr}}_{\xi \upharpoonright x}$
. -
(iv) Trivially satisfied.
-
(v) Follows from C5.
-
(vi) True, by hypothesis.
Corollary 7. Suppose that, for each
$m\in \mathbb {N}$
,
$T\vdash {\texttt {RfC}}^n_{\xi \upharpoonright \overline {m}}$
. Then, there is a numeration
$\tau $
of S in T such that
$T\vdash {\texttt {RfC}}^n_\tau $
.
Proof. Similar to the previous cases.
Definition 7. We say that S is T-reflexive for the general notion of consistency
$\mathcal {C}_{\alpha }$
if T satisfies condition (vi) of Theorem 2.
Theorem 2, using reflexivity, ensures the existence of a numeration
$\tau $
such that
$T\vdash \mathcal {C}_\tau $
; the next result proves, in a sense, the converse claim: if there is such a numeration
$\tau $
, then condition (vi) needs to be satisfied.
Theorem 3. Suppose that
$\mathcal {C}_{\alpha }$
is a general notion of consistency defined for each numeration
$\alpha $
of S in
$T\supseteq S$
and that
$\xi $
does
$\Delta _0(T)$
-numerate S in T.Footnote
15
If T is such that there is
$\tau $
that numerates the axioms of S in T and
$T\vdash \mathcal {C}_\tau $
, and
$\mathcal {C}_{\alpha }$
satisfies (v) of Theorem 2, then S is T-reflexive for the general notion of consistency
$\mathcal {C}_{\alpha }$
.
Proof. Consider
$n\in \mathbb {N}$
and the respective numeration
$\xi \upharpoonright \overline {n}$
. Clearly, there are
$m_0,\ldots ,m_\ell \in \mathbb {N}$
such that
$T\vdash (\xi \upharpoonright \overline {n})(v)\rightarrow \bigvee _{i=0}^\ell (v=\overline {m_i})$
. As
$\tau $
numerates S in T, then, for
$0\leq i\leq \ell $
,
$T\vdash \tau (\overline {m_i})$
. So,
$T\vdash (\xi \upharpoonright \overline {n})(v)\rightarrow \tau (v)$
, i.e.,
$T\vdash \xi \upharpoonright \overline {n}\rightarrow \tau $
. Using (v),
$T\vdash \mathcal {C}_\tau \rightarrow \mathcal {C}_{\xi \upharpoonright \overline {n}}$
, and so
$T\vdash \mathcal {C}_{\xi \upharpoonright \overline {n}}$
.
Corollary 8. If there is a numeration
$\tau $
of S in S such
$S\vdash {\texttt {Con}}_\tau $
, then S is reflexive.
Proof. It is just Theorem 3 for
$T=S$
and for the usual notion of consistency,
${\texttt {Con}}_{\alpha }$
.
4 Slow consistency
Throughout this section,
${\texttt {g}}$
stands for a term representing a function in S. We start this section by defining slow consistency as in [Reference Friedman, Rathjen and Weiermann7].
Definition 8. We define:
$$ \begin{align*} &{\texttt{Pr}}_{\alpha\upharpoonright{\texttt{g}}}(x):=\exists s. {\texttt{Prf}}_{\alpha\upharpoonright{\texttt{g}}({(s)}_0)}(x,{(s)}_1); & {\texttt{Con}}^{{\texttt{g}}}_{\alpha}:=\neg {\texttt{Pr}}_{\alpha\upharpoonright{\texttt{g}}}(\ulcorner\perp\urcorner). \end{align*} $$
Moreover, we use the term
$\texttt {maxax}_\xi $
that represents the following elementary function:
$$ \begin{align*} {maxax}_\xi(n):=\begin{cases} 0, & n \text{ is not the code of a } \xi\text{-proof}\\ k, & k \text{ is the greatest code of a } \xi\text{-axiom}\\ &\text{occurring in the } \xi\text{-proof } n. \end{cases} \end{align*} $$
It is immediate that
$$ \begin{align} S\vdash {\texttt{Prf}}_{\xi\upharpoonright x}(y,z)\rightarrow \texttt{maxax}(z)\leq x. \end{align} $$
It is usual, in this context, to introduce, for
$\alpha $
including
$\xi $
, the statement
${\texttt {Con}}^*_{\alpha }:=\forall x. {\texttt {Con}}_{\alpha \upharpoonright F^{-1}_{\varepsilon _0}(x)}$
, where
$F_{\varepsilon _0}$
is a fast growing function as presented in [Reference Friedman, Rathjen and Weiermann7, definition 1.3]. It is a known fact that 
(see [Reference Friedman, Rathjen and Weiermann7], proposition 3.3).
Now we introduce a generalization of this consistency statement.
Definition 9. We say that
$\mathcal {C}_{\alpha }:=\forall \mathcal {A}(x).\mathcal {C}_{\alpha }(x)$
is a
${\texttt {g}}$
-general notion of consistency if there are terms
${\texttt {f}}$
and
${\texttt {h}}$
of S and a false sentence
$\mathcal {F}$
satisfying
$S\vdash \forall s. {\texttt {Proof}}_\xi ({(s)}_1)\rightarrow \mathcal {A}({\texttt {h}}(s))$
,
$S\vdash \forall s. {({\texttt {f}}({\texttt {h}}(s)))}_1={(s)}_1$
,
$S\vdash {\texttt {Proof}}_\xi ({(s)}_1)\land \texttt {maxax}({(s)}_1)\leq {\texttt {g}}({(s)}_0)\rightarrow \texttt {maxax}({(s)}_1)\leq {\texttt {g}}({({\texttt {f}}({\texttt {h}}(s)))}_0)$
, and
$$\begin{align} S\vdash \mathcal{C}_{\alpha}(x)\rightarrow \neg{\texttt{Prf}}_{\xi\upharpoonright{\texttt{g}}({({\texttt{f}}(x))}_0)}(\ulcorner\mathcal{F}\urcorner,{({\texttt{f}}(x))}_1), \end{align}$$
whenever
$\alpha $
includes
$\xi $
. We also assume the condition (i) and (ii).
The conditions of this definition generalize the conditions of Definition 5; this is going to be made explicit in the following proposition.
Proposition 2. If
$\mathcal {C}_{\alpha }$
is a general notion of provability, then
$\mathcal {C}_{\alpha }$
is an
${\texttt {id}}$
-general notion of consistency.
Proof. Let
${\texttt {f}}$
and
${\texttt {h}}$
be the terms given by the definition of general notion of consistency. Define
$$ \begin{align*} &{\texttt{f}}'(x):=\langle\texttt{maxax}({\texttt{f}}(x)),{\texttt{f}}(x)\rangle; &{\texttt{h}}'(s):={\texttt{h}}({(s)}_1). \end{align*} $$
Clearly,
$S\vdash \forall s. {\texttt {Proof}}_\xi ({(s)}_1)\rightarrow \mathcal {A}({\texttt {h}}'(s))$
. Moreover,
$$ \begin{align*} S\vdash {({\texttt{f}}'({\texttt{h}}'(s)))}_1&={(\langle\texttt{maxax}({\texttt{f}}({\texttt{h}}'(s))),{\texttt{f}}({\texttt{h}}'(s))\rangle)}_1={\texttt{f}}({\texttt{h}}'(s))\\ &={\texttt{f}}({\texttt{h}}({(s)}_1))={(s)}_1. \end{align*} $$
In addition,
$$ \begin{align*}S\vdash {\texttt{id}}({({\texttt{f}}'({\texttt{h}}'(s)))}_0)&={({\texttt{f}}'({\texttt{h}}'(s)))}_0={(\langle\texttt{maxax}({\texttt{f}}({\texttt{h}}'(s))),{\texttt{f}}({\texttt{h}}'(s))\rangle)}_0\\ &=\texttt{maxax}({\texttt{f}}({\texttt{h}}'(s)))=\texttt{maxax}({\texttt{f}}({\texttt{h}}({(s)}_1)))\\ &=\texttt{maxax}({(s)}_1). \end{align*} $$
Consequently,
$S\vdash {\texttt {Proof}}_\xi ({(s)}_1)\land \texttt {maxax}({(s)}_1)\leq {\texttt {id}}({(s)}_0)\rightarrow \texttt {maxax}({(s)}_1)\leq {\texttt {id}}({({\texttt {f}}'({\texttt {h}}'(s)))}_0)$
. Finally, we haveFootnote
16
$$ \begin{align*} S\vdash \mathcal{C}_{\alpha}(x)&\rightarrow\neg{\texttt{Prf}}_\xi(\ulcorner\mathcal{F}\urcorner,{\texttt{f}}(x))\rightarrow\neg{\texttt{Prf}}_{\xi\upharpoonright\texttt{maxax}({\texttt{f}}(x))}(\ulcorner\mathcal{F}\urcorner,{\texttt{f}}(x))\\ &\rightarrow \neg{\texttt{Prf}}_{\xi\upharpoonright {({\texttt{f}}'(x))}_0}(\ulcorner\mathcal{F}\urcorner,{({\texttt{f}}'(x))}_1). \end{align*} $$
Conditions (i) and (ii) are already satisfied.
Proposition 3.
${\texttt {Con}}^{{\texttt {g}}}_{\alpha }$
is a
${\texttt {g}}$
-general notion of consistency.
Proof. By definition,
$S\vdash {\texttt {Con}}^{{\texttt {g}}}_{\alpha }\leftrightarrow \forall s. \neg {\texttt {Prf}}_{\alpha \upharpoonright {\texttt {g}}({(s)}_0)}(\ulcorner \perp \urcorner ,{(s)}_1)$
. The result is immediate by considering
${\texttt {f}}:={\texttt {h}}:={\texttt {id}}$
, and
$\mathcal {A}(s):={\texttt {Proof}}_{\alpha }({(s)}_1)$
, since
$S\vdash {\texttt {Prf}}_{\xi \upharpoonright {\texttt {g}}({(s)}_0)} (\ulcorner \perp \urcorner ,{(s)}_1)\rightarrow {\texttt {Prf}}_{\alpha \upharpoonright {\texttt {g}}({(s)}_0)}(\ulcorner \perp \urcorner ,{(s)}_1)$
.
The next result generalizes the fact that 
, a version of G2.
Theorem 4. Let
${\texttt {g}}$
be a term representing a function in S such that, for each
$k\in \mathbb {N}$
, there is m such that
$S\vdash {\texttt {g}}(\overline {m})\geq \overline {k}$
. If
$\mathcal {C}_{\alpha }$
is a
${\texttt {g}}$
-general notion of consistency,
$\alpha $
includes
$\xi $
, and, for all
$\ell \in \mathbb {N}$
, 
, then 
.
Proof. Clearly,
$S\vdash \exists \mathcal {A}(x).{\texttt {Prf}}_{\xi \upharpoonright {\texttt {g}}({({\texttt {f}}(x))}_0)}(\ulcorner \mathcal {F}\urcorner ,{({\texttt {f}}(x))}_1)\rightarrow {\texttt {Pr}}_{\xi \upharpoonright {\texttt {g}}}(\ulcorner \mathcal {F}\urcorner )$
. Let us reason inside S for the converse direction. Assume
${\texttt {Pr}}_{\xi \upharpoonright {\texttt {g}}}(\ulcorner \mathcal {F}\urcorner )$
. Hence,
$\exists s. {\texttt {Prf}}_{\xi \upharpoonright {\texttt {g}}({(s)}_0)} (\ulcorner \mathcal {F}\urcorner ,{(s)}_1)$
. Take such an s and consider
$y:={\texttt {h}}(s)$
. We know that
${({\texttt {f}}(y))}_1={({\texttt {f}}({\texttt {h}}(s)))}_1={(s)}_1$
. SoFootnote
17
, as we also have by hypothesis
$\mathcal {A}(y)$
and
${\texttt {Proof}}_\xi ({(s)}_1)\land \texttt {maxax}({(s)}_1)\leq {\texttt {g}}({(s)}_0)$
, it follows that
$\texttt {maxax}({(s)}_1)\leq {\texttt {g}}({({\texttt {f}}({\texttt {h}}(s)))}_0)={\texttt {g}}({({\texttt {f}}(y))}_0)$
; consequently
$\exists \mathcal {A}(y).{\texttt {Prf}}_{\xi \upharpoonright {\texttt {g}}({({\texttt {f}}(y))}_0)}(\ulcorner \mathcal {F}\urcorner ,{({\texttt {f}}(y))}_1)$
. Going outside S, we can conclude
$$ \begin{align} S\vdash \exists \mathcal{A}(y).{\texttt{Prf}}_{\xi\upharpoonright{\texttt{g}}({({\texttt{f}}(y))}_0)}(\ulcorner\mathcal{F}\urcorner,{({\texttt{f}}(y))}_1)\leftrightarrow {\texttt{Pr}}_{\xi\upharpoonright{\texttt{g}}}(\ulcorner\mathcal{F}\urcorner). \end{align} $$
Assume, by way of contradiction, that
$S\vdash \mathcal {C}_{\alpha }$
. So,
$S\vdash \forall \mathcal {A}(x).\mathcal {C}_{\alpha }(x)$
, hence, using (GenCon
$^{{\texttt {g}}}$
) and (I),
$S\vdash \neg {\texttt {Pr}}_{\xi \upharpoonright {\texttt {g}}}(\ulcorner \mathcal {F}\urcorner )$
.
For a sufficiently large k
Footnote
18
,
$S\upharpoonright k\vdash \neg {\texttt {Pr}}_{\xi \upharpoonright {\texttt {g}}}(\ulcorner \mathcal {F}\urcorner )$
. Let
$m_0$
be such that
$S\vdash {\texttt {g}}(\overline {m_0})\geq \overline {k}$
. As
${\texttt {g}}(\overline {m_0})\geq \overline {k}$
is
$\Sigma _1$
-sentence, it follows that
$S\upharpoonright k\vdash {\texttt {g}}(\overline {m_0})\geq \overline {k}$
. Take
$\ell $
with
$S\upharpoonright k\vdash \overline {\ell }={\texttt {g}}(\overline {m_0})$
.
Reason inside
$S\upharpoonright k$
. We know that
$\forall s. \neg {\texttt {Prf}}_{\xi \upharpoonright {\texttt {g}}({(s)}_0)}(\ulcorner \mathcal {F}\urcorner ,{(s)}_1)$
. By considering, for each x,
$s:=\langle \overline {m_0},x\rangle $
, we can conclude
$\forall x. \neg {\texttt {Prf}}_{\xi \upharpoonright {\texttt {g}}(\overline {m_0})}(\ulcorner \mathcal {F}\urcorner ,x)$
. Going outside
$S\upharpoonright k$
, as
$k\leq \ell $
,
$S\upharpoonright \ell \vdash \forall x. \neg {\texttt {Prf}}_{\xi \upharpoonright \overline {\ell }}(\ulcorner \mathcal {F}\urcorner ,x)$
, and so
$S\upharpoonright \ell \vdash \neg {\texttt {Pr}}_{\xi \upharpoonright \overline {\ell }}(\ulcorner \mathcal {F}\urcorner )$
, and thus
$S\upharpoonright \ell \vdash \neg {\texttt {Pr}}_{\xi \upharpoonright \overline {\ell }}(\ulcorner \perp \urcorner )$
, which contradicts the hypothesis.
We can also generalize Feferman’s result for this setting, observe that the original Theorem 2 holds in this setting. In a similar way to what we considered in Definition 6, we introduce the following concept.
Definition 10. We say that
$\mathcal {C}_{\alpha }$
is a canonical
${\texttt {g}}$
-general notion of consistency with respect to S and T if it is a
${\texttt {g}}$
-general notion of consistency and satisfies the conditions of Theorem 2.
We now present a new hybrid notion of consistency: it has the layout of
$\omega $
-consistency, but adapted to slow consistency.
Definition 11. We define:
Now we show that
$\omega \text {-}{\texttt {Con}}^{{\texttt {g}}}_{\alpha }$
fits Definition 9, and thus constitutes a meaningful example that arises from our analysis.
Proposition 4.
$\omega \text {-}{\texttt {Con}}^{{\texttt {g}}}_{\alpha }$
is a
${\texttt {g}}$
-general notion of consistency if
$S\vdash {\texttt {g}}(x)\geq x$
and
$S\vdash {\texttt {Pr}}_{\alpha \upharpoonright {\texttt {g}}}(\ulcorner \perp \urcorner )\rightarrow {\texttt {Pr}}_{\alpha \upharpoonright {\texttt {g}}}(x)$
.
Proof. Consider
${\texttt {f}}_0$
,
${\texttt {f}}_1$
,
${\texttt {f}}_0^{-1}$
, and
${\texttt {f}}_1^{-1}$
as in the proof of Proposition 1. Define
$\mathcal {A}(x):=1{\texttt {-var}}(x)$
,
${\texttt {f}}'(x):={\texttt {f}}_1({\texttt {f}}_0^{-1}(x))$
,
${\texttt {h}}'(x):={\texttt {f}}_0({\texttt {f}}_1^{-1}(x))$
; moreover, consider
$$ \begin{align*} &{\texttt{f}}(x):=\langle\texttt{maxax}({\texttt{f}}'(x)),{\texttt{f}}'(x)\rangle; &{\texttt{h}}(s):={\texttt{h}}'({(s)}_1). \end{align*} $$
Clearly,
$S\vdash \forall s. {\texttt {Proof}}_\xi ({(s)}_1)\rightarrow \mathcal {A}({\texttt {h}}(s))$
. In addition, just like in the proofs of Propositions 1 and 2,
$$ \begin{align*}S\vdash \forall s. {({\texttt{f}}({\texttt{h}}(s)))}_1&={(\langle\texttt{maxax}({\texttt{f}}'({\texttt{h}}(s))),{\texttt{f}}'({\texttt{h}}(s))\rangle)}_1={\texttt{f}}'({\texttt{h}}(s))\\ &={\texttt{f}}'({\texttt{h}}'({(s)}_1))={(s)}_1. \end{align*} $$
Moreover,
$$ \begin{align*}S\vdash {\texttt{g}}({({\texttt{f}}({\texttt{h}}(s)))}_0)&={\texttt{g}}({(\langle\texttt{maxax}({\texttt{f}}'({\texttt{h}}(s))),{\texttt{f}}'({\texttt{h}}(s))\rangle)}_0)={\texttt{g}}(\texttt{maxax}({\texttt{f}}'({\texttt{h}}(s))))\\ &={\texttt{g}}(\texttt{maxax}({\texttt{f}}'({\texttt{h}}'({(s)}_1))))={\texttt{g}}(\texttt{maxax}({(s)}_1))\geq \texttt{maxax}({(s)}_1). \end{align*} $$
This amounts to
$S\vdash {\texttt {Proof}}_\xi ({(s)}_1)\land \texttt {maxax}({(s)}_1)\leq {\texttt {g}}({(s)}_0)\rightarrow \texttt {maxax}({(s)}_1)\leq {\texttt {g}}({({\texttt {f}}({\texttt {h}}(s)))}_0)$
. Finally,
Conditions (i) and (ii) are also satisfied.
5 Notion of provability from a general notion of consistency
In this section, we create notions of provability from our general notions of consistency; for that, we assume that S and
$\mathcal {C}_{\alpha }$
satisfy the following simple properties:
-
Numeration 1:
; -
Numeration 2:
.
;
.The goal of this section is not to find new results about provability predicates; on the contrary, we use this section to show that our approach to consistency is so natural that all the usual properties about provability can be obtained in our new framework; in this sense, this serves as a confirmation of the naturalness of our view of consistency.
Definition 12. Given a general notion of consistency
$\mathcal {C}_{\alpha }$
, we define its notion of provability by
The previous definition is aligned with what was considered in [Reference Boolos3, p. 191] for
$\omega $
-consistency; we generalize that approach for different notions of consistency. In a sense,
$\mathcal {P}_{\mathcal {C}_{\alpha }}(x)$
expresses “
is inconsistent, according to the considered general notion of consistency, with the theory
$\alpha $
”, or equivalently “the theory 
is inconsistent, according to the considered general notion of consistency”.
It is important to observe that in our initial analysis of G2 and Feferman’s result we did not implicitly require any form of non-trivial derivability conditions of the corresponding notion of provability, this means that our proofs do not rely on an implicit use of the modal logic
$\mathsf {GLB}$
.
The following result confirms that a general notion of consistency
$\mathcal {C}_{\alpha }$
is, in fact, the usual consistency statement,
$\neg {\texttt {Pr}}_{\alpha }(\ulcorner \perp \urcorner )$
, for the corresponding notion of provability,
$\neg \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \perp \urcorner )$
.
Proposition 5. Given
$\mathcal {C}_{\alpha }$
a general notion of consistency, we have
$S\vdash \mathcal {C}_{\alpha }\leftrightarrow \neg \mathcal {P}_{\mathcal {C}_{\alpha }} (\ulcorner \perp \urcorner )$
.
Proof. It is clear that, for a numeration
$\alpha $
,
$S\vdash \alpha (v)\leftrightarrow (\alpha +\ulcorner \neg \perp \urcorner )(v)$
. This entails, from Definition 5,
$S\vdash \mathcal {C}_{\alpha }\leftrightarrow \mathcal {C}_{\alpha +\ulcorner \neg \perp \urcorner }$
. Consequently, we obtain
$S\vdash \mathcal {C}_{\alpha }\leftrightarrow \mathcal {C}_{\alpha +\ulcorner \neg \perp \urcorner }\leftrightarrow \neg \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \perp \urcorner )$
.
The next result shows that the notion of provability that arises from the usual consistency statement,
${\texttt {Con}}_{\alpha }$
, is the usual notion of provability,
${\texttt {Pr}}_{\alpha }$
.
Proposition 6.
$S\vdash \mathcal {P}_{{\texttt {Con}}_{\alpha }}\leftrightarrow {\texttt {Pr}}_{\alpha }$
.
Proof. It is easy to see that 
.
We end this section by relating properties of the general notion of consistency to properties of its respective notion of provability.
Theorem 5. Let
$\mathcal {C}_{\alpha }$
be a general notion of consistency and
$\alpha $
a numeration of a theory
$T\supseteq S$
satisfying:
-
1.
; -
2.
; -
3.
.
;
;
.Then
$\mathcal {P}_{\mathcal {C}_{\alpha }}$
satisfies the following derivability conditions:
-
C1:
$S\vdash {\texttt {Pr}}_{\alpha }(x)\rightarrow \mathcal {P}_{\mathcal {C}_{\alpha }}(x)$
; -
C2:
; -
C3:
.
;
. Condition 1 expresses the fact that if 
is consistent, according to considered general notion of consistency, with
$\alpha $
, then x cannot be proved, in the classical sense, i.e.,
$\neg {\texttt {Pr}}_{\alpha }(x)$
. Condition 2 expresses that (according to the general notion of consistency) whenever 
is consistent and 
is inconsistent, then we can extend 
to 
without loosing consistency; as a particular case, if 
is inconsistent, then
$\alpha +x$
needs to be consistent. The last condition (3) states that if the consistency statement 
is consistent, according to the general notion of consistency, with the considered theory
$\alpha $
, then we also need to have that 
is consistent with
$\alpha $
, videlicet 
is consistent.
Proof of Theorem 5.
-
C1: Using 1, we have immediately the desired condition.
-
C2: From 2, we get
. -
C3: From 3, we can conclude
.
.
. The next result confirms that a form of G1 holds for the notion of provability
$\mathcal {P}_{\mathcal {C}_{\alpha }}$
when it satisfies the previous derivability conditions.
Proposition 7. Let
$\mathcal {C}_{\alpha }$
be a general notion of consistency satisfying the conditions of Theorem 5. Then,
Proof. Let
$\mathcal {G}_{\alpha }$
be the Gödel-sentence given by the Diagonalization lemma such that
$S\vdash \mathcal {G}_{\alpha }\leftrightarrow \neg \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {G}_{\alpha }\urcorner )$
.
Reason inside
$S+\neg \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \perp \urcorner )\urcorner )$
. Assume, by way of contradiction, that
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {G}_{\alpha }\urcorner )$
. Then, using C3,
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {G}_{\alpha }\urcorner )\urcorner )$
. From C1 and C2, we get
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \neg \mathcal {G}_{\alpha }\urcorner )$
, and thus, from C2,
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \perp \urcorner )$
, and consequently
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \perp \urcorner )\urcorner )$
, a contradiction. Thus,
$\neg \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {G}_{\alpha }\urcorner )$
.
Now assume
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \neg \mathcal {G}_{\alpha }\urcorner )$
. From C1 and C2,
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {G}_{\alpha }\urcorner )\urcorner )$
; furthermore, by C3,
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \neg \mathcal {G}_{\alpha }\urcorner )\urcorner )$
. Using C1 and C2, we can conclude that
$\mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \perp \urcorner )\urcorner )$
, a contradiction. Therefore,
$\neg \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \neg \mathcal {G}_{\alpha }\urcorner )$
.
Observation 5. It is easy to characterize the statements of the form used in the previous result, namely the statements of the form
$\neg \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \mathcal {P}_{\mathcal {C}_{\alpha }}(\ulcorner \perp \urcorner )\urcorner )$
, in terms of
$\mathcal {C}_{\alpha }$
. Consider, for
$n\in \mathbb {N}$
,
It is easy to conclude that, for each
$n\in \mathbb {N}$
,
$S\vdash \mathcal {C}_{\alpha }^n\leftrightarrow \neg \mathcal {P}_{\mathcal {C}_{\alpha }}^{n}(\ulcorner \perp \urcorner )$
.
Theorem 6. Let
$\mathcal {C}_{\alpha }$
be a general notion of consistency and
$\alpha $
a numeration of a theory
$T\supseteq S$
satisfying:
-
4.
.
.Then
$\mathcal {P}_{\mathcal {C}_{\alpha }}$
satisfies the following derivability condition:
-
C4:
.
. Condition 4 expresses an adapted form of G2: if
$\alpha +y$
is consistent, then the statement
$\mathcal {C}_{\alpha +{y}}$
is not provable, that is to say
$\neg \mathcal {C}_{\alpha +{y}}$
is not refutable, equivalently 
is consistent.
Proof of Theorem 6.
We have, by considering 
, 
.
Proposition 8. Let
$\mathcal {C}_{\alpha }$
be a general notion of consistency and
$\alpha $
a numeration of a theory
$T\supseteq S$
satisfying:
-
5.
.
.Then
$\mathcal {P}_{\mathcal {C}_{\alpha }}$
satisfies the following derivability condition:
-
C5:
.
. 5 is a version of Lindenbaum’s lemma; see [Reference Salehi17, proposition 2.3] for a proof that
$\omega \text {-}{\texttt {Con}}_{\alpha }$
satisfies the mentioned condition (this condition was firstly proved in [Reference Isaacson10]).
Proof of Proposition 8.
It follows from a straightforward application of the definitions.
6 Notion of interpretability from a general notion of consistency
We aim at encompassing interpretability into our framework of generalized consistency; just like the previous section, this serves to confirm that our notions are natural, not necessarily to find new results about interpretability; as the reader can confirm, we are able to recover in terms of properties about consistency most of the usual properties of interpretability logic. It is a known fact that there is a close relation between interpretability and consistency statements of finite segments of theories of arithmetic; more precisely, [Reference Hájek and Pudlák8, p. 169, theorem 2.39] guarantees that
$T \rhd S$
(“T interprets S”) if, and only if, for all n,
$T\vdash {\texttt {Con}}_{\xi \upharpoonright \overline {n}}$
. As usual,
$\varphi \rhd \psi $
denotes
$S+\varphi \rhd S+\psi $
. Interpretability logic
$\mathsf {IL}$
—the logic of
$\varphi \rhd \psi $
together with the usual modal logic for provability—has been thoroughly studied; see, for example, [Reference Joosten and Visser11] and [Reference Visser and Petkov20]. Inspired by the previously presented characterization of interpretability, we developed the following definition.
Definition 13. Given
$\mathcal {C}_{\alpha }$
a general notion of consistency, we define its notion of interpretability by
Like we did with notions of provability, we present some important properties from
$\mathsf {IL}$
that are satisfied for
$\rhd _{\mathcal {C}_{\alpha }}$
in terms of properties of
$\mathcal {C}_{\alpha }$
; a similar approach can be followed for the remaining properties of
$\mathsf {IL}$
and even for other logics of interpretability, like
$\mathsf {ILM}$
[Reference Visser and Petkov20, p. 21].
Proposition 9. Let
$\mathcal {C}_{\alpha }$
be a general notion of consistency and
$\alpha $
a numeration of a theory
$T\supseteq S$
. Then,
$\rhd _{\mathcal {C}_{\alpha }}$
satisfies the following property:
-
C6:
.
.Proof.
-
C6: We know that
, so as wanted.
, so 
Proposition 10. Let
$\mathcal {C}_{\alpha }$
be a general notion of consistency and
$\alpha $
a numeration of a theory
$T\supseteq S$
satisfying:
-
6.
$S\vdash \mathcal {C}_{\alpha +x}\leftrightarrow \forall z. \mathcal {C}_{(\alpha +x)\upharpoonright z}$
.
Then,
$\rhd _{\mathcal {C}_{\alpha }}$
satisfies the following property:
-
C7:
.
.Proof.
-
C7: We have that
, so, by 6, we can conclude , thus , i.e., .
, so, by 6, we can conclude 
, thus 
, i.e., 
.Proposition 11. Let
$\mathcal {C}_{\alpha }$
be a general notion of consistency and
$\alpha $
a numeration of a theory
$T\supseteq S$
satisfying:
-
6.
$S\vdash \mathcal {C}_{\alpha +x}\leftrightarrow \forall z. \mathcal {C}_{(\alpha +x)\upharpoonright z}$
; -
7.
.
.Then,
$\rhd _{\mathcal {C}_{\alpha }}$
satisfies the following property.
-
C8:
.
.Proof.
-
C8: We have that
.
.7 Conclusions
We singled out two important facts that a general notion of consistency should satisfy (besides, of course, expressing some form of non-contradiction): G2 and Feferman’s result. We took a quasi-empirical approach to the problem, in the sense that we started from a set of sufficiently diverse consistency statements and we generalized them, by verifying that they fit our definition: this is the empirical part, we have no “proof” that our definition accounts for any sentences we recognize as expressing consistency.
We presented the definition of a general notion of consistency, Definition 5, and we showed that the following consistency statements fit our considerations: usual consistency (
${\texttt {Con}}_{\alpha }$
),
$\omega $
-consistency (
$\omega \text {-}{\texttt {Con}}_{\alpha }$
,
$\omega \text {-}{\texttt {Con}}^\alpha $
), n-consistency (
$n\text {-}{\texttt {Con}}_{\alpha }$
), iterated consistency (
${\texttt {Con}}^n_{\alpha }$
,
${\texttt {Con}}^{1;n}_{\alpha }$
), and consistency via reflection principles (
${\texttt {RfC}}^n_{\alpha }$
). We showed that our definition satisfies G2 (see Theorem 1) and Feferman’s result (see Theorem 2); for the latter, we needed some extra conditions that depend on the underlying theories; to a general notion of consistency that satisfies those conditions we gave the name canonical general notion of consistency (with respect to S and T), cf. Definition 6.
From that, we accounted for slow consistency by considering the hybrid notion of a
${\texttt {g}}$
-general notion of consistency. We showed that our initial notion is a particular of the new one (cf. Proposition 2), and we showed that slow consistency is also a particular case of it (see Proposition 3). We proved G2 for this new notion (done in Theorem 4); and we observed that Feferman’s result can be generalized for this setting, since the original Theorem 2 holds in this framework. We developed a hybrid notion of provability, a form of
$\omega $
-consistency joint with slow consistency (see Definition 11 and Proposition 4):
$\omega \text {-}{\texttt {Con}}^{{\texttt {g}}}_{\alpha }$
.
To show how transversal and natural our approach is, we created, for each general notion of consistency, a corresponding notion of provability (cf. Definition 12). We showed the relation between these notions of provability and the consistency statements (Proposition 5); we verified that, for the usual consistency statement, the corresponding notion of provability is the usual provability (Proposition 6); and we studied some derivability conditions in this setting (Theorem 5 and Theorem 6). In a similar spirit, we developed a notion of interpretability for each general notion of provability (Definition 13) and we studied some of its properties (Propositions 9, 10, and 11).
Acknowledgments
The author would like to enthusiastically thank the anonymous reviewer for the comments and suggestions that were made, allowing this work to be of a higher quality and clarity.
Funding
The author was supported by national funds through the FCT–Fundação para a Ciência e a Tecnologia, I.P., under the scope of the projects UIDB/04561/2020 and UIDP/04561/2020 (CMAFcIO, UL).
; we opted to consider the simpler condition (i) in our definition to avoid unnecessary complexity of our main concept of general notion of consistency.
