Russellian Propositional Logic and the BHK Interpretation

TL;DR

This paper develops a hierarchical propositional logic framework based on Russellian typed languages to interpret the BHK proof hierarchy, introducing new logics and establishing their soundness and completeness.

Contribution

It introduces hierarchical counterparts of key propositional logics using a typed language with multiple implications, linking syntax to the proof hierarchy in BHK interpretation.

Findings

Defined hierarchical propositional logics for BHK interpretation

Proved soundness and completeness theorems for these logics

Showed how different logics model various proof hierarchies

Abstract

The BHK interpretation interprets propositional statements as descriptions of the world of proofs; a world which is hierarchical in nature. It consists of different layers of the concept of proof; the proofs, the proofs about proofs and so on. To describe this hierarchical world, one approach is the Russellian approach in which we use a typed language to reflect this hierarchical nature in the syntax level. In this case, since the connective responsible for this hierarchical behavior is implication, we will use a typed language equipped with a hierarchy of implications, $\{\rightarrow_n\}_{n=0}^{\infty}$. In fact, using this typed propositional language, we will introduce the hierarchical counterparts of the logics $\mathbf{BPC}$, $\mathbf{EBPC}$, $\mathbf{IPC}$ and $\mathbf{FPL}$ and then by proving their corresponding soundness-completeness theorems with respect to their natural BHK interpretations, we will show how these different logics describe different worlds of proofs embodying different hierarchical behaviors.

Equations

$$A,(\top \to (A\to B)),((A\wedge (A\to B))\to B)⊢A\to B$$

$$\mathbb{N}\models {\square }_{n+1}(A^{\sigma }\wedge {\square }_n(A^{\sigma }\to B^{\sigma })\to B^{\sigma })$$

$$(A\wedge (A{\to }_{n}B){\to }_{n+1}B){⊢}_{{\mathbf{FPL}}_h}A{\to }_{n}B$$

$$L_{\square }⊢{\square }_n(\bigwedge {\Gamma }^b\to (A^b\to B^b))$$

$$L_{\square }⊢{\square }_n(\bigwedge {\Gamma }^b)\to {\square }_n(A^b\to B^b)$$

$$L_{\square }⊢\bigwedge {\Gamma }^b\to {\square }_n(\bigwedge {\Gamma }^b)(\ast )$$

$$L_{\square }⊢\bigwedge {\Gamma }^b\to (A{\to }_{n}B{)}^b$$

$$L_{\square }⊢\bigwedge {\Gamma }^b\to {\square }_n(A^b\to B^b)$$

$$L_{\square }⊢\bigwedge {\Gamma }^b\to {\square }_n(A^b\to C^b)$$

$$L_{\square }⊢\bigwedge {\Gamma }^b\to {\square }_n(A^b\to B^b\wedge C^b)$$

$${KD4}_h⊢\bigwedge {\Gamma }^b\to {\square }_n(A^b\to {\square }_0\perp )\wedge A^b$$

$${KD4}_h⊢{\square }_n({\square }_0\perp \leftrightarrow \perp )$$

$${KD4}_h⊢\bigwedge {\Gamma }^b\to {\square }_n\perp$$

$${KD4}_h⊢\bigwedge {\Gamma }^b\to {\square }_0\perp$$

$${S4}_h⊢\bigwedge {\Gamma }^b\to {\square }_n(A^b\to B^b)\wedge A^b$$

$${S4}_h⊢\bigwedge {\Gamma }^b\to {\square }_n{B}^b$$

$${S4}_h⊢\bigwedge {\Gamma }^b\to B^b$$

$${\mathbf{GL}}_h⊢{\square }_{n+1}(A^b\wedge {\square }_n(A\to B)\to B^b)$$

$${\mathbf{GL}}_h⊢{\square }_{n+1}({\square }_n(A^b\to B^b)\to (A^b\to B^b))$$

$${\mathbf{GL}}_h⊢{\square }_n(A^b\to B^b)$$

$${\Gamma }^b,\{B_i^b\to C_i^b{\}}_{i\in I},\{p_j{\}}_{j\in J}\Rightarrow {\Delta }^b,\{D_r^b\to E_r^b{\}}_{r\in R},\{q_s{\}}_{s\in S}$$

$$G(L_{\square })⊢{\Gamma }^b,\{B_i^b\to C_i^b{\}}_{i\in I},\{p_j{\}}_{j\in J}\Rightarrow {\Delta }^b,\{D_r^b\to E_r^b{\}}_{r\in R},\{q_s{\}}_{s\in S}$$

$$\Gamma ,\{p_j{\}}_{j\in J},\{D_r{\}}_{r\in R},\{C_i{\}}_{i\in X}{⊢}_L\bigvee \{\Delta ,\{q_s{\}}_{s\in S},\{E_r{\}}_{r\in R},\{B_i{\}}_{i\notin X}\}$$

$$\{G_r{\}}_{r\in Y},\{p_j{\}}_{j\in J},\{B_i{\to }_{n_i}{C}_i{\}}_{i\in I},\{C_i{\}}_{i\in X},D{⊢}_{{\mathbf{BPC}}_h}\{F_r{\}}_{r\notin Y},\{B_i{\}}_{i\notin X},E$$

$$\{F_r{\to }_n{G}_r{\}}_{r\in R},\{p_j{\}}_{j\in J},\{B_i{\to }_{n_i}{C}_i{\}}_{i\in I}{⊢}_{{\mathbf{BPC}}_h}D{\to }_{n}E.$$

$$\bigwedge \{G_r{\}}_{r\in Y}\wedge \bigwedge \{C_i{\}}_{i\in X}\wedge D{\to }_n\bigvee \{F_r{\}}_{r\notin Y}\vee \bigvee \{B_i{\}}_{i\notin X}\vee E.$$

$$\bigwedge \{G_r{\}}_{r\in Y}\wedge \bigwedge \{C_i{\}}_{i\in Z}\wedge D{\to }_n\bigvee \{F_r{\}}_{r\notin Y}\vee \bigvee \{B_i{\}}_{i\notin Z}\vee {\mathbf{B}}_{\mathbf{i}}\vee E$$

$$\bigwedge \{G_r{\}}_{r\in Y}\wedge \bigwedge \{C_i{\}}_{i\in Z}\wedge {\mathbf{C}}_{\mathbf{i}}\wedge D{\to }_n\bigvee \{F_r{\}}_{r\notin Y}\vee \bigvee \{B_i{\}}_{i\notin Z}\vee E.$$

$$\bigwedge \{G_r{\}}_{r\in Y}\wedge \bigwedge \{C_i{\}}_{i\in Z}\wedge D{\to }_n\bigvee \{F_r{\}}_{r\notin Y}\vee \bigvee \{B_i{\}}_{i\notin Z}\vee E$$

$$\Sigma {⊢}_{{\mathbf{BPC}}_h}\bigwedge \{G_r{\}}_{r\in Y}\wedge D{\to }_n\bigvee \{F_r{\}}_{r\notin Y}\vee E.$$

Full text

1 Introduction

The intuitionistic tradition is based on the core concept of proof and its most important claim is that the statements in the language are descriptions of the world of proofs rather than the actual Platonistic world.222Notice that our paraphrase of the intuitionistic tradition’s claim seems extremly unorthodox. The reason is that we refer to the Platonistic world which can not exist in the intuitionistic terms. But it is not actually a paradox or a misinterpretation. In fact, following Gödel, [4], we interpret intuitionism from outside of its paradigm and we assume that we live in a Platonistic world in which intuitionism is a way of describing the sub-world of the classical proofs. This approach has been shown to be extremely useful. For more discussion about this approach and other approaches, see [1]. Therefore, the intended semantics of intuitionistic mathematics is just a relation which describes the way that intuitionistic logic describes the world of proofs. This semantics has a very complicated character and resists any kind of natural formalization. The reason is the hierarchical nature of the concept of proof which claims that there are different layers in the world of proofs. The first layer is the layer of proofs about the facts of the world. The second is the level of proofs about the proofs in the first level and there are also the third one, the fourth and so on. The important thing is that these higher level proofs occur in a very natural way. For instance, consider the statement “$A$* implies $B$*”. A proof for this statement is a proof which transforms proofs of $A$ to proofs for $B$. Hence, this proof is about proofs, meaning that it belongs to a higher level of the levels of the proofs of $A$ and $B$.

