A General Axiomatization for the logics of the Hierarchy ${\mathbb{I}}^n {\mathbb{P}}^k$

TL;DR

This paper introduces a unified axiomatization for a family of logical systems that generalize weakly-intuitionistic and paraconsistent logics, providing a formal framework and natural ordering.

Contribution

It presents a general axiomatization for the hierarchy ${\mathbb{I}}^n {\mathbb{P}}^k$ using finite matrices, unifying and extending previous logics.

Findings

The family ${\mathbb{I}}^n {\mathbb{P}}^k$ can be ordered naturally.

An adequate axiomatics for each logic $I^n P^k$ is established.

The logics are formally defined and characterized.

Abstract

In this paper, the logics of the family ${\mathbb{I}}^n {\mathbb{P}}^k$:=$\{{ I^n P^k}\}_{(n,k) \in \omega^2}$ are formally defined by means of finite matrices, as a simultaneous generalization of the weakly-intuitionistic logic $I^1$ and of the paraconsistent logic $P^1$. It is proved that this family can be naturally ordered, and it is shown an adequate axiomatics for each logic of the form $I^n P^k$.

Full text

Keywords: Many-Valued Logic; Paraconsistent Logic; Completeness Proofs.

MSC 2010: 03B50, 03B53

1 Introduction and preliminaries

The propositional logic ${P^{1}}$ was defined by A. Sette in [11], within the context of a wide research about Paraconsistent Logic developed in the 70’s. It possesses special characteristics that distinguish it from the family $\{C^{n}\}_{\{0\leq n\leq\omega\}}$, the fundamental paraconsistent hierarchy (see [3]). Among other properties, even when $P^{1}$ can be defined by means of a Hilbert-Style axiomatics, it can be also obtained by means of a finite matrix (meanwhile no one of the $C^{n}$-logics can be characterized in this way). The matrix semantics for $P^{1}$ is built taking as basis a set of three truth-values: $T_{0}$ and $F_{0}$ (intended as the “classical truth-values”) together with $T_{1}$ (which can be associated to an “intermediate truth”). Besides that, $P^{1}$ is maximal w.r.t to the propositional classical logic (${CL}$), in the sense that, if any axiom-schema (independent of the original ones) is added to the axiomatics of ${P^{1}}$, then this new axiomatics generates ${CL}$. Finally, $P^{1}$ is algebraizable, as it was shown in [6].

As a dual counterpart of this logic, A. Sette and W. Carnielli defined in [12] the logic ${I^{1}}$, which, in general terms, shares with $P^{1}$ several properties among the already mentioned (finite axiomatizability, maximality relative to ${CL}$ and algebraizability). Besides that, one of the more remarkable differences between ${I^{1}}$ and ${P^{1}}$ is the following: in ${P^{1}}$ is not valid the non-contradiction principle $NCP$: $\neg(\neg\phi\wedge\phi)$, but it holds the middle excluded principle $MEP$: $\neg\phi\vee\phi$. On the other hand, $I^{1}$ behaves exactly in the opposite way: it verifies $NCP$ and it does not verify $MEP$.

The logic ${I^{1}}$ is defined by means of a $3$-valued matrix, too: in this case (and unlike $P^{1}$), the “new truth value” is $F_{1}$, an “intermediate truth-value of falsehood”. Considering this fact, it was suggested in [12] a generalization of these logics by the addition of new intermediate truth-values, in such a way that the “new logics” already obtained constitute a family (which could be ordered in a natural way). Following (and simplifying at some extent) these suggestions, it was defined in [4] the family ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$ = $\{{I^{n}P^{k}}\}_{(n,k)\in\omega^{2}}$. Every member of ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$ (usually mentioned here just as an ${I^{n}P^{k}}$-logic) can be considered as a generalization of ${I^{1}}$ and of ${P^{1}}$ at the same time, by several reasons. First of all, the classical logic $CL$ can be identified simply with ${I^{0}P^{0}}$. Similarly, $P^{1}$ (resp. $I^{1}$) is simply ${I^{0}P^{1}}$ (resp. ${I^{1}P^{0}}$). Moreover, every ${I^{n}P^{k}}$-logic has $n+k+2$ truth-values (as it will be seen later). In addition, it can be estabilished an order relation within ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$ . The logics of this family fail to verify $NCP$ and/or $MEP$ (with the obvious exception of $I^{0}P^{0}$ that satisfies both properties). It is worth to comment that, since the ${I^{n}P^{k}}$-logics are finite-valued, and (mostly) paraconsistent/weakly-intuitionistic ones, they can be used as “laboratory logics” in the study of several interesting properties (see [2] or [10], for example).

However, an open problem referred to this family consists of providing an adequate (i.e. sound and complete) axiomatics for all the ${I^{n}P^{k}}$-logics. This paper is essentially devoted to offer a suitable axiomatics for them. Moreover, the soundness and completeness theorems shown here can be considered general in this sense: their proofs are given in such a way that the adequacity of all the logics of ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$ (w.r.t. to the axiomatics here presented) is demonstrated in a structured mode, common to any pair $(n,k)\in\omega^{2}$ previously fixed. The technique to prove this result is adapted to the well-known Kalmár’s method to prove completeness for $CL$ (see [8]).

To avoid unnecesary information or formalism, the notions to be used to prove adequacity will be reduced as much as possible (this entails that this paper will contain some notational abuses). Besides that, the structure of this article is as follows: in the next section the ${I^{n}P^{k}}$-logics will be defined by means of finite matrices, some simple properties will be shown here, and it will be defined an order relation $\preceq$ in the family ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$ (this justifies the expression “hierarchy” used for this family). In addition, it will be demonstrated that ${I^{n_{1}}P^{k_{1}}}\preceq{I^{n_{2}}P^{k_{2}}}$ if and only if $(n_{2},k_{2})\leq(n_{1},k_{1})$. In Section 3, it will presented a general axiomatics for all the $I^{n}P^{k}$-logics and it will proven some properties, which are essential to the proof of adequacity (result developed in Section 4). For that, it is assumed that the reader is familiarized with the notions of formal proof, schema axioms, inference rules and so on, within the context of Hilbert-Style axiomatics. So, the definitions of these concepts (and other related ones) will be omitted. This paper concludes with some comments about future work.

2 Semantic Presentation of the Hierarchy ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$

To define a matrix semantics for the logics of the family ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$, it is necessary to start with the definition of the language $L(C)$, common to all the $I^{n}P^{k}$-logics:

Definition 2.1

The set of connectives of all the $I^{n}P^{k}$-logics is $C$:=$\{\neg,\rightarrow\}$, with obvious arities. The language $L(C)$ (or set of formulas) for the $I^{n}P^{k}$-logics is the algebra of words generated by $C$ over a countable set $\mathcal{V}$, in the usual way.

Along this paper, the uppercase greek letters $\Gamma,\Delta,\Sigma\dots$ denote sets of formulas of $L(C)$. In addition, the lowercase greek letters $\phi$, $\psi$, $\theta$ are metavariables ranging over the individual formulas of $L(C)$. Finally, the letters $\alpha$, $\alpha_{1}$, $\alpha_{2},\dots$ will be used as metavariables referred only to the atomic formulas (that is, the elements of $\mathcal{V}$). All these notations can be used with subscripts, when neccesary. On the other hand, the expression $\phi[\alpha_{1},\dots,\alpha_{m}]$ indicates that the atomic formulas ocurring on $\phi$ are precisely $\alpha_{1},\dots,\alpha_{m}$ (this expression will be applied in the developement of the completeness proof).

Despite their common language, the difference between each one of the $I^{n}P^{k}$-logics is given by their respective matrix semantics, defined as follows:

Definition 2.2

Let $(n,k)\in\omega^{2}$, with $\omega$ = $\{0,1,2,\dots\}$. The matrix $M(n,k)$ is defined as a pair $M_{(n,k)}$ = $(({A_{(n,k)}},C_{(n,k)}),D_{(n,k)})$, where:

a) $(A_{(n,k)},C_{(n,k)})$ is an algebra, similar to $L(C)$, with support

$A_{(n,k)}$: = $\{F_{0},F_{1},\cdots,F_{n},T_{0},T_{1},\cdots T_{k}\}$ 222Every algebra $(A_{(n,k)},C_{(n,k)})$ will be identified with its support, if there is no risk of confussion.

b) $D_{(n,k)}$ = $\{T_{0},T_{1},\cdots T_{k}\}$.

In addition, The operations $\neg$ and $\rightarrow$ of $C_{(n,k)}$ (also called truth-functions) 333Strictly speaking, the operations of $C_{(n,k)}$ are not the connectives of $C$, of course. However, they will be denoted in the same way for the sake of simplicity. are defined by the truth tables indicated below.

\begin{array}[]{|c|c c c c|}\hline\cr&F_{0}&F_{r}&T_{i}&T_{0}\\ \hline\cr\neg&T_{0}&F_{r-1}&T_{i-1}&F_{0}\\ \hline\cr\end{array}

\begin{array}[]{|c|c c c c|}\hline\cr\rightarrow&F_{0}&F_{s}&T_{j}&T_{0}\\ \hline\cr F_{0}&T_{0}&T_{0}&T_{0}&T_{0}\\ F_{r}&T_{0}&T_{0}&T_{0}&T_{0}\\ T_{i}&F_{0}&F_{0}&T_{0}&T_{0}\\ T_{0}&F_{0}&F_{0}&T_{0}&T_{0}\\ \hline\cr\end{array}

With $1\leq r,s\leq n;\hskip 5.69046pt1\leq i,j\leq k$ .

Remark 2.3

Realize that the truth-values $F_{1},\dots,F_{n}$ can be considered informally as intermediate values of falsehood, meanwhile $T_{1},\dots,T_{k}$ are intermediate values of truth. In addition, every application of $\neg$ to a “non classical value”, approximates more and more the value to the “classical ones”, $F_{0}$ and $T_{0}$. Note that there are needed $n$ negations at most to pass from $F_{r}$ to $F_{0}$. Similarly, the values of the form $T_{i}$ “become” $T_{0}$ after $k$ negations at most. On the other hand, the implication $\rightarrow$ cannot distinguish between classical or intermediate truth-values: it just considers every value of the form $F_{i}$ as being $F_{0}$, and every value of the form $T_{j}$ as being $T_{0}$.

Taking into account the previous truth-tables, some secondary (and useful) truth-functions can be defined. As a motivation, it would be desirable that disjunction ($\vee$) and conjunction ($\wedge$) behave as $\rightarrow$ in this aspect: they cannot distinguish classical from intermediate truth-values. For that, it is taken as starting point the unary function of “classicalization” $\copyright$ (the meaning of this neologism is obvious), defined by $\copyright(A)$ := $(A\rightarrow A)\rightarrow A$, for every $A\in A_{(n,k)}$. So, the truth-table associated to it is

\begin{array}[]{|c|c c c c|}\hline\cr&T_{0}&T_{i}&F_{r}&F_{0}\\ \hline\cr\copyright&T_{0}&T_{0}&F_{0}&F_{0}\\ \hline\cr\end{array}

From $\copyright$ it is defined the truth-function $\sim$, of strong (also called classical) negation, as $\sim A$ : = $\neg(\copyright A)$. So, its associated truth-table is

\begin{array}[]{|c|c c c c|}\hline\cr&F_{0}&F_{r}&T_{i}&T_{0}\\ \hline\cr\sim&T_{0}&T_{0}&F_{0}&F_{0}\\ \hline\cr\end{array}

