Proof. It is an immediate consequence of Theorems 5.8 and 5.4.

Proof. Straightforward, by induction on the complexity of $\alpha $ .

Proof. By induction on k.

Base $k=0$ : Suppose that $\Gamma \vdash _{IPL}^0 \Delta $ . Then $\Gamma \Rightarrow \Delta $ is an instance of the axiom ( $Ax$ ), that is: $\Gamma \Rightarrow \Delta = \alpha ,\Gamma ' \Rightarrow \alpha $ for some multiset $\Gamma '$ . Let $v \in \mathcal {L}_0^{IPL}$ such that $v \models \Gamma ' \cup \{\alpha \}$ . In particular, $v \models \alpha $ , hence $v \models \Gamma \Rightarrow \Delta $ . From this, $\Gamma \models _0 \Delta $ .

Inductive step: Suppose that, for any sequent $\Gamma \Rightarrow \Delta $ , if $\Gamma \vdash _{IPL}^j \Delta $ then $\Gamma \models _j\Delta $ , for every $j \leq k$ , for a given $k \geq 0$ (induction hypothesis (IH)). Let $\Gamma \Rightarrow \Delta $ be a sequent such that $\Gamma \vdash _{IPL}^{k+1} \Delta $ . If $\Gamma \Rightarrow \Delta $ is an instance of the axiom, it can be proven as above that $\Gamma \models _{k+1}\Delta $ . Suppose now that $\Gamma \Rightarrow \Delta $ was obtained from other sequents by applying a rule of LI in a derivation of depth $k+1$ . We have the following cases:

( $contr\Rightarrow $ ): Suppose that $\Gamma \Rightarrow \Delta = \alpha ,\Gamma ' \Rightarrow \Delta $ is obtained from $\alpha ,\alpha ,\Gamma '\Rightarrow \Delta $ by applying rule ( $contr\Rightarrow $ ). Then $\alpha ,\alpha ,\Gamma ' \vdash _{IPL}^k \Delta $ and so $\alpha ,\alpha ,\Gamma ' \models _k \Delta $ , by (IH). But the latter clearly implies that $\alpha ,\Gamma ' \models _k \Delta $ and so $\alpha ,\Gamma ' \models _{k+1} \Delta $ , given that $\mathcal {L}_{k+1}^{IPL} \subseteq \mathcal {L}_k^{IPL}$ .

( $\Rightarrow w$ ): Suppose that $\Gamma \Rightarrow \Delta = \Gamma \Rightarrow \alpha $ is obtained from $\Gamma \Rightarrow $ by ( $\Rightarrow w$ ). Then $\Gamma \vdash _{IPL}^k $ and so, by (IH), $\Gamma \models _k$ . This means that, for every $v \in \mathcal {L}_k^{IPL}$ , $v\not \models \Gamma $ and so $v\models \Gamma \Rightarrow \alpha $ . From this it follows that $\Gamma \models _{k+1}\Delta $ , given that $\mathcal {L}_{k+1}^{IPL} \subseteq \mathcal {L}_k^{IPL}$ .

( $cut$ ): Assume that $\Gamma \Rightarrow \Delta $ follows from $\Gamma \Rightarrow \alpha $ and $\alpha , \Gamma \Rightarrow \Delta $ by ( $cut$ ) rule. Then $\Gamma \vdash _{IPL}^k\alpha $ and $\alpha , \Gamma \vdash _{IPL}^k\Delta $ and so, by (IH), $\Gamma \models _k\alpha $ and $\alpha , \Gamma \models _k\Delta $ . Suppose first that $\Delta =\emptyset $ . Let $v \in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma $ ; in particular, $v \in \mathcal {L}_{k}^{IPL}$ and so $v \models \Gamma \Rightarrow \alpha $ . From this it follows that $v\models \alpha $ . But this is impossible, given that $v \models \Gamma \cup \{\alpha \} \Rightarrow $ , by (IH). From this, $v \not \models \Gamma $ for every $v\in \mathcal {L}_{k+1}^{IPL}$ . That is, $v\models \Gamma \Rightarrow $ , for every $v\in \mathcal {L}_{k+1}^{IPL}$ . Now, suppose that $\Delta =\{\gamma \}$ for some formula $\gamma $ , and let $v\in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma $ . Once again, since $v \models \Gamma \Rightarrow \alpha $ we infer that $v\models \alpha $ . But then $v \models \Gamma \cup \{\alpha \}$ and so $v\models \gamma $ , given that $v \models \Gamma \cup \{\alpha \}\Rightarrow \gamma $ . This means that $v \models \Gamma \Rightarrow \Delta $ , for every $v\in \mathcal {L}_{k+1}^{IPL}$ . That is, $\Gamma \models _{k+1}\Delta $ .