So far we have shown that the world of proofs is hierarchical in nature. Therefore, like any other hierarchical phenomenon, there are two main approaches to describe it: The Zermelo approach and the Russelian one. The Zermelo approach uses an untyped language to investigate the orderless propositions about the phenomenon, i.e. the propositions which are true in the world regardless of the levels of the objects in the world. The classical example of this approach is Zermelo’s set theory in the untyped first order language. Although there is a canonical order in the world of sets, i.e. the rank of sets, Zermelo’s set theory ignores this order and axiomatizes the universe uniformly.

Now, consider using the Zermelo approach for the world of proofs. We need two different components. First, an untyped language which in this case is the usual propositional language and second, an interpretation to interpret this language as a way of describing the world of proofs. The latter is provided by the following BHK interpretation:

$\bullet$ a proof for $A\wedge B$ is a pair of a proof for $A$ and a proof for $B$.

$\bullet$ a proof for $A\vee B$ is a proof for $A$ or a proof for $B$.

$\bullet$ a proof for $A\rightarrow B$ is a construction which transforms any proof of $A$ to a proof for $B$.

$\bullet$ $\bot$ does not have any proof.

This approach seems natural and easy to follow. We have an untyped simple language which is informally capable of describing the whole complexity of the world of proofs. Therefore, it seems natural to try to formalize this BHK interpretation as a formalized intended semantics for intuitionistic mathematics. But there are some fundamental problems along the way. The reason is that some of the most important statements in the language do have an internal inherent order and therefore the Zermelo approach has to ignore them; the situation which is not what we expect. Let us illuminate the idea by an example. Consider the following theorem of $\mathbf{IPC}$: $(\top\rightarrow\bot)\rightarrow\bot$. If we interpret this statement by the BHK interpretation, its content would be the following: “There is a proof which shows that the provability of the provability of $\bot$ implies the provability of $\bot$.” It seems that just by the informal interpretation of this statement we can be sure of its truth and it should be considered as an axiom in our Zermelo theory. The reason is that it is just a special case of the soundness of our theories which we intuitively believe. On the other hand, investigating the formula more precisely, we will notice that there are different levels of proofs in the statement, and if we can ignore the order in the world of proofs, then it should be true or false regardless the levels of proofs we are using. If we interpret all of the proofs as proofs in the same level, say in the theory $T$, then the statement means that $\Box_{T}(\Box_{T}\Box_{T}\bot\rightarrow\Box_{T}\bot)$. Using Löb’s theorem, it implies that $\Box_{T}\Box_{T}\bot$ which contradicts with the intuitive condition that there are no proofs of $\bot$. But if we interpret the “provability” in the statement as the provability in $T$, the provability as the provability in its meta-theory $S$ and proof as a proof in the meta-theory of $S$, say $R$, then it means that $R$ proves $\Box_{S}\Box_{T}\bot\rightarrow\Box_{T}\bot$. This is possible if $R$ is strong enough to prove the soundness of $S$; a condition that seems natural and acceptable. It actually is the informal reason behind our belief in the intuitive truth of this theorem of $\mathbf{IPC}$.

This observation shows that we can not ignore the natural order of implications in the statements. Hence, we can not follow the Zermelo approach in a very natural way of ignoring orders in interpreting the implications. But is there any way to deal with these kinds of referring problems in the Zermelo approach? Can we handle it? In [1] we showed that by some natural techniques, it is possible to use an untyped language to describe the hierarchical world of proofs. However, we have to emphasize that those techniques make the whole work too complicated to follow. For more information, see [1].

Another approach is the Russellian approach. In spite of the Zermelo approach, it is based on using a typed language to reflect the hierarchical nature of the world in a very syntactical way. Here again, the main example is set theory, in this case, the Russellian one. As it is well-known, it limits the syntax of the language in a way that we can not use statements such as $a\in b$ in which the level of $b$ is less than or equal to the level of $a$. Now, consider using this approach for the world of proofs. It is clear that instead of just one implication, we need a hierarchy of implications, $\{\rightarrow_{n}\}_{n=0}^{\infty}$ to reflect the hierarchical concept of provability. Moreover, we have to limit the formulas in the language in a way that $A\rightarrow_{n}B$ is a formula iff $n$ is larger than all the indices of the implications in $A$ and $B$. It means that the implication $\rightarrow_{n}$ refers to a higher level than the implications in $A$ or $B$. In the following, we will persue the Russellian approach. Indeed, we will use the above mentioned language to formalize the hierarchical world of proofs on the one hand, and define the BHK interpretation as the intended interpretation of this language on the other. Then, we will establish the soundness-completeness results for some of the propositional logics with respect to their canonical BHK interpretations. These logics can be considered as the description of different kinds of behaviors of the hierarchies of provabilities.

2 Preliminaries

Our main strategy to prove the soundness-completeness theorems for our propositional logics is reducing them to the soundness-completeness theorems for their modal counterparts introduced in [2]. In this section we will cover what we need from [2] to follow this strategy.

First of all we need a new modal language to capture the provability-based behavior of hierarchies:

Definition 2.1**.**

Consider the language of modal logics with infinitely many modalities, $\{\Box_{n}\}_{n=0}^{\infty}$, The set of formulas in this language, $\mathcal{L}_{\infty}^{\Box}$, is defined as the least set of expressions which includes all atomic formulas and is closed under all boolean operations and also the following operation: If $A\in\mathcal{L}_{\infty}^{\Box}$ and $n$ is bigger than all indices of boxes occurred in $A$ then $\Box_{n}A\in\mathcal{L}_{\infty}^{\Box}$. In other words, $A\in\mathcal{L}_{\infty}^{\Box}$, if $A$ is a usual formula in the modal language and also the index of any box is bigger than the indices of all other boxes in its scope.

The intuition behind this definition is that the outer box refers to the provability predicate of a meta-theory and the inner boxes refer to the lower theories in the hierarchy. Therefore, it seems natural to assume that the situation in which a theory speaks about itself or higher theories, should be considered as a syntactical error.

After introducing the language, we need the intended semantics. The following is a formalization of the combination of a real world which atomic statements informally refer to, and the hierarchy of theories, meta-theories, meta-meta-theories and so on to interpret the boxes in the language.

Definition 2.2**.**

A provability model is a pair $(M,\{T_{n}\}_{n=0}^{\infty})$ where $M$ is a model of $I\Sigma_{1}$ and $\{T_{n}\}_{n=0}^{\infty}$ is a hierarchy of arithmetical r.e. theories such that for any $n$, $I\Sigma_{1}\subseteq T_{n}\subseteq T_{n+1}$ provably in $I\Sigma_{1}$.

We also need the notions of arithmetical substitution, evaluation of modal formulas by substitutions and finally the satisfaction relation:

Definition 2.3**.**

Let $(M,\{T_{n}\}_{n=0}^{\infty})$ be a provability model and $A\in\mathcal{L}_{\infty}^{\Box}$ be a formula. Then by an arithmetical substitution $\sigma$, we mean a function from atomic formulas to the set of arithmetical sentences. Moreover, by $A^{\sigma}$ we mean an arithmetical sentence which is resulted by substituting the atomic formulas by $\sigma$ and interpreting any $\Box_{n}$ as the provability predicate of $T_{n}$. The interpretation of boolean connectives are themselves. Moreover, if $\Gamma$ is a sequence of formulas $A_{i}$, by $\Gamma^{\sigma}$ we mean the sequence of $A_{i}^{\sigma}$.

Definition 2.4**.**

Let $(M,\{T_{n}\}_{n=0}^{\infty})$ be a provability model and $A\in\mathcal{L}_{\infty}^{\Box}$ be a formula. Then we say $(M,\{T_{n}\}_{n=0}^{\infty})\vDash A$ if for any arithmetical substitution $\sigma$, $M\vDash A^{\sigma}$. Moreover, if $\Gamma$ and $\Delta$ are sequences of formulas and $\mathcal{C}$ a class of provability models, by $\mathcal{C}\vDash\Gamma\Rightarrow\Delta$, we mean that for any $(M,\{T_{n}\}_{n=0}^{\infty})\in\mathcal{C}$, and for any arithmetical substitution $\sigma$, if $M\vDash\bigwedge\Gamma^{\sigma}$, then $M\vDash\bigvee\Delta^{\sigma}$.

So far, we have defined provability models to capture the informal hierarchical concept of provability and also we introduced an appropriate language to reflect these models. Next is a definition of some of the natural modal theories in this language to formalize some of the natural properties of hierarchies:

Definition 2.5**.**