It is possible to define $\vee$ and $\wedge$ now, adapting the usual definition for $CL$: $A\vee B$:= $\sim A\rightarrow B$, meanwhile $A\wedge B$:= $\sim(A\rightarrow\,\sim B)$. For these connectives, their associated truth-functions are:

\begin{array}[]{|c|c c c c|}\hline\cr\vee&F_{0}&F_{s}&T_{j}&T_{0}\\ \hline\cr F_{0}&F_{0}&T_{0}&T_{0}&T_{0}\\ F_{r}&F_{0}&F_{0}&T_{0}&T_{0}\\ T_{i}&T_{0}&T_{0}&{T_{0}}&{T_{0}}\\ T_{0}&T_{0}&T_{0}&{T_{0}}&{T_{0}}\\ \hline\cr\end{array}                   \begin{array}[]{|c|c c c c|}\hline\cr\wedge&F_{0}&F_{s}&T_{j}&T_{0}\\ \hline\cr F_{0}&F_{0}&F_{0}&{F_{0}}&{F_{0}}\\ F_{r}&F_{0}&F_{0}&{F_{0}}&{F_{0}}\\ T_{i}&{F_{0}}&{F_{0}}&{T_{0}}&{T_{0}}\\ T_{0}&{F_{0}}&{F_{0}}&{T_{0}}&{T_{0}}\\ \hline\cr\end{array}

With $1\leq i,j\leq k;\hskip 5.69046pt1\leq r,s\leq n$.

From the previous definitions, it is clear that all the binary truth-functions consider all the non-designated values $F_{j}$ as behaving as $F_{0}$, and similarly for all the values $T_{i}$. The same fact holds for $\sim$. In the case of $\neg$, however, all the truth-values can be differentiated. This is the main difference of $\neg$ and $\sim$, and justifies the definition and the study of the $I^{n}P^{k}$-logics. For example, when $n\geq 1$, $MEP$: $\neg\phi\vee\phi$ it is not an $I^{n}P^{k}$-tautology (it is enough to consider a valuation $v$ such that $v(A)$ = $T_{i}$ with $i\geq 1$), meanwhile this principle is valid if $\neg$ is replaced by $\sim$. That is, $\models_{(n,k)}\sim\phi\vee\phi$ for any $I^{n}P^{k}$-logic. In a dual way, when $k\geq 1$, $\sim(\sim\phi\,\wedge\phi)$ is a $I^{n}P^{k}$-tautology. (for every $(n,k)\in\omega^{2}$), but $\neg(\neg\phi\wedge\phi)$ is not valid in all the $I^{n}P^{k}$-logics. Indeed, $\neg(\neg\phi\wedge\phi)$ is only valid in the $I^{n}P^{0}$-logics.

After a deeper analysis it is possible to see that, given a fixed logic $I^{n}P^{k}$, $\models_{(n,k)}\neg\phi\vee\phi$ iff $\phi$ = $\neg^{t}(\phi\rightarrow\theta)$ (with $t\geq 0$), or $\phi$ = $\neg^{t}\alpha$, with $\alpha\in\mathcal{V}$, with $t\geq n$: otherwise (when $\phi$ = $\neg^{t}\alpha$ with $t<n$) $\not\models_{(n,k)}\neg\phi\vee\phi$. In a similar way, $\models_{(n,k)}\neg(\neg\phi\wedge\phi)$ iff $\phi$ = $\neg^{t}(\psi\rightarrow\theta)$ with $t\geq 0$, or $\phi$ = $\neg^{t}\alpha$, with $t\geq k$, $\alpha\in\mathcal{V}$. From these comments can see that $NCP$ and $MEP$ are not valid in general terms. So, it is natural to distinguish between “well-behaved” formulas and “not well-behaved” ones (with respect to each of the mentioned principles). This distinction is formalized with the unary “well-behavior” truth-functions, defined in the obvious way: $A^{\ast}$:= $\neg A\vee A$; $A^{\circ}$:= $\neg(\neg A\wedge A)$, for every $A\in A_{(n,k)}$. Its respective truth-tables are

\begin{array}[]{|c|c c c c|}\hline\cr&F_{0}&F_{r}&T_{i}&T_{0}\\ \hline\cr^{\ast}&T_{0}&F_{0}&T_{0}&T_{0}\\ \hline\cr\end{array}                  \begin{array}[]{|c|c c c c|}\hline\cr&F_{0}&F_{r}&T_{i}&T_{0}\\ \hline\cr^{\circ}&T_{0}&T_{0}&F_{0}&T_{0}\\ \hline\cr\end{array}

Besides the behavior of the truth-function in each matrix $M_{(n,k)}$, recall that its definition is motivated by the definition of a consequence relation on $L(C)$ (and therefore of a logic), in the usual way:

Definition 2.4

An $M_{(n,k)}$-valuation is any homomorphism $v:L(C)\to A_{(n,k)}$ (this notion makes sense because $L(C)$ and ${A_{(n,k)}}$ are similar algebras). Recall here that every $M_{(n,k)}$-valuation can be defined just considering functions $v:\mathcal{V}\to A_{(n,k)}$ and extending it to all $L(C)$. The logic $I^{n}P^{k}$ is the pair $I^{n}P^{k}$:=$(C,\models_{(n,k)})$, being $\models_{(n,k)}\subseteq\wp(L(C))\times L(C)$ defined as usual: $\Gamma\models_{(n,k)}\phi$ iff, for very $M_{(n,k)}$-valuation $v$, $v(\Gamma)\subseteq D_{(n,k)}$ implies $v(\phi)\in D_{(n,k)}$. In this context, $\phi$ is an $I^{n}P^{k}$-tautology iff $\emptyset\models_{(n,k)}\phi$ (this fact will be denoted by $\models_{(n,k)}\phi$, as usual). The family $\{I^{n}P^{k}\}_{(n,k)\in\omega^{2}}$ will be denoted by ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$.

Remark 2.5

The family ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$. includes some well-known logics. Indeed, $I^{0}P^{0}$ is just the classical logic $CL$. On the other hand, the logic $I^{1}P^{0}$ is $I^{1}$ indeed meanwhile $I^{0}P^{1}$ is just $P^{1}$. In addition, all the $I^{n}P^{k}$-logics can be “naturally ordered”, taking into account the following definition:

Definition 2.6

The order relation \preceq\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}({\mathbb{I}}^{n}{\mathbb{P}}^{k})^{2} is defined in the following natural way: $I^{n_{1}}P^{k_{1}}\preceq I^{n_{2}}P^{k_{2}}$ iff, for every \Gamma\cup\{\phi\}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}L(C), $\Gamma\models_{(n_{1},k_{1})}\phi$ implies $\Gamma\models_{(n_{2},k_{2})}\phi$.**

Taking into account the previous definition, it is natural to visualize $({\mathbb{I}}^{n}{\mathbb{P}}^{k},\preceq)$ as a lattice:

Proposition 2.7

In the logic $I^{n}P^{k}$ ($n$, $k$ fixed), the following formulas are tautologies:

a) $\neg^{n+1}\phi\vee\neg^{n}\phi$                  ($(n+1)$-generalization of $MEP$.)

b) $\neg(\neg^{k+1}\phi\wedge\neg^{k}{\phi})$              ($(k+1)$-generalization of $NCP$).

Proposition 2.8

$I^{n_{1}}P^{k_{1}}\preceq I^{n_{2}}P^{k_{2}}$ iff $(n_{2},k_{2})\leq_{\Pi}(n_{1},k_{1})$ (being $\leq_{\Pi}$ the order of the product on $\omega^{2}$). Therefore, the Hierarchy $({\mathbb{I}}^{n}{\mathbb{P}}^{k},\preceq)$ is a lattice.

Proof: If $(n_{2},k_{2})\leq_{\Pi}(n_{1},k_{1})$, then A_{(n_{2},k_{2})}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}A_{(n_{1},k_{1})}, and D_{(n_{2},k_{2})}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}D_{(n_{1},k_{1})}. Now suppose that $\Gamma_{0}\not\models_{(n_{2},k_{2})}\phi_{0}$ for some \Gamma_{0}\cup\{\phi_{0}\}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}L(C). So, there exists a valuation $v:\mathcal{V}\to A_{(n_{2},k_{2})}$ such that v(\Gamma_{0})\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}D_{(n_{2},k_{2})}, $v(\phi_{0})\notin D_{(n_{2},k_{2})}$. Define the valuation $w:\mathcal{V}\to A_{(n_{1},k_{1})}$ as $w(\alpha)$ = $v(\alpha)$, for every $\alpha\in\mathcal{V}$. It can be proved that, for every $\psi\in L(C)$, $w(\psi)$ = $v(\psi)$. Thus, w(\Gamma_{0})\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}D_{(n_{2},k_{2})}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}D_{(n_{1},k_{1})} and w(\phi_{0})\in\{F_{0},\dots,F_{n_{2}}\}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}\{F_{0},\dots,F_{n_{1}}\}. That is, $\Gamma_{0}\not\models_{(n_{1},k_{1})}\phi_{0}$. The previous argument shows that $I^{n_{1}}P^{k_{1}}\preceq I^{n_{2}}P^{k_{2}}$.

For the converse, suppose $(n_{2},k_{2})\not\leq_{\Pi}(n_{1},k_{1})$. There are two cases that must be analyzed in different ways. First, if $n_{2}>n_{1}$ consider any formula $\phi_{1}$:= $\neg^{n_{1}+1}\alpha\vee\neg^{n_{1}}\alpha$, with $\alpha\in\mathcal{V}$. So, $\models_{(n_{1},k_{1})}\phi_{1}$, by Prop. 2.7.a). Now, defining the valuation $v_{1}:\mathcal{V}\to A_{(n_{2},k_{2})}$ by $v_{1}(\alpha)$:=$F_{n_{2}}$, it holds $v_{1}(\phi_{1})$ = $\neg^{n_{1}+1}F_{n_{2}}\vee\neg^{n_{1}}F_{n_{2}}$ = $F_{n_{2}-(n_{1}+1)}\vee F_{n_{2}-n_{1}}$ = $F_{0}$ (since $n_{1}+1\leq n_{2}$). Thus, $\not\models_{(n_{2},k_{2})}\phi_{1}$. On the other hand, if $k_{2}>k_{1}$, let $\phi_{2}$:=$\neg(\neg^{k_{1}+1}\alpha\wedge\neg^{k_{1}}\alpha)$. As in the first case, $\models_{(n_{1},k_{1})}\phi_{2}$, by Prop. 2.7.b). Now, if it is defined the valuation $v_{2}:\mathcal{V}\to A_{(n_{2},k_{2})}$ such that $v_{2}(\alpha)$ = $T_{k_{2}}$, then $\not\models_{(n_{1},k_{1})}\phi_{2}$ (note here that $k_{1}+1\leq k_{2}$). So, for both possibilities it holds $I^{n_{1}}P^{k_{1}}\not\preceq I^{n_{2}}P^{k_{2}}$. This concludes the proof.   $\Box$

Some consequences of the previous result, useful to visualize $\preceq$ (actually, its underlying strict order $\prec$) are the following:

Corollary 2.9

In ${I^{n}P^{k}}$ it holds that:

a) $I^{n+1}P^{k}\prec I^{n}P^{k}$.

b) $I^{n}P^{k+1}\prec I^{n}P^{k}$.