( $\vee \Rightarrow $ ): Assume that $\Gamma \Rightarrow \Delta =\alpha \vee \beta ,\Gamma ' \Rightarrow \Delta $ follows from $\alpha , \Gamma '\Rightarrow \Delta $ and $\beta , \Gamma '\Rightarrow \Delta $ by ( $\vee \Rightarrow $ ). By (IH), $\alpha , \Gamma ' \models _k \Delta $ and $\beta , \Gamma ' \models _k \Delta $ . Suppose first that $\Delta =\emptyset $ . By hypothesis, if $v \in \mathcal {L}_{k+1}^{IPL}$ is such that $v\models \Gamma '$ , then $v\not \models \alpha $ and $v\not \models \beta $ , and so $v\not \models \alpha \vee \beta $ . This means that $v \models \Gamma ' \cup \{\alpha \vee \beta \}\Rightarrow $ , for every $v\in \mathcal {L}_{k+1}^{IPL}$ . Now, if $\Delta =\{\gamma \}$ for some formula $\gamma $ , let $v\in \mathcal {L}_{k+1}^{IPL}$ . By hypothesis, if $v\models \Gamma '$ and $v\models \alpha $ , then $v\models \gamma $ ; and if $v\models \Gamma '$ and $v\models \beta $ , then $v\models \gamma $ . From this, if $v\models \Gamma '$ and $v\models \alpha \vee \beta $ then, by definition of $\mathcal {M}_{IPL}$ , either $v\models \alpha $ or $v\models \beta $ and so, by hypothesis, $v\models \gamma $ . That is, $v \models \Gamma \Rightarrow \Delta $ for every $v\in \mathcal {L}_{k+1}^{IPL}$ and so $\Gamma \models _{k+1}\Delta $ .

( $\Rightarrow \vee _i$ ): It is enough to observe that, if either $v\models \alpha $ or $v\models \beta $ then $v\models \alpha \vee \beta $ , by definition of $\mathcal {M}_{IPL}$ .

( $\wedge \Rightarrow $ ): Suppose that $\Gamma \Rightarrow \Delta =\alpha \land \beta ,\Gamma ' \Rightarrow \Delta $ follows from $\alpha , \beta ,\Gamma '\Rightarrow \Delta $ by ( $\wedge \Rightarrow $ ). Assume first that $\Delta =\emptyset $ . Then, if $v \in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma '$ it follows that $v \not \models \{\alpha ,\beta \}$ , since $\mathcal {L}_{k+1}^{IPL} \subseteq \mathcal {L}_k^{IPL}$ and $\alpha , \beta ,\Gamma '\models _{k}\Delta $ by (IH). From this, either $v \not \models \alpha $ or $v \not \models \beta $ . By definition of $\mathcal {M}_{IPL}$ , $v \not \models \alpha \land \beta $ . That is, $v \not \models \Gamma ' \cup \{\alpha \land \beta \}$ for every $v\in \mathcal {L}_{k+1}^{IPL}$ , i.e., $\alpha \wedge \beta , \Gamma '\models _{k+1}$ . In turn, if $\Delta =\{\gamma \}$ for some formula $\gamma $ , let $v \in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma ' \cup \{\alpha \land \beta \}$ . By definition of $\mathcal {M}_{IPL}$ , $v \models \Gamma ' \cup \{\alpha ,\beta \}$ and so $v\models \gamma $ , by (IH) and the fact that $v \in \mathcal {L}_k^{IPL}$ . That is, $v\models \Gamma ' \cup \{\alpha \land \beta \}\Rightarrow \Delta $ for every $v\in \mathcal {L}_{k+1}^{IPL}$ .

( $\Rightarrow \wedge $ ): It is enough to observe that, if both $v\models \alpha $ and $v\models \beta $ then $v\models \alpha \wedge \beta $ , by definition of $\mathcal {M}_{IPL}$ .