Consider the following set of axioms:

• $(\mathbf{H})$

$\Box_{n}A\rightarrow\Box_{n+1}A$

• $(\mathbf{K}_{h})$

$\Box_{n}(A\rightarrow B)\rightarrow(\Box_{n}A\rightarrow\Box_{n}B)$

• $(\mathbf{4}_{h})$

$\Box_{n}A\rightarrow\Box_{n+1}\Box_{n}A$

• $(\mathbf{D}_{h})$

$\neg\Box_{n}\bot$

• $(\mathbf{L}_{h})$

$\Box_{n+1}(\Box_{n}A\rightarrow A)\rightarrow\Box_{n}A$

• $(\mathbf{T}_{h})$

$\Box_{n}A\rightarrow A$

• $(\mathbf{5}_{h})$

$\neg\Box_{n}A\rightarrow\Box_{n+1}\neg\Box_{n}A$

Let $X$ be a set of these axioms. By $L(X)$ we mean the least set of formulas in $\mathcal{L}_{\infty}^{\Box}$, which contains all classical tautologies on formulas in $\mathcal{L}_{\infty}^{\Box}$, includes all instances of the set $X$ and is closed under the following rules:

• $(\mathbf{MP})$

If $A\in L(X)$ and $A\rightarrow B\in L(X)$ then $B\in L(X)$.

• $(\mathbf{NC}_{h})$

If $A\in L(X)$ then $\Box_{n}A\in L(X)$.

Moreover, if $\Gamma\cup\{A\}\subseteq\mathcal{L}_{\infty}$, by $\Gamma\vdash_{L(X)}A$ we mean that there exists a finite set $\Delta\subseteq\Gamma$ such that $L(X)\vdash\bigwedge\Delta\rightarrow A$.

Finally, we define $\mathbf{K4}_{h}=L(\mathbf{H},\mathbf{K}_{h},\mathbf{4}_{h})$, $\mathbf{KD4}_{h}=L(\mathbf{H},\mathbf{K}_{h},\mathbf{4}_{h},\mathbf{D}_{h})$, $\mathbf{S4}_{h}=L(\mathbf{H},\mathbf{K}_{h},\mathbf{4}_{h},\mathbf{T}_{h})$, $\mathbf{GL}_{h}=L(\mathbf{H},\mathbf{K}_{h},\mathbf{4}_{h},\mathbf{L}_{h})$, $\mathbf{KD45}_{h}=L(\mathbf{H},\mathbf{K}_{h},\mathbf{D}_{h},\mathbf{4}_{h},\mathbf{5}_{h})$ and $\mathbf{S5}_{h}=L(\mathbf{H},\mathbf{K}_{h},\mathbf{4}_{h},\mathbf{T}_{h},\mathbf{5}_{h})$.

Fortunately, some of these logics have a nice proof theoretic behavior. For instance, the logics $\mathbf{K4}_{h}$, $\mathbf{KD4}_{h}$ and $\mathbf{S4}_{h}$ have reasonable sequent calculi which have the cut elimination property. To introduce them, consider the following set of rules:

Axioms:

[TABLE]

Structural Rules:

[TABLE]

Propositional Rules:

[TABLE]

Modal Rules:

[TABLE]

[TABLE]

The condition of applying the rules $\Box_{4_{h}}R$, $\Box_{D_{h}}R$ and $\Box_{S_{h}}R$ is that for all $i\in I$, $n_{i}<n$.

The system $G(\mathbf{K4}_{h})$ is the system that consists of the axioms, structural rules, propositional rules and the modal rule $\Box_{4_{h}}R$. $G(\mathbf{KD4}_{h})$ is $G(\mathbf{K4}_{h})$ plus the rule $\Box_{D_{h}}R$ and finally, $G(\mathbf{S4}_{h})$ is the system $G(\mathbf{K4}_{h})$ when we replace the rule $\Box_{4_{h}}R$ by $\Box_{S_{h}}R$ and add the rule $\Box_{h}L$.

Theorem 2.6**.**

[2]** The systems $G(\mathbf{K4}_{h})$, $G(\mathbf{KD4}_{h})$ and $G(\mathbf{S4}_{h})$ are equivalent to the logics $\mathbf{K4}_{h}$, $\mathbf{KD4}_{h}$ and $\mathbf{S4}_{h}$, respectively. Moreover, all of these sequent calculi have the cut elimination property.

Using these sequent calculi we also proved the strong disjunction property.

Definition 2.7**.**

Logic $L$ has the strong disjunction property if for all formulas $\Box_{n}A$ and $\Box_{m}B$, if $L\vdash\Box_{n}A\vee\Box_{m}B$ then $L\vdash A$ or $L\vdash B$.

Theorem 2.8**.**

(Strong disjunction property) [2] All of the logics $\mathbf{K4}_{h}$, $\mathbf{KD4}_{h}$, $\mathbf{S4}_{h}$ and $\mathbf{GL}_{h}$ have strong disjunction property.

And finally, the natural classes of provability models and the soundness-completeness theorem:

Definition 2.9**.**

• $(i)$

The class of all provability models will be denoted by $\mathbf{PrM}$.

• $(ii)$

A provability model $(M,\{T_{n}\}_{n=0}^{\infty})$ is called consistent if for any $n$, $M$ thinks that $T_{n}$ is consistent and $T_{n+1}\vdash\mathrm{Cons}(T_{n})$, i.e. $M\vDash\mathrm{Cons}(T_{n})$ and $M\vDash\mathrm{Pr}_{T_{n+1}}(\mathrm{Cons}(T_{n}))$. Moreover, the class of all consistent provability models will be denoted by $\mathbf{Cons}$.

• $(iii)$

A provability model $(M,\{T_{n}\}_{n=0}^{\infty})$ is reflexive if for any $n$, $M$ thinks that $T_{n}$ is sound and $T_{n+1}\vdash\mathrm{Rfn}(T_{n})$, i.e. $M\vDash\mathrm{Pr}_{T_{n}}(A)\rightarrow A$ and $M\vDash\mathrm{Pr}_{T_{n+1}}(\mathrm{Pr}_{T_{n}}(A)\rightarrow A)$ for any sentence $A$. Moreover, the class of all reflexive provability models will be denoted by $\mathbf{Ref}$.

• $(iv)$

A provability model $(M,\{T_{n}\}_{n=0}^{\infty})$ is constant if for any $n$ and $m$, $(M,\{T_{n}\}_{n=0}^{\infty})$ thinks that $T_{n}=T_{m}$, i.e. $M\vDash\mathrm{Pr}_{T_{m}}(A)\leftrightarrow\mathrm{Pr}_{T_{n}}(A)$ and $M\vDash\mathrm{Pr}_{T_{0}}(\mathrm{Pr}_{T_{m}}(A)\leftrightarrow\mathrm{Pr}_{T_{n}}(A))$ for any sentence $A$. The class of all constant provability models will be denoted by $\mathbf{Cst}$.

Theorem 2.10**.**

(Soundness-Completeness)[2]

• $(i)$

$\Gamma\vdash_{\mathbf{K4}_{h}}A$* iff $\mathbf{PrM}\vDash\Gamma\Rightarrow A$.*

• $(ii)$

$\Gamma\vdash_{\mathbf{KD4}_{h}}A$* iff $\mathbf{Cons}\vDash\Gamma\Rightarrow A$.*

• $(iii)$

$\Gamma\vdash_{\mathbf{S4}_{h}}A$* iff $\mathbf{Ref}\vDash\Gamma\Rightarrow A$.*

• $(iv)$

$\Gamma\vdash_{\mathbf{GL}_{h}}A$* iff $\mathbf{Cst}\vDash\Gamma\Rightarrow A$.*

3 Russellian Propositional Logics

In this section we will define an appropriate language to capture the hierarchical nature of intuitionism and its BHK interpretation. Then we will define some natural theories in this language and finally we will use the Gödel translation to find a connection between these propositional logics and the modal systems introduced in the Preliminaries.

Definition 3.1**.**

Consider the language of propositional logics in which the implication is replaced by infinitely many implications, $\{\rightarrow_{n}\}_{n=1}^{\infty}$. Define the set of formulas, $\mathcal{L}_{\infty}$, as the least set of expressions that includes all atomic variables, $\top$ and $\bot$, closed under conjunction and disjunction and finally closed under the following operation: If $A,B\in\mathcal{L}_{\infty}$, and $n$ is strictly greater than all numbers occurring as indices of implications in $A$ and $B$, then $A\rightarrow_{n}B\in\mathcal{L}_{\infty}$.