c) $I^{n}P^{k+1}$ and $I^{n+1}P^{k}$ are not comparables.

This section concludes with the mention of the following result that will be applied at the end of this paper:

Proposition 2.10

The consequence relation $\models_{(n,k)}$ verifies:

a) $\Gamma\models_{(n,k)}\phi$ implies $\Gamma\cup\{\psi\}\models_{(n,k)}\phi$ [Monotonicity]

b) $\Gamma,\phi\models_{(n,k)}\psi$ iff $\Gamma\models_{(n,k)}\phi\rightarrow\psi$ [Semantic Deduction Theorem]

c) If $\Gamma\models_{(n,k)}\phi$, then $\Gamma{{}^{\prime}}\models_{(n,k)}\phi$ for some finite set \Gamma{{}^{\prime}}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}\Gamma [Finitariness]

Proof: Obviously, it is holds a). The claim b) arises from the truth-table of $\rightarrow$. With respect to c), $\models_{(n,k)}$ is finitary because is naturally defined by means of a single finite matrix (result indebted to R. Wójcicki: see [13]). $\Box$

3 A Hilbert-Style Axiomatics for the $I^{n}P^{k}$-logics

From now on, consider an $I^{n}P^{k}$-logic fixed, with $(n,k)\in\omega^{2}$. To obtain the desired axiomatics, the secondary truth-functions $\sim$, $\copyright$, $\vee$ and $\wedge$ from the previous section will be reflected by means of the definition of secondary connectives in $L(C)$. Formally:

Definition 3.1

The secondary connectives $\sim$, $\copyright$, $\vee$, $\wedge$ are defined in $L(C)$ in the following way:

$\copyright\phi$:= $(\phi\rightarrow\phi)\rightarrow\phi$

$\sim\phi$:= $\neg(\copyright\phi)$

$\phi\vee\psi$:= $\sim\phi\rightarrow\psi$

$\phi\wedge\psi$:= $\sim(\phi\rightarrow\sim\psi)$.

$\phi^{\ast}$:= $\neg\phi\vee\phi$

$\phi^{\circ}$:= $\neg(\neg\phi\wedge\phi)$

In addition, the conncectives $\vee_{CL}$ and $\wedge_{CL}$ are defined by:

$\phi\vee_{CL}\psi$:= $\neg\phi\rightarrow\psi$

$\phi\wedge_{CL}\psi$:= $\neg(\phi\rightarrow\neg\psi)$ 444The “classical” connectives $\wedge_{CL}$ and $\vee_{CL}$ are not essential in the proof of Completeness. However, they are indicated here for a better explanation of the comparison between these connectives w.r.t $\wedge$ and $\vee$, as it will be remarked later..

Finally, the expression $\neg^{q}\phi$ indicates $\neg(\dots(\neg\phi))\dots)$, $q$ times. $\neg^{0}\phi$ is merely $\phi$.

Taking into account the previous conventions, the axiomatics for the $I^{n}P^{k}$-logics will be presented in the sequel. For that consider, from now on, an arbitrary (fixed) pair $(n,k)\in\omega^{2}$.

Definition 3.2

The consequence relation \vdash_{(n,k)}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}\wp(L(C))\times L(C) is defined by means of the following Hilbert-Style axiomatics, considering these schema axioms:

$Ax_{1}$ $\phi\rightarrow(\psi\rightarrow\phi)$

$Ax_{2}$ $(\phi\rightarrow(\psi\rightarrow\theta))\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\theta))$

$Ax_{3}$ $(\phi\rightarrow\psi)^{\ast}$

$Ax_{4}$ $(\phi\rightarrow\psi)^{\circ}$

$Ax_{5}$ $(\neg^{n}\phi)^{\ast}$

$Ax_{6}$ $(\neg^{k}\phi)^{\circ}$

$Ax_{7}$ $\phi^{\ast}\rightarrow[\psi^{\circ}\rightarrow((\neg\phi\rightarrow\neg\psi)\rightarrow((\neg\phi\rightarrow\psi)\rightarrow\phi))]$

$Ax_{8}$ $\phi^{\ast}\rightarrow[\psi^{\circ}\rightarrow((\phi\rightarrow\neg\psi)\rightarrow((\phi\rightarrow\psi)\rightarrow\neg\phi))]$

$Ax_{9}$ $\phi^{\ast}\rightarrow(\neg\neg\phi\rightarrow\phi)$

$Ax_{10}$ $\phi^{\circ}\rightarrow(\phi\rightarrow\neg\neg\phi)$

$Ax_{11}$ $\phi^{\ast}\rightarrow(\neg\phi)^{\ast}$

$Ax_{12}$ $\phi^{\circ}\rightarrow(\neg\phi)^{\circ}$

The only inference rule for this axiomatics is

\mbox{Modus Ponens (MP):}\hskip 14.22636pt\parbox{11.51393pt}{\raisebox{-28.45274pt}{\stackrel{{\scriptstyle\textstyle\underline{\hskip 8.5359pt\phi,\hskip 14.22636pt\phi\rightarrow\psi\hskip 8.5359pt}}}{{\psi}}}}\,.\hskip 14.22636pt

From this definition, the well-known notions of formal proof (with or without hypotheses), formal theorem, etc. are the usual. Because of this, $\vdash_{(n,k)}$ is monotonic: $\Gamma\vdash_{(n,k)}\phi$ implies $\Gamma\cup\{\psi\}\vdash_{(n,k)}\phi$. This fact will be widely used.

Remark 3.3

It is well known that the inclusion of $Ax_{1}$, $Ax_{2}$ and $MP$ entail that it is valid $\vdash_{(n,k)}\phi\rightarrow\phi$. Moreover:

Theorem 3.4

$\vdash_{(n,k)}$ satisfies the (syntactic) Deduction Theorem (DT). That is, $\Gamma,\phi\vdash_{(n,k)}\psi$ iff $\Gamma\vdash_{(n,k)}\phi\rightarrow\psi$.

Proof: This result holds because the inclusion of axioms $Ax_{1}$ and $Ax_{2}$ too, and considering that the only (primitive) inference rule is Modus Ponens. See [8] for a detailed proof. $\Box$

$Ax_{1}$ and $Ax_{2}$ allow to obtain some useful rules in relation to $\vdash_{(n,k)}$, too:

Proposition 3.5

Given the logic $I^{n}P^{k}$, the following secondary rules are valid:

Permutation (Perm):     

$\stackrel{{\scriptstyle\textstyle\underline{\hskip 8.5359pt\phi\rightarrow(\psi\rightarrow\theta)\hskip 8.5359pt}}}{{\psi\rightarrow(\phi\rightarrow\theta)}}$

 .

Transitivity (Trans):     

$\stackrel{{\scriptstyle\textstyle\underline{\hskip 8.5359pt\phi\rightarrow\psi,\hskip 14.22636pt\psi\rightarrow\theta\hskip 8.5359pt}}}{{\phi\rightarrow\theta}}$

 .

Reduction (Red):     

$\stackrel{{\scriptstyle\textstyle\underline{\hskip 8.5359pt(\phi\rightarrow\psi)\rightarrow\theta\hskip 8.5359pt}}}{{\psi\rightarrow\theta}}$

 .

The following two results involve formulas of the form $\phi^{\ast}$ or $\phi^{\circ}$:

Proposition 3.6

For every $\phi\in L(C)$, for every $(n,k)\in\omega^{2}$, it holds:

$\vdash_{(n,k)}(\phi^{\ast})^{\ast}$; $\vdash_{(n,k)}(\phi^{\ast})^{\circ}$; $\vdash_{(n,k)}(\copyright\,\phi)^{\ast}$; $\vdash_{(n,k)}(\copyright\,\phi)^{\circ}$.

This result is valid since $\phi^{\ast}$:= $\sim(\neg\phi)\rightarrow\phi$ and $\copyright\,\phi$ = $(\phi\rightarrow\phi)\rightarrow\phi$, and considering axioms $Ax_{3}$ and $Ax_{4}$ from Definition 3.2.

Proposition 3.7

If $\models_{(n,k)}\phi$, then $\vdash_{(n,k)}\phi^{\ast}$ and $\vdash_{(n,k)}\phi^{\circ}$.

Proof: If $\models_{(n,k)}\phi$ then (checking the truth-tables of $I^{n}P^{k}$) $\phi$ is necessarily of the form $\neg^{q}(\psi\rightarrow\theta)$, with $q\geq 0$. From this, apply $Ax_{3}$, $Ax_{4}$ (and, eventually, $Ax_{11}$ and $Ax_{12}$). $\Box$

The next result shows some basic $I^{n}P^{k}$-theorems:

Proposition 3.8

The following formulas of $L(C)$ are theorems w.r.t. $\vdash_{(n,k)}$ :

a) $\phi\rightarrow\copyright\phi$;                   a’) $\copyright\phi\rightarrow\phi$

b) $\phi^{\ast}\rightarrow(\sim\phi\rightarrow\neg\phi)$

c) $\phi^{\ast}\rightarrow[\psi^{\circ}\rightarrow((\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi))]$

d) $\phi^{\ast}\rightarrow[\psi^{\circ}\rightarrow((\phi\rightarrow\psi)\rightarrow(\neg\psi\rightarrow\neg\phi))]$

e) $(\sim\phi\rightarrow\sim\psi)\rightarrow((\sim\phi\rightarrow\copyright\psi)\rightarrow\copyright\phi)$

f) $(\sim\phi\rightarrow\sim\psi)\rightarrow((\sim\phi\rightarrow\psi)\rightarrow\phi))$

Proof: The following are schematic formal proofs (in the context of $\vdash_{(n,k)}$) for every formula above indicated. Sometimes it will be applied Theorem 3.4 or Proposition 3.5 without explicit mention.

For a): $\phi\rightarrow\copyright\phi$ = $\phi\rightarrow((\phi\rightarrow\phi)\rightarrow\phi)$ is a particular case of $Ax_{1}$. For the case of a’):

$1)$ $(\phi\rightarrow\phi)\rightarrow\phi$ [Hyp.; Def. $\copyright\phi$]

$2)$ $\phi\rightarrow\phi$ [Remark 3.3]

$3)$ $\phi$ [1), 2), MP]

So, it is valid $\copyright\phi\vdash_{(n,k)}\phi$.

For b):

$1)$ $\phi^{\ast}$ [Hyp.]

$2)$ $(\copyright\phi)^{\circ}$ [Prop. 3.6]

$3)$ $\phi^{\ast}\rightarrow[\,(\copyright\phi)^{\circ}\rightarrow((\phi\rightarrow\sim\phi)\rightarrow((\phi\rightarrow\copyright\phi)\rightarrow\neg\phi)]$ [$Ax_{8}$, Def. 3.1 (of $\sim$)]

$4)$ $(\phi\rightarrow\sim\phi)\rightarrow((\phi\rightarrow\copyright\phi)\rightarrow\neg\phi)$ [$1)$, $2)$, $3)$, MP ]

$5)$ $(\phi\rightarrow\copyright\phi)\rightarrow((\phi\rightarrow\sim\phi)\rightarrow\neg\phi)$ [$4)$, Perm.]

$6)$ $\phi\rightarrow\copyright\phi$ [a)]

$7)$ $(\phi\rightarrow\sim\phi)\rightarrow\neg\phi$ [$5)$, $6)$, MP]

$8)$ $\sim\phi\rightarrow(\phi\rightarrow\sim\phi)$ [$Ax_{1}$ ]