( $\to \Rightarrow $ ) Suppose that $\Gamma \Rightarrow \Delta = \alpha \to \beta ,\Gamma '\Rightarrow \Delta $ is obtained from $\Gamma ' \Rightarrow \alpha $ and $\beta , \Gamma ' \Rightarrow \Delta $ by ( $\to \Rightarrow $ ). By (IH), $\Gamma '\models _{k} \alpha $ and $\beta , \Gamma ' \models _{k}\Delta $ . Assume first that $\Delta =\emptyset $ . Let $v \in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma ' \cup \{\alpha \to \beta \}$ . Then, $v \in \mathcal {L}_{k}^{IPL}$ such that $v \models \Gamma '$ and so $v\models \alpha $ , by hypothesis. Since $v \models \alpha \to \beta $ then $v \models \beta $ , by definition of $\mathcal {M}_{IPL}$ . That is, $v \in \mathcal {L}_{k}^{IPL}$ is such that $v \models \Gamma '\cup \{\beta \}$ , which contradicts the fact that $\beta , \Gamma ' \models _{k}$ . From this, $v \not \models \Gamma ' \cup \{\alpha \to \beta \}$ for every $v \in \mathcal {L}_{k+1}^{IPL}$ , which means that $\alpha \to \beta ,\Gamma '\models _{k+1}$ . Now, suppose that $\Delta =\{\gamma \}$ for some formula $\gamma $ . Let $v \in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma ' \cup \{\alpha \to \beta \}$ . By reasoning as above, $v \in \mathcal {L}_{k}^{IPL}$ is such that $v \models \Gamma '\cup \{\beta \}$ . But then $v \models \gamma $ , by hypothesis. This implies that $v \models \Gamma ' \cup \{\alpha \to \beta \} \Rightarrow \gamma $ for every $v \in \mathcal {L}_{k+1}^{IPL}$ .

( $\Rightarrow \to $ ): Assume that $\Gamma \Rightarrow \Delta = \Gamma \Rightarrow \alpha \to \beta $ is obtained from $\alpha , \Gamma \Rightarrow \beta $ by ( $\Rightarrow \to $ ). By (IH), $\alpha , \Gamma \models _{k} \beta $ . Let $v \in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma $ . Suppose that $v(\alpha \to \beta )=\mathbf {F}$ . By definition of $\mathcal {M}_{IPL}$ , $v(\alpha )=\mathbf {T}$ and $v(\beta ) \in \{\mathbf {U},\mathbf {F}\}$ . That is, $v \models \Gamma \cup \{\alpha \}$ but $v \not \models \beta $ , which contradicts the fact that $\alpha , \Gamma \models _{k} \beta $ , given that $v \in \mathcal {L}_{k}^{IPL}$ . Hence, $v(\alpha \to \beta )\neq \mathbf {F}$ . Suppose now that $v(\alpha \to \beta )=\mathbf {U}$ . By Definition 7.6 of level valuations, there exists $w \in \mathcal {L}_{k}^{IPL}$ such that $w(\alpha \to \beta )=\mathbf {F}$ and $w \models \Gamma $ . By reasoning as above, $w(\alpha )=\mathbf {T}$ and $w(\beta ) \in \{\mathbf {U},\mathbf {F}\}$ . But then $w \models \Gamma \cup \{\alpha \}$ and $w \not \models \beta $ , which contradicts the fact that $\alpha , \Gamma \models _{k} \beta $ . From this, it follows that $v(\alpha \to \beta )=\mathbf {T}$ . That is, $v\models \Gamma \Rightarrow \alpha \to \beta $ for every $v \in \mathcal {L}_{k+1}^{IPL}$ .

( $\neg \Rightarrow $ ): Assume that $\Gamma \Rightarrow \Delta = \neg \alpha ,\Gamma '\Rightarrow $ is obtained from $\Gamma ' \Rightarrow \alpha $ by ( $\neg \Rightarrow $ ). By (IH), $\Gamma '\models _{k} \alpha $ . Let $v \in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma ' \cup \{\neg \alpha \}$ . Then, $v \in \mathcal {L}_{k}^{IPL}$ such that $v \models \Gamma '$ and so $v \models \alpha $ , by hypothesis, which contradicts the fact that $v \models \neg \alpha $ . From this, $v \not \models \Gamma ' \cup \{\neg \alpha \}$ for every $v \in \mathcal {L}_{k+1}^{IPL}$ , which means that $\neg \alpha ,\Gamma '\models _{k+1}$ .