Remark 3.2**.**

For the simplicity, negations are not assumed as primitives in the language. But for any type of implication, we can define $\neg_{n}A$ as $A\rightarrow_{n}\bot$.

Just like the modal language introduced in the Preliminaries, we assume that the indices of implications should be in an increasing order. The reason again is that we think that the situation in which a theory speaks about itself or the higher levels in the hierarchy should be considered as a syntactical error. This is actually the essence of the Russellian approach discussed in the Introduction. To have an example, notice that the expression $((p\rightarrow_{1}q)\wedge r)\rightarrow_{2}s$ is a formula in the language $\mathcal{L}_{\infty}$, while the expression $(p\rightarrow_{1}(q\rightarrow_{1}r))$ is not. The reason is that in the second expression the theory $T_{1}$ speaks about the provability behavior of itself which is not valid.

To introduce some formal systems in this language, consider the following set of natural deduction rules:

Propositional Rules:

[TABLE]

Formalized Rules:

[TABLE]

[TABLE]

Structural Rules:

[TABLE]

Moreover, consider the following set of rules:

[TABLE]

The condition for the rule $H$ is that $m\geq n$ and the condition of applying the rule $\rightarrow I$ is that $n$ should be strictly greater than all the indices occurred in the hypothesis of the deduction, including $A$.

The logic $\mathbf{BPC}_{h}$ is defined as the system consists of the propositional rules, the structural rules and the formalized rules. Then $\mathbf{EBPC}_{h}$ is defined as $\mathbf{BPC}_{h}+C$, $\mathbf{FPL}_{h}$ is defined as $\mathbf{BPC}_{h}+L$, $\mathbf{IPC}_{h}$ is defined as $\mathbf{BPC}_{h}+R$ and finally $\mathbf{CPC}_{h}$ is defined as $\mathbf{IPC}_{h}+D$.

Remark 3.3**.**

Consider the following rules:

[TABLE]

It is possible to define $\mathbf{EBPC}_{h}$ as $\mathbf{BPC}_{h}+D^{\prime}$ and define $\mathbf{IPC}_{h}$ as $\mathbf{BPC}_{h}+R^{\prime}$. It is clear that $D^{\prime}$ and $R^{\prime}$ are special cases of $D$ and $R$, respectively. Therefore it remains to show that $D^{\prime}$ and $R^{\prime}$ can simulate $D$ and $R$, respectively. The following proofs show that it is the case:

[TABLE]

Remark 3.4**.**

The usual logics $\mathbf{BPC}$, $\mathbf{EBPC}$, $\mathbf{IPC}$ and $\mathbf{CPC}$ are defined just like their counterparts replacing all $\rightarrow_{n}$ by $\rightarrow$. (See [5], [3].) Moreover, the logic $\mathbf{FPL}$ is defined as $\mathbf{BPC}$ plus the following rule (See [5]):

[TABLE]

It is also possible to define $\mathbf{FPL}$ as $\mathbf{BPC}$ plus the rule:

[TABLE]

The equivalence of these two definitions, is based on the fact that the first rule is a special case of the second rule when we have $A=\top$ and the following proof which shows that the first is also powerful enough to simulate the second:

[TABLE]

Notice that the double lines mean simple sub-proofs that we do not mention and $(*)$ is the sub-proof which proves

[TABLE]

Remark 3.5**.**

In the untyped case of logics introduced in Remark 3.4, there is no need to add the rule $tr$, simply because it is admissible. It is enough to put a proof for $\Gamma,A\vdash B$ under the proof of $\Gamma^{\prime}\vdash A$ to have a proof for $\Gamma,\Gamma^{\prime}\vdash B$. Unfortunately, this is not the case for the typed version. The reason is simple: If we put the proof of $\Gamma^{\prime}\vdash A$ under the proof of $\Gamma,A\vdash B$ it means that we keep the structure of two proofs, by changing the premises to the set $\Gamma\cup\Gamma^{\prime}$. But then it is possible that some applications of the rule $\rightarrow I$ become invalid simply because it is possible to have formulas in the set $\Gamma^{\prime}$ with greater indices. To have an example, consider the following trees:

[TABLE]

The left tree is a valid proof while the right one is not. The reason is that in applying the rule $\rightarrow I$ in $(**)$, the index $1$ is not greater than all the indices occurring in the premises which is $2$, in this case. But in the left tree, applying $\rightarrow I$ in $(*)$ is valid because there is no index in the premises which in this case is the empty set.

In the following we will define the provability interpretation (BHK interpretation) of the statements in the propositional language $\mathcal{L}_{\infty}$:

Definition 3.6**.**

Let $(M,\{T_{n}\}_{n=0}^{\infty})$ be a provability model and $A\in\mathcal{L}_{\infty}$ a formula. Then by an arithmetical substitution $\sigma$ we mean a function from atomic formulas to the set of arithmetical sentences. Moreover, define $A^{\sigma}$ as follows:

• $(i)$

If $p$ is an atomic formula, $p^{\sigma}=\mathrm{Pr}_{0}(\sigma(p))$. Moreover, $\top^{\sigma}=\mathrm{Pr}_{0}(\top)$ and $\bot^{\sigma}=\mathrm{Pr}_{0}(\bot)$.

• $(ii)$

$(B\circ C)^{\sigma}=B^{\sigma}\circ C^{\sigma}$ for all $\circ\in\{\wedge,\vee\}$.

• $(iii)$

$(A\rightarrow_{n}B)^{\sigma}=\mathrm{Pr}_{n}(A^{\sigma}\rightarrow B^{\sigma})$.

Moreover, if $\Gamma$ is a sequence of formulas $A_{i}$, by $\Gamma^{\sigma}$ we mean the sequence of $A_{i}^{\sigma}$.

Definition 3.7**.**

Let $(M,\{T_{n}\}_{n=0}^{\infty})$ be a provability model and $A\in\mathcal{L}_{\infty}$ a formula. Then we say $(M,\{T_{n}\}_{n=0}^{\infty})\vDash A$ if for any arithmetical substitution $\sigma$, $M\vDash A^{\sigma}$. Moreover, if $\Gamma$ and $\Delta$ are sequences of formulas and $\mathcal{C}$ a class of provability models, by $\mathcal{C}\vDash\Gamma\Rightarrow\Delta$, we mean that for any $(M,\{T_{n}\}_{n=0}^{\infty})\in\mathcal{C}$, and for any arithmetical substitution $\sigma$, if $M\vDash\bigwedge\Gamma^{\sigma}$, then $M\vDash\bigvee\Delta^{\sigma}$.

Let us illuminate this definition by an example:

Example 3.8**.**

Consider the pair $(\mathbb{N},\{T_{n}\}_{n=0}^{\infty})$ in which $T_{0}=\mathrm{PA}$ and $T_{n+1}=T_{n}+\mathrm{Rfn}(T_{n})$. First of all, it is easy to check that this pair is a reflexive provability model. Secondly, we want to show that this model satisfies the statement $(A\wedge(A\rightarrow_{n}B))\rightarrow_{n+1}B$. To show this fact, suppose that $\sigma$ is an arbitrary arithmetical substitution, then we have to show

[TABLE]

which holds because $T_{n+1}$ has the reflection principle for the theory $T_{n}$. Specially, $T_{n+1}\vdash\Box_{n}(A^{\sigma}\rightarrow B^{\sigma})\rightarrow(A^{\sigma}\rightarrow B^{\sigma})$.

In the remaining part of this section we will introduce the Gödel translation $b:\mathcal{L}_{\infty}\to\mathcal{L}_{\infty}^{\Box}$ and we will show its soundness-completeness property.

Definition 3.9**.**

The translation $b:\mathcal{L}_{\infty}\to\mathcal{L}_{\infty}^{\Box}$ is defined as follows:

$(i)$

$p^{b}=\Box_{0}p$, $\top^{b}=\Box_{0}\top$ and $\bot^{b}=\Box_{0}\bot$.

$(ii)$

$(A\wedge B)^{b}=A^{b}\wedge B^{b}$

$(iii)$

$(A\vee B)^{b}=A^{b}\vee B^{b}$

$(iv)$

$(A\to_{n}B)^{b}=\Box_{n}(A^{b}\to B^{b})$

Remark 3.10**.**