$9)$ $\sim\phi\rightarrow\neg\phi$ [$7)$, $8)$, Trans.]

That is, $\phi^{\ast}\vdash_{(n,k)}\sim\phi\rightarrow\neg\phi$.

For c):

$1)$ $\phi^{\ast}$ [Hyp.]

$2)$ $\psi^{\circ}$ [Hyp.]

$3)$ $\neg\phi\rightarrow\neg\psi$ [Hyp.]

$4)$ $\psi$ [Hyp.]

$5)$ $\psi\rightarrow(\neg\phi\rightarrow\psi)$ [$Ax_{1}$]

$6)$ $\neg\phi\rightarrow\psi$ [4), 5), MP]

$7)$ $\phi^{\ast}\rightarrow[\psi^{\circ}\rightarrow((\neg\phi\rightarrow\neg\psi)\rightarrow((\neg\phi\rightarrow\psi)\rightarrow\phi))]$ [$Ax_{7}$]

$8)$ $(\neg\phi\rightarrow\neg\psi)\rightarrow((\neg\phi\rightarrow\psi)\rightarrow\phi)$ [7), 1), 2), MP]

$9)$ $(\neg\phi\rightarrow\psi)\rightarrow\phi$ [8), 3), MP]

$10)$ $\phi$ [9), 6), MP]

Thus, $\phi^{\ast},\psi^{\circ},\neg\phi\rightarrow\neg\psi,\psi\vdash_{(n,k)}\phi$.

For d): adapt the proof of c), using $Ax_{8}$ instead of $Ax_{7}$. Then, it will be valid $\phi^{\ast},\psi^{\circ},\phi\rightarrow\psi,\neg\psi\vdash_{(n,k)}\neg\phi$.

For e):

$1)$ $(\copyright\phi)^{\ast}$ [Prop. 3.6 ]

$2)$ $(\copyright\psi)^{\circ}$ [Prop. 3.6]

$3)$ $(\copyright\phi)^{\ast}\rightarrow[(\copyright\psi)^{\circ}\rightarrow((\sim\phi\rightarrow\sim\psi)\rightarrow((\sim\phi\rightarrow\copyright\psi)\rightarrow\copyright\phi))]$

[Def. 3.1 (of $\sim$), $Ax_{7}$.]

$4)$ $(\sim\phi\rightarrow\sim\psi)\rightarrow((\sim\phi\rightarrow\copyright\psi)\rightarrow\copyright\phi)$ [1), 2), 3), MP]

So, $\vdash_{(n,k)}(\sim\phi\rightarrow\sim\psi)\rightarrow((\sim\phi\rightarrow\copyright\psi)\rightarrow\copyright\phi)$.

For f):

$1)$ $\sim\phi\rightarrow\sim\psi$ [Hyp.]

$2)$ $\sim\phi\rightarrow\psi$ [Hyp.]

$3)$ $\psi\rightarrow\copyright\psi$ [a)]

$4)$ $\sim\phi\rightarrow\copyright\psi$ [2), 3), Trans.]

$5)$ $(\sim\phi\rightarrow\sim\psi)\rightarrow((\sim\phi\rightarrow\copyright\psi)\rightarrow\copyright\phi))$ [e)]

$6)$ $\copyright\phi$ [1), 4), 5), MP]

$7)$ $\copyright\phi\rightarrow\phi$ [a’)]

$8)$ $\phi$ [6), 7), MP]

From all this, $\sim\phi\rightarrow\sim\psi,\sim\phi\rightarrow\psi\vdash_{(n,k)}\psi$. Now, apply Theorem 3.4, as in the previous results. This concludes the proof. $\Box$

Remark 3.9

Now is convenient to relate the axiomatics given in Definition 3.2 with a well-known axiomatics for $CL$ = $I^{0}P^{0}$. According [8], $CL$ can be axiomatized by MP joined with the following three schema axioms:

$Bx_{1}$ = $Ax_{1}$

$Bx_{2}$ = $Ax_{2}$

$Bx_{3}$ = $(\neg\phi\rightarrow\neg\psi)\rightarrow((\neg\phi\rightarrow\psi)\rightarrow\phi)$.

Note that, cf. Definition 3.2, fixed an arbitrary consequence relation $\vdash_{(n,k)}$, the axiom $Bx_{3}$ of the previous axiomatics is replaced by a weaker version ($Ax_{7}$). Anyway, since in the particular case of $\vdash_{(0,0)}$, axioms $Ax_{5}$ and $Ax_{6}$ establish that, for every formula $\phi\in L(C)$, $\vdash_{(0,0)}\phi^{\ast}$ and $\vdash_{(0,0)}\phi^{\circ}$, it is possible to recover the axiomatics determined by $Bx_{1}$, $Bx_{2}$ and $Bx_{3}$, actually. Moreover:

Proposition 3.10

Let $\phi\in L(C)$, in such a way that $\phi$ is a formal theorem of $CL$ (that is, $\vdash_{(0,0)}\phi$), and let $\phi{{}^{\prime}}\in L(C)$, obtained by $\phi$ replacing all the ocurrences of the symbol $\neg$ in $\phi$ by $\sim$. Then $\vdash_{(n,k)}\phi{{}^{\prime}}$.

Proof: Consider the axiomatics for $I^{0}P^{0}$ indicated in Remark 3.9, and compare it with the general axiomatics given in Definition 3.2. First of all note that neither $Bx_{1}$ (= $Ax_{1}$) nor $Bx_{2}$ (= $Ax_{2}$) have ocurrences of $\neg$. Besides, since $Bx_{3}$=$(\neg\phi\rightarrow\neg\psi)\rightarrow((\neg\phi\rightarrow\psi)\rightarrow\phi))$, and considering Prop. 3.8.f), it holds $\vdash_{(n,k)}(\sim\phi\rightarrow\sim\psi)\rightarrow((\sim\phi\rightarrow\psi)\rightarrow\phi)$ ( = ${Bx_{3}}{{}^{\prime}}$). From these facts, it can be easily proved by induction of the lenght of the formal proof of $\phi$ (w.r.t $\vdash_{(0,0)}$) that $\vdash_{(0,0)}\phi$ implies $\vdash_{(n,k)}\phi{{}^{\prime}}$. $\Box$

Corollary 3.11

Suppose $\phi\in L(C)$, and let the formula $\phi{{}^{\prime\prime}}\in L(C)$ built by $\phi$ replacing the eventual ocurrences of $\neg$ in $\phi$ by $\sim$, and replacing every ocurrence of $\vee_{CPL}$ (resp. $\wedge_{CPL}$), understood as an abbreviation (cf. Definition 3.1), by $\vee$ (resp. $\wedge$). Then, $\vdash_{(0,0)}\phi$ implies $\vdash_{(n,k)}\phi{{}^{\prime\prime}}$.

For instance, since $\vdash_{(0,0)}\neg\phi\vee_{CL}\phi$, then $\vdash_{(n,k)}\sim\phi\vee\phi$. However, it is not generally valid that $\vdash_{(n,k)}\neg\phi\vee_{CL}\phi$, obviously. The next result collects some particular cases of the previous corollary:

Corollary 3.12

The relation $\vdash_{(n,k)}$ verifies, given $(n,k)\in\omega^{2}$:

a) $\vdash_{(n,k)}\phi\rightarrow\phi\vee\psi$;                    a’) $\vdash_{(n,k)}\psi\rightarrow\phi\vee\psi$

b) $\vdash_{(n,k)}\phi\wedge\psi\rightarrow\phi$;                    b’) $\vdash_{(n,k)}\phi\wedge\psi\rightarrow\psi$

c) $\vdash_{(n,k)}(\phi\rightarrow\theta)\rightarrow((\psi\rightarrow\theta)\rightarrow(\phi\vee\psi\rightarrow\theta))$

d) $\vdash_{(n,k)}\phi\rightarrow(\psi\rightarrow(\phi\wedge\psi))$.

e) $\vdash_{(n,k)}\phi\wedge\psi\rightarrow\phi\vee\psi$.

Finally, to prove Completeness, it will be necessary:

Proposition 3.13

The following are $I^{n}P^{k}$-theorems:

a) $\phi\rightarrow\phi^{\ast}$

b) $\phi^{\circ}\rightarrow(\neg\phi\rightarrow(\phi\rightarrow\psi))$

c) $(\phi^{\circ})^{\circ}$

d) $\neg(\phi^{\ast})\rightarrow\phi^{\circ}$

e) $\,\sim\phi\rightarrow\phi^{\circ}$

f) $\phi^{\ast}\rightarrow(\neg(\phi\vee\psi)\rightarrow\neg\phi)$

g) $\psi^{\circ}\rightarrow(\phi\rightarrow(\neg\psi\rightarrow\neg(\phi\rightarrow\psi)))$

h) $(\neg(\phi\rightarrow\psi))^{\ast}$;       $(\neg(\phi\rightarrow\psi))^{\circ}$

i) $(\neg(\phi^{\ast}))^{\circ}$

j) $\neg(\phi^{\ast})\rightarrow(\phi\rightarrow\psi)$

Proof: these formal theorems are formally demonstrated as in Proposition 3.8, applying DT and Proposition 3.5 if were necessary:

For a): taking into account Corollary 3.12.a’), it is valid $\vdash_{(n,k)}\phi\rightarrow\neg\phi\vee\phi$. That is, $\vdash_{(n,k)}\phi\rightarrow\phi^{\ast}$.

For b):

$1)$ $\phi^{\circ}$ [Hyp.]

$2)$ $\neg\phi$ [Hyp.]

$3)$ $(\neg\phi\rightarrow\psi)^{\ast}$ [$Ax_{3}$]

$4)$ $(\neg\phi\rightarrow\psi)^{\ast}\rightarrow[\phi^{\circ}\rightarrow((\neg(\neg\phi\rightarrow\psi)\rightarrow\neg\phi)\rightarrow(\phi\rightarrow(\neg\phi\rightarrow\psi)))]$

[Prop. 3.8.c)]

$5)$ $(\neg(\neg\phi\rightarrow\psi)\rightarrow\neg\phi)\rightarrow(\phi\rightarrow(\neg\phi\rightarrow\psi))$ [1), 3), 4), MP]

$6)$ $\neg\phi\rightarrow(\neg(\neg\phi\rightarrow\psi)\rightarrow\neg\phi)$ [$Ax_{1}$]

$7)$ $\neg(\neg\phi\rightarrow\psi)\rightarrow\neg\phi$ [2), 6), MP]

$8)$ $\phi\rightarrow(\neg\phi\rightarrow\psi)$ [5), 7),MP]

$9)$ $\neg\phi\rightarrow(\phi\rightarrow\psi)$ [8), Perm.]

$10)$ $\phi\rightarrow\psi$ [2), 9), MP]

Thus, it holds $\phi^{\circ}\vdash_{(n,k)}\neg\phi\rightarrow(\phi\rightarrow\psi)$, as was desired.

For c):

$1)$ $(\copyright(\neg\phi\rightarrow\sim\phi))^{\circ}$ [Prop. 3.6]

$2)$ $(\sim(\neg\phi\rightarrow\sim\phi))^{\circ}$ [$1)$, $Ax_{12}$]

$3)$ $(\neg\phi\wedge\phi)^{\circ}$ [$2)$, Def. 3.1 (of $\wedge$)]

$4)$ $(\neg(\neg\phi\wedge\phi))^{\circ}$ [$3)$, $Ax_{12}$]