( $\Rightarrow \neg $ ): Assume that $\Gamma \Rightarrow \Delta = \Gamma \Rightarrow \neg \alpha $ is obtained from $\alpha , \Gamma \Rightarrow $ by ( $\Rightarrow \neg $ ). By (IH), $\alpha , \Gamma \models _{k} $ . Let $v \in \mathcal {L}_{k+1}^{IPL}$ such that $v \models \Gamma $ . Suppose that $v(\neg \alpha )=\mathbf {F}$ . By definition of $\mathcal {M}_{IPL}$ , $v(\alpha )=\mathbf {T}$ , hence $v \models \Gamma \cup \{\alpha \}$ , which contradicts the fact that $\alpha , \Gamma \models _{k}$ , since $v \in \mathcal {L}_{k}$ . Now, suppose that $v(\neg \alpha )=\mathbf {U}$ . By Definition 7.6 of level valuations, there exists $w \in \mathcal {L}_{k}^{IPL}$ such that $w(\neg \alpha )=\mathbf {F}$ and $w \models \Gamma $ . As proven above, $w(\alpha )=\mathbf {T}$ and so $w \models \Gamma \cup \{\alpha \}$ , contradicting the fact that $\alpha , \Gamma \models _{k}$ . From this, it follows that $v(\neg \alpha )=\mathbf {T}$ . That is, $v\models \Gamma \Rightarrow \neg \alpha $ for every $v \in \mathcal {L}_{k+1}^{IPL}$ .

This concludes the proof.

Proof. Suppose that $\Gamma \vdash _{IPL} \varphi $ . By definition, there exists a finite set $\Gamma _0 \subseteq \Gamma $ such that the sequent $\Gamma _0 \Rightarrow \varphi $ is derivable in LI. But then, there exists $k\geq 0$ such that $\Gamma _0 \vdash _{IPL}^k \varphi $ . By Proposition 7.11, $\Gamma _0\models _k \varphi $ . This implies that $\Gamma \models _{\mathcal {R}(\mathcal {M}_{IPL})} \varphi $ , given that $\mathcal {L}_{IPL} \subseteq \mathcal {L}_{k}^{IPL}$ .

Proof. Observe that, by definition and by Remark 7.13, $v_\Delta (\alpha )=\mathbf {T}$ iff $\alpha \in \Delta $ , for every formula $\alpha $ . Moreover, $v_\Delta (p) \in \{\mathbf {T},\mathbf {F}\}$ for every propositional variable p.

Negation: Let us prove first that $v_\Delta (\neg \alpha ) \in \neg ^{IPL}(v_\Delta (\alpha ))$ for every $\alpha $ . If $v_\Delta (\neg \alpha )=\mathbf {T}$ then $\neg \alpha \in \Delta $ , by definition. Hence, $\alpha \notin \Delta $ and so $v_\Delta (\alpha ) \in \{\mathbf {U},\mathbf {F}\}$ . From this, $v_\Delta (\neg \alpha ) = \mathbf {T} \in \{\mathbf {U},\mathbf {T}\}=\neg ^{IPL}(v_\Delta (\alpha ))$ . Now, if $v_\Delta (\neg \alpha )=\mathbf {U}$ then $\alpha \notin \Delta $ , by definition. Hence $v_\Delta (\alpha ) \in \{\mathbf {U},\mathbf {F}\}$ and so $v_\Delta (\neg \alpha ) = \mathbf {U} \in \{\mathbf {U},\mathbf {T}\}=\neg ^{IPL}(v_\Delta (\alpha ))$ . Finally, if $v_\Delta (\neg \alpha )=\mathbf {F}$ then $\alpha \in \Delta $ , by definition. Hence $v_\Delta (\alpha )=\mathbf {T}$ and so $v_\Delta (\neg \alpha ) = \mathbf {F} \in \{\mathbf {F}\}=\neg ^{IPL}(v_\Delta (\alpha ))$ .

Implication: There are three cases:

(I1) Suppose that $v_\Delta (\alpha \to \beta )=\mathbf {T}$ . Then $\alpha \to \beta \in \Delta $ , by definition.

– If $\alpha \notin \Delta $ then $v_\Delta (\alpha ) \in \{\mathbf {U},\mathbf {F}\}$ . Hence, $v_\Delta (\alpha \to \beta )=\mathbf {T} \in {\to }^{IPL}(v_\Delta (\alpha ),v_\Delta (\beta ))$ .