It is possible to have a similar translation $b^{\prime}:\mathcal{L}\to\mathcal{L}_{\Box}$ which is like the translation $b$ except in the implicational case which is defined as $(A\rightarrow B)^{b^{\prime}}=\Box(A^{b^{\prime}}\rightarrow B^{b^{\prime}})$. Since it is possible to recognize from the context that which translation we are using, we will use $b$ for $b^{\prime}$ as well.

First we need the following important lemma which intuitively states that all translated formulas are boxed inherently:

Lemma 3.11**.**

$\mathbf{K4}_{h}\vdash A^{b}\rightarrow\Box_{n}A^{b}$.

Proof.

The proof is by induction on the complexity of $A$. If $A$ is an atom, $\top$ or $\bot$, we have $A^{b}=\Box_{0}(A)$. Therefore, by axiom $\mathbf{4}_{h}$, we have $\mathbf{K4}_{h}\vdash\Box_{0}A\rightarrow\Box_{n}\Box_{0}A$. For conjunction, by IH we have $\mathbf{K4}_{h}\vdash B^{b}\rightarrow\Box_{n}B^{b}$ and $\mathbf{K4}_{h}\vdash C^{b}\rightarrow\Box_{n}C^{b}$, therefore, we have $\mathbf{K4}_{h}\vdash B^{b}\wedge C^{b}\rightarrow\Box_{n}(B^{b}\wedge C^{b})$. For disjunction, by IH, we have $\mathbf{K4}_{h}\vdash B^{b}\rightarrow\Box_{n}B^{b}$ and $\mathbf{K4}_{h}\vdash C^{b}\rightarrow\Box_{n}C^{b}$. Therefore, $\mathbf{K4}_{h}\vdash B^{b}\vee C^{b}\rightarrow\Box_{n}B^{b}\vee\Box_{n}C^{b}$ and since $\mathbf{K4}_{h}\vdash\Box_{n}B^{b}\vee\Box_{n}C^{b}\rightarrow\Box_{n}(B^{b}\vee C^{b})$, we have the claim. For the implication $B\rightarrow_{m}C$, again by $\mathbf{4}_{h}$, we have $\mathbf{K4}_{h}\vdash\Box_{m}(B^{b}\rightarrow C^{b})\rightarrow\Box_{n}\Box_{m}(B^{b}\rightarrow C^{b})$. ∎

We need the following theorems about the systems $\mathbf{FPL}$, $\mathbf{GL}$, $\mathbf{FPL}_{h}$ and $\mathbf{GL}_{h}$. The strategy is reducing the soundness-completeness of the translation $b$ between $\mathbf{FPL}_{h}$ and $\mathbf{GL}_{h}$ to the soundness-completeness between $\mathbf{FPL}$ and $\mathbf{GL}$.

Theorem 3.12**.**

[5]** $\Gamma\vdash_{\mathbf{FPL}}A$ iff $\Gamma^{b}\vdash_{\mathbf{GL}}A^{b}$.

Definition 3.13**.**

Let $A$ be a usual propositional formula. By a witness $w$ for $A$ we mean an assignment which assigns natural numbers to implications in a way that if $n$ is assigned to the implication in $A\rightarrow B$ then $n$ should be strictly greater than all numbers assigned to the implications in $A$ and $B$. Moreover, by $A(w)$ we mean a formula in $\mathcal{L}_{\infty}$ substituting any occurrence of implication with $\rightarrow_{n}$ when $n$ is a number which $w$ assigns to that occurrence. Moreover, by the forgetful translation $f:\mathcal{L}_{\infty}\to\mathcal{L}$ we mean a function which translates atomic formulas, conjunctions and disjunctions to themselves and sends $\rightarrow_{n}$ to $\rightarrow$. Notice that there exists a witness $w$ for $A^{f}$ such that $A^{f}(w)=A$.

Lemma 3.14**.**

• $(i)$

For any $A\in\mathcal{L}_{\infty}$ and any natural numbers $m,n$ greater than all the indices in $A$ and $B$, $A\rightarrow_{m}B\vdash_{\mathbf{FPL}_{h}}A\rightarrow_{n}B$.

• $(ii)$

For any $A\in\mathcal{L}$ and any witnesses $u$ and $v$ for $A$, $A(u)\vdash_{\mathbf{FPL}_{h}}A(v)$

Proof.

For $(i)$ it is enough to show that if $n$ is greater than all indices in $A$ and $B$, $A\rightarrow_{n+1}B\vdash_{\mathbf{FPL}_{h}}A\rightarrow_{n}B$. We have $A\rightarrow_{n+1}B\vdash_{\mathbf{FPL}_{h}}(A\wedge(A\rightarrow_{n}B)\rightarrow_{n+1}B)$. By the rule $L$

[TABLE]

hence $A\rightarrow_{n+1}B\vdash_{\mathbf{FPL}_{h}}A\rightarrow_{n}B$.

For $(ii)$. Use induction on $A$. The atomic case and the case for conjunction and disjunction are easy to check. For the implicational case assume $A=B\rightarrow C$. Then we know that $u=(u^{\prime},n,u^{\prime\prime})$ and $v=(v^{\prime},m,v^{\prime\prime})$ such that $n$ is bigger than all numbers in $u^{\prime}$ and $u^{\prime\prime}$ and also $m$ is bigger than all numbers in $v^{\prime}$ and $v^{\prime\prime}$. Pick $k=max\{m,n\}$. By IH, $B(v^{\prime})\vdash_{\mathbf{FPL}_{h}}B(u^{\prime})$ and $C(u^{\prime\prime})\vdash_{\mathbf{FPL}_{h}}C(v^{\prime\prime})$ Therefore, $\mathbf{FPL}_{h}\vdash B(v^{\prime})\rightarrow_{k}B(u^{\prime})$ and $\mathbf{FPL}_{h}\vdash C(u^{\prime\prime})\rightarrow_{k}C(v^{\prime\prime})$. By $tr_{f}$ we have $B(u^{\prime})\rightarrow_{k}C(u^{\prime\prime})\vdash_{\mathbf{FPL}_{h}}B(v^{\prime})\rightarrow_{k}C(v^{\prime\prime})$. On the other hand by $(i)$ we have $B(u^{\prime})\rightarrow_{n}C(u^{\prime\prime})\vdash_{\mathbf{FPL}_{h}}B(u^{\prime})\rightarrow_{k}C(u^{\prime\prime})$ and $B(v^{\prime})\rightarrow_{k}C(v^{\prime\prime})\vdash_{\mathbf{FPL}_{h}}B(v^{\prime})\rightarrow_{m}C(v^{\prime\prime})$ hence $B(u^{\prime})\rightarrow_{n}C(u^{\prime\prime})\vdash_{\mathbf{FPL}_{h}}B(v^{\prime})\rightarrow_{m}C(v^{\prime\prime})$. ∎

Theorem 3.15**.**

• $(i)$

If $\Gamma\vdash_{\mathbf{FPL}_{h}}A$ then $\Gamma^{f}\vdash_{\mathbf{FPL}}A^{f}$.

• $(ii)$

Let $\Gamma\cup\{A\}\subseteq\mathcal{L}$ be a set of usual propositional formulas and $w$ and $w^{\prime}$ are witnesses for $\Gamma$ and $A$ respectively, then if $\Gamma\vdash_{\mathbf{FPL}}A$ then $\Gamma(w)\vdash_{\mathbf{FPL}_{h}}A(w^{\prime})$.

Proof.

$(i)$ is clear by the Remark 3.4. For $(ii)$, use induction on the length of the proof of $A$. The important cases are the axiom case, the case of $\rightarrow I$ and the case of $tr_{f}$.

1. For the axiom case, we have $A\in\Gamma$. Assume that the witness for $A$ in $\Gamma$ is $u$, then by Theorem 3.14, $A(u)\vdash_{\mathbf{FPL}_{h}}A(w^{\prime})$ which completes the proof.

2. For the $\rightarrow I$ case, if $w=(u,n,v)$ then by IH, we know that $\Gamma(w),B(u)\vdash_{\mathbf{FPL}_{h}}C(v)$. Pick $k$ bigger than all numbers in $w$, $u$ and $v$. Then by $\rightarrow I$ in $\mathbf{FPL}_{h}$ we have $\Gamma(w)\vdash_{\mathbf{FPL}_{h}}B(u)\rightarrow_{k}C(v)$. Now by Theorem 3.14, we will have $\Gamma(w)\vdash_{\mathbf{FPL}_{h}}B(u)\rightarrow_{n}C(v)$.