$5)$ $(\phi^{\circ})^{\circ}$ [$4)$, Def. 3.1 (of $\circ$)]

For d):

$1)$ $(\phi^{\ast})^{\circ}$ [Prop. 3.6]

$2)$ $(\copyright(\neg\phi\rightarrow\sim\phi))^{\ast}$ [Prop. 3.6]

$3)$ $(\neg\phi\wedge\phi)^{\ast}$ [2), Def. 3.1 (of $\wedge$), $Ax_{11}$]

$4)$ $(\neg\phi\wedge\phi)^{\ast}\rightarrow[(\phi^{\ast})^{\circ}\rightarrow((\neg\phi\wedge\phi\rightarrow\phi^{\ast})\rightarrow((\neg(\phi^{\ast})\rightarrow\phi^{\circ}))]$ [Prop. 3.8.d)]

$5)$ $(\neg\phi\wedge\phi\rightarrow\neg\phi\vee\phi)\rightarrow((\neg(\phi^{\ast})\rightarrow\phi^{\circ})$ [1), 3), 4), MP]

$6)$ $\neg\phi\wedge\phi\rightarrow\neg\phi\vee\phi$ [Corollary 3.12.e)]

$7)$ $\neg(\phi^{\ast})\rightarrow\phi^{\circ}$ [5), 6), MP]

So, $\vdash_{(n,k)}\neg(\phi^{\ast})\rightarrow\phi^{\circ}$

For e):

$1)$ $(\neg\phi\wedge\phi)^{\ast}\rightarrow[(\copyright\phi)^{\circ}\rightarrow((\neg\phi\wedge\phi\rightarrow\copyright\phi)\rightarrow(\sim\phi\rightarrow\phi^{\circ}))]$

[Prop. 3.8.d), Def. 3.1 (of $\sim$ and $\circ$)]

$2)$ $\neg\phi\wedge\phi\rightarrow\phi$ [Corollary 3.12.b’)]

$3)$ $\phi\rightarrow\copyright\phi$ [Prop. 3.8.a)]

$4)$ $\neg\phi\wedge\phi\rightarrow\copyright\phi$ [2), 3), Trans.]

$5)$ $(\copyright\phi)^{\circ}$ [Prop. 3.6]

$6)$ $(\copyright(\neg\phi\rightarrow\sim\phi))^{\ast}$ [Prop. 3.6]

$7)$ $(\sim(\neg\phi\rightarrow\sim\phi))^{\ast}$ [6), Def. 3.1 (of $\sim$), $Ax_{11}$]

$8)$ $(\neg\phi\wedge\phi)^{\ast}$ [7), Def. 3.1 (of $\wedge$)]

$9)$ $\sim\phi\rightarrow\phi^{\circ}$ [1), 4), 5), 8), MP]

Therefore, $\vdash_{(n,k)}\sim\phi\rightarrow\phi^{\circ}$

For f):

$1)$ $\phi^{\ast}$ [Hyp.]

$2)$ $(\phi\vee\psi)^{\circ}$ [$Ax_{4}$, Def. 3.1 (of $\vee$)]

$3)$ $\phi^{\ast}\rightarrow[(\phi\vee\psi)^{\circ}\rightarrow((\phi\rightarrow\phi\vee\psi)\rightarrow(\neg(\phi\vee\psi)\rightarrow\neg\phi)]$ [Prop. 3.8.d)]

$4)$ $(\phi\rightarrow\phi\vee\psi)\rightarrow(\neg(\phi\vee\psi)\rightarrow\neg\phi)$ [1), 2), 3), MP]

$5)$ $\phi\rightarrow\phi\vee\psi$ [Corollary 3.12.a)]

$6)$ $\neg(\phi\vee\psi)\rightarrow\neg\phi$ [4), 5), MP]

Thus, $\phi^{\ast}\vdash_{(n,k)}\neg(\phi\vee\psi)\rightarrow\neg\phi$.

For g):

$1)$ $\psi^{\circ}$ [Hyp.]

$2)$ $(\phi\rightarrow\psi)^{\ast}$ [$Ax_{3}$]

$3)$ $(\phi\rightarrow\psi)^{\ast}\rightarrow[\psi^{\circ}\rightarrow(((\phi\rightarrow\psi)\rightarrow\psi)\rightarrow(\neg\psi\rightarrow\neg(\phi\rightarrow\psi)))]$ [Prop. 3.8.d)]

$4)$ $((\phi\rightarrow\psi)\rightarrow\psi)\rightarrow(\neg\psi\rightarrow\neg(\phi\rightarrow\psi))$ [1), 2), 3), MP]

$5)$ $(\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\psi)$ [Remark 3.3]

$6)$ $\phi\rightarrow((\phi\rightarrow\psi)\rightarrow\psi)$ [5), Perm.]

$7)$ $\phi\rightarrow(\neg\psi\rightarrow\ (\phi\rightarrow\psi))$ [4), 6), Trans.]

So, $\psi^{\circ}\vdash_{(n,k)}\phi\rightarrow(\neg\psi\rightarrow\neg(\phi\rightarrow\psi))$ is obtained.

For h): By $Ax_{3}$ and $Ax_{11}$ it holds $\vdash_{(n,k)}(\neg(\phi\rightarrow\psi))^{\ast}$; By $Ax_{4}$ and $Ax_{12}$ it holds $\vdash_{(n,k)}(\neg(\phi\rightarrow\psi))^{\circ}$.

For i): It is a particular case of h).

For j):

$1)$ $\neg(\phi^{\ast})$ [Hyp.]

$2)$ $\phi$ [Hyp.]

$3)$ $\phi\rightarrow\phi^{\ast}$ [a)]

$4)$ $\phi^{\ast}$ [2), 3), MP]

$5)$ $(\phi^{\ast})^{\circ}$ [Prop. 3.6 ]

$6)$ $(\phi^{\ast})^{\circ}\rightarrow(\neg(\phi^{\ast})\rightarrow(\phi^{\ast}\rightarrow\psi))$ [b)]

$7)$ $\psi$ [1), 4), 5). 6), MP]

That is, it holds $\neg(\phi^{\ast}),\phi\vdash_{(n,k)}\psi$. Then, apply Theorem 3.4. This last result completes the proof. $\Box$

4 General Soundness and Completeness

It is easy to check that the axioms given in Definition 3.2 are $I^{n}P^{k}$-tautologies. So, taking into account that MP preserves $I^{n}P^{k}$-tautologies, it holds:

Theorem 4.1

[Weak Soundness] If $\vdash_{(n,k)}\phi$, then $\models_{(n,k)}\phi$.

A theorem of (weak) Completeness arises as an adaptation of the well-known Kalmár’s proof for Classical Logic $CL$, cf. [8]:

Definition 4.2

For every formula $\phi[{\alpha}_{1},{\alpha}_{2},\dots,{\alpha}_{m}]\in L(C)$, for every $I^{n}P^{k}$-valuation $v$, for every atomic formula ${\alpha}_{p}$ ($1\leq p\leq m$) let $Q_{p}^{v}$ be the set associated to $\alpha_{p}$ and to $v$, defined by:

• •

If $v({\alpha}_{p})$ = $F_{r}$ (with $1\leq r\leq n$), then:

$Q_{p}^{v}$ = $\{\neg({{\alpha}_{p}}^{\ast}),\neg((\neg{\alpha}_{p})^{\ast}),\dots,\neg((\neg^{r-1}{\alpha}_{p})^{\ast}),(\neg^{r}{\alpha}_{p})^{\ast}\}$

• •

If $v({\alpha}_{p})$ = $T_{i}$ (with $1\leq i\leq k$), then:

$Q_{p}^{v}$ = $\{\neg{\alpha}_{p}\wedge{\alpha}_{p},\neg^{2}{\alpha}_{p}\wedge\neg{\alpha}_{p},\dots,\neg^{i}{\alpha}_{p}\wedge\neg^{i-1}{\alpha}_{p},(\neg^{i}{\alpha}_{p})^{\circ}\}$

• •

If $v({\alpha}_{p})$ = $F_{0}$, then $Q_{p}^{v}$= $\{\sim{\alpha}_{p},({\alpha}_{p})^{\ast}\}$

• •

If $v({\alpha}_{p})$ = $T_{0}$, then $Q_{p}^{v}$ = $\{\copyright{\alpha}_{p},({\alpha}_{p})^{\circ}\}$

In addition, let the set $\Delta_{\phi}^{v}$:= $Q_{1}^{v}\cup Q_{2}^{v},\dots\cup Q_{m}^{v}$.

On the other hand, for every $I^{n}P^{k}$-valuation $v$ indicated above, the formula $\phi^{v}$ (determined by $\phi$ and $v$) is defined as follows:

• •

If $v(\phi)$ = $F_{r}$ (with $0\leq r\leq n$), then $\phi^{v}$ = $\neg^{r+1}\phi$.

• •

If $v(\phi)$ = $T_{i}$ (with $0\leq i\leq k$), then $\phi^{v}$ = $\phi$.

For the next technical (and essential) result, the following obvious fact will be applied without explicit mention: according to the previous definition, if $\phi\in L(C)$ and $\psi$ is a subformula of $\phi$ then, for every valuation $v$, \Delta_{\psi}^{v}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}\Delta_{\phi}^{v}. Bearing this in mind it is possible to demonstrate:

Lemma 4.3

For every formula $\phi$=$\phi[\alpha_{1},\dots,\alpha_{m}]\in L(C)$, for every $I^{n}P^{k}$-valuation $v$, it holds that $\Delta_{\phi}^{v}\vdash_{(n,k)}{\phi}^{v}$.

Proof: By induction on the complexity of $\phi$. The analysis is divided in the following cases:

Case 1): $\phi\in\mathcal{V}$ (without losing generality, $\phi$ = $\alpha_{1}$, which implies $\Delta_{\phi}^{v}$ = $Q_{1}^{v}$). Then:

If $v(\phi)$ = $F_{0}$, then $\phi^{v}$ = $\neg\phi$ and $\Delta_{\phi}^{v}$ = $\{\sim\phi,{\phi}^{\ast}\}$. So, $\Delta_{\phi}^{v}\vdash_{(n,k)}\phi^{v}$ by Prop. 3.8.b).

If $v(\phi)$ = $F_{r}$ ($1\leq r\leq n$), then $\phi^{v}$ = $\neg^{r+1}\phi$ and \{(\neg^{r}\phi)^{\ast},\neg(\neg^{r}\phi\vee\neg^{r-1}\phi)\}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}\Delta_{\phi}^{v}. Now, by Prop. 3.13.f), $\vdash_{(n,k)}{(\neg^{r}\phi)}^{\ast}\rightarrow(\neg(\neg^{r}\phi\vee\neg^{r-1}\phi)\rightarrow\neg^{r+1}\phi)$. From all this, $\Delta_{\phi}^{v}\vdash_{(n,k)}\neg^{r+1}\phi$ (= $\phi^{v}$).

If $v(\phi)$ = $T_{i}$ ($1\leq i\leq k$), then $\neg\phi\wedge\phi\in\Delta_{\phi}^{v}$. By Corollary 3.12.b’), $\Delta_{\phi}^{v}\vdash_{(n,k)}\phi$ (=$\phi^{t}$).