– If $\alpha \in \Delta $ then $\beta \in \Delta $ , by (DM). Hence $v_\Delta (\alpha )=v_\Delta (\beta )=\mathbf {T}$ and so $v_\Delta (\alpha \to \beta )=\mathbf {T} \in \{\mathbf {T}\}= {\to }^{IPL}(v_\Delta (\alpha ),v_\Delta (\beta ))$ .

(I2) Suppose that $v_\Delta (\alpha \to \beta )=\mathbf {U}$ . Then $\alpha \to \beta \notin \Delta $ and $\alpha \notin \Delta $ , by definition. Moreover, $\beta \notin \Delta $ , by Remark 7.13. Then $v_\Delta (\alpha ) \in \{\mathbf {U},\mathbf {F}\}$ and $v_\Delta (\beta ) \in \{\mathbf {U},\mathbf {F}\}$ . Hence, $v_\Delta (\alpha \to \beta )=\mathbf {U} \in \{\mathbf {U},\mathbf {T}\}={\to }^{IPL}(v_\Delta (\alpha ),v_\Delta (\beta ))$ .

(I3) Suppose that $v_\Delta (\alpha \to \beta )=\mathbf {F}$ . Then $\alpha \to \beta \notin \Delta $ and $\alpha \in \Delta $ , by definition. Moreover, $\beta \notin \Delta $ , by Remark 7.13. Then $v_\Delta (\alpha ) =\mathbf {T}$ and $v_\Delta (\beta ) \in \{\mathbf {U},\mathbf {F}\}$ . Hence, $v_\Delta (\alpha \to \beta )=\mathbf {F} \in \{\mathbf {F}\}={\to }^{IPL}(v_\Delta (\alpha ),v_\Delta (\beta ))$ .

Conjunction: There are two cases:

(C1) Suppose that $v_\Delta (\alpha \land \beta )=\mathbf {T}$ . Then $\alpha \in \Delta $ and $\beta \in \Delta $ , by definition. From this, $v_\Delta (\alpha )=v_\Delta (\beta )=\mathbf {T}$ . Hence, $v_\Delta (\alpha \land \beta )=\mathbf {T} \in \{\mathbf {T}\}= \land ^{IPL}(v_\Delta (\alpha ),v_\Delta (\beta ))$ .

(C2) Suppose that $v_\Delta (\alpha \land \beta )=\mathbf {F}$ . Then, either $\alpha \notin \Delta $ or $\beta \notin \Delta $ , by definition. From this, $v_\Delta (\alpha ) \in \{\mathbf {U},\mathbf {F}\}$ or $v_\Delta (\beta ) \in \{\mathbf {U},\mathbf {F}\}$ . Hence, $v_\Delta (\alpha \land \beta )=\mathbf {F} \in \{\mathbf {F}\}= \land ^{IPL}(v_\Delta (\alpha ),v_\Delta (\beta ))$ .

Disjunction: There are two cases:

(D1) Suppose that $v_\Delta (\alpha \vee \beta )=\mathbf {T}$ . Then, either $\alpha \in \Delta $ or $\beta \in \Delta $ , by definition. From this, $v_\Delta (\alpha )=\mathbf {T}$ or $v_\Delta (\beta )=\mathbf {T}$ . Hence, $v_\Delta (\alpha \vee \beta )=\mathbf {T} \in \{\mathbf {T}\}= \vee ^{IPL}(v_\Delta (\alpha ),v_\Delta (\beta ))$ .

(D2) Suppose that $v_\Delta (\alpha \vee \beta )=\mathbf {F}$ . Then $\alpha \notin \Delta $ and $\beta \notin \Delta $ , by definition. From this, $v_\Delta (\alpha ) \in \{\mathbf {U},\mathbf {F}\}$ and $v_\Delta (\beta ) \in \{\mathbf {U},\mathbf {F}\}$ . Hence, $v_\Delta (\alpha \land \beta )=\mathbf {F} \in \{\mathbf {F}\}= \vee ^{IPL}(v_\Delta (\alpha ),v_\Delta (\beta ))$ .

This concludes the proof.

Proof. By Proposition 7.16, $v_\Delta (\alpha )=\mathbf {T}$ iff $\alpha \in \Delta $ for every $\alpha $ . It will be shown, by induction on n, that $v_\Delta \in \mathcal {L}^{IPL}_n$ for every $n \geq 0$ .