3. For the $tr$ case, assume that $w^{\prime}=(u,n,v)$. Pick $y$ as a witness for $C$ and $k$ bigger than all numbers in $w$, $w^{\prime}$ and $y$. By IH, we have $\Gamma(w)\vdash_{\mathbf{FPL}_{h}}B(u)\rightarrow_{k}C(y)$ and $\Gamma(w)\vdash_{\mathbf{FPL}}C(y)\rightarrow_{k}D(v)$, then by $tr_{f}$ in $\mathbf{FPL}_{h}$ we have $\Gamma(w)\vdash_{\mathbf{FPL}_{h}}B(u)\rightarrow_{k}D(v)$. Finally by using the Theorem 3.14 part $(i)$, $\Gamma(w)\vdash_{\mathbf{FPL}_{h}}B(u)\rightarrow_{n}D(v)$. ∎

It is time to prove the soundness-completeness of the translation $b$.

Theorem 3.16**.**

(Soundness-completeness of $b$)

• $(i)$

$\Gamma\vdash_{\mathbf{BPC}_{h}}A$* iff $\Gamma^{b}\vdash_{\mathbf{K4}_{h}}A^{b}$.*

• $(ii)$

$\Gamma\vdash_{\mathbf{EBPC}_{h}}A$* iff $\Gamma^{b}\vdash_{\mathbf{KD4}_{h}}A^{b}$.*

• $(iii)$

$\Gamma\vdash_{\mathbf{IPC}_{h}}A$* iff $\Gamma^{b}\vdash_{\mathbf{S4}_{h}}A^{b}$.*

• $(iv)$

$\Gamma\vdash_{\mathbf{FPL}_{h}}A$* iff $\Gamma^{b}\vdash_{\mathbf{GL}_{h}}A^{b}$.*

Proof.

(Soundness of the translation $b$). The proof is by induction on the length of the proofs in the propositional logics. More precisely, if we denote the propositional logic by $L$ and its modal counterpart by $L_{\Box}$, then we will show that if $\Gamma\vdash_{L}A$ then $L_{\Box}\vdash\bigwedge\Gamma^{b}\rightarrow A^{b}$.

1. For the rules $\wedge I$, $\wedge E$, $\vee I$ and $\vee E$, the claim is easy to check. It is just an easy consequence of the fact that the translation $b$ commutes with conjunctions and disjunctions.

The following cases for the rules $\rightarrow I$, $\bot$ and the formalized rules are shown for $\mathbf{K4}_{h}$ but the proof for the other modal logics are the same.

2. For the rule $\rightarrow I$, by IH, we have $L_{\Box}\vdash\bigwedge\Gamma^{b}\wedge A^{b}\rightarrow B^{b}$. Therefore, $L_{\Box}\vdash\bigwedge\Gamma^{b}\rightarrow(A^{b}\rightarrow B^{b})$. Since $n$ is bigger than all the indices in the statement $\bigwedge\Gamma^{b}\rightarrow(A^{b}\rightarrow B^{b})$, by necessitation, we have

[TABLE]

By the use of the axiom $\mathbf{K}_{h}$, we have

[TABLE]

By Lemma 3.11, we have

[TABLE]

therefore, by $(*)$ and the definition of $b$,

[TABLE]

3. For the rule $\bot$, by induction on $A$ we will show that $L_{\Box}\vdash\Box_{0}\bot\rightarrow A^{b}$. For the atomic case, we have $L_{\Box}\vdash\bot\rightarrow p$, therefore by necessitation and the axiom $\mathbf{K}_{h}$ we have $L_{\Box}\vdash\Box_{0}\bot\rightarrow\Box_{0}p$ which is what we wanted. The conjunction and dijunction cases are easy to check. For the implication, we have $L_{\Box}\vdash\bot\rightarrow(A^{b}\rightarrow B^{b})$. Hence, $L_{\Box}\vdash\Box_{n}\bot\rightarrow\Box_{n}(A^{b}\rightarrow B^{b})$. Since $0\leq n$, $L_{\Box}\vdash\Box_{0}\bot\rightarrow\Box_{n}\bot$, thus $L_{\Box}\vdash\Box_{0}\bot\rightarrow(A\rightarrow_{n}B)^{b}$.

For the rule $tr$, by IH if $L_{\Box}\vdash\bigwedge\Gamma^{b}\rightarrow A^{b}$ and $L_{\Box}\vdash\bigwedge\Gamma^{\prime b}\wedge A^{b}\rightarrow B^{b}$, then we obviously have $L_{\Box}\vdash\bigwedge\Gamma^{b}\wedge\bigwedge\Gamma^{\prime b}\rightarrow B^{b}$.

4. The case of formalized $\land I$, formalized $\vee E$ and $tr$. For the formalized $\wedge I$, by IH, we have

[TABLE]

and

[TABLE]

therefore, by some applications of the axiom $\mathbf{K}_{h}$ and the modus ponens rule, we have

[TABLE]

which completes the proof. The case for formalized $\vee E$ and $tr$ are the same.

5. For the rule $C$, by IH, we have

[TABLE]

By Lemma 3.11, $\mathbf{K4}_{h}\vdash A^{b}\rightarrow\Box_{n}A^{b}$ and

[TABLE]

we have

[TABLE]

and since $\mathbf{KD4}_{h}\vdash\Box_{n}\bot\rightarrow\bot$ and $\mathbf{KD4}_{h}\vdash\bot\rightarrow\Box_{0}\bot$ then

[TABLE]

For the rule $R$ by IH, we have

[TABLE]

By Lemma 3.11, $\mathbf{K4}_{h}\vdash A^{b}\rightarrow\Box_{n}A^{b}$, which means

[TABLE]

we know that $\mathbf{S4}\vdash\Box_{n}B^{b}\rightarrow B^{b}$, hence

[TABLE]

And finally for the rule, $L$, by IH

[TABLE]

which means

[TABLE]

therefore

[TABLE]

hence $\mathbf{GL}_{h}\vdash(A\rightarrow_{n}B)^{b}$. ∎

Proof.

(Completeness of the translation $b$.) For the completeness part for the logics $\mathbf{BPC}_{h}$, $\mathbf{EBPC}_{h}$ and $\mathbf{IPC}_{h}$ we will use the sequent calculi for $\mathbf{K4}_{h}$, $\mathbf{KD4}_{h}$ and $\mathbf{S4}_{h}$ as introduced in the Preliminaries. Moreover, the structure of the proof for all of these logics are the same. Therefore, we will prove their completeness theorems simultaneously. To achieve this goal, denote the propositional logic by $L$, its modal counterpart by $L_{\Box}$ and the sequent calculi for $L_{\Box}$ by $G(L_{\Box})$. Assume that $\Gamma^{b}\vdash_{L_{\Box}}A^{b}$. Then $G(L_{\Box})\vdash\Gamma^{b}\Rightarrow A^{b}$. Hence, there is a cut-free proof for $\Gamma^{b}\Rightarrow A^{b}$. Call it $\pi$. It is obvious that all the formulas occurring in $\pi$ are sub-formulas of $A^{b}$ or sub-formulas of the elements of $\Gamma^{b}$. We know that all of these sub-formulas have the following forms: $B^{b}$; $B^{b}\rightarrow C^{b}$ and atoms $p$. ($\top$ and $\bot$ are considered as atomic in this proof.) Therefore, every sequent in $\pi$ has the following form:

[TABLE]

We will prove the following claim:

Claim. If

[TABLE]

then for any $X\subseteq I$

[TABLE]

The proof is by induction on the length of the cut-free proof in $G(L_{\Box})$. The case for axioms and structural rules are easy to check. If the last rule is a conjunction or a disjunction rule, then the main formula is in the first form. Then since it is possible to simulate all conjunction and disjunction rules in $\mathbf{BPC}_{h}$, the case of conjunction and disjunction rules are also easy to check. If the last rule is an implication rule, since we define our claim up to using implicational rules, there is nothing to prove in this case. Finally, if the last rule is a modal rule, then, we have different cases:

1. The case $L=\mathbf{K4}_{h}$. If the last rule is a modal rule, based on the form of the formulas and the fact that in those three forms a boxed formula should have the first form, we have two cases. The first case is when the boxed formula in the right side has the form $\Box_{n}(D^{b}\rightarrow E^{b})$. The second case is when the formula has the form $\Box_{0}p$. For the first case, the last rule has the following form:

[TABLE]