If $v(\phi)$ = $T_{0}$, then $\Delta_{\phi}^{t}$ = $\{\copyright{\phi},(\phi)^{\circ}\}$. Thus, $\Delta_{\phi}^{t}\vdash_{(n,k)}\copyright\phi$ ( = $(\phi\rightarrow\phi)\rightarrow\phi$)). So, since $\vdash_{(n,k)}\phi\rightarrow\phi$, it holds $\Delta_{\phi}^{t}\vdash_{(n,k)}\phi$ (= $\phi^{t}$). The proof of Case 1) is completed.

Case 2): when $\phi$ is of the form $\neg\psi$. Consider the following subcases:

2.1): $v(\psi)$ = $F_{0}$. By (I.H), $\Delta_{\psi}^{v}\vdash_{(n,k)}\psi^{v}$ (= $\neg\psi$ = $\phi^{v}$). Hence, $\Delta_{\phi}^{v}\vdash_{(n,k)}\phi^{v}$.

2.2): $v(\psi)$ = $F_{r}$, with $1\leq r\leq n$. Note that $v(\phi)$ = $F_{r-1}$, which implies $\phi^{v}$ = $\neg^{r}\phi$ = $\neg^{r+1}\psi$ = $\psi^{v}$. So, $\Delta_{\phi}\vdash_{(n,k)}\phi^{v}$, by (I.H).

2.3): $v(\psi)$ = $T_{1}$. From Definition 2.2, $\psi$ = $\neg^{q-1}\alpha$, with $1\leq q\leq k$, $\alpha\in\mathcal{V}$, and $v(\alpha)$ = $T_{q}$. Thus, $\Delta_{\psi}^{v}$ = $Q_{\alpha}^{v}$ = $\{(\neg\alpha\wedge\alpha),\dots,(\neg^{q}\alpha\wedge\neg^{q-1}\alpha),(\neg^{q}\alpha)^{\circ}\}$. From this, using Corollary 3.12.b), it holds $\Delta_{\phi}^{v}\vdash_{(n,k)}\neg^{q}\alpha$ (=$\phi^{v}$).

2.4): $v(\psi)$ = $T_{i}$, with $2\leq i\leq k$. So, $v(\phi)$ = $T_{i-1}$, $1\leq i-1\leq k-1$. In addition, $\psi$ = $\neg^{q}\alpha$, with $0\leq q\leq k-i$, $v(\alpha)$ = $T_{i+q}$ and $\alpha\in\mathcal{V}$ From this, $\phi\wedge\psi$ = $\neg^{q+1}\alpha\wedge\neg^{q}\alpha\in Q_{\alpha}^{v}$ = $\Delta_{\psi}^{v}$ = $\Delta_{\phi}^{v}$ (since $q+1\leq k$). So, applying Corollary 3.12.b), $\Delta_{\phi}^{v}\vdash_{(n,k)}\phi$ = $\phi^{v}$.

2.5): $v(\psi)$ = $T_{0}$. Then, $v(\phi)$ = $F_{0}$. To prove that $\Delta_{\phi}^{v}\vdash_{(n,k)}\neg\phi$ (= $\neg\neg\psi$) it suffices to demonstrate $\Delta_{\psi}^{v}\vdash_{(n,k)}\psi^{\circ}$ ${(\star)}$. Indeed, if this fact holds, from $Ax_{10}$, then it would be verified $\Delta_{\psi}^{v}\vdash_{(n,k)}\psi\rightarrow\neg\neg\psi$. And, since it holds $\Delta_{\psi}^{v}\vdash_{(n,k)}\psi$ (by (I.H)), it will be obtained $\Delta_{\phi}^{v}\vdash_{(n,k)}\phi^{v}$. Now, to prove ${(\star)}$, consider the following possibilities:

2.5.1): $\psi$ is of the form ${\neg}^{q}(\theta_{1}\rightarrow\theta_{2})$ (with $0\leq q$). Applying $Ax_{4}$ and (eventually) $Ax_{12}$, it holds $\vdash_{(n,k)}\psi^{\circ}$, and therefore $\Delta_{\phi}^{v}\vdash_{(n,k)}\psi^{\circ}$.

2.5.2): $\psi$ is of the form ${\neg}^{q}\alpha$, $\alpha\in\mathcal{V}$, $0\leq q$. In this case, $Q_{\alpha}^{v}$ = $\Delta_{\psi}^{v}$. Consider here the different possibilities for $v(\alpha)$:

2.5.2.1): $v(\alpha)$ = $F_{0}$. Then, $\Delta_{\alpha}^{v}$ = $\{\sim{\alpha},\alpha^{\ast}\}$. By Prop. 3.13.e), $\Delta_{\psi}^{v}\vdash_{(n,k)}\alpha^{\circ}$. Then, apply $Ax_{12}$ ($q$ times).

2.5.2.2): $v(\alpha)$ = $F_{r}$ (with $1\leq r\leq n$). Since $\neg(\alpha^{\ast})\in\Delta_{\alpha}^{v}$, it holds $\Delta_{\alpha}^{v}\vdash_{(n,k)}\alpha^{\circ}$, because Prop. 3.13.d). From this, $\Delta_{\psi}^{v}\vdash_{(n,k)}\psi^{\circ}$, by $Ax_{12}$ again.

2.5.2.3): $v(\alpha)$ = $T_{i}$ (with $1\leq i\leq k$). So, $i\leq q$ (in fact: if $i>q$, then $v(\psi)$ = $T_{i-q}$, $i-q\geq 1$, contradicting $v(\psi)$ = $T_{0}$). Besides, note that $(\neg^{i}\alpha)^{\circ}\in\Delta_{\alpha}^{v}$, which implies $\Delta_{\psi}^{v}\vdash_{(n,k)}(\neg^{i}\alpha)^{\circ}$. So, since $i\leq q$, $\Delta_{\psi}\vdash_{(n,k))}(\psi)^{\circ}$, again by $Ax_{12}$.

2.5.2.4): $v(\alpha)$ = $T_{0}$. Then, $\Delta_{\psi}^{v}\vdash_{(n,k)}\alpha^{\circ}$, since \alpha^{\circ}\in Q_{\alpha}^{v}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}\Delta_{\psi}^{v}. Then, applying $Ax_{12}$ one more time, ${\bf(\star)}$ is valid. The proof of Case 2) is concluded.

Case 3): $\phi$ is of the form $\psi\rightarrow\theta$. There exist the following possibilities 555The first three subcases indicate the possibilities for $v(\phi)$ = $T_{0}$. The last two cases correspond to $v(\phi)$ = $F_{0}$. :

3.1): $v(\psi)$ = $F_{0}$ (and so, $\phi^{v}$ = $\psi\rightarrow\theta$). By (I.H), $\Delta_{\psi}^{v}\vdash_{(n,k)}\neg\psi$ ($\star$). In addition, it can be proved that $\Delta_{\psi}^{v}\vdash_{(n,k)}\psi^{\circ}$ ($\star\star$) (such a proof runs as follows, according the internal structure of $\psi$):

3.1.1): $\psi$ = $\alpha\in\mathcal{V}$. So, $\Delta_{\psi}^{v}\vdash_{(n,k)}\sim\psi$. Applying Prop. 3.13.e), it holds ($\star\star$).

3.1.2): $\psi$ = $\neg^{q}\alpha$, $1\leq q$, $\alpha\in\mathcal{V}$. Consider the following possibilities for $v(\alpha)$:

3.1.2.1): $v(\alpha)$ = $F_{0}$. Then, by Prop. 3.13.e), $Q_{\alpha}^{v}\vdash_{(n,k)}\alpha^{\circ}$ .

3.1.2.2): $v(\alpha)$ = $F_{r}$ ($1\leq r\leq n$). Then, $q\geq r$ (because $q<r$ implies $v(\psi)$ = $v(\neg^{q}\alpha)$ = $\neg^{q}(v(\alpha))$ = $F_{r-q}\neq F_{0}$, which is absurd). Besides that, $\neg((\neg^{r-1}\alpha)^{\ast})\in Q_{\alpha}^{v}$. Therefore $Q_{\alpha}^{v}\vdash_{(n,k)}(\neg^{r-1}\alpha)^{\circ}$, because Prop. 3.13.d).

3.1.2.3): $v(\alpha)$ = $T_{i}$ ($1\leq i\leq k$). So, $q\geq i$ (by similar reasons to 3.1.3.2)). In addition, $(\neg^{i}\alpha)^{\circ}\in Q_{\alpha}^{v}$, and so $Q_{\alpha}^{v}\vdash_{(n,k)}(\neg^{i}\alpha)^{\circ}$.

3.1.2.4): $v(\alpha)$ = $T_{0}$. Obviously, $Q_{\alpha}^{v}\vdash_{(n,k)}(\alpha)^{\circ}$, from Def. 4.2.

Now note that $Ax_{12}$ can be applied in all the subcases 3.1.2.1)-3.1.2.4), in such a way to obtain $\Delta_{\psi}^{v}\vdash_{(n,k)}\psi^{\circ}$, completing the proof $(\star\star)$ for Subcase 3.1.2).

3.1.3): $\psi$ = $\neg^{q}(\theta_{1}\rightarrow\theta_{2})$, with $0\leq q$. By $Ax_{3}$, $\vdash_{(n,k)}(\theta_{1}\rightarrow\theta_{2})^{\circ}$. Now, apply $Ax_{12}$, $q$ times.

So, it was proven $(\star\star)$ for all the possibilities of Subcase 3.1. From this, $(\star)$ and Prop. 3.13.b), it holds $\Delta_{\phi}^{v}\vdash_{(n,k)}\psi\rightarrow\theta$ (=$\phi^{v}$).

3.2): $v(\psi)$ = $F_{r}$, $1\leq r\leq n$. Again, $v(\phi)$ = $T_{0}$ and so $\phi^{v}$ = $\psi\rightarrow\theta$. Note that, since $v(\psi)$ = $F_{r}$, $\psi$ = $\neg^{q}\alpha$, with $q\geq 0$, $\alpha\in\mathcal{V}$. Thus, $v(\alpha)$ = $F_{r+q}$, with $r+q\leq n$, which implies $Q_{\alpha}^{v}$ = $\{\neg(\alpha^{\ast}),\neg((\neg\alpha)^{\ast}),\dots,\neg((\neg^{r+q-1}\alpha)^{\ast}),(\neg^{r+q}\alpha)^{\ast}\}$. So, $\neg((\neg^{q}\alpha)^{\ast})\in Q_{\alpha}^{v}$, because $r\geq 1$. Thus, $\Delta_{\phi}^{v}\vdash_{(n,k)}\neg(\psi^{\ast})$. From this and Prop. 3.13.j), $\Delta_{\phi}^{v}\vdash_{(n,k)}\phi^{v}$.

3.3): $v(\theta)$ = $T_{i}$, $0\leq i\leq k$. So, $\phi^{v}$ = $\psi\rightarrow\theta$ one more time. By (I.H), $\Delta_{\theta}^{v}\vdash_{(n,k)}\theta$. Now apply $Ax_{1}$.