Base $n=0$ : $v_\Delta \in \mathcal {L}^{IPL}_0 = Val^{nd}_+(\mathcal {M}_{IPL})$ , by Proposition 7.16.

Inductive step: Assume that, for every $\varphi '$ and for every $\varphi '$ -saturated set $\Delta '$ , $v_{\Delta '} \in \mathcal {L}^{IPL}_k$ for every $k \leq n$ , for a given $n \geq 0$ (IH). Let us prove that $v_\Delta \in \mathcal {L}^{IPL}_{n+1}$ . By IH, $v_\Delta \in \mathcal {L}^{IPL}_n$ . Let $\alpha \in For(\Omega )$ such that $v_\Delta (\alpha )=\mathbf {U}$ . By Definition 7.14, $\alpha \neq p$ for every propositional variable p; and $\alpha \neq \beta \# \gamma $ for $\#\in \{\land ,\vee \}$ and every formulas $\beta ,\gamma $ . Then, there are two cases to analyze:

(1) $\alpha =\neg \beta $ for some $\beta $ . By Definition 7.14, $\neg \beta \not \in \Delta $ and $\beta \not \in \Delta $ . Suppose that $\Delta ,\beta \vdash _{IPL} \neg \beta $ . By the DM, $\Delta \vdash _{IPL} \beta \to \neg \beta $ , and so the sequent $\Delta _0 \Rightarrow \beta \to \neg \beta $ is provable in LI, for some finite set $\Delta _0 \subseteq \Delta $ . But, for every finite multiset $\Gamma $ , the sequent $\Gamma ,\beta \to \neg \beta \Rightarrow \neg \beta $ is provable in LI. Indeed, from axiom $\Gamma ,\beta \Rightarrow \beta $ it follows $\Gamma ,\beta , \neg \beta \Rightarrow $ , by ( $\neg \Rightarrow $ ). From this, and by using axiom $\Gamma ,\beta \Rightarrow \beta $ once again, by ( $\to \Rightarrow $ ) we infer $\Gamma ,\beta , \beta \to \neg \beta \Rightarrow $ . Finally, $\Gamma ,\beta \to \neg \beta \Rightarrow \neg \beta $ follows by ( $\Rightarrow \neg $ ). In particular, $\Delta _0,\beta \to \neg \beta \Rightarrow \neg \beta $ is provable in LI and so, by ( $cut$ ) with $\Delta _0 \Rightarrow \beta \to \neg \beta $ , it follows that $\Delta _0 \Rightarrow \neg \beta $ is provable in LI. That is, $\Delta \vdash _{IPL} \neg \beta $ , hence $\neg \beta \in \Delta $ , a contradiction. From this, $\Delta ,\beta \nvdash _{IPL} \neg \beta $ . Then, there exists a $\neg \beta $ -saturated set $\Delta '$ in IPL such that $\Delta \cup \{\beta \} \subseteq \Delta '$ . By IH, $v_{\Delta '} \in \mathcal {L}^{IPL}_n$ such that, by Definition 7.14, $v_{\Delta '}(\neg \beta )=\mathbf {F}$ . Moreover, for every $\delta \in For(\Omega )$ , if $v_\Delta (\delta )=\mathbf {T}$ then $v_{\Delta '}(\delta )=\mathbf {T}$ , since $\Delta \subseteq \Delta '$ .

(2) $\alpha =\beta \to \gamma $ for some $\beta $ and $\gamma $ . By Definition 7.14, $\beta \to \gamma \not \in \Delta $ and $\beta \not \in \Delta $ . Suppose that $\Delta ,\beta \vdash _{IPL} \beta \to \gamma $ . By (DM), $\Delta ,\beta \vdash _{IPL} \gamma $ and so, by (DM) again, $\Delta \vdash _{IPL} \beta \to \gamma $ , a contradiction. From this, $\Delta ,\beta \nvdash _{IPL} \beta \to \gamma $ . Then, there exists a $(\beta \to \gamma )$ -saturated set $\Delta "$ in IPL such that $\Delta \cup \{\beta \} \subseteq \Delta "$ . By IH, $v_{\Delta "} \in \mathcal {L}^{IPL}_n$ such that, by Definition 7.14, $v_{\Delta "}(\beta \to \gamma )=\mathbf {F}$ . Moreover, for every $\delta \in For(\Omega )$ , if $v_\Delta (\delta )=\mathbf {T}$ then $v_{\Delta "}(\delta )=\mathbf {T}$ , since $\Delta \subseteq \Delta "$ .

From the previous analysis we conclude that $v_\Delta \in \mathcal {L}^{IPL}_{n+1}$ . This shows that $v_\Delta \in \mathcal {L}^{IPL}_{n}$ for every $n \geq 0$ and so $v_\Delta \in \mathcal {L}_{IPL}$ .

Proof. Suppose that $\Gamma \nvdash _{IPL} \varphi $ . Then, there exists a $\varphi $ -saturated set $\Delta $ in LI such that $\Gamma \subseteq \Delta $ . By Proposition 7.17, $v_\Delta $ is a level valuation in $\mathcal {M}_{IPL}$ such that $v_\Delta (\alpha )=\mathbf {T}$ for every $\alpha \in \Gamma $ , but $v_\Delta (\varphi )\neq \mathbf {T}$ . This shows that $\Gamma \not \models _{ \mathcal {R}(\mathcal {M}_{IPL})} \varphi $ .

Proof. It follows from Theorems 7.18 and 7.12 and the fact that LI is finitary.

Proof. It follows from Theorems 7.18 and 7.12 and the fact that $\mathbf {LI}$ satisfies the DM (recall Remark 7.8).

Proof. Let $\Gamma =\{\alpha \in For(\Omega ) \mid v(\alpha )=\mathbf {T}\}$ and suppose that $\Gamma \vdash _{IPL} \alpha $ . By the soundness of ${IPL}$ w.r.t. level valuation semantics (Theorem 7.12), $\Gamma \models _{\mathcal {R}(\mathcal {M}_{IPL})} \alpha $ . Given that $v \in \mathcal {L}_{IPL}$ such that $v\models \Gamma $ , it follows that $v \models \alpha $ . That is, $v(\alpha )=\mathbf {T}$ and so $\alpha \in \Gamma $ .

Proof. $v \in \mathcal {L}_{IPL}$ , and $\alpha \in For(\Omega )$ such that $v(\alpha )=\mathbf {U}$ . Since, in particular, $v \in Val^{nd}_+(\mathcal {M}_{IPL})$ (recall Definitions 7.5 and 7.6), $v(\alpha )=\mathbf {U}$ implies that $\alpha $ cannot be a propositional variable. By definition of the conjunction and disjunction tables in $\mathcal {M}_{IPL}$ (Figure 5), and since $v(\alpha )=\mathbf {U}$ , it follows that $\alpha $ cannot be either a conjunction or a disjunction. Let $\Gamma =\{\gamma \in For(\Omega ) \mid v(\gamma )=\mathbf {T}\}$ . Then, $\alpha \not \in \Gamma $ . By the observations above, there are only two cases to consider:

(1) $\alpha =\neg \beta $ for some $\beta $ . As noted above, $\alpha \not \in \Gamma $ , i.e., $\neg \beta \not \in \Gamma $ . Hence $\Gamma \nvdash _{IPL}\neg \beta $ , given that $\Gamma $ is closed by Proposition 7.20. If $\beta \in \Gamma $ then $v(\beta )=\mathbf {T}$ and so, by definition of $\mathcal {M}_{IPL}$ , $v(\alpha )=v(\neg \beta )=\mathbf {F}$ , a contradiction. Then, $\beta \not \in \Gamma $ . Suppose that $\Gamma ,\beta \vdash _{IPL}\neg \beta $ . As in the proof of Proposition 7.17 we infer that $\Gamma \vdash _{IPL}\neg \beta $ . But this leads us to a contradiction since, as pointed out before, $\Gamma \nvdash _{IPL}\neg \beta $ . From this, $\Gamma ,\beta \nvdash _{IPL}\neg \beta $ . Thus, there exists a $\neg \beta $ -saturated set $\Delta $ in ${IPL}$ such that $\Gamma \cup \{\beta \} \subseteq \Delta $ . By Proposition 7.17, the function $v_\Delta $ is a level valuation such that $v_\Delta (\alpha )=\mathbf {F}$ (since $v_\Delta (\beta )=\mathbf {T}$ ) and $v_\Delta (\gamma )=\mathbf {T}$ for every formula $\gamma $ such that $v(\gamma )=\mathbf {T}$ , as required.

(2) $\alpha =\beta \to \delta $ for some $\beta $ and $\delta $ . Since $\Gamma ,\delta \vdash _{IPL} \beta \to \delta $ and $\Gamma \nvdash _{IPL} \beta \to \delta $ then $\Gamma \nvdash _{IPL} \delta $ . Suppose that $\Gamma ,\beta \vdash _{IPL}\beta \to \delta $ . By (DM), $\Gamma ,\beta \vdash _{IPL} \delta $ and so, by (DM) again, $\Gamma \vdash _{IPL}\beta \to \delta $ , a contradiction. From this, $\Gamma ,\beta \nvdash _{IPL}\beta \to \delta $ . Thus, there exists a $(\beta \to \delta )$ -saturated set $\Delta $ in ${IPL}$ such that $\Gamma \cup \{\beta \} \subseteq \Delta $ . By reasoning as above, we conclude that $\delta \not \in \Delta $ . By Proposition 7.17, $v_\Delta \in \mathcal {L}_{IPL}$ is such that $v_\Delta (\alpha )=\mathbf {F}$ (since $v_\Delta (\beta )=\mathbf {T}$ and $v(\delta )\neq \mathbf {T}$ ) and $v_\Delta (\gamma )=\mathbf {T}$ for every formula $\gamma $ such that $v(\gamma )=\mathbf {T}$ , as required.

Notation 8.6. Given $\Lambda \in FCS(\Omega )$ with $n\geq 1$ elements, consider an arrangement $\alpha _1, \ldots ,\alpha _n$ of this set such that the complexity of $\alpha _i$ is less than or equal to the complexity of $\alpha _j$ if $i < j$ (so the atomic formulas occurring in $\Lambda $ appear as the first elements of the sequence, in arbitrary order). In this way, any subformula of $\alpha _j$ appears as $\alpha _i$ for some unique $i\leq j$ . Suppose that the set $iPV(\Lambda )$ has $m \geq 1$ elements. Consider now an arrangement $v_p^1, \ldots , v_p^m$ of its elements, ordered by lexicographical order, by stipulating that $\mathbf {F} < \mathbf {U} < \mathbf {T}$ . In this way, $iPV(\Lambda )$ can be represented as a two-dimensional array (i.e., an array of arrays, or a matrix) V such that each row $V[i]$ , for $1 \leq i \leq m$ , corresponds to the $ith$ element $v_p^i$ of $iPV(\Lambda )$ . In turn, $V[i][j]$ is the truth-value assigned to the formula $\alpha _j \in \Lambda $ by the partial valuation $V[i]= v_p^i$ . That is, $V[i][j] = v_p^i(\alpha _j)$ . This notation will be used in Algorithm 1, to be described in the sequel, also for subsets of $iPV(\Lambda )$ .

Proof. Given $\Lambda \in FCS(\Omega )$ , define the sequences $(\alpha _1, \ldots ,\alpha _n)$ and $(v_p^1, \ldots , v_p^m)$ representing $\Lambda $ and $iPV(\Lambda )$ as in Notation 8.6, and then execute Algorithm 1 as described. Notice that $iPV(\Lambda )$ is a finite set, and the algorithm operates on a subset $V \subseteq iPV(\Lambda )$ in each round. If the algorithm does not stop in a given round, it deletes some elements from V and restarts the process with a new subset that is strictly smaller than the previous one. This shows that the process will eventually terminate. There are two possible termination conditions: either every element of V is eliminated, or a set $IPV = V$ is produced. In the second case, every element of $IPV$ is supported (as no removal is possible at this point); hence, $iPLV(\Lambda ):=IPV$ satisfies the condition of Remark 8.4. In turn, the first possibility (arriving to a set $IPV=\emptyset $ ) is impossible by the following reason: every partial valuation $v :\Lambda \rightarrow V_{IPL}$ such that $v(\alpha ) \in \{\mathbf {T},\mathbf {F}\}$ for every $\alpha \in \Lambda $ (i.e., every classical partial valuation) is never removed from $iPV(\Lambda )$ by means of Algorithm 1. Indeed, any classical valuation v never satisfies that $v(\alpha _j)=\mathbf {U}$ for some j, hence it will never be removed. Since there are exactly $2^k$ classical valuations in $iPV(\Lambda )$ (where k is the number of different propositional variables occurring in $\Lambda $ ), the set $IPV$ produced by Algorithm 1 is non-empty, having at least $2^k$ elements. We have proven, therefore, the existence of a (non-empty) subset $IPV$ of $iPV(\Lambda )$ satisfying the condition of Remark 8.4.