By IH and for any $X\subseteq I$ and $Y\subseteq R$ we have

[TABLE]

and we want to prove

[TABLE]

First notice that we know $n>n_{i}$, therefore by the rule $\rightarrow I$ the following is provable by $\Sigma=\{p_{j}\}_{j\in J}\cup\{B_{i}\rightarrow_{n_{i}}C_{i}\}_{i\in I}$

[TABLE]

Fix $i\in I$ and also fix some $Z\subseteq I-\{i\}$. Both of the following statements are theorems of $\Sigma$:

[TABLE]

and

[TABLE]

Since $\Sigma\vdash B_{i}\rightarrow_{n_{i}}C_{i}$ by using the rule $H$ and the fact that $n_{i}<n$, we will have $\Sigma\vdash\mathbf{B_{i}}\rightarrow_{n}\mathbf{C_{i}}$. Then by using appropriate formalized rules we have

[TABLE]

provable by $\Sigma$ in $\mathbf{BPC}_{h}$. By iterating this method we can eliminate all the elements in $I$ and finally for any $Y\subseteq R$, we have

[TABLE]

Define $\Sigma^{\prime}=\Sigma+\{F_{r}\rightarrow_{n}G_{r}\}_{r\in R}$. Therefore for any any $Y\subseteq R$

[TABLE]

but $\Sigma^{\prime}\vdash_{\mathbf{BPC}_{h}}F_{r}\rightarrow_{n}G_{r}$, hence by the same method as above we can eliminate $R$ and hence we will have

[TABLE]

which is what we wanted to prove.

If the boxed formula in the right side of the rule is $\Box_{0}p$, since [math] is the lowest possible index, the rule has the following form:

[TABLE]

therefore, by IH, $\{p_{j}\}_{j\in J}\vdash_{\mathbf{BPC}_{h}}p$, which is what we wanted.

2. The case $L=\mathbf{KD4}_{h}$. If the last rule is $\Box_{4_{h}}R$, the proof is the same as the case 1. If the last rule is $\Box_{D_{h}}R$, then everything in the proof is the same as the proof for case 1 when we put $D=\top$ and $E=\bot$. Therefore, we have

[TABLE]

Then by the rule $C$, we will have

[TABLE]

which is what we wanted.

3. The case $L=\mathbf{S4}_{h}$. If the last rule is $\Box_{S_{h}}R$, then the proof is similar to the case 1. If the last rule is $\Box_{h}L$, then there are two cases. First, the case in which the boxed formula has the form $\Box_{n}(B^{b}\rightarrow C^{b})$. And the second case in which the boxed formula has the form $\Box_{0}p$. For the first case, the rule should have the following form:

[TABLE]

Therefore by IH, for any $X\subseteq I$ and $Y\subseteq R$ we have

[TABLE]

and

[TABLE]

Since

[TABLE]

and we have $B\rightarrow_{m}C,B\vdash_{\mathbf{IPC}_{h}}C$, then

[TABLE]

By using some appropriate formalized rule and $tr$ on $C$ we will have

[TABLE]

which is what we wanted. The second case is straightforward by IH.

After proving the claim, the theorem is an easy consequence: Since there is a proof of $\Gamma^{b}\Rightarrow A^{b}$ in $G(L_{\Box})$, then by claim we have $\Gamma\vdash_{L}A$.

For the logic $\mathbf{GL}_{h}$, if $\Gamma^{b}\vdash_{\mathbf{GL}_{h}}A^{b}$ then by using the forgetful translation, which forgets the indices of the boxes, we will have $(\Gamma^{b})^{f}\vdash_{\mathbf{GL}}(A^{b})^{f}$. Since for any formula $X\in\mathcal{L}_{\infty}$, $(X^{b})^{f}=(X^{f})^{b}$, hence $(\Gamma^{f})^{b}\vdash_{\mathbf{GL}}(A^{f})^{b}$. Therefore by completeness of $b$ between $\mathbf{GL}$ and $\mathbf{FPL}$, we have $\Gamma^{f}\vdash_{\mathbf{FPL}}A^{f}$. Define $w_{\Gamma}$ and $w_{A}$ such that $\Gamma^{f}(w_{\Gamma})=\Gamma$ and $A^{f}(w_{A})=A$. Then by Theorem 3.15 we have $\Gamma^{f}(w_{\Gamma})\vdash_{\mathbf{FPL}_{h}}A^{f}(w_{A})$ which completes the proof. ∎

And the final part of this section contains the proof of the fact that these propositional logics have the disjunction property, as we expect for any constructive logic:

Theorem 3.17**.**

All of the logics $\mathbf{BPC}_{h}$, $\mathbf{EBPC}_{h}$, $\mathbf{IPC}_{h}$ and $\mathbf{FPL}_{h}$ have disjunction property.

Proof.

The proof for all of these logics are the same. Assume $L$ is one of the mentioned propositional logics, and $L_{\Box}$ is its modal counterpart. Then if $L\vdash A\vee B$ then by soundness of the translation $b$, $L_{\Box}\vdash A^{b}\vee B^{b}$. Then, by Lemma 3.11, we have $L_{\Box}\vdash\Box_{n}A^{b}\vee\Box_{m}B^{b}$ for some big enough $m$ and $n$. Then by strong disjunction property for $L_{\Box}$, Theorem 2.8, we have: $L_{\Box}\vdash A^{b}$ or $L_{\Box}\vdash B^{b}$. Therefore, by completeness of the translation $b$, we will have $L\vdash A$ or $L\vdash B$. ∎

4 Soundness-Completeness Theorems

In this section we will prove the soundness-completeness theorems for propositional logics that we introduced in the previous section. To do so, we have to define the notion of a BHK model. It is clear that formalizing the BHK interpretation needs formalizing two different kinds of conditions: The first is the way that the BHK interpretation interprets propositional connectives and the second is the consistency assumption which states that there is no proof for inconsistency. For the first one, we defined the satisfaction relation between provability models and propositional formulas exactly as what the BHK interpretation demands. For the second condition, we need the following discussion: First of all, it seems clear that the natural formalization of this condition is the consistency assumption on the provability model which states that $M\vDash\neg\mathrm{Pr}_{n}(\bot)$ for all $n\geq 0$. But we have to notice that in the intuitionistic tradition everything should be also reflected in the level of provability. To implement this idea, there are two possible natural ways: The first one is assuming that the meta-theory of $T_{n}$ is strong enough to prove its consistency, i.e. $M\vDash\mathrm{Pr}_{n+1}(\neg\mathrm{Pr}_{n}(\bot))$. This statement seems totally natural to assume, but the cost is a lot. In fact, it makes the BHK interpretation much more limited than what we expected. For instance, on the one hand, the statement $(\top\rightarrow_{n}\bot)\rightarrow_{n+1}\bot$ would be valid in all the BHK models which means that $\mathbf{BHK}\vDash(\top\rightarrow_{n}\bot)\rightarrow_{n+1}\bot$ and on the other hand, $(\top\rightarrow_{n}\bot)\rightarrow_{n+1}\bot$ is the essential axiom of $\mathbf{EBPC}_{h}$. Therefore, there is no BHK characterization of logics below $\mathbf{EBPC}_{h}$ which is not what we expected. The second approach is based on assuming a weaker version which states that $T_{n+1}$ can not prove the inconsistency of $T_{n}$, i.e $M\vDash\neg\mathrm{Pr}_{n+1}(\mathrm{Pr}_{n}(\bot))$ for all $n\geq 0$. This formalization seems more liberal than the first one, and we will choose it as our formalization. Notice that for the logics above $\mathbf{EBPC}_{h}$, this condition is not needed, since the provability models are strong enough to satisfy it automatically.

Definition 4.1**.**

A provability model $(M,\{T_{n}\}_{n=0}^{\infty})$ is called a BHK model if for all $n\geq 0$, $M\vDash\neg\mathrm{Pr}_{n+1}(\mathrm{Pr}_{n}(\bot))$. We will denote the class of all BHK models by $\mathbf{BHK}$ and the class of all constant BHK models by $\mathbf{cBHK}$.

Theorem 4.2**.**

(Soundness-Completeness)

• $(i)$

$\Gamma\vdash_{\mathbf{BPC}_{h}}A$* iff $\mathbf{PrM}\vDash\Gamma\Rightarrow A$. Moreover, $\mathbf{BPC}_{h}\vdash A$ iff $\mathbf{BHK}\vDash A$.*

• $(ii)$