3.4): $v(\psi)$ = $T_{i}$, $v(\theta)$ = $F_{r}$ ($0\leq i\leq k$, $1\leq r\leq n$). Using (I.H), $\Delta_{\phi}\vdash_{(n,k)}\psi$, which implies $\Delta_{\phi}\vdash_{(n,k)}(\psi\rightarrow\theta)\rightarrow\theta$, because $\vdash_{(n,k)}\psi\rightarrow((\psi\rightarrow\theta)\rightarrow\theta)$. Hence, $\Delta_{\phi}\vdash_{(n,k)}(\psi\rightarrow\theta)\rightarrow\theta^{\ast}$, by Prop. 3.13.a). Now, considering that $\Delta_{\phi}^{v}\vdash_{(n,k)}(\psi\rightarrow\theta)^{\ast}$ and $\Delta_{\phi}^{v}\vdash_{(n,k)}(\theta^{\ast})^{\circ}$ (because $Ax_{3}$ and Prop. 3.6, resp.), it is valid that $\Delta_{\phi}\vdash_{(n,k)}\neg(\theta^{\ast})\rightarrow\neg(\psi\rightarrow\theta)$, by Prop. 3.8.d). In addition, reasoning as in Subcase 3.2) (w.r.t $\theta$), $\Delta_{\phi}\vdash_{(n,k)}\neg(\theta)^{\ast}$. Thus, $\Delta_{\phi}\vdash_{(n,k)}\neg(\psi\rightarrow\theta)$ (= $\phi^{v}$), as it is desired.

3.5): $v(\psi)$ = $T_{i}$ ($0\leq i\leq k$), $v(\theta)$ = $F_{0}$. Adapting $(\star\star)$ of Subcase 3.1) to $\theta$ it can be obtained $\Delta_{\phi}^{v}\vdash_{(n,k)}\theta^{\circ}$. Besides that, by (I.H), $\Delta_{\phi}^{v}\vdash_{(n,k)}\psi$ and $\Delta_{\phi}^{v}\vdash_{(n,k)}\neg\theta$. Considering Prop. 3.13.g) now, it holds $\Delta_{\phi}^{v}\vdash_{(n,k)}\neg(\psi\rightarrow\theta)$ = $\phi^{v}$.

The analysis of this last subcase finishes the proof. $\Box$

Lemma 4.4

Let $\Delta\cup\{\psi,\theta\}$ be a subset of $L(C)$. If the following $n+k+4$ syntactic consequences are valid:

\begin{array}[]{ll}{1)}&\Delta,\neg(\psi^{\ast}),(\neg\psi)^{\ast}\vdash_{(n,k)}\theta\\ {2)}&\Delta,\neg(\psi^{\ast}),\neg((\neg\psi)^{\ast}),(\neg^{2}\psi)^{\ast}\vdash_{(n,k)}\theta\\ \vdots&\vdots\\ {n-1)}&\Delta,\neg(\psi^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast}),(\neg^{n-1}\psi)^{\ast}\vdash_{(n,k)}\theta\\ {n)}&\Delta,\neg(\psi^{\ast}),\dots,\neg((\neg^{n-1}\psi)^{\ast}),(\neg^{n}\psi)^{\ast}\vdash_{(n,k))}\theta\\ {n+1)}&\Delta,\,\neg\psi\wedge\psi,\,(\neg\psi)^{\circ}\vdash_{(n,k)}\theta\\ {n+2)}&\Delta,\,\neg\psi\wedge\psi,\,\neg^{2}\psi\wedge\neg\psi,\,(\neg^{2}\psi)^{\circ}\vdash_{(n,k)}\theta\\ \vdots&\vdots\\ {n+k-1)}&\Delta,\,\neg\psi\wedge\psi,\,\dots,\,\neg^{k-1}\psi\wedge\neg^{k-2}\psi,\,(\neg^{k-1}\psi)^{\circ}\vdash_{(n,k)}\theta\\ {n+k)}&\Delta,\neg\psi\wedge\psi,\,\dots,\neg^{k}\psi\wedge\neg^{k-1}\psi,\,(\neg^{k}\psi)^{\circ}\vdash_{(n,k)}\theta\\ {n+k+1)}&\Delta,\sim\psi,\psi^{\ast}\vdash_{(n,k)}\theta\\ {n+k+2)}&\Delta,\copyright\psi,\psi^{\circ}\vdash_{(n,k)}\theta\\ {n+k+3)}&\vdash_{(n,k)}\theta^{\ast}\\ {n+k+4)}&\vdash_{(n,k)}\theta^{\circ}\\ \end{array}

Then it is valid that $\Delta\vdash_{(n,k)}\theta$.

Proof: First, by Hypothesis ${1)}$ to $n)$ can be obtained ${\Delta,\neg(\psi^{\ast})\vdash_{(n,k)}\theta}$ $(\star)$. Indeed: by $n-1)$, $\Delta,\neg(\psi^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash_{(n,k)}(\neg^{n-1}\psi)^{\ast}\rightarrow\theta$. Besides that, it holds that $\vdash_{(n,k)}((\neg^{n-1}\psi)^{\ast})^{\ast}$ (by Prop. 3.6), and $\vdash\theta^{\circ}$ (by Hypothesis n+k+4)). Applying all this to Prop. 3.8.d) it is verified:

$\Delta,\neg({\psi}^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash_{(n,k)}\neg\theta\rightarrow\neg((\neg^{n-1}\psi)^{\ast})$ $({\dagger})$.

It is also valid $\Delta,\neg(\psi^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash_{(n,k))}\neg((\neg^{n-1}\psi)^{\ast})\rightarrow\theta$, because $Ax_{5}$, $n)$ and DT. In addition, $\vdash_{(n,k)}(\neg((\neg^{n-1}\psi)^{\ast}))^{\ast}$ , because Proposition 3.6 and $Ax_{11}$. Thus, considering Prop. 3.8.d) and Hyp. n+k+4) again, it holds:

$\Delta,\neg({\psi}^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash_{(n,k)}\neg\theta\rightarrow\neg^{2}((\neg^{n-1}\psi)^{\ast})$ $({\dagger}{\dagger})$.

Hence, from $({\dagger})$ and $({\dagger}{\dagger})$ and Corollary 3.12.d):

$\Delta,\neg({\psi}^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash\neg\theta\rightarrow[\neg^{2}((\neg^{n-1}\psi)^{\ast})\wedge\neg((\neg^{n-1}\psi)^{\ast})]$ $(\Diamond)$.

On the other hand, it holds $\vdash_{(n,k)}(\neg\theta)^{\ast}$, because Hyp. $n+k+3)$ and $Ax_{11}$. And, of course, $\vdash_{(n,k)}[\neg^{2}((\neg^{n-1}\psi)^{\ast})\wedge\neg((\neg^{n-1}\psi)^{\ast})]^{\circ}$. So, by Proposition 3.8.d):

$\Delta,\neg({\psi}^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash_{(n,k)}\neg[\neg^{2}((\neg^{n-1}\psi)^{\ast})\wedge\neg((\neg^{n-1}\psi)^{\ast})]\rightarrow\neg\neg\theta$. That is, $\Delta,\neg({\psi}^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash_{(n,k)}(\neg((\neg^{n-1}\psi)^{\ast}))^{\circ}\rightarrow\neg\neg\theta$. Thus, from Prop. 3.13.i), $\Delta,\neg({\psi}^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash_{(n,k)}\neg\neg\theta$. Thus (by Hyp. n+k+3) and $Ax_{9}$), $\Delta,\neg({\psi}^{\ast}),\dots,\neg((\neg^{n-2}\psi)^{\ast})\vdash_{(n,k)}\theta$ $(\Diamond\Diamond)$.

The procedure used above to prove $(\Diamond\Diamond)$ can be applied using (in decreasing order) the Hypotheses $1)$ … $n-1)$, proving $(\star)$ (note that the formula $\neg({\psi}^{\ast})$ cannot be “suppressed” yet).

From $(\star)$ (and monotonicity), $\Delta,\sim\psi\vdash\neg(\psi^{\ast})\rightarrow\theta$. Moreover, from Hyp. $n+k+1)$, it holds $\Delta,\sim\psi\vdash\psi^{\ast}\rightarrow\theta$. From these facts and Corollary 3.12.c), it is valid $\Delta,\sim\psi\vdash_{(n,k)}\neg(\psi^{\ast})\vee\psi^{\ast}\rightarrow\theta$. Now realizing that $\vdash_{(n,k)}\neg(\psi^{\ast})\vee\psi^{\ast}$ (because Prop. 3.6), it is obtained $\Delta,\sim\psi\vdash_{(n,k)}\theta$. ${\bf(I)}$.

On the other hand, from $n+1)$ to $n+k)$ it is valid $\Delta,\psi\wedge\neg\psi\vdash_{(n,k)}\theta$ $(\star\star)$. The reasoning is as follows: using ${n+k)}$ and $Ax_{6}$, it holds:

$\Delta,\neg\psi\wedge\psi,\dots,\,\neg^{k-1}\psi\wedge\neg^{k-2}\psi\vdash_{(n,k)}\neg^{k}\psi\wedge\neg^{k-1}\psi\,\rightarrow\theta$. It is also valid

$\Delta,\neg\psi\wedge\psi,\,\dots,\neg^{k-1}\psi\wedge\neg^{k-2}\psi\,\vdash_{(n,k)}(\neg^{k-1}\psi)^{\circ}\rightarrow\theta$, because Hyp. $n+k-1)$. Hence, by Corollary 3.12.c) and recalling Definition 3.1:

$\Delta,\dots,\,\neg^{k-1}\psi\wedge\neg^{k-2}\psi\vdash_{(n,k)}\,\neg(\neg^{k}\psi\wedge\neg^{k-1}\psi)\vee(\neg^{k}\psi\wedge\neg^{k-1}\psi)\,\rightarrow\theta$. That is, $\Delta,\dots,\,\neg^{k-1}\psi\wedge\neg^{k-2}\psi\,\vdash_{(n,k)}(\neg^{k}\psi\wedge\neg^{k-1}\psi)^{\ast}\rightarrow\theta$. In addition, it holds $\vdash_{(n,k)}(\neg^{k-1}\psi\wedge\neg^{k}\psi)^{\ast}$, by Definition 3.1, $Ax_{3}$ and $Ax_{11}$. From these two facts, it holds $\Delta,\dots,\,\neg^{k-2}\psi\wedge\neg^{k-1}\psi\,\vdash_{(n,k)}\theta$. $(\Diamond\Diamond\Diamond)$

Adapting the reasoning applied in $(\Diamond\Diamond\Diamond)$ to the Hypotheses $n+k-2),\dots,n+1)$ (in a decreasing order, as before), it is obtained $(\star\star)$, as desired.

From $(\star\star)$ and monotonicity it is valid $\Delta,\copyright\psi\vdash_{(n,k)}\neg\psi\wedge\psi\rightarrow\theta$. So (by Hyp. n+k+4), Prop. 3.6, $Ax_{11}$ and Prop. 3.8.d)), $\Delta,\copyright\psi\vdash_{(n,k)}\neg\theta\rightarrow\psi^{\circ}$. On the other hand, by Hyp. $n+k+2)$, it holds $\Delta,\copyright\psi\vdash_{(n,k)}\psi^{\circ}\rightarrow\theta$. So, $\Delta,\copyright\psi\vdash_{(n,k)}\neg\theta\rightarrow\neg(\psi^{\circ})$ (again, by Hyp. n+k+4), Prop. 3.6, $Ax_{11}$ and Prop. 3.8.d)). Thus, $\Delta,\copyright\psi\vdash_{(n,k)}\neg\theta\rightarrow(\neg(\psi^{\circ})\wedge\psi^{\circ})$, by Corollary 3.12.d). Therefore, $\Delta,\copyright\psi\vdash_{(n,k)}\neg(\neg(\psi^{\circ})\wedge\psi^{\circ})\rightarrow\neg\neg\theta$ (because Hyp. n+k+3), $Ax_{11}$ and Prop. 3.8.d)) . That is, $\Delta,\copyright\psi\vdash_{(n,k)}(\psi^{\circ})^{\circ}\rightarrow\neg\neg\theta$. Hence, $\Delta,\copyright\psi\vdash_{(n,k)}\neg\neg\theta$, because Prop. 3.13.c). Now, taking into account Hyp. n+k+3) and $Ax_{9}$, it is valid $\Delta,\copyright\psi\vdash_{(n,k)}\theta$. ${\bf(II)}$.

From ${\bf(I)}$, ${\bf(II)}$ and Corollary 3.12.c), is verified $\Delta\vdash_{(n,k)}(\copyright\psi)^{\ast}\rightarrow\theta$. Hence, it is valid $\Delta\vdash_{(n,k)}\theta$, by Prop 3.6. $\Box$

Thus, using Lemmas 4.3 and 4.4 it is possible to demonstrate (weak) completeness as the following result shows:

Theorem 4.5

[Weak Completeness] $\models_{(n,k)}\phi$ implies $\vdash_{(n,k)}\phi$.

Proof: Suppose $\models_{(n,k)}\phi$, with $\phi$ = $\phi[\alpha_{1},\dots,\alpha_{m}]$, and consider the set $VAL_{\phi}:=$ $\{v_{t}\}_{1\leq t\leq(n+k+2)^{m}}$ (the set of all the $I^{n}P^{k}$-valuations effectively used to evaluate $\phi$). Define in $VAL_{\phi}$ the equivalence relation $\equiv_{1}$, as follows: for every $v_{t_{1}},v_{t_{2}}\in VAL_{\phi}$, $v_{t_{1}}\equiv_{1}v_{t_{2}}$ iff, for every $\alpha_{p}$ with $2\leq p\leq m$, $v_{t_{1}}(\alpha_{p})$ = $v_{t_{2}}(\alpha_{p})$. This relation has $(n+k+2)^{m-1}$ equivalence classes (indicated, in a general way, by $||v||$). Besides that, taking into account Definition 4.2, it holds that (given a fixed equivalence class $||v||$) $Q_{p}^{v_{t_{1}}}$ = $Q_{p}^{v_{t_{2}}}$, for every $2\leq p\leq m$, for every pair $v_{t_{1}}$, $v_{t_{2}}\in||v||$. This allows to define the set $\Delta_{1}^{||v||}$:= $Q_{2}^{v_{t}}\cup\dots\cup Q_{m}^{v_{t}}$, being $v_{t}$ any element of $||v||$. In addition, note that every class $||v||$ has exactly $(n+k+2)$ valuations and verifies that, for every $v_{t_{1}}$, $v_{t_{2}}\in||v||$, $v_{t_{1}}\neq v_{t_{2}}$ implies $v_{t_{1}}(\alpha_{1})\neq v_{t_{2}}(\alpha_{1})$. Finally, note that, since $\models_{(n,k)}\phi$, for every $v\in VAL_{\phi}$, $\phi^{v}$ = $\phi$. All these facts (together with Lemma 4.3) imply that (for every $||v||$) the following formal proofs can be built:

\begin{array}[]{ll}{1)}&\Delta_{1}^{||v||},\neg({\alpha}_{1}^{\ast}),(\neg{\alpha}_{1})^{\ast}\vdash_{(n,k)}\phi\\ {1.2)}&\Delta_{1}^{||v||},\neg({\alpha}_{1}^{\ast}),\neg((\neg{\alpha}_{1})^{\ast}),(\neg^{2}{\alpha}_{1})^{\ast}\vdash_{(n,k)}\phi\\ \vdots&\vdots\\ {1.n)}&\Delta_{1}^{||v||},\neg({\alpha}_{1}^{\ast}),\dots,\neg((\neg^{n-1}{\alpha}_{1})^{\ast}),(\neg^{n}{\alpha}_{1})^{\ast}\vdash_{(n,k))}\phi\\ {1.(n+1))}&\Delta_{1}^{||v||},\,{\alpha}_{1}\wedge\neg{\alpha}_{1},\,(\neg{\alpha}_{1})^{\circ}\vdash_{(n,k)}\phi\\ {1.n+2))}&\Delta_{1}^{||v||},\,{\alpha}_{1}\wedge\neg{\alpha}_{1},\,\neg^{2}{\alpha}_{1}\wedge\neg{\alpha}_{1},\,(\neg^{2}{\alpha}_{1})^{\circ}\vdash_{(n,k)}\phi\\ \vdots&\vdots\\ {1.(n+k))}&\Delta_{1}^{||v||},\,\neg{\alpha}_{1}\wedge{\alpha}_{1},\dots,\,\neg^{k}{\alpha}_{1}\wedge\neg^{k-1}{\alpha}_{1},\,(\neg^{k}{\alpha}_{1})^{\circ}\vdash_{(n,k)}\phi\\ {1.(n+k+1))}&\Delta_{1}^{||v||},\sim{\alpha}_{1},{\alpha}_{1}^{\ast}\vdash_{(n,k)}\phi\\ {1.(n+k+2))}&\Delta_{1}^{||v||},\copyright{\alpha}_{1},{\alpha}_{1}^{\circ}\vdash_{(n,k)}\phi\\ \end{array}

Moreover, by Proposition 3.7, it is valid:

\begin{array}[]{ll}{1.(n+k+3))}&\Delta_{1}^{||v||}\vdash_{(n,k)}\phi^{\ast}\\ {1.(n+k+4))}&\Delta_{1}^{||v||}\vdash_{(n,k)}\phi^{\circ}\\ \end{array}

All the previous facts allow to apply Lemma 4.4 in such a way that for every $||v||$ it holds $\Delta_{1}^{||v||}\vdash_{(n,k)}\phi$ (there are $(n+k+2)^{m-1}$ formal proof of this type). That is, it is possible “to eliminate” any referrence to formulas of the form $\alpha_{1}^{v}$ in every formal proof obtained, by means of an adequate subdivision of the set $VAL_{\phi}$, and by the application of Lemma 4.4. Note here that this process can be applied one more time, reagrouping the formal proofs already obtained. So, by a new application of Lemma 4.4 and of Proposition 3.7, any referrence to formulas of the form $\alpha_{2}^{v}$ can be supressed. The same prodedure can be applied by a finite number of times, until obtaining the following formal proofs:

\begin{array}[]{ll}{m.1)}&\neg({\alpha}_{m}^{\ast}),(\neg{\alpha}_{m})^{\ast}\vdash_{(n,k)}\phi\\ {m.2)}&\neg({\alpha}_{m}^{\ast}),\neg((\neg{\alpha}_{m})^{\ast}),(\neg^{2}{\alpha}_{m})^{\ast}\vdash_{(n,k)}\phi\\ \vdots&\vdots\\ {m.n)}&\neg({\alpha}_{m}^{\ast}),\dots,\neg((\neg^{n-1}{\alpha}_{m})^{\ast}),(\neg^{n}{\alpha}_{m})^{\ast}\vdash_{(n,k))}\phi\\ {m.(n+1))}&\neg{\alpha}_{m}\wedge{\alpha}_{m},\,(\neg{\alpha}_{m})^{\circ}\vdash_{(n,k)}\phi\\ {m.(n+2))}&\neg{\alpha}_{m}\wedge{\alpha}_{m},\,\neg^{2}{\alpha}_{m}\wedge\neg{\alpha}_{m},\,(\neg^{2}{\alpha}_{m})^{\circ}\vdash_{(n,k)}\phi\\ \vdots&\vdots\\ {m.(n+k))}&\neg{\alpha}_{m}\wedge{\alpha}_{m},\,\dots,\neg^{k}{\alpha}_{m}\wedge\neg^{k-1}{\alpha}_{m},\,(\neg^{k}{\alpha}_{m})^{\circ}\vdash_{(n,k)}\phi\\ {m.(n+k+1))}&\sim{\alpha}_{m},{\alpha}_{m}^{\ast}\vdash_{(n,k)}\phi\\ {m.(n+k+2))}&\copyright{\alpha}_{m},{\alpha}_{m}^{\circ}\vdash_{(n,k)}\phi\\ {m.(n+k+3))}&\vdash_{(n,k)}\phi^{\ast}\\ {m.(n+k+4))}&\vdash_{(n,k)}\phi^{\circ}\\ \end{array}

Applying Lemma 4.4 and Proposition 3.7 for a last time, $\vdash_{(n,k)}\phi$. $\Box$

Note that, in the proof developed above, all the ${(n+k+2)}^{m}$ valuations of $VAL_{\phi}$ are needed to obtain the formal proofs that allow to demonstrate $\vdash_{(n,k)}\phi$.

Theorems 4.1 and 4.5 prove weak adequacity: $\models_{(n,k)}\phi$ iff $\vdash_{(n,k)}\phi$. This result can be improved:

Theorem 4.6

[Strong Adequacity]: for every \Gamma\cup\{\phi\}\mbox{\hskip 2.84544pt\subseteq\hskip 2.84544pt}L(C), $\Gamma\models_{(n,k)}\phi$ iff $\Gamma\vdash_{(n,k)}\phi$.

Proof: By Proposition 2.10, $\models_{(n,k)}$ verifies Semantics Deduction Theorem and is finitary. Moreover, by the definition of formal proof used in this paper, $\vdash_{(n,k)}$ is finitary, and (by Theorem 3.4) it verifies Sintactic Deduction Theorem, as was already mentioned. From all this facts, and taking into account that both $\models_{(n,k)}$ and $\vdash_{(n,k)}$ are monotonic, strong adequacity is demonstrated. $\Box$

5 Concluding remarks

Despite its interest as a general result (for a countable, non-lineal family of logics), the adequate axiomatics shown here can be applied in different ways. First of all, a natural problem to be solved is the independence of the axiomatics presented here and it is part of a future work.

On the other hand, another of the possible uses of this axiomatics is the study of algebraizability of the $I^{n}P^{k}$-logics. It is worth to comment here that $I^{1}P^{0}$ is algebraizable (see [12]), as in the case of $I^{0}P^{1}$ (this fact was already indicated). Moreover, in [5] it was demonstrated that all the logics of ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$ are algebraizable. So, the properties of the class of algebras associated to each $I^{n}P^{k}$-logic deserve to be investigated. By the way, the class of algebras associated to $I^{0}P^{1}$ was already studied in [7] and in [9]. In both works, the axiomatics obtained for this logic are very useful for the study of the so-called class of $P^{1}$-algebras. This is because there is a connection between the axiomatics of an algebraizable logic and its equivalent algebraic semantics, cf. [1]. As a generalization of this fact, the axiomatics shown here would allow to study the different classes of (say) $I^{n}P^{k}$-algebras in a more efficient way.

Finally, note this fact about the complexity of the formulas: given a fixed logic $I^{n}P^{k}$, every formula $\phi\in L(C)$ with complexity $Comp(\phi)\geq max\{n,k\}$ behaves “in a classical way” (this fact is related to the inclusion of $Ax_{5}$ and $Ax_{6}$ in the axiomatics presented in this paper). This would suggest to define a special kind of logics: the family $\mathbb{SC}$ of “stationary classically logics”. Obviously, ${\mathbb{I}}^{n}{\mathbb{P}}^{k}$ would be a particular subclass of $\mathbb{SC}$. The study of the latter class deserves special attention in a future research.