$\Gamma\vdash_{\mathbf{EBPC}_{h}}A$* iff $\mathbf{Cons}\vDash\Gamma\Rightarrow A$.*

• $(iii)$

$\Gamma\vdash_{\mathbf{IPC}_{h}}A$* iff $\mathbf{Ref}\vDash\Gamma\Rightarrow A$.*

• $(iv)$

$\Gamma\vdash_{\mathbf{FPL}_{h}}A$* iff $\mathbf{Cst}\vDash\Gamma\Rightarrow A$. Moreover, $\mathbf{FPL}_{h}\vdash A$ iff $\mathbf{cBHK}\vDash A$.*

• $(v)$

There is no BHK model $(M,\{T_{n}\}_{n=0}^{\infty})$ such that $(M,\{T_{n}\}_{n=0}^{\infty})\vDash\mathbf{CPC}_{h}$.

Proof.

First of all notice that for any formula $A\in\mathcal{L}_{\infty}$ and any provability model $(M,\{T_{n}\}_{n=0}^{\infty})$, $(M,\{T_{n}\}_{n=0}^{\infty})\vDash A$ is equivalent to $(M,\{T_{n}\}_{n=0}^{\infty})\vDash A^{b}$ by definition. Therefore $(i)$, $(ii)$, $(iii)$ and $(iv)$ are easy consequences of the Theorem 3.16 and the soundness-completeness theorem of the corresponding modal logics (Theorem 2.10). The remaining part is the completeness theorem for the classes $\mathbf{BHK}$ and $\mathbf{cBHK}$ for $\mathbf{BPC}_{h}$ and $\mathbf{FPL}_{h}$, respectively. For $\mathbf{BPC}_{h}$, define $\Delta$ as the set consisting of all instances of the formula $\neg\Box_{n+1}\Box_{n}\bot$ for any $n\geq 0$. Notice that $(M,\{T_{n}\}_{n=0}^{\infty})\vDash\Delta$, iff $(M,\{T_{n}\}_{n=0}^{\infty})$ is a BHK model. Since $(M,\{T_{n}\}_{n=0}^{\infty})\vDash A$ is equivalent to $(M,\{T_{n}\}_{n=0}^{\infty})\vDash A^{b}$, and since $\mathbf{BHK}\vDash A$, hence $\mathbf{PrM}\vDash\Delta\Rightarrow A^{b}$. By completeness of $\mathbf{K4}_{h}$, we have $\Delta\vdash_{\mathbf{K4}_{h}}A^{b}$. Therefore, there are finite instances of the formulas in $\Delta$ such that $\{\neg\Box_{n_{i}+1}\Box_{n_{i}}\bot\}_{i=0}^{r}\vdash_{\mathbf{K4}_{h}}A^{b}$. Hence,

[TABLE]

Since by the axiom $\mathbf{H}$ we can increase $n_{i}$’s, w.l.o.g assume $n_{i}>0$. Moreover we have $\mathbf{K4}_{h}\vdash\Box_{n_{i}+1}\Box_{n_{i}}\bot\rightarrow\Box_{n_{i}+1}\Box_{n_{i}}\Box_{0}\bot$ and also we know that $(\top\rightarrow_{n_{i}+1}(\top\rightarrow_{n_{i}}\bot))^{b}$ is equivalent to $\Box_{n_{i}+1}\Box_{n_{i}}\Box_{0}\bot$ provably in $\mathbf{K4}_{h}$, hence

[TABLE]

and by completeness of the translation $b$, Theorem 3.16, we have

[TABLE]

By the disjunction property of $\mathbf{BPC}_{h}$, Theorem 3.17, we have $\mathbf{BPC}_{h}\vdash A$ or for some $i$, $\mathbf{BPC}_{h}\vdash(\top\rightarrow_{n_{i}+1}(\top\rightarrow_{n_{i}}\bot))$. The latter is impossible because if $\mathbf{BPC}_{h}\vdash(\top\rightarrow_{n_{i}+1}(\top\rightarrow_{n_{i}}\bot))$ then by the soundness of $\mathbf{BPC}$, the formula $(\top\rightarrow_{n_{i}+1}(\top\rightarrow_{n_{i}}\bot))$ should be true in the provability model $(\mathbb{N},\{I\Sigma_{1}\}_{n=0}^{\infty})$. It means that $\mathbb{N}\vDash\mathrm{Pr}_{n_{i}+1}(\mathrm{Pr}_{n_{i}}(\mathrm{Pr}_{0}(\bot)))$. Hence, $I\Sigma_{1}\vdash\mathrm{Pr}_{I\Sigma_{1}}(\mathrm{Pr}_{I\Sigma_{1}}(\bot))$ which also means that $I\Sigma_{1}\vdash\bot$ which is not the case. Hence, $\mathbf{BPC}_{h}\vdash A$. The case for $\mathbf{FPL}_{h}$ is exactly the same.

For $(v)$, we will prove the claim by contradiction. Firstly, we want to show that the following two statements hold:

• $(i)$

$M$ thinks that $T_{2}\vdash\mathrm{Pr}_{1}(\mathrm{Pr}_{0}(\bot))\rightarrow\mathrm{Pr}_{0}(\bot)$ (a weak version of the provability of the consistency assumption).

• $(ii)$

For any arithmetical statement $\phi$, $M$ thinks

[TABLE]

(a weak version of the axiom $\mathbf{5}_{h}$).

For $(i)$, consider the formula $(\top\rightarrow_{1}\bot)\rightarrow_{2}\bot$. Since it is a theorem of $\mathbf{CPC}_{h}$, then

[TABLE]

and therefore, we will have $(i)$.

Secondly, we know $\mathbf{CPC}_{h}\vdash p\vee\neg_{1}p$. Hence, for any arithmetical substitution $\sigma$ we have $(M,\{T_{n}\}_{n=0}^{\infty})\vDash\mathrm{Pr}_{0}(p^{\sigma})\vee\mathrm{Pr}_{1}(\mathrm{Pr}_{0}(p^{\sigma})\rightarrow\mathrm{Pr}_{0}(\bot))$. Therefore, if we assume $p^{\sigma}=\phi$, then $(ii)$ follows.

Using these two statements, we will reach the contradiction. First of all, to simplify the proof, we will use $\mathrm{Pr}(A)$ for $\mathrm{Pr}_{S}$ in which $S=T_{1}+\mathrm{Cons}(T_{0})$. Put $\phi=\mathrm{Pr}(\bot)$, then $(ii)$ would be equivalent to

[TABLE]

On other hand by the formalized $\Sigma_{1}$-completeness, we have

[TABLE]

hence,

[TABLE]

Moreover, by $\Sigma_{1}$-completeness, we have

[TABLE]

Therefore,

[TABLE]

And since $M\vDash I\Sigma_{1}$, we have

[TABLE]

Based on Gödel’s second incompleteness theorem formalized in $I\Sigma_{1}$, we can conclude

[TABLE]

On the other hand, since $(M,\{T_{n}\}_{n=0}^{\infty})$ is a BHK model, we have $M\vDash\neg\mathrm{Pr}_{1}(\mathrm{Pr}_{0}(\bot)),$ hence $M\vDash\neg\mathrm{Pr}(\bot)$. Since $M\vDash I\Sigma_{1}$, $M\vDash\neg\mathrm{Pr}(\neg\mathrm{Pr}(\perp)).$ Therefore, $M\vDash\mathrm{Pr}_{0}(\mathrm{Pr}(\bot))$ and thus by the definition of $S$ we have $M\vDash\mathrm{Pr}_{0}(\mathrm{Pr}_{1}(\mathrm{Pr}_{0}(\bot))).$ By $(i)$, $M\vDash\mathrm{Pr}_{2}(\mathrm{Pr}_{1}(\mathrm{Pr}_{0}(\bot))\rightarrow\mathrm{Pr}_{0}(\bot))$. Since $M\vDash\mathrm{Pr}_{0}(\mathrm{Pr}_{1}(\mathrm{Pr}_{0}(\bot)))$, we have $M\vDash\mathrm{Pr}_{2}(\mathrm{Pr}_{0}(\bot))$. Therefore, we have $M\vDash\mathrm{Pr}_{2}(\mathrm{Pr}_{1}(\bot))$ which contradicts with the condition of being a BHK model. Therefore, we reach a contradiction and it proves the theorem. ∎

Acknowledgment. We wish to thank Raheleh Jalali and Masoud Memarzadeh for their careful reading of the earlier draft and their useful comments.