1 Introduction
Omniscience principles have been playing an important role in neutral (Bishop’s) constructive mathematics [Reference Bishop3–Reference Bridges and Richman5, Reference Bridges and Vîţă7]. Those are principles which are derivable in classical logic but underivable in intuitionistic logic, and are used to construct a weak counterexample which shows that a statement is constructively underivable by proving that the statement implies an omniscience principle, in contrast with a counterexample which shows that a statement is false. Also omniscience principles have been a driving force of constructive reverse mathematics [Reference Ishihara18] where we are interested in which (omniscience) principle is necessary and sufficient to prove a (constructively underivable) theorem (see also [Reference Simpson30, Reference Veldman34] for classical reverse mathematics).
Then, necessarily, separations among omniscience principles have become crucial. Akama et al. [Reference Akama, Berardi, Hayashi, Kohlenbach and Ganzinger1] showed some separations in intuitionistic first-order arithmetic
$\mathbf {HA}$
using, case by case, an extension of
$\mathbf {HA}$
, the Kleene realizability, the monotone modified realizability, and the Lifschitz realizability (see also [Reference Kohlenbach24]). Would there be any uniform technique for separating omniscience principles? In this paper, we present a possible direction of finding such a uniform technique.
The omniscience principle, called Markov’s principle (
$\mathrm {MP}$
), is of the form:
$$\begin{align*}\forall x (A \lor \lnot A) \mathbin{\rightarrow} (\lnot\lnot \exists x A \mathbin{\rightarrow} \exists x A) , \end{align*}$$
and it has a special case (
$\mathrm {MP}_{\mathrm {PR}}$
):
$$\begin{align*}\lnot\lnot \exists x A \mathbin{\rightarrow} \exists x A \quad (A\ \mbox{primitive recursive}) \end{align*}$$
(see [Reference Troelstra and van Dalen33, Chapter 4, Section 5]). Note that
$\mathrm {MP}_{\mathrm {PR}}$
is a substitution instance of double negation elimination (
$\mathrm {DNE}$
):
$$\begin{align*}\lnot\lnot p \mathbin{\rightarrow} p \end{align*}$$
in intuitionistic propositional logic
$\mathbf {IPC}$
by a
$\Sigma _1$
-formula
$\exists x A$
, and
$\mathrm {DNE}$
is refuted in the IPC-Kripke model given by Figure 1. The weak limited principle of omniscience (
$\mathrm {WLPO}$
) is an omniscience principle of the form:
$$\begin{align*}\forall x (A \lor \lnot A) \mathbin{\rightarrow} (\lnot \exists x A \lor \lnot\lnot \exists x A) , \end{align*}$$
and its special case (
$\mathrm {WLPO}_{\mathrm {PR}}$
) is the following:
$$\begin{align*}\lnot \exists x A \lor \lnot\lnot \exists x A \quad (A\ \mbox{primitive recursive}). \end{align*}$$
Note that
$\mathrm {WLPO}_{\mathrm {PR}}$
is a substitution instance of the weak principle of the excluded middle (
$\mathrm {WPEM}$
):
$$\begin{align*}\lnot p \lor \lnot\lnot p \end{align*}$$
in
$\mathbf {IPC}$
by a
$\Sigma _1$
-formula
$\exists x A$
, and
$\mathrm {WPEM}$
is valid in the above IPC-Kripke model (even valid on the frame). Therefore the IPC-Kripke model may be used to separate
$\mathrm {MP}_{\mathrm {PR}}$
from
$\mathrm {WLPO}_{\mathrm {PR}}$
.
Figure 1 Kripke model refuting DNE.
The special cases of many omniscience principles, such as the limited principle of omniscience (
$\mathrm {LPO}$
), the lesser limited principle of omniscience (
$\mathrm {LLPO}$
), the disjunctive Markov principle (
$\mathrm {MP}^\lor $
), and
$\Delta _1\mbox {-}\mathrm {PEM}$
, are substitu tion instances of propositional formulae, such as the principle of the excluded middle (
$\mathrm {PEM}$
):
$ p \lor \lnot p , $
De Morgan’s law (
$\mathrm {DML}$
):
$ \lnot (p \land q) \mathbin {\rightarrow } \lnot p \lor \lnot q , $
weak De Morgan’s law (
$\mathrm {WDML}$
):
$ \lnot (\lnot p \land \lnot q) \mathbin {\rightarrow } \lnot \lnot p \lor \lnot \lnot q , $
and the restricted principle of the excluded middle (
$\mathrm {RPEM}$
):
$ (p \mathbin {\leftrightarrow } \lnot q) \mathbin {\rightarrow } p \lor \lnot p , $
respectively, by
$\Sigma _1$
-formulae. Figure 2 shows implications among those special cases. For
$\mathrm {LPO}$
and
$\mathrm {LLPO}$
, see [Reference Troelstra and van Dalen33, Chapter 4, Section 3.4] where those are called
$\exists \mbox {-}\mathrm {PEM}$
and
$\mathrm {SEP}$
, respectively; for
$\mathrm {MP}^\lor $
, see [Reference Ishihara17, Reference Mandelkern28] where it is called
$\mathrm {LLPE}$
; for
$\Delta _1\mbox {-}\mathrm {PEM}$
, see [Reference Fujiwara, Ishihara and Nemoto9] where it is called
$\mathrm {III}_a$
, and [Reference Kohlenbach25] where it is called
$\Delta ^0_1\mbox {-}\mathrm {LEM}$
.
Figure 2 Derivabilities between omniscience principles.
Of course, there are exceptions (see [Reference Ishihara16, Reference Ishihara17, Reference Kohlenbach23]). However, since IPC-Kripke models are simple and easy to handle, a method of separation based on an IPC-Kripke model would give us a good uniform technique for separating many omniscience principles.
In this paper, we aim at developing a systematic method of separating omniscience principles by constructing Kripke models for intuitionistic predicate logic
$\mathbf {IQC}$
and
$\mathbf {HA}$
from an IPC-Kripke model. A similar approach was adopted by de Jongh and Smoryński to show underivability of substitution instances of propositional formulae in
$\mathbf {HA}$
(see [Reference Smoryński32, Chapter V, Section 3], and also [Reference Visser35]). Here we are interested in not only underivability, but also separation between substitution instances of propositional formulae in
$\mathbf {IQC}$
and
$\mathbf {HA}$
. In Section 2, we introduce the notion of an extended frame which will play a crucial role in the following sections. We show that each IPC-Kripke model generates an extended frame and show a separation theorem (Theorem 2.7). We give several examples of the extended frame generated by an IPC-Kripke model. In Section 3, we introduce the notion of a schema, and, by using the extended frame generated by an IPC-Kripke model, give a separation theorem (Theorem 3.15) of a schema from a set of schemata in
$\mathbf {IQC}$
. We then apply the separation theorem to the examples in the previous section. In Section 4, we apply the results in the previous section to
$\mathbf {HA}$
, and show a separation theorem (Theorem 4.17) of a sentence from a set of schemata. We then see the examples which give us separations among omniscience principles. We conclude the paper with discussing a possible relativization of the results and lifting Theorem 4.17 up to
$\Sigma _{n}$
-level.
To quickly grasp the story of the paper, follow Definition 2.1, Remark 2.2, Definition 2.3, Example 2.4, Remark 2.6, Theorem 2.7, and Examples 2.10–2.14 in Section 2; Definition 3.7, Definition 3.8, Definition 3.11, Theorem 3.15, and Example 3.16 in Section 3; Definition 4.15, Theorem 4.17, Example 4.18, Theorem 4.23, and Example 4.24 in Section 4.
We use classical logic and set theory at the meta-level.
2 Extended frames
In this section, we introduce the notion of an extended frame which will play a crucial role in the following sections. We show that each IPC-Kripke model generates an extended frame and show a separation theorem (Theorem 2.7). We give several examples (Examples 2.10–2.14) of the extended frame generated by an IPC-Kripke model.
We use the standard language
$\mathcal {L}(\mathbf {IPC})$
of intuitionistic propositional logic
$\mathbf {IPC}$
containing the (countable) set
$\mathcal {V}$
of propositional variables, and
$\land , \lor , \mathbin {\rightarrow }$
, and
$\bot $
as primitive logical operators. Prime formulae are atomic formulae (propositional variables) or
$\bot $
, and we introduce the abbreviations
$\lnot \varphi \equiv \varphi \mathbin {\rightarrow } \bot $
and
$\varphi \mathbin {\leftrightarrow } \psi \equiv (\varphi \mathbin {\rightarrow } \psi ) \land (\psi \mathbin {\rightarrow } \varphi )$
. The set
$\mathrm {Vars}(\varphi )$
of propositional variables in a formula
$\varphi $
is defined as usual:
$\mathrm {Vars}(\bot ) = \emptyset $
;
$\mathrm {Vars}(p) = \{p\}$
;
$\mathrm {Vars}(\varphi \circ \psi ) = \mathrm {Vars}(\varphi ) \cup \mathrm {Vars}(\psi )$
for
$\circ \in \{\land ,\lor ,\mathbin {\rightarrow }\}$
. We sometimes write
$\varphi [p_1,\ldots ,p_n]$
for a formula
$\varphi $
with
$\mathrm {Vars}(\varphi ) = \{p_1,\ldots ,p_n\}$
. For a formula
$\varphi $
, a sequence
$\vec {p} \equiv p_1,\ldots ,p_n$
of distinct variables and a sequence
$\vec {\chi } \equiv \chi _1, \ldots , \chi _n$
of formulae, the (simultaneous) substitution
$ \varphi [\vec {p}/\vec {\chi }] $
is defined as usual:
$ \bot [\vec {p}/\vec {\chi }] \equiv \bot; $
$ q[\vec {p}/\vec {\chi }] \equiv \chi _m $
if
$q \equiv p_m$
for some
$m \in \{1,\ldots ,n\}$
, q otherwise;
$ (\varphi \circ \psi )[\vec {p}/\vec {\chi }] \equiv \varphi [\vec {p}/\vec {\chi }] \circ \psi [\vec {p}/\vec {\chi }] $
for
$\circ \in \{\land ,\lor ,\mathbin {\rightarrow }\}$
. For a formula
$\varphi [p_1,\ldots ,p_n]$
, we write
$\varphi [\chi _1,\ldots ,\chi _n]$
for
$\varphi [\vec {p}/\vec {\chi }]$
. In the following, we use
$\vdash _{\mathbf {IPC}}$
for deducibility in
$\mathbf {IPC}$
, and sometimes write
$\mathbf {IPC}$
for the set of theorems of
$\mathbf {IPC}$
.
Let
$(K, \leq )$
be a partially ordered set. Then a subset S of K is upward closed if
$k \in S$
and
$k \leq k'$
imply
$k' \in S$
for all
$k, k' \in K$
, and we write
$\Omega _K$
for the class of upward closed subsets of K. For each
$k \in K$
, we write
$\mathop {\uparrow } k$
for the upward closed subset
$ \{ k' \in K \mid k \leq k' \} , $
and for each subset S of K, we write
$\mathop {\uparrow } S$
for the upward closed subset
$ \bigcup _{k \in S} \mathop {\uparrow } k. $
Definition 2.1. A frame is a nonempty partially ordered set
$(K, \leq )$
. A valuation
$\Vdash $
on a frame
$(K,\leq )$
is a binary relation between K and
$\mathcal {V}$
such that
$$\begin{align*}k \Vdash p\text{ and }k \leq k' \mathbin{\Rightarrow} k' \Vdash p \end{align*}$$
for all
$k, k' \in K$
and
$p \in \mathcal {V}$
, that is,
$ \{ k \in K \mid k \Vdash p \} \in \Omega _K $
for all
$p \in \mathcal {V}$
. The valuation
$\Vdash $
is then extended to logically compound formulae of
$\mathcal {L}(\mathbf {IPC})$
by the following clauses.
-
1.
$k \not \Vdash \bot $
. -
2.
${k \Vdash \varphi \land \psi } \mathbin {\Leftrightarrow } k \Vdash \varphi \text { and }k \Vdash \psi .$
-
3.
${k \Vdash \varphi \lor \psi } \mathbin {\Leftrightarrow } k \Vdash \varphi \text { or }k \Vdash \psi .$
-
4.
${k \Vdash \varphi \mathbin {\rightarrow } \psi } \mathbin {\Leftrightarrow } k' \Vdash \varphi \text { implies }k' \Vdash \psi \text { for all }k' \geq k$
.
Note that
$ \{ k \in K \mid k \Vdash \varphi \} \in \Omega _K $
for all formula
$\varphi $
. An IPC-Kripke model is a triple
$\mathcal {K} = (K,\leq ,\Vdash )$
, where
$(K,\leq )$
is a frame, and
$\Vdash $
is a valuation on it. A formula
$\varphi $
is valid in
$\mathcal {K}$
if
$k \Vdash \varphi $
for all
$k \in K$
, and we then write
$\mathcal {K} \Vdash \varphi $
(see [Reference Troelstra and van Dalen33, 2.5.2–2.5.4]). A formula
$\varphi $
is valid on the frame
$(K,\leq )$
if
$\mathcal {K} \Vdash \varphi $
for all IPC-Kripke model
$\mathcal {K} = (K,\leq ,\Vdash )$
, that is, for all valuation
$\Vdash $
on
$(K,\leq )$
, and we then write
$(K,\leq ) \models \varphi $
.
Remark 2.2. The set
$$\begin{align*}L(K,\leq) = \{ \varphi \mid (K,\leq) \models \varphi \} \end{align*}$$
of formulae forms an intermediate propositional logic (or simply, a logic) in the following sense:
$ \mathbf {IPC} \subseteq L(K,\leq ) \subseteq \mathbf {CPC} , $
where
$\mathbf {CPC}$
is (the set of theorems of) classical propositional logic; if
$\varphi \mathbin {\rightarrow } \psi , \varphi \in L(K,\leq )$
, then
$\psi \in L(K,\leq )$
; if
$\varphi \in L(K,\leq )$
, then
$\varphi [\vec {p}/\vec {\chi }] \in L(K,\leq )$
for all sequence
$\vec {p}$
of distinct propositional variables and sequence
$\vec {\chi }$
of formulae.
Definition 2.3. An extended frame
$\mathcal {E} = ((K,\leq ),f,(I,\leq _I))$
is a triple of frames
$(K,\leq )$
and
$(I,\leq _I)$
, and a monotone mapping f between them, that is,
$k \leq k'$
implies
$f(k) \leq _I f(k')$
for all
$k, k' \in K$
. Each IPC-Kripke model
$\mathcal {I} = (I,\leq _I,\Vdash )$
induces an IPC-Kripke model
$\mathcal {K}_{\mathcal {E},\mathcal {I}} = (K,\leq ,\Vdash _{\mathcal {E},\mathcal {I}})$
by defining
$$\begin{align*}k \Vdash_{\mathcal{E},\mathcal{I}} p \mathbin{\Leftrightarrow} f(k) \Vdash p \end{align*}$$
for each
$k \in K$
and
$p \in \mathcal {V}$
. A formula
$\varphi $
is valid on
$\mathcal {E}$
if
$\mathcal {K}_{\mathcal {E},\mathcal {I}} \Vdash _{\mathcal {E},\mathcal {I}} \varphi $
for all IPC-Kripke model
$\mathcal {I} = (I,\leq _I,\Vdash )$
, that is, for all valuation
$\Vdash $
on
$(I,\leq _I)$
; we then write
$ \mathcal {E} \models \varphi. $
A trivial example of an extended frame is
$((K,\leq ),\mathrm {id}_K,(K,\leq ))$
for a frame
$(K,\leq )$
, and a simple, but non-trivial example is given in Figure 3.
Figure 3 An example of extended frame.
Example 2.4. Let
$\mathcal {K} = (K,\leq ,\Vdash )$
be an IPC-Kripke model, and define a set
$\Phi _{\mathcal {K}}$
of upward closed subsets of K by
$$\begin{align*}\Phi_{\mathcal{K}} = \{\{k \in K \mid k \Vdash p\} \mid p \in \mathcal{V}\}. \end{align*}$$
Define binary relations
$\preceq _{\mathcal {K}}$
and
$\sim _{\mathcal {K}}$
on K by
$$ \begin{align*} k \preceq_{\mathcal{K}} k' & \mathbin{\Leftrightarrow} \forall U \in \Phi_{\mathcal{K}} (k \in U \mathbin{\Rightarrow} k' \in U) , \\ k \sim_{\mathcal{K}} k' & \mathbin{\Leftrightarrow} k \preceq_{\mathcal{K}} k' \land k' \preceq_{\mathcal{K}} k. \end{align*} $$
Then
$\preceq _{\mathcal {K}}$
is a preorder and
$\sim _{\mathcal {K}}$
is an equivalence relation on K. Let
$$ \begin{align*} I_{\mathcal{K}} & = K/\sim_{\mathcal{K}} , & [k]_{\mathcal{K}} \leq_{\mathcal{K}} [k']_{\mathcal{K}} & \mathbin{\Leftrightarrow} k \preceq_{\mathcal{K}} k' , & f_{\mathcal{K}}(k) & = [k]_{\mathcal{K}} , \end{align*} $$
where
$[k]_{\mathcal {K}}$
is the equivalence class of k with respect to
$\sim _{\mathcal {K}}$
. Then
$$\begin{align*}\mathcal{E}_{\mathcal{K}} = ((K,\leq),f_{\mathcal{K}},(I_{\mathcal{K}},\leq_{\mathcal{K}})) \end{align*}$$
is an extended frame, and we call it the extended frame generated by the IPC-Kripke model
$\mathcal {K}$
.
Example 2.5. Let
$\mathcal {K} = (K,\leq ,\Vdash )$
be an IPC-Kripke model, and define a valuation
$\Vdash _{\mathcal {K}}$
on the frame
$(I_{\mathcal {K}},\leq _{\mathcal {K}})$
, introduced in Example 2.4, by
$$\begin{align*}[k]_{\mathcal{K}} \Vdash_{\mathcal{K}} p \mathbin{\Leftrightarrow} k \Vdash p \end{align*}$$
for each
$[k]_{\mathcal {K}} \in I_{\mathcal {K}}$
and
$p \in \mathcal {V}$
. Then
$\mathcal {I}_{\mathcal {K}} = (I_{\mathcal {K}},\leq _{\mathcal {K}},\Vdash _{\mathcal {K}})$
is an IPC-Kripke model, and induces an IPC-Kripke model
$\mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}_{\mathcal {K}}} = (K,\leq ,\Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}_{\mathcal {K}}})$
. Since
$$\begin{align*}k \Vdash p \mathbin{\Leftrightarrow} [k]_{\mathcal{K}} \Vdash_{\mathcal{K}} p \mathbin{\Leftrightarrow} k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}_{\mathcal{K}}} p \end{align*}$$
for all
$k \in K$
and
$p \in \mathcal {V}$
, we have
$$\begin{align*}k \Vdash \varphi \mathbin{\Leftrightarrow} k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}_{\mathcal{K}}} \varphi \end{align*}$$
for all
$k \in K$
and formula
$\varphi $
of
$\mathcal {L}(\mathbf {IPC})$
.
Remark 2.6. Let
$\mathcal {E} = ((K,\leq ),f,(I,\leq _I))$
be an extended frame. Then the set
$$\begin{align*}T(\mathcal{E}) = \{ \varphi \mid \mathcal{E} \models \varphi \} \end{align*}$$
does not form a logic in general, but forms a theory in the following sense:
$ \mathbf {IPC} \subseteq T(\mathcal {E}); $
if
$ \varphi \mathbin {\rightarrow } \psi , \varphi \in T(\mathcal {E}) , $
then
$ \psi \in T(\mathcal {E}). $
In fact, consider the extended frame
$\mathcal {E} = ((K,\leq ),f,(I,\leq _I))$
given in Figure 3. Then
$ (p \mathbin {\rightarrow } q) \lor (q \mathbin {\rightarrow } p) \in T(\mathcal {E}). $
However,
$$\begin{align*}0 \not\Vdash_{\mathcal{E},\mathcal{I}} (p \mathbin{\rightarrow} \lnot r) \lor (\lnot r \mathbin{\rightarrow} p) \end{align*}$$
for the IPC-Kripke model
$\mathcal {I} = (I,\leq _I,\Vdash )$
with
$ a \not \Vdash p , $
$ a \not \Vdash r , $
$ b \Vdash p $
, and
$ b \Vdash r. $
Therefore,
$ ((p \mathbin {\rightarrow } q) \lor (q \mathbin {\rightarrow } p))[q/\lnot r] \not \in T(\mathcal {E}). $
See Example 5.2 for the details.
Theorem 2.7. Let
$\mathcal {K} = (K,\leq ,\Vdash )$
be an IPC-Kripke model, and let
$\varphi $
be a formula of
$\mathcal {L}(\mathbf {IPC})$
. If
$\mathcal {K} \not \Vdash \varphi $
, then
$$\begin{align*}T(\mathcal{E}_{\mathcal{K}}) \not\vdash_{\mathbf{IPC}} \varphi. \end{align*}$$
Proof Let
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}_{\mathcal {K}}} = (K,\leq ,\Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}_{\mathcal {K}}}) $
be the IPC-Kripke model induced by the IPC-Kripke model
$ \mathcal {I}_{\mathcal {K}} = (I_{\mathcal {K}},\leq _{\mathcal {K}},\Vdash _{\mathcal {K}}) $
in Example 2.5. Then
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}_{\mathcal {K}}} \not \Vdash \varphi , $
whenever
$ \mathcal {K} \not \Vdash \varphi. $
On the other hand, we have
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}_{\mathcal {K}}} \Vdash \chi $
for all
$\chi \in T(\mathcal {E}_{\mathcal {K}})$
. By the soundness theorem [Reference Troelstra and van Dalen33, Chapter 2, Section 5.10], we have
$ T(\mathcal {E}_{\mathcal {K}}) \not \vdash _{\mathbf {IPC}} \varphi. $
Remark 2.8. Let
$\mathcal {K} = (K,\leq ,\Vdash )$
be an IPC-Kripke model, and let
$\varphi $
be a formula of
$\mathcal {L}(\mathbf {IPC})$
. If
$\mathcal {K} \not \Vdash \varphi $
, then
$k_0 \not \Vdash \varphi $
for some
$k_0 \in K$
, and, by considering the truncated model
$ \mathcal {K}' = (K',\leq ',\Vdash ') , $
where
$ K' = \mathop {\uparrow } k_0 , $
$ {\leq '} = {{\leq } \cap {(K' \times K')}} $
and
$ {\Vdash '} = {{\Vdash } \cap {(K' \times \mathcal {V})}} , $
we may assume that
$\mathcal {K}$
is an IPC-Kripke model with a root (see [Reference Troelstra and van Dalen33, Chapter 2, Section 5.4]). Furthermore, if
$ \mathcal {K}' = (K',\leq ',\Vdash ') $
is an IPC-Kripke model with root
$k_0 \in K'$
and
$ k_0 \not \Vdash \varphi , $
then there exists a finite model
$ \mathcal {K}" = (K",\leq ",\Vdash ") $
such that
$ K" \subseteq K' , $
$ {\leq "} = {{\leq '} \cap {(K" \times K")}} $
and
$ {k \Vdash " \psi } \mathbin {\Leftrightarrow } {k \Vdash ' \psi } $
for all
$k \in K"$
and subformula
$\psi $
of
$\varphi $
(see [Reference Troelstra and van Dalen33, Chapter 2, Section 6.11]). Therefore we may assume that
$\mathcal {K}$
is a finite IPC-Kripke model with a root.
Note that if
$\mathcal {K}$
is a finite IPC-Kripke model with a root, then
$(I_{\mathcal {K}},\leq _{\mathcal {K}})$
is a finite partially ordered set with a root.
Definition 2.9. An extended frame
$\mathcal {E} = ((K,\leq ),f,(I,\leq _I))$
is locally directed if
$f^{-1}(\mathop {\uparrow } i) \cap {\mathop {\uparrow } k}$
is directed for all
$i \in I$
and
$k \in K$
, that is, for each
$i \in I$
and
$k \in K$
, if
$l, l' \in f^{-1}(\mathop {\uparrow } i) \cap {\mathop {\uparrow } k}$
, then there exists
$l" \in f^{-1}(\mathop {\uparrow } i) \cap {\mathop {\uparrow } k}$
such that
$l" \leq l$
and
$l" \leq l'$
.
In the following, we shall give several examples of extended frame generated by an IPC-Kripke model (see [Reference Fujiwara8] for more examples). Before that, we quickly review the relation between some intermediate propositional logics and frames.
For a logic L, let
$L + \varphi _0 + \cdots + \varphi _{n-1}$
denote the logic obtained from L by adding axiom schemata
$\varphi _0, \ldots , \varphi _{n-1}$
, and let
$$\begin{align*}L^{\mathrm{lin}} = L + (\varphi \mathbin{\rightarrow} \psi) \lor (\psi \mathbin{\rightarrow} \varphi). \end{align*}$$
For
$n \geq 1$
, the slice
$\mathcal {S}_n$
consists of logics L such that
$ L^{\mathrm {lin}} = L(J_n,\leq _n) , $
and the slice
$\mathcal {S}_\omega $
consists of logics L such that
$ L^{\mathrm {lin}} = \bigcap _{n < \omega } L(J_n,\leq _n) , $
where
$ (J_n,\leq _n) $
is the linear frame with n elements. Then
$\mathcal {S}_1 = \{\mathbf {CPC}\}$
and
$\mathbf {IPC} \in \mathcal {S}_\omega $
, and any logic belongs to exactly one
$\mathcal {S}_n$
(
$n \leq \omega $
) (see [Reference Hosoi14, Part I, 4.1] and [Reference Hosoi and Ono15]).
Let
$\rho _1, \rho _2, \ldots $
and
$\zeta _1, \zeta _2, \ldots $
be sequences of axiom schemata defined by
$$ \begin{align*} \rho_1 & \equiv ((\varphi_1 \mathbin{\rightarrow} \varphi_0) \mathbin{\rightarrow} \varphi_1) \mathbin{\rightarrow} \varphi_1 , \\ \rho_{n+1} & \equiv ((\varphi_{n+1} \mathbin{\rightarrow} \rho_n) \mathbin{\rightarrow} \varphi_{n+1}) \mathbin{\rightarrow} \varphi_{n+1} , \\ \zeta_n & \equiv \bigvee_{0 \leq i < j \leq n} (\varphi_i \mathbin{\leftrightarrow} \varphi_j) \end{align*} $$
(see [Reference Hosoi14] where
$\rho _n$
and
$\zeta _n$
are written by
$P_n$
and
$X_n$
, respectively). For each
$k \geq 1$
, let
$\mathbf {T}_k = \mathbf {IPC} + \rho _2 + \zeta _k$
, and let
$\mathbf {M}_k = \mathbf {T}_{2^k+1}$
and
$\mathbf {M}_\omega = \mathbf {IPC} + \rho _2$
. Then
$ \{\mathbf {M}_1,\mathbf {M}_2, \ldots , \mathbf {M}_n, \ldots \mathbf {M}_\omega \} $
is the decreasing enumeration of the second slice
$\mathcal {S}_2$
(see [Reference Hosoi and Ono15, Theorem 1.6]).
Note that the axiom schema
$\rho _n$
says that the heightFootnote
1
of a frame is at most n. For a rooted frame, the axiom schema
$\zeta _n$
says that the number of upward closed subsets of the frame is at most n; hence, for a rooted frame with the height
$2$
, the axiom schema
$\zeta _{2^k+1}$
says that the number of maximal elements of the frame is at most k (see [Reference Gabbay and De Jongh12, Reference Ono29] for other axiomatizations).
In contrast with
$\mathcal {S}_2$
, we know little about the internal structure of
$\mathcal {S}_n$
(
$n \geq 3$
).
Let
$\mathrm {PEM}$
,
$\mathrm {DNE}$
,
$\mathrm {WPEM}$
,
$\mathrm {DML}$
,
$\mathrm {WDML}$
, and
$\mathrm {RPEM}$
be the following formulae:
$$ \begin{align*} \mathrm{PEM}[p] & \equiv p \lor \lnot p. \\ \mathrm{DNE}[p] & \equiv \lnot\lnot p \mathbin{\rightarrow} p. \\ \mathrm{WPEM}[p] & \equiv \lnot p \lor \lnot\lnot p. \\ \mathrm{DML}[p,q] & \equiv \lnot (p \land q) \mathbin{\rightarrow} \lnot p \lor \lnot q. \\ \mathrm{WDML}[p,q] & \equiv \lnot (\lnot p \land \lnot q) \mathbin{\rightarrow} \lnot\lnot p \lor \lnot\lnot q. \\ \mathrm{RPEM}[p,q] & \equiv (p \mathbin{\leftrightarrow} \lnot q) \mathbin{\rightarrow} p \lor \lnot p. \end{align*} $$
Then we have the following examples of Theorem 2.7.
Example 2.10. Let
$\mathcal {E}_{\mathcal {K}_1} = ((K_1,\leq _1),f_{\mathcal {K}_1},(I_{\mathcal {K}_1},\leq _{\mathcal {K}_1}))$
be the extended frame generated by the IPC-Kripke model
$\mathcal {K}_1 = (K_1,\leq _1,\Vdash _1)$
given in Figure 4. Then
$ \mathcal {K}_1 \not \Vdash _1 \mathrm {DNE}[p] , $
and hence
$$\begin{align*}T(\mathcal{E}_{\mathcal{K}_1}) \not\vdash_{\mathbf{IPC}} \mathrm{DNE}[p]. \end{align*}$$
The theory
$T(\mathcal {E}_{\mathcal {K}_1})$
is the logic
$L(K_1,\leq _1)$
axiomatized by the axiom schemata
$\rho _2$
and
$\zeta _3$
.
Figure 4 The Kripke model and the extended frame in Example 2.10.
Furthermore,
$T(\mathcal {E}_{\mathcal {K}_1})$
contains
$ \mathrm {WPEM}[p] $
for all propositional variable p. To see this, consider an IPC-Kripke model
$\mathcal {I} = (I_{\mathcal {K}_1},\leq _{\mathcal {K}_1},\Vdash ')$
. If
$[1]_{\mathcal {K}_1} \Vdash ' p$
, then
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_1},\mathcal {I}} \lnot \lnot p$
; or else if
$[1]_{\mathcal {K}_1} \not \Vdash ' p$
, then
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_1},\mathcal {I}} \lnot p$
.
Note that
$\mathcal {E}_{\mathcal {K}_1}$
is locally directed.
Example 2.11. Let
$\mathcal {E}_{\mathcal {K}_2} = ((K_2,\leq _2),f_{\mathcal {K}_2},(I_{\mathcal {K}_2},\leq _{\mathcal {K}_2}))$
be the extended frame generated by the IPC-Kripke model
$\mathcal {K}_2 = (K_2,\leq _2,\Vdash _2)$
given in Figure 5. Then
$ \mathcal {K}_2 \not \Vdash _2 \mathrm {WPEM}[p] , $
and hence
$$\begin{align*}T(\mathcal{E}_{\mathcal{K}_2}) \not\vdash_{\mathbf{IPC}} \mathrm{WPEM}[p]. \end{align*}$$
The theory
$T(\mathcal {E}_{\mathcal {K}_2})$
contains the logic
$L(K_2,\leq _2)$
axiomatized by the axiom schemata
$\rho _2$
and
$\zeta _5$
.
Figure 5 The Kripke model and the extended frame in Example 2.11.
Furthermore,
$T(\mathcal {E}_{\mathcal {K}_2})$
contains
$\mathrm {DML}[q,r]$
and
$\mathrm {DNE}[q]$
for all q and r. To see this, consider an IPC-Kripke model
$\mathcal {I} = (I_{\mathcal {K}_2},\leq _{\mathcal {K}_2},\Vdash ')$
. If
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_2},\mathcal {I}} \lnot (q \land r)$
, then
$[0]_{\mathcal {K}_2} \Vdash ' q$
implies
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_2},\mathcal {I}} \lnot r$
,
$[0]_{\mathcal {K}_2} \Vdash ' r$
implies
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_2},\mathcal {I}} \lnot q$
, and
$[0]_{\mathcal {K}_2} \not \Vdash ' q$
and
$[0]_{\mathcal {K}_2} \not \Vdash ' r$
imply
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_2},\mathcal {I}} \lnot q \lor \lnot r$
, since
$[1]_{\mathcal {K}_2} \not \Vdash ' q \land r$
. If
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_2},\mathcal {I}} \lnot \lnot q$
, then
$2 \Vdash _{\mathcal {E}_{\mathcal {K}_2},\mathcal {I}} q$
, that is,
$ [2]_{\mathcal {K}_2} = [0]_{\mathcal {K}_2} \Vdash ' q , $
and hence
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_2},\mathcal {I}} q$
.
Note that
$\mathcal {E}_{\mathcal {K}_2}$
is locally directed.
Example 2.12. Let
$\mathcal {E}_{\mathcal {K}_3} = ((K_3,\leq _3),f_{\mathcal {K}_3},(I_{\mathcal {K}_3},\leq _{\mathcal {K}_3}))$
be the extended frame generated by the IPC-Kripke model
$\mathcal {K}_3 = (K_3,\leq _3,\Vdash _3)$
given in Figure 6. Then
$ \mathcal {K}_3 \not \Vdash _3 \mathrm {DML}[p,q] , $
and hence
$$\begin{align*}T(\mathcal{E}_{\mathcal{K}_3}) \not\vdash_{\mathbf{IPC}} \mathrm{DML}[p,q]. \end{align*}$$
The theory
$T(\mathcal {E}_{\mathcal {K}_3})$
contains the logic
$L(K_3,\leq _3)$
axiomatized by the axiom schemata
$\rho _2$
and
$\zeta _9$
.
Figure 6 The Kripke model and the extended frame in Example 2.12.
Furthermore,
$T(\mathcal {E}_{\mathcal {K}_3})$
contains
$\mathrm {DNE}[r]$
for all r. To see this, consider an IPC-Kripke model
$ \mathcal {I} = (I_{\mathcal {K}_3},\leq _{\mathcal {K}_3},\Vdash '). $
If
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_3},\mathcal {I}} \lnot \lnot r$
, then
$3 \Vdash _{\mathcal {E}_{\mathcal {K}_3},\mathcal {I}} r$
, that is,
$ [3]_{\mathcal {K}_3} = [0]_{\mathcal {K}_3} \Vdash ' r , $
and hence
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_3},\mathcal {I}} r$
.
Note that
$\mathcal {E}_{\mathcal {K}_3}$
is locally directed.
Example 2.13. Let
$\mathcal {E}_{\mathcal {K}_4} = ((K_4,\leq _4),f_{\mathcal {K}_4},(I_{\mathcal {K}_4},\leq _{\mathcal {K}_4}))$
be the extended frame generated by the IPC-Kripke model
$\mathcal {K}_4 = (K_4,\leq _4,\Vdash _4)$
given in Figure 7. Then
$ \mathcal {K}_4 \not \Vdash _4 \mathrm {WDML}[p,q] , $
and hence
$$\begin{align*}T(\mathcal{E}_{\mathcal{K}_4}) \not\vdash_{\mathbf{IPC}} \mathrm{WDML}[p,q]. \end{align*}$$
The theory
$ T(\mathcal {E}_{\mathcal {K}_4}) $
contains the logic
$L(K_4,\leq _4)$
.
Figure 7 The Kripke model and the extended frame in Example 2.13.
Furthermore
$ T(\mathcal {E}_{\mathcal {K}_4}) $
contains
$ \mathrm {RPEM}[r,s] $
for all r and s. To see this, consider an IPC-Kripke model
$ \mathcal {I} = (I_{\mathcal {K}_4},\leq _{\mathcal {K}_4},\Vdash '). $
Suppose that
$i \Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} r \mathbin {\leftrightarrow } \lnot s$
. We show that
$i \Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} r \lor \lnot r$
. Suppose otherwise. Then i is not maximal. Without loss of generality, we may assume that
$i \leq _4 1$
. If
$3 \Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} r $
, then
$3 \Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} \neg s$
, and hence
$1\Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} \neg s$
, and hence
$1\Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} r$
, which implies
$0\Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} r$
by the structure of
$\mathcal {E}_{\mathcal {K}_4}$
. This is a contradiction. Thus
$3 \not \Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} r $
. Then
$ 1\Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} \neg r$
, and hence
$i=0$
. Then we also have
$4 \not \Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} r $
as above. Then
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} \neg r$
follows. This is a contradiction. Thus we have shown
$i \Vdash _{\mathcal {E}_{\mathcal {K}_4},\mathcal {I}} r \lor \lnot r$
.
Note that
$\mathcal {E}_{\mathcal {K}_4}$
is locally directed.
Example 2.14. Let
$\mathcal {E}_{\mathcal {K}_5} = ((K_2,\leq _2),f_{\mathcal {K}_5},(I_{\mathcal {K}_5},\leq _{\mathcal {K}_5}))$
be the extended frame generated by the IPC-Kripke model
$\mathcal {K}_5 = (K_2,\leq _2,\Vdash _5)$
given in Figure 8. Then
$ \mathcal {K}_5 \not \Vdash _5 \mathrm {RPEM}[p,q] , $
and hence
$$\begin{align*}T(\mathcal{E}_{\mathcal{K}_5}) \not\vdash_{\mathbf{IPC}} \mathrm{RPEM}[p,q]. \end{align*}$$
The theory
$T(\mathcal {E}_{\mathcal {K}_5})$
is the logic
$L(K_2,\leq _2)$
.
Figure 8 The Kripke model and the extended frame in Example 2.14.
Note that
$\mathcal {E}_{\mathcal {K}_5}$
is locally directed.
3 Separations by extended frames in
$\mathbf {IQC}$
In this section, we introduce the notion of a schema, and by using the extended frame generated by an IPC-Kripke model, give a separation theorem (Theorem 3.15) of a schema from a set of schemata in
$\mathbf {IQC}$
. We then apply the separation theorem to the examples in the previous section (Example 3.16).
We use the standard language
$\mathcal {L}(\mathbf {IQC})$
of intuitionistic first-order predicate logic
$\mathbf {IQC}$
containing the propositional connectives and
$\forall , \exists $
as primitive logical operators. The sets
$\mathrm {FV}(t)$
and
$\mathrm {FV}(A)$
of free variables in a term t and a formula A, respectively, of
$\mathcal {L}(\mathbf {IQC})$
are defined as usual:
$\mathrm {FV}(x) = \{x\}$
;
$\mathrm {FV}(c) = \emptyset $
;
$\mathrm {FV}(f(t_1,\ldots ,t_n)) = \mathrm {FV}(t_1) \cup \cdots \cup \mathrm {FV}(t_n)$
;
$\mathrm {FV}(\bot ) = \emptyset $
;
$\mathrm {FV}(R(t_1,\ldots ,t_n)) = \mathrm {FV}(t_1) \cup \cdots \cup \mathrm {FV}(t_n)$
;
$\mathrm {FV}(B \circ C) = \mathrm {FV}(B) \cup \mathrm {FV}(C)$
for
$\circ \in \{\land ,\lor ,\mathbin {\rightarrow }\}$
;
$\mathrm {FV}(\forall x B) = \mathrm {FV}(\exists x B) = \mathrm {FV}(B) \setminus \{x\}$
; we set
$\mathrm {FV}(A_1,\ldots ,A_n) = \mathrm {FV}(A_1) \cup \cdots \cup \mathrm {FV}(A_n)$
for a sequence
$A_1,\ldots ,A_n$
of formulae. In the following, we use
$\vdash _{\mathbf {IQC}}$
for deducibility in
$\mathbf {IQC}$
.
Definition 3.1. An IQC-Kripke model is a tuple
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
, where
$(I,\leq _I)$
is a frame,
$M = \{M_{i}\}_{i \in I}$
is a family of nonempty sets,
$\eta $
is a family
$\{\eta _{i i'} \in M_i \to M_{i'} \mid i \leq _I i'\}$
of restrictions such that:
-
•
$\eta _{i i}$
is the identity on
$M_i$
, -
•
$\eta _{i' i"} \circ \eta _{i i'} = \eta _{i i"}$
for
$i \leq _I i' \leq _I i"$
,
and
$\Vdash $
is a relation, called a valuation, from I to the set of atomic formulae of the language extended by adding a constant symbols a for each element
$ a \in \bigcup \{ M_i \mid i \in I \} $
such that:
-
•
$i \Vdash R(a_1,\ldots ,a_n) \mathbin {\Rightarrow } a_m \in M_i$
for
$m \in \{1,\ldots ,n\}$
, -
•
$ i \Vdash R(a_1,\ldots ,a_n)\text { and }i \leq i' \mathbin {\Rightarrow } i' \Vdash R(\eta _{i i'}(a_1),\ldots ,\eta _{i i'}(a_n)) $
for all
$i, i' \in I$
. An n-ary function f is interpreted in
$\mathcal {I}$
by a family
$f = \{f_i \in M_i^n \to M_i \mid i \in I \}$
commuting with the restrictions for
$i' \geq _I i$
$$\begin{align*}\eta_{i i'}(f_i(a_1,\ldots,a_n)) = f_{i'}(\eta_{i i'}(a_1),\ldots,\eta_{i i'}(a_n)). \end{align*}$$
The valuation
$\Vdash $
is then extended to logically compound formulae of
$\mathcal {L}(\mathbf {IQC})$
by the clauses in the previous section for the propositional connectives and the following clauses:
-
1.
$ i \Vdash \forall x A \mathbin {\Leftrightarrow } i' \Vdash A[x/a] \text { for all }i' \geq i\text { and }a \in M_{i'}. $
-
2.
$ i \Vdash \exists x A \mathbin {\Leftrightarrow } i \Vdash A[x/a] \text { for some }a \in M_i. $
Note that
$ \{ i \in I \mid i \Vdash A \} \in \Omega _I $
for all sentence A of
$\mathcal {L}(\mathbf {IQC})$
. A formula A with
$\mathrm {FV}(A) \subseteq \{\vec {x}\}$
is valid in
$\mathcal {I}$
if
$i \Vdash A[\vec {x}/\vec {a}]$
for all
$i \in I$
and
$\vec {a} \in M_i$
, and we then write
$\mathcal {I} \Vdash A$
(see [Reference Troelstra and van Dalen33, Chapter 2, Section 5.12]).
Remark 3.2. Let
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
be an IQC-Kripke model with a family of interpretations
$f = \{f_i \in M_i^n \to M_i \mid i \in I \}$
for all n-ary function f. For each
$i \in I$
, define a (first-order) structure
$ \mathcal {M}_i = (M_i,\vec {R}_i,\vec {f}_i) $
by
$$ \begin{align*} R_i & = \{ (a_1,\ldots,a_m) \mid i \Vdash R(a_1,\ldots,a_m) \} , & f_i & = f_i. \end{align*} $$
Then
$\{ \mathcal {M}_i \mid i \in I \}$
is a family of structures satisfying
$$ \begin{align*} (a_1,\ldots,a_m) \in R_i & \mathbin{\Rightarrow} (\eta_{i i'}(a_1),\ldots,\eta_{i i'}(a_m)) \in R_{i'} \\ \eta_{i i'}(f_i(a_1,\ldots,a_n)) & = f_{i'}(\eta_{i i'}(a_1),\ldots,\eta_{i i'}(a_n)) \end{align*} $$
(see [Reference van Dalen6, Chapter 2, Section 2.2–2.4]). Conversely, a family
$\{ \mathcal {M}_i \mid i \in I \}$
of structures together with a family
$\eta $
of restrictions satisfying the above conditions gives an IQC-Kripke model
$(I,\leq _I,M,\eta ,\Vdash )$
defined by
$$\begin{align*}{i \Vdash R(a_1,\ldots,a_m)} \mathbin{\Leftrightarrow} {\mathcal{M}_i \models_c R(a_1,\ldots,a_m)} \end{align*}$$
for each
$i \in I$
, where
$\models _c$
denotes the classical interpretation in the structure; we sometimes simply write
$M_i \models _c A$
for
$\mathcal {M}_i \models _c A$
.
Definition 3.3. Let
$\mathcal {E} = ((K,\leq ),f,(I,\leq _I))$
be an extended frame. Then each IQC-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
induces an IQC-Kripke model
$\mathcal {K}_{\mathcal {E},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E},\mathcal {I}})$
by defining for each
$k , k' \in K$
with
$k \leq k'$
,
$$ \begin{align*} D_k & = M_{f(k)} , \\ \epsilon_{k k'} & = \eta_{f(k) f(k')} , \\ k \Vdash_{\mathcal{E},\mathcal{I}} R(a_1,\ldots,a_n) & \mathbin{\Leftrightarrow} f(k) \Vdash R(a_1,\ldots,a_n) \end{align*} $$
for prime formula
$R(a_1,\ldots ,a_n)$
with
$a_1, \ldots , a_n \in D_k$
.
We introduce the notion of a schema following [Reference Leivant26], [Reference Troelstra and van Dalen33, Chapter 2, Section 3.13], and [Reference Ishihara and Nemoto19, Reference Ishihara and Nemoto20].
Definition 3.4. We introduce certain predicate symbols
$\nu _1, \nu _2, \nu _3, \ldots $
(being outside of our standard language), called place holders, to deal with schemata as syntactic objects similar to formulae. Schemata are inductively defined by:
-
1. a prime formula is a schema;
-
2. if
$\nu $
is an n-ary place holder and
$t_1, \ldots , t_n$
are terms, then
$\nu (t_1, \ldots , t_n)$
is a schema; -
3. if
$\alpha $
and
$\beta $
are schemata, then
$\alpha \circ \beta $
is a schema for
$\circ \in \{ \land , \lor , \mathbin {\rightarrow } \}$
; -
4. if
$\alpha $
is a schema, then
$Q x \alpha $
is a schema for
$Q \in \{ \forall , \exists \}$
.
Formulae are schemata without place holders.
For example, the induction schema is given by a schema
$$\begin{align*}\nu(0) \land \forall x (\nu(x) \mathbin{\rightarrow} \nu(Sx)) \mathbin{\rightarrow} \forall x \nu(x) , \end{align*}$$
where
$\nu $
is a unary place holder.
Definition 3.5. Let
$\alpha $
be a schema, and let
$B_1, \ldots , B_k$
be formulae. Let
$\nu _1, \ldots , \nu _k$
be place holders, and let
$\vec {x}_1, \ldots , \vec {x}_k$
be sequences of variables with lengths of the arities of
$\nu _1, \ldots , \nu _k$
, respectively. Then a schema
$$\begin{align*}\alpha[\nu_1/\lambda \vec{x}_1.B_1, \ldots, \nu_k/\lambda \vec{x}_k.B_k] \end{align*}$$
is defined by:
-
1.
$P[\nu _1/\lambda \vec {x}_1.B_1, \ldots , \nu _k/\lambda \vec {x}_k.B_k] \equiv P$
for P prime; -
2.
$\nu (t_1, \ldots , t_n)[\nu _1/\lambda \vec {x}_1.B_1, \ldots , \nu _k/\lambda \vec {x}_k.B_k] \equiv B_i[y_1/t_1, \ldots , y_n/t_n]$
if
$\nu \equiv \nu _i$
and
$\vec {x}_i \equiv y_1, \ldots , y_n$
, and
$\nu (t_1, \ldots , t_n)$
otherwise; -
3.
$ (\alpha \circ \beta )[\nu _1/\lambda \vec {x}_1.B_1, \ldots , \nu _k/\lambda \vec {x}_k.B_k] $
$ \kern10pt \equiv \alpha [\nu _1/\lambda \vec {x}_1.B_1, \ldots , \nu _k/\lambda \vec {x}_k.B_k] \circ \beta [\nu _1/\lambda \vec {x}_1.B_1, \ldots , \nu _k/\lambda \vec {x}_k.B_k] $
for
$\circ \in \{ \land , \lor , \mathbin {\rightarrow } \}$
; -
4.
$ (Q x \alpha )[\nu _1/\lambda \vec {x}_1.B_1, \ldots , \nu _k/\lambda \vec {x}_k.B_k] $
$ \kern110pt \equiv Q x (\alpha [\nu _1/\lambda \vec {x}_1.B_1, \ldots , \nu _k/\lambda \vec {x}_k.B_k]) $
for
$Q \in \{ \forall , \exists \}$
.
We simply write
$\alpha [\nu _1/B_1, \ldots , \nu _k/B_k]$
or even
$\alpha [B_1, \ldots , B_k]$
for
$$\begin{align*}\alpha[\nu_1/\lambda \vec{x}_1.B_1, \ldots, \nu_k/\lambda \vec{x}_k.B_k] \end{align*}$$
whenever possible, if it does not cause confusion. An instance of a schema
$\alpha $
with place holders exactly
$\vec {\nu }$
is a formula
$\alpha [\vec {\nu }/\vec {B}]$
or
$\alpha [\vec {B}]$
.
Remark 3.6. In using the substitution notations
$\alpha [\vec {\nu }/\vec {B}]$
, we shall assume that
$\lambda \vec {x}. \vec {B}$
are free for
$\vec {\nu }$
in
$\alpha $
, or we assume that a suitable renaming of bound variables is carried out. Here
$\lambda \vec {x}.B$
is free for
$\nu $
in P for prime P;
$\lambda \vec {x}.B$
is free for
$\nu $
in
$\nu '(t_1,...,t_n)$
;
$\lambda \vec {x}.B$
is free for
$\nu $
in
$\alpha \circ \beta $
if
$\lambda \vec {x}.B$
is free for
$\nu $
in
$\alpha $
and
$\beta $
, where
$\circ \in \{\land ,\lor ,\mathbin {\rightarrow }\}$
;
$\lambda \vec {x}.B$
is free for
$\nu $
in
$Q y \alpha $
if
$y \in \mathrm {FV}(B) \setminus \{\vec {x}\}$
and
$\lambda \vec {x}. B$
is free for
$\nu $
in
$\alpha $
, where
$Q \in \{\forall ,\exists \}$
.
Definition 3.7. We extend the deducibility relation
$\vdash $
and the forcing relation
$\Vdash $
to schemata as follows. Let
$\Gamma $
and
$\Delta $
be a set of schemata, let
$\alpha $
be a schema, and let C be a formula. Then
$\Gamma \vdash C$
if
$$\begin{align*}\{ B \mid B\text{ is an instance of a schema in }\Gamma \} \vdash C; \end{align*}$$
$\Gamma \vdash \alpha $
if
$\Gamma \vdash B$
for all instance B of
$\alpha $
;
$\Gamma \vdash \Delta $
if
$\Gamma \vdash \alpha $
for all
$\alpha \in \Delta $
. Similarly, for IQC-Kripke model
$\mathcal {K}$
,
$\mathcal {K} \Vdash \alpha $
if
$\mathcal {K} \Vdash B$
for all instance B of
$\alpha $
;
$\mathcal {K} \Vdash \Delta $
if
$\mathcal {K} \Vdash \alpha $
for all
$\alpha \in \Delta $
.
Definition 3.8. Each formula
$\varphi [p_1,\ldots ,p_n]$
of
$\mathcal {L}(\mathbf {IPC})$
may be naturally regarded as a schema
$$\begin{align*}\varphi^\ast \equiv \varphi[\nu_1^0,\ldots,\nu_n^0] , \end{align*}$$
where
$\nu _1^0,\ldots ,\nu _n^0$
are nullary place holders.
Lemma 3.9. Let
$(K,\leq ,D,\epsilon ,\Vdash )$
be an IQC-Kripke model, and let
$(K,\leq ,\Vdash ')$
be an IPC-Kripke model. Let
$\varphi [p_1,\ldots ,p_n]$
be a formula of
$\mathcal {L}(\mathbf {IPC})$
, and let
$A_1,\ldots ,A_n$
be formulae of
$\mathcal {L}(\mathbf {IQC})$
with
$\mathrm {FV}(A_1,\ldots ,A_n) \subseteq \{\vec {x}\}$
. For each
$k \in K$
and
$\vec {a} \in D_k$
, if
$$\begin{align*}k' \Vdash' p_m \mathbin{\Leftrightarrow} k' \Vdash A_m[\vec{x}/\epsilon_{k k'}(\vec{a})] \end{align*}$$
for all
$k' \geq k$
and
$m \in \{1,\ldots ,n\}$
, then
$$\begin{align*}k' \Vdash' \varphi \mathbin{\Leftrightarrow} k' \Vdash (\varphi[A_1,\ldots,A_n])[\vec{x}/\epsilon_{k k'}(\vec{a})] \end{align*}$$
for all
$k' \geq k$
.
Proof Straightforward by induction on the complexity of
$\varphi $
.
Proposition 3.10. Let
$\mathcal {E} =((K,\leq ),f,(I,\leq _I))$
be an extended frame. If
$\varphi \in L(K,\leq )$
, then
$$\begin{align*}\mathcal{K}_{\mathcal{E},\mathcal{I}} \Vdash_{\mathcal{E},\mathcal{I}} \varphi^\ast \end{align*}$$
for all IQC-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
.
Proof Suppose that
$\varphi \in L(K,\leq )$
, and consider an IQC-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
and an instance
$$\begin{align*}\varphi[A_1,\ldots,A_n] \end{align*}$$
of the schema
$\varphi ^\ast $
. Let
$\mathcal {K}_{\mathcal {E},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E},\mathcal {I}})$
be the induced IQC-Kripke model. Then for each
$k \in K$
and
$\vec {a} \in D_k$
, defining a valuation
$\Vdash '$
on
$(K,\leq )$
by
$$\begin{align*}k' \Vdash' p_m \mathbin{\Leftrightarrow} k' \Vdash_{\mathcal{E},\mathcal{I}} A_m[\vec{x}/\epsilon_{k k'}(\vec{a})] \end{align*}$$
for each
$k' \geq k$
and
$m \in \{1,\ldots ,n\}$
, by Lemma 3.9, we have
$$\begin{align*}k \Vdash' \varphi \mathbin{\Leftrightarrow} k \Vdash_{\mathcal{E},\mathcal{I}} (\varphi[A_1,\ldots,A_n])[\vec{x}/\vec{a}]. \end{align*}$$
Since
$\varphi $
is valid on
$(K,\leq )$
, we have
$$\begin{align*}k \Vdash_{\mathcal{E},\mathcal{I}} (\varphi[A_1,\ldots,A_n])[\vec{x}/\vec{a}].\\[-35pt] \end{align*}$$
Definition 3.11. For each formula
$\varphi [p_1,\ldots ,p_n]$
of
$\mathcal {L}(\mathbf {IPC})$
, define a schema
$\Sigma \text {-}\varphi $
by
$$ \begin{align*} \Sigma\text{-}\varphi \equiv \forall \vec{x} (\nu_1(\vec{x}) \lor \lnot \nu_1(\vec{x})) \land \cdots \land & \forall \vec{x} (\nu_n(\vec{x}) \lor \lnot \nu_n(\vec{x})) \\ & \mathbin{\rightarrow} \varphi[ \exists \vec{x} \nu_1(\vec{x}),\ldots,\exists \vec{x} \nu_n(\vec{x}) ] , \end{align*} $$
where
$\nu _1,\ldots ,\nu _n$
are place holders with the arity of the length of
$\vec {x}$
.
Proposition 3.12. Let
$\mathcal {E}_{\mathcal {K}} = ((K,\leq ),f_{\mathcal {K}},(I_{\mathcal {K}},\leq _{\mathcal {K}}))$
be the extended frame generated by an IPC-Kripke model
$\mathcal {K} = (K,\leq ,\Vdash )$
, and let
$\varphi [p_1,\ldots ,p_n]$
be a formula of
$\mathcal {L}(\mathbf {IPC})$
. If
$ \mathcal {K} \not \Vdash \varphi , $
then
$$\begin{align*}\mathcal{K}_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \not\Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \Sigma\text{-}\varphi \end{align*}$$
for some IQC-Kripke model
$ \mathcal {I} = (I_{\mathcal {K}},\leq _{\mathcal {K}},M,\eta ,\Vdash '). $
Proof Recall the construction in Example 2.4 of the extended frame
$\mathcal {E}_{\mathcal {K}}$
. Suppose that
$ \mathcal {K} \not \Vdash \varphi. $
Let
$R_1(\vec {x}),\ldots ,R_n(\vec {x})$
be predicate symbols, and let
$ U_q = \{ k \in K \mid k \Vdash q \} $
for each
$q \in \mathcal {V}$
. Then define an IQC-Kripke model
$ \mathcal {I} = (I_{\mathcal {K}},\leq _{\mathcal {K}},M,\eta ,\Vdash ') $
by
$$ \begin{align*} M_{[k]_{\mathcal{K}}} & = \{ U_q \mid k \Vdash q \} \cup \{K\}, \\ \eta_{[k]_{\mathcal{K}} [k']_{\mathcal{K}}} & = \text{the inclusion map }M_{[k]_{\mathcal{K}}} \to M_{[k']_{\mathcal{K}}}, \\ [k]_{\mathcal{K}} \Vdash' R_m(U_{q_1},\ldots,U_{q_{n'}}) & \mathbin{\Leftrightarrow} U_{q_1} \cap \cdots \cap U_{q_{n'}} \subseteq U_{p_m} \end{align*} $$
for each
$[k]_{\mathcal {K}}, [k']_{\mathcal {K}} \in I_{\mathcal {K}}$
with
$[k]_{\mathcal {K}} \leq _{\mathcal {K}} [k']_{\mathcal {K}}$
,
$U_{q_1},\ldots ,U_{q_{n'}} \in M_{[k]_{\mathcal {K}}}$
and
$m \in \{1,\ldots ,n\}$
. Let
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}}) $
be the induced IQC-Kripke model, and assume that
$$ \begin{align*} k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \forall \vec{x} (R_1(\vec{x}) \lor \lnot R_1(\vec{x})) \land \cdots \land & \forall \vec{x} (R_n(\vec{x}) \lor \lnot R_n(\vec{x})) \\ & \mathbin{\rightarrow} \varphi[\exists \vec{x} R_1(\vec{x}),\ldots,\exists \vec{x} R_n(\vec{x})] \end{align*} $$
for all
$k \in K$
. Then given a
$k \in K$
, if
$[k]_{\mathcal {K}} \Vdash ' R_m(U_{q_1},\ldots ,U_{q_{n'}})$
for some
$U_{q_1},\ldots ,U_{q_{n'}} \in D_k = M_{[k]_{\mathcal {K}}}$
, then
$k \in U_{q_1} \cap \cdots \cap U_{q_{n'}} \subseteq U_{p_m}$
, and hence
$k \Vdash p_m$
; if
$k \Vdash p_m$
, then
$U_{p_m} \in M_{[k]_{\mathcal {K}}} = D_k$
, and hence
$[k]_{\mathcal {K}} \Vdash ' R_m(U_{p_m},\ldots ,U_{p_m})$
. Therefore
$$ \begin{align} k \Vdash p_m \mathbin{\Leftrightarrow} k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \exists \vec{x} R_m(\vec{x}) \end{align} $$
for all
$k \in K$
and
$m \in \{1,\ldots ,n\}$
. For each
$k \in K$
,
$U_{q_1},\ldots ,U_{q_{n'}} \in D_k$
and
$m \in \{1,\ldots ,n\}$
, either
$$\begin{align*}[k]_{\mathcal{K}} \Vdash' R_m(U_{q_1},\ldots,U_{q_{n'}}) \text{ or } [k]_{\mathcal{K}} \not\Vdash' R_m(U_{q_1},\ldots,U_{q_{n'}}). \end{align*}$$
In the latter case, if
$[k']_{\mathcal {K}} \Vdash ' R_m(U_{q_1},\ldots ,U_{q_{n'}})$
for some
$k' \geq k$
, then
$U_{q_1} \cap \cdots \cap U_{q_{n'}} \subseteq U_{p_m}$
, and hence
$[k]_{\mathcal {K}} \Vdash ' R_m(U_{q_1},\ldots ,U_{q_{n'}})$
, a contradiction. Therefore
$ k \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \lnot R_m(U_{q_1},\ldots ,U_{q_{n'}}). $
Thus,
$$\begin{align*}k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \forall \vec{x} (R_m(\vec{x}) \lor \lnot R_m(\vec{x})) \end{align*}$$
for all
$k \in K$
and
$m \in \{1,\ldots ,n\}$
, and so
$$\begin{align*}k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \varphi[\exists \vec{x} R_1(\vec{x}),\ldots,\exists \vec{x} R_n(\vec{x})] \end{align*}$$
for all
$k \in K$
. By (†) and Lemma 3.9, we have
$ k \Vdash \varphi $
for all
$k \in K$
, a contradiction.
Lemma 3.13. Let
$\mathcal {E} =((K,\leq ),f,(I,\leq _I))$
be a locally directed extended frame, and let
$\mathcal {K}_{\mathcal {E},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E},\mathcal {I}})$
be the induced IQC-Kripke model by an IQC-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
. Then for each formula A of
$\mathcal {L}(\mathbf {IQC})$
with
$\mathrm {FV}(\exists \vec {x} A) \subseteq \{\vec {y}\}$
,
$k \in K$
, and
$\vec {b} \in D_{k}$
, there exists an upward closed subset U of I such that if
$$\begin{align*}k \Vdash_{\mathcal{E},\mathcal{I}} (\forall \vec{x} (A \lor \lnot A))[\vec{y}/\vec{b}] , \end{align*}$$
then
$$\begin{align*}f(k') \in U \mathbin{\Leftrightarrow} k' \Vdash_{\mathcal{E},\mathcal{I}} (\exists \vec{x} A)[\vec{y}/\epsilon_{k k'}(\vec{b})] \end{align*}$$
for all
$k' \geq k$
.
Proof Consider formula A of
$\mathcal {L}(\mathbf {IQC})$
and
$k \in K$
. We may assume without loss of generality that
$\mathrm {FV}(\exists \vec {x} A) = \emptyset $
. Define an upward closed subset U of I by
$$\begin{align*}U = \bigcup \{ \mathop{\uparrow} f(l) \mid k \leq l \land l \Vdash_{\mathcal{E},\mathcal{I}} \exists \vec{x} A \} , \end{align*}$$
and suppose that
$ k \Vdash _{\mathcal {E},\mathcal {I}} \forall \vec {x} (A \lor \lnot A). $
Then given
$k' \geq k$
, we show that
$$\begin{align*}f(k') \in U \mathbin{\Leftrightarrow} k' \Vdash_{\mathcal{E},\mathcal{I}} \exists \vec{x} A. \end{align*}$$
Assume that
$f(k') \in U$
. Then there exists
$l \geq k$
such that
$ f(l) \leq _I f(k') $
and
$ l \Vdash _{\mathcal {E},\mathcal {I}} A[\vec {x}/\vec {a}] $
for some
$\vec {a} \in D_{l}$
. Since
$k', l \in f^{-1}(\mathop {\uparrow } f(l)) \cap {\mathop {\uparrow } k}$
, there exists
$l' \in f^{-1}(\mathop {\uparrow } f(l)) \cap {\mathop {\uparrow } k}$
such that
$l' \leq k'$
and
$l' \leq l$
. Note that
$f(l') = f(l)$
and
$\vec {a} \in D_l = M_{f(l)} = D_{l'}$
. Since
$ k \Vdash _{\mathcal {E},\mathcal {I}} \forall \vec {x} (A \lor \lnot A) $
and
$k \leq l'$
, either
$$\begin{align*}l' \Vdash_{\mathcal{E},\mathcal{I}} A[\vec{x}/\vec{a}] \quad\mbox{or}\quad l' \Vdash_{\mathcal{E},\mathcal{I}} \lnot A[\vec{x}/\vec{a}]. \end{align*}$$
However, since
$ l \Vdash _{\mathcal {E},\mathcal {I}} A[\vec {x}/\vec {a}] $
and
$l \geq l'$
, the former must be the case. Therefore
$ l' \Vdash _{\mathcal {E},\mathcal {I}} \exists \vec {x} A , $
and, since
$l' \leq k'$
, we have
$ k' \Vdash _{\mathcal {E},\mathcal {I}} \exists \vec {x} A. $
Conversely, if
$ k' \Vdash _{\mathcal {E},\mathcal {I}} \exists \vec {x} A , $
then trivially
$ f(k') \in U. $
Proposition 3.14. Let
$\mathcal {E} =((K,\leq ),f,(I,\leq _I))$
be a locally directed extended frame. If
$\varphi \in T(\mathcal {E})$
, then
$$\begin{align*}\mathcal{K}_{\mathcal{E},\mathcal{I}} \Vdash_{\mathcal{E},\mathcal{I}} \Sigma\text{-}\varphi \end{align*}$$
for all IQC-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
.
Proof Suppose that
$\varphi \in T(\mathcal {E})$
, and consider an IQC-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
and an instance
$$\begin{align*}\forall \vec{x} (A_1 \lor \lnot A_1) \land \cdots \land \forall \vec{x} (A_n \lor \lnot A_n) \mathbin{\rightarrow} \varphi[\exists \vec{x} A_1,\ldots,\exists \vec{x} A_n] \end{align*}$$
of the schema
$\Sigma \text {-}\varphi $
. Let
$k \in K$
. We may assume without loss of generality that
$ \mathrm {FV}(\exists \vec {x} A_1,\ldots ,\exists \vec {x} A_n) = \emptyset. $
Given a
$k' \geq k$
, by Lemma 3.13, there exist upward closed subsets
$U_1,\ldots ,U_n$
of I such that for each
$ m \in \{1,\ldots ,n\}$
, if
$ k' \Vdash _{\mathcal {E},\mathcal {I}} \forall \vec {x} (A_m \lor \lnot A_m) , $
then
$$\begin{align*}f(k") \in U_m \mathbin{\Leftrightarrow} k" \Vdash_{\mathcal{E},\mathcal{I}} \exists \vec{x} A_m \end{align*}$$
for all
$k" \geq k'$
. Let
$\mathcal {I}' = (I,\leq _I,\Vdash ')$
be an IPC-Kripke model defined by
$$\begin{align*}i \Vdash' p_m \mathbin{\Leftrightarrow} i \in U_m \end{align*}$$
for each
$i \in I$
and
$m \in \{1,\ldots ,n\}$
. Assume that
$ k' \Vdash _{\mathcal {E},\mathcal {I}} \forall \vec {x} (A_m \lor \lnot A_m) $
for all
$m \in \{1,\ldots ,n\}$
. Then
$$\begin{align*}k" \Vdash_{\mathcal{E},\mathcal{I}'} p_m \mathbin{\Leftrightarrow} k" \Vdash_{\mathcal{E},\mathcal{I}} \exists \vec{x} A_m \end{align*}$$
for all
$k" \geq k'$
and
$m \in \{1,\ldots ,n\}$
. By Lemma 3.9, we have
$$\begin{align*}k' \Vdash_{\mathcal{E},\mathcal{I}'} \varphi \mathbin{\Leftrightarrow} k' \Vdash_{\mathcal{E},\mathcal{I}} \varphi[\exists \vec{x} A_1,\ldots,\exists \vec{x} A_n]. \end{align*}$$
Therefore, since
$\varphi $
is valid on
$\mathcal {E}$
, we have
$$\begin{align*}k' \Vdash_{\mathcal{E},\mathcal{I}} \varphi[\exists \vec{x} A_1,\ldots,\exists \vec{x} A_n]. \end{align*}$$
Thus
$ k \Vdash _{\mathcal {E},\mathcal {I}} \forall \vec {x} (A_1 \lor \lnot A_1) \land \cdots \land \forall \vec {x} (A_n \lor \lnot A_n) \mathbin {\rightarrow } \varphi [\exists \vec {x} A_1,\ldots ,\exists \vec {x} A_n]. $
For a set S of formulae of
$\mathcal {L}(\mathbf {IPC})$
, define sets
$S^\ast $
and
$\Sigma \text {-}S$
of schemata by
$ S^\ast = \{ \varphi ^\ast \mid \varphi \in S \} $
and
$ \Sigma \text {-}S = \{ \Sigma \text {-}\varphi \mid \varphi \in S \}. $
Now, we arrive at a separation theorem for
$\mathbf {IQC}$
.
Theorem 3.15. Let
$\mathcal {K} = (K,\leq ,\Vdash )$
be an IPC-Kripke model, and let
$\varphi $
be a formula of
$\mathcal {L}(\mathbf {IPC})$
. If
$\mathcal {K} \not \Vdash \varphi $
and
$\mathcal {E}_{\mathcal {K}}$
is locally directed, then
$$\begin{align*}L(K,\leq)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}}) \not\vdash_{\mathbf{IQC}} \Sigma\text{-}\varphi. \end{align*}$$
Proof Straightforward by Proposition 3.10, Proposition 3.12, Proposition 3.14, and the soundness theorem [Reference Troelstra and van Dalen33, Chapter 2, Section 5.10].
Example 3.16. By applying Theorem 3.15 to Example 2.10, we have
$$\begin{align*}L({K}_1,\leq_1)^\ast \not\vdash_{\mathbf{IQC}} \Sigma\text{-}\mathrm{DNE} , \end{align*}$$
especially
$ \mathrm {WPEM}^\ast \not \vdash _{\mathbf {IQC}} \Sigma \text {-}\mathrm {DNE}; $
to Example 2.11, we have
$$\begin{align*}L({K}_2,\leq_2)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_2}) \not\vdash_{\mathbf{IQC}} \Sigma\text{-}\mathrm{WPEM} , \end{align*}$$
especially
$ \Sigma \text {-}\mathrm {DML} + \Sigma \text {-}\mathrm {DNE} \not \vdash _{\mathbf {IQC}} \Sigma \text {-}\mathrm {WPEM}; $
to Example 2.12, we have
$$\begin{align*}L({K}_3,\leq_3)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_3}) \not\vdash_{\mathbf{IQC}} \Sigma\text{-}\mathrm{DML} , \end{align*}$$
especially
$ \Sigma \text {-}\mathrm {DNE} \not \vdash _{\mathbf {IQC}} \Sigma \text {-}\mathrm {DML}; $
to Example 2.13, we have
$$\begin{align*}L({K}_4,\leq_4)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_4}) \not\vdash_{\mathbf{IQC}} \Sigma\text{-}\mathrm{WDML} , \end{align*}$$
especially
$ \Sigma \text {-}\mathrm {RPEM} \not \vdash _{\mathbf {IQC}} \Sigma \text {-}\mathrm {WDML}; $
to Example 2.14, we have
$$\begin{align*}L({K}_2,\leq_2)^\ast \not\vdash_{\mathbf{IQC}} \Sigma\text{-}\mathrm{RPEM}. \end{align*}$$
Note that
$\Sigma \mbox {-}\mathrm {DNE}$
,
$\Sigma \mbox {-}\mathrm {WPEM}$
,
$\Sigma \mbox {-}\mathrm {DML}$
,
$\Sigma \mbox {-}\mathrm {WDML}$
, and
$\Sigma \mbox {-}\mathrm {RPEM}$
correspond to
$\mathrm {MP}$
,
$\mathrm {WLPO}$
,
$\mathrm {LLPO}$
,
$\mathrm {MP}^\lor $
, and
$\Delta _1\mbox {-}\mathrm {PEM}$
, respectively.
4 Separations by extended frames in
$\mathbf {HA}$
In this section, we apply the results in the previous section to
$\mathbf {HA}$
, and show a separation theorem (Theorem 4.17) of a sentence from a set of schemata. We then see the examples which give us separations among omniscience principles (Example 4.18).
We use the standard language
$\mathcal {L}_1 = \mathcal {L}(\mathbf {HA})$
of intuitionistic first-order arithmetic
$\mathbf {HA}$
containing the constant
$0$
, the unary function symbol S, the binary function symbols
$+$
and
$\times $
, and the binary predicate
$=$
(equality). The axioms and rules are those of
$\mathbf {IQC}$
with equality, the axioms
$$ \begin{align*} & Sx = Sy \mathbin{\rightarrow} x = y , & & \lnot 0 = Sx , & & \lnot 0 = x \mathbin{\rightarrow} \exists y (x = Sy) \end{align*} $$
and
$$ \begin{align*} x + 0 & = x , & x + Sy & = S(x+y) , & x \times 0 & = 0 , & x \times Sy & = (x \times y) + x , \end{align*} $$
and the induction axiom schema
$$\begin{align*}A(0) \land \forall x (A(x) \mathbin{\rightarrow} A(Sx)) \mathbin{\rightarrow} \forall x A(x) \end{align*}$$
(see [Reference Lindström27, Chapter 1]).
A
$\Sigma _0$
-formula (and
$\Pi _0$
-formula) is a formula built up from prime formulae by the propositional connectives
$\land $
,
$\lor $
, and
$\mathbin {\rightarrow }$
, and the bounded quantifiers
$\forall x \leq t$
and
$\exists x \leq t$
; A
$\Sigma _{n+1}$
-formula is a
$\Pi _n$
-formula or a formula of the form
$\exists x A$
, where A is a
$\Pi _n$
-formula, and a
$\Pi _{n+1}$
-formula is a
$\Sigma _n$
-formula or a formula of the form
$\forall x A$
, where A is a
$\Sigma _n$
-formula. A
$\Sigma _n$
-sentence (respectively,
$\Pi _n$
-sentence) is a
$\Sigma _n$
-formula (respectively,
$\Pi _n$
-formula) without free variables.
In the following, we use
$\vdash $
and
$\vdash _c$
for deducibilities of intuitionistic and classical first-order predicate logic
$\mathbf {IQC}$
and
$\mathbf {CQC}$
, respectively. Recall that
$\models _c$
denotes the classical interpretation in a (first-order) structure.
Definition 4.1. Let
$\mathbf {HA}$
also denote the (recursive) set of
$\mathcal {L}_1$
-sentences consisting of (the universal closures of) axioms and instances of the axiom schema of
$\mathbf {HA}$
. Then
$\mathbf {HA} \vdash _c A$
means that a formula A is derivable in classical first-order arithmetic
$\mathbf {PA}$
. Let
$\mathrm {Th}(\omega )$
denote the set of
$\mathcal {L}_1$
-sentences which are true in
$\omega $
, that is,
$ \mathrm {Th}(\omega ) = \{ A \mid \omega \models _c A \}. $
For a set T of
$\mathcal {L}_1$
-sentences, a
$\Sigma _{1}$
-representation of T is a
$\Sigma _{1}$
-formula
$\tau (x)$
such that
$$ \begin{gather*} \mathbf{HA} \vdash_{c} \forall x [ (\tau(x)\to "x\text{ is a sentence"}) \wedge (\tau_{\mathbf{HA}}(x)\to\tau(x)) ] , \text{ and} \\ A\in T\text{ if and only if } \mathbf{HA} \vdash_{c}\tau(\lceil A\rceil) (\text{ or equivalently }\omega\models_{c}\tau(\lceil A\rceil)) \end{gather*} $$
for all
$\mathcal {L}_{1}$
-sentence A, where
$\lceil A\rceil $
is a Gödel number of A and
$\tau _{\mathbf {HA}}(x)$
denotes
$$ \begin{align*} &"x \text{ is (a Gödel number of) a sentence"}\\ &\, \wedge "x\text{ is an axiom or an instance of the axiom schema of }\mathbf{HA}.\text{"} \end{align*} $$
A set T of
$\mathcal {L}_1$
-sentences is well-behaved if T has a
$\Sigma _{1}$
-representation and
$ \mathbf {HA} \subseteq T \subseteq \mathrm {Th}(\omega ). $
Remark 4.2. It is easy to see that if T has a
$\Sigma _{1}$
-representation, then it is recursively enumerable. Conversely, if T (
$\supseteq \mathbf {HA}$
) is recursively enumerable, then there exists a
$\Sigma _{1}$
-formula which represents T. For each recursively enumerable set T (
$\supseteq \mathbf {HA}$
), we fix a
$\Sigma _1$
-representation (say, by choosing the one with the smallest Gödel number), and identify T with its
$\Sigma _{1}$
-representation. With this identification, one may refer to the consistency statement
$ \mathrm {Con}(T) \equiv \lnot "T \vdash _c \bot " $
of T within
$\mathbf {HA}$
.
Definition 4.3. Let M be an
$\mathcal {L}_1$
-structure. Then a subset S of
$M^n$
is definable in M if there exists a formula B with
$\mathrm {FV}(B) = \{x_1,\ldots ,x_n\}$
such that
$$\begin{align*}S = \{ (a_1,\ldots,a_n) \in M^n \mid M \models_c B[x_1,\ldots,x_n/a_1,\ldots,a_n] \}; \end{align*}$$
a function is definable in M if its graph is a definable subset in M. An
$\mathcal {L}_1$
-structure
$\hat {M}$
is a definable structure in M if the universe of
$\hat {M}$
is a definable subset in M, and the interpretations of
$+$
and
$\times $
in
$\hat {M}$
are definable functions in M (see [Reference Hájek and Pudlák13, Reference Kaye22] for the basic notions of model theory of arithmetic).
Remark 4.4. Let M be an
$\mathcal {L}_1$
-structure such that
$M \models _c \mathbf {HA}$
, and let
$\hat {M}$
be a definable
$\mathcal {L}_1$
-structure in M. Then the interpretation of closed
$\mathcal {L}_1$
-terms in
$\hat {M}$
, that is, a function
$\sigma _0$
from the codes (in M) of closed
$\mathcal {L}_1$
-terms into
$\hat {M} \subseteq M$
, is definable in M. This
$\sigma _{0}$
yields the canonical embedding
$\theta : M \to \hat {M}$
, defined by
$\theta (m) = \sigma _0(\bar {m})$
where
$\bar {m}$
is the m-th numeral coded in M. Moreover, this
$\theta $
is a
$\Sigma _0$
-elementary embedding, that is,
$ {M \models _c B[\vec {x}/\vec {a}]} \mathbin {\Leftrightarrow } {\hat {M} \models _c B[\vec {x}/\theta (\vec {a})]} $
for all
$\Sigma _0$
-formula B and
$\vec {a} \in M$
(see [Reference Smoryński31, Lemma 6.12 and Lemma 3.8]).
Theorem 4.5 (Arithmetized completeness theorem).
Let T be a well-behaved set of
$\mathcal {L}_1$
-sentences, and let M be an
$\mathcal {L}_1$
-structure such that
$$\begin{align*}M \models_c \mathbf{HA} +\mathrm{Con}(T). \end{align*}$$
Then there exist a definable
$\mathcal {L}_1$
-structure
$\hat {M}$
in M and a
$\Sigma _0$
-elementary embedding
$\theta : M \to \hat {M}$
such that
$ \hat {M} \models _c T. $
Moreover, for each formula B, there exists a formula
$[B]$
such that
$\mathrm {FV}([B]) = \mathrm {FV}(B)$
and
$$\begin{align*}{M \models_c [B][\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {\hat{M} \models_c B[\vec{x}/\theta(\vec{a})]} \end{align*}$$
for all
$\vec {a} \in M$
, where
$\vec {x}$
are the free variables of B.
This is the semantic form of the arithmetized completeness theorem [Reference Smoryński31, Theorem 6.10] together with the
$\Sigma _{0}$
-elementary canonical embedding obtained in Remark 4.4. This theorem is also referred to as the interpretability theorem (see, e.g., [Reference Ardeshir and Mojtahedi2, Reference de Jongh, Verbrugge and Visser21]). We will digest the proof of the relativized form of this theorem in Appendix B.
Lemma 4.6 (Fixed point lemma [Reference Lindström27, Chapter 1, Lemma 1(b)]).
Let
$k\ge 1$
. For any
$\Pi _{k}$
-formula
$\gamma (w,n)$
, there exists a
$\Pi _{k}$
-formula
$\xi \equiv \xi (v)$
such that
$$\begin{align*}\mathbf{HA}\vdash_{c}\forall n(\xi(n)\leftrightarrow \gamma(\lceil \xi\rceil,n)).\end{align*}$$
Lemma 4.7 [Reference Lindström27, Chapter 2, Exercise 11].
Let T be a well-behaved set of
$\mathcal {L}_1$
-sentences. Then there exists a
$\Pi _1$
-formula
$K(v)$
such that
$ T \not \vdash _c K(m) $
for all natural number m, and
$ \mathbf {HA} \vdash _c K(m) \lor K(l) $
for all natural numbers m and l with
$m \neq l$
.
Proof We follow the hint in [Reference Lindström27]. Let
$\gamma (w,n)$
be a formula which denotes
$$ \begin{align*} &"w\text{ is a formula such that }\mathrm{FV}(w)\subseteq \{v\}\text{"}\\ &\to\forall y["y\text{ is a proof of }T\vdash_{c} w[v/\bar n]\text{"}\\ &\to \exists z\exists u(\langle u,z\rangle < \langle n,y\rangle \wedge "z\text{ is a proof of }T\vdash_{c} w[v/\bar u]\text{"})], \end{align*} $$
where
$\langle \cdot ,\cdot \rangle $
denotes the usual pairing function. Then apply the fixed point lemma and obtain a
$\Pi _{1}$
-formula
$K\equiv K(v)$
such that
$\mathbf {HA}\vdash _{c}\forall n(K(n)\leftrightarrow \gamma (\lceil K\rceil , n)).$
It is easy to check that this
$K(v)$
satisfies the desired conditions.
Lemma 4.8. Let
$\{ T_1, \ldots , T_n \}$
be a nonempty and finite set of well-behaved sets of
$\mathcal {L}_1$
-sentences. Then there exist a well-behaved set T of
$\mathcal {L}_1$
-sentences with
$\bigcup _{j=1}^n T_j \subseteq T$
and a set
$\{ A_1, \ldots , A_n \}$
of
$\Sigma _1$
-sentences such that:
-
1.
$ T \vdash _c \mathrm {Con}(T_j + A_j) , $
-
2.
$ T \vdash _c \lnot A_j, $
-
3. if
$j \neq j'$
, then
$ \mathbf {HA} \vdash _c \lnot (A_j \land A_{j'}), $
for all
$j, j' \in \{1,\ldots ,n\}$
.
Proof Let
$\{ T_1, \ldots , T_n \}$
be a nonempty and finite set of well-behaved sets of
$\mathcal {L}_1$
-sentences, and let
$ T' = \bigcup _{j=1}^n T_j. $
Then
$T'$
is a well-behaved set of
$\mathcal {L}_1$
-sentences. By Lemma 4.7, there exists a
$\Sigma _1$
-formula
$K(x)$
such that
$ T' \not \vdash _c \lnot K(m) $
for all natural number m, and
$ \mathbf {HA} \vdash _c \lnot (K(m) \land K(l)) $
for all natural numbers m and l with
$m \neq l$
. Note that for each natural number m, since
$T' + K(m) \not \vdash _c \bot $
, we have
$\mathrm {Con}(T' + K(m)) \in \mathrm {Th}(\omega )$
. Since
$$\begin{align*}\mathbf{HA} \vdash_c K(m) \mathbin{\rightarrow} "\mathbf{HA} \vdash_c K(m)," \end{align*}$$
by
$\Sigma _1$
-completeness of the provability predicate [Reference Lindström27, Chapter 1, Fact 9], we have
$$\begin{align*}\mathbf{HA} \vdash_c K(m) \mathbin{\rightarrow} "\mathbf{HA} + K(l) \vdash_c K(m)," \end{align*}$$
and hence
$ \mathbf {HA} \vdash _c K(m) \mathbin {\rightarrow } "\mathbf {HA} + K(l) \vdash _c \bot " $
for all natural numbers m and l with
$m \neq l$
. Therefore,
$$\begin{align*}\mathbf{HA} \vdash_c K(m) \mathbin{\rightarrow} \lnot\mathrm{Con}(\mathbf{HA} + K(l)) , \end{align*}$$
and so
$ \mathbf {HA} \vdash _c \mathrm {Con}(\mathbf {HA}+K(l)) \mathbin {\rightarrow } \lnot K(m). $
Let
$ A_j \equiv K(j) $
for each
$j \in \{1,\ldots ,n\}$
, and let
$$\begin{align*}T = T' + \{\mathrm{Con}(T'+K(0)),\mathrm{Con}(T'+A_1),\ldots,\mathrm{Con}(T'+A_n)\}. \end{align*}$$
Then
$ \mathbf {HA} \vdash _c \lnot (A_j \land A_{j'}) $
for all
$j, j' \in \{1,\ldots ,n\}$
with
$j \neq j'$
, and T is a well-behaved set of
$\mathcal {L}_1$
-sentences. For each
$j \in \{1,\ldots ,n\}$
, since
$ \mathbf {HA} \vdash _c \mathrm {Con}(T'+A_j) \mathbin {\rightarrow } \mathrm {Con}(T_j + A_j) $
and
$ \mathbf {HA} \vdash _c \mathrm {Con}(T'+K(0)) \mathbin {\rightarrow } \mathrm {Con}(\mathbf {HA} + K(0)) , $
we have
$ T \vdash _c \mathrm {Con}(T_j+A_j) $
and
$ T \vdash _c \lnot A_j. $
In the following, we call an IQC-Kripke model for the language
$\mathcal {L}_1$
an
$\mathcal {L}_1$
-Kripke model. The construction in the proof of the following lemma is essentially the same as Smoryński’s construction for the refinement of de Jongh’s theorem (see [Reference Smoryński32, Chapter V, Section 2–3]).
Lemma 4.9. Let
$T_{0}$
be a well-behaved set of
$\mathcal {L}_{1}$
-sentences, and let
$(I,\leq _I)$
be a finite tree with the root
$i_0 \in I$
. Then there exists a well-behaved set T of
$\mathcal {L}_1$
-sentences with
$T_0 \subseteq T$
such that for each
$\Sigma _1$
-sentence
$C_0$
and
$\mathcal {L}_1$
-structure
$M_0$
, if
$$\begin{align*}M_0 \models_c T + C_0 , \end{align*}$$
then there exist an
$\mathcal {L}_1$
-Kripke model
$\mathcal {I} = (I,\leq _I,\{M_i \mid i \in I\},\eta ,\Vdash )$
and a family
$\{ C_i \mid i \in I \}$
of
$\Sigma _1$
-sentences with
$M_{i_0} = M_0$
and
$C_{i_0} \equiv C_0$
satisfying that for each
$i \in I$
,
-
1.
$ M_i \models _c T_{0} + C_i; $
-
2.
$i \leq _I i'$
implies
$ \mathbf {HA} \vdash _c C_{i'} \mathbin {\rightarrow } C_i $
for all
$i' \in I$
; -
3.
$ M_{i'} \models _c C_i $
implies
$ i \leq _I i' $
for all
$i' \in I$
; -
4. for each
$i' \in I$
with
$i \leq _I i'$
and formula B, there exists an
$\mathcal {L}_{1}$
-formula
$[B]^{i'}_{i}$
such that
$\mathrm {FV}([B]_{i}^{i'}) = \mathrm {FV}(B)$
and for all
$$\begin{align*}{M_i \models_c [B]_{i}^{i'}[\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {M_{i'} \models_c B[\vec{x}/\eta_{i i'}(\vec{a})]} \end{align*}$$
$\vec {a} \in M_{i}$
, where
$\vec {x}$
are the free variables of B;
-
5. if B is a
$\Sigma _0$
-formula, then for all
$$\begin{align*}{M_i \models_c B[\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {M_{i'} \models_c B[\vec{x}/\eta_{i i'}(\vec{a})]} \end{align*}$$
$i' \in I$
with
$i \leq _I i'$
and
$\vec {a} \in M_{i}$
, where
$\vec {x}$
are the free variables of B.
Proof We proceed by induction on the complexity of
$(I,\leq _I)$
.
Basis: If
$i_0$
is a leaf, then note that
$I = \{i_0\}$
, and set
$T = T_{0}$
. For each
$\Sigma _1$
-sentence
$C_0$
and
$\mathcal {L}_1$
-structure
$M_0$
with
$$\begin{align*}M_0 \models_c T + C_0 , \end{align*}$$
setting
$M_{i_0} = M_0$
, define an
$\mathcal {L}_1$
-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
by
$ M = \{M_{i_0}\} , $
$ \eta = \{\mathrm {id}_{M_{i_0}}\} $
and
$ {i_0 \Vdash P} \mathbin {\Leftrightarrow } {M_{i_0} \models _c P} $
for each atomic P, and set
$C_{i_0} \equiv C_0$
. Then it is straightforward to see that
$\mathcal {I}$
and
$\{ C_{i_0} \}$
satisfy (1)–(5) for all
$i \in I$
.
Induction step: Let J be the (nonempty and finite) set of direct descendants (children) of
$i_0$
, and note that
$ i_0 = i \lor \exists ! j \in J (j \leq _I i) $
for all
$i \in I$
. Then, since
$(\mathop {\uparrow } j,\leq _I)$
is a finite tree with the root j for all
$j \in J$
, there exist, by the induction hypothesis, the set
$\{ T_j \mid j \in J \}$
of well-behaved sets including
$T_0$
such that for each
$j \in J$
,
$\Sigma _1$
-sentence
$C_j$
and
$\mathcal {L}_1$
-structure
$M_j$
, if
$ M_j \models _c T_j + C_j , $
then there exist an
$\mathcal {L}_1$
-Kripke model
$(\mathop {\uparrow } j,\leq _I,M^j,\eta ^j,\Vdash ^j)$
and a family
$\{ C^j_i \mid i \in \mathop {\uparrow } j \}$
of
$\Sigma _1$
-sentences satisfying that (1)–(5) for all
$i \in \mathop {\uparrow } j$
. By Lemma 4.8, there exist a well-behaved set T of
$\mathcal {L}_1$
-sentences with
$\bigcup _{j \in J} T_j \subseteq T$
and a set
$\{ A_j \mid j \in J \}$
of
$\Sigma _1$
-sentences such that
$ T \vdash _c \mathrm {Con}(T_j + A_j) , $
$ T \vdash _c \lnot A_j, $
and if
$j \neq j'$
, then
$ \mathbf {HA} \vdash _c \lnot (A_j \land A_{j'}) $
for all
$j, j' \in J$
. Consider a
$\Sigma _1$
-sentence
$C_0$
and an
$\mathcal {L}_1$
-structure
$M_0$
such that
$$\begin{align*}M_0 \models_c T + C_0. \end{align*}$$
Then
$ M_0 \models _c \mathbf {HA} + \mathrm {Con}(T_j + A_j) $
and
$ M_0 \models _c \lnot A_j $
for all
$j \in J$
. By the arithmetized completeness theorem, for each
$j \in J$
there exist a definable
$\mathcal {L}_1$
-structure
$\hat {M}_j$
in
$M_0$
and a
$\Sigma _0$
-elementary embedding
$\theta _j : M_0 \to \hat {M}_j$
such that
$ \hat {M}_j \models _c T_j + A_j. $
Let
$C_j$
be a
$\Sigma _1$
-sentences such that
$ \mathbf {HA} \vdash _c C_j \mathbin {\leftrightarrow } C_0 \land A_j. $
Then, since
$\hat {M}_j$
is a
$\Sigma _0$
-elementary extension of
$M_0$
, we have
$ \hat {M}_j \models _c C_0 , $
and hence
$$\begin{align*}\hat{M}_j \models_c T_j + C_j. \end{align*}$$
Therefore there exist an
$\mathcal {L}_1$
-Kripke model
$(\mathop {\uparrow } j,\leq _I,M^j,\eta ^j,\Vdash ^j)$
, where
$M^j = \{ M^j_i \mid i \in \mathop {\uparrow } j \}$
, and a family
$\{ C^j_i \mid i \in \mathop {\uparrow } j \}$
of
$\Sigma _1$
-sentences satisfying (1)–(5), and
$M^j_j = \hat {M}_j$
and
$C^j_j \equiv C_j$
. Setting
$M_{i_0} = M_0$
, define an
$\mathcal {L}_1$
-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
by
$$ \begin{align*} M & = \{M_{i_0}\} \cup \bigcup_{j \in J} M^j , & \eta & = \{ \eta_{i_0 i} \mid i \in I \} \cup \bigcup_{j \in J} \eta^j , & \Vdash & = \{\Vdash_0\} \cup \bigcup_{j \in J} \Vdash^j , \end{align*} $$
where
$ \eta _{i_0 i_0} = \mathrm {id}_{M_{i_0}} $
and
$ \eta _{i_0 i} = \eta ^j_{j i} \circ \theta _j $
for
$i \in I$
with
$j \in J$
and
$j \leq _I i$
, and
$\Vdash _0$
is defined by
$ {i_0 \Vdash _0 P} \mathbin {\Leftrightarrow } {M_{i_0} \models _c P} $
for each atomic P. Set
$ C_i \equiv C_0 $
if
$i = i_0$
;
$ C_i \equiv C^j_i $
if
$i \in I$
with
$j \in J$
and
$j \leq _I i$
. We show that
$\mathcal {I}$
and
$\{C_i \mid i \in I\}$
satisfy (1)–(5). Let
$i \in I$
.
-
(1): Either (i)
$i = i_0$
; or (ii)
$j \leq _I i$
for some
$j \in J$
.-
(i): We have
$M_{i_0} \models _c T_{0} + C_{i_0}$
. -
(ii): We have
$M_i \models _c T_{0} + C_i$
, by the induction hypothesis.
-
-
(2): If
$i \leq _I i'$
, then either (i)
$i = i' = i_0$
; (ii)
$i = i_0$
and
$j \leq _I i'$
for some
$j \in J$
; or (iii)
$j \leq _I i \leq _I i'$
for some
$j \in J$
.-
(i): It is trivial.
-
(ii): Since
$\mathbf {HA} \vdash _c C_j \mathbin {\rightarrow } C_{i_0}$
, we have
$\mathbf {HA} \vdash _c C_{i'} \mathbin {\rightarrow } C_i$
, by the induction hypothesis. -
(iii): It follows from the induction hypothesis.
-
-
(3): Suppose that
$M_{i'} \models _c C_i$
. Then either (i)
$i = i_0$
; (ii)
$i' = i_0$
and
$j \leq _I i$
for some
$j \in J$
; or (iii)
$j \leq _I i$
and
$j' \leq _I i'$
for some
$j, j' \in J$
.-
(i): There is nothing to prove.
-
(ii): Since
$M_{i_0} \models _c C_i$
and
$\mathbf {HA} \vdash _c C_i \mathbin {\rightarrow } C_j$
, we have
$M_{i_0} \models _c C_j$
, and hence
$M_{i_0} \models _c A_j$
, a contradiction to
$M_{i_0} \models _c \lnot A_j$
. -
(iii): Since
$M_{i'} \models _c C_i$
,
$M_{i'} \models _c C_{i'}$
,
$\mathbf {HA} \vdash _c C_i \mathbin {\rightarrow } C_j$
, and
$\mathbf {HA} \vdash _c C_{i'} \mathbin {\rightarrow } C_{j'}$
, we have
$M_{i'} \models _c C_j$
and
$M_{i'} \models _c C_{j'}$
, and hence
$M_{i'} \models _c A_j \land A_{j'}$
. Therefore, since
$j \neq j'$
implies a contradiction to
$M_{i'} \models _c \lnot (A_j \land A_{j'})$
, we have
$j = j'$
, and so
$i \leq i'$
, by the induction hypothesis.
-
-
(4): Consider
$i' \in I$
with
$i \leq _I i'$
. Then either (i)
$i = i' = i_0$
; (ii)
$i = i_0$
and
$j \leq _I i'$
for some
$j \in J$
; or (iii)
$j \leq _I i$
for some
$j \in J$
.-
(i): It is trivial.
-
(ii): Since for each formula B there exists a formula
$[B]$
with
$\mathrm {FV}(B) = \mathrm {FV}([B]) = \{\vec {x}\}$
such that for all
$$\begin{align*}{M_{i_0} \models_c [B][\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {\hat{M}_j \models_c B[\vec{x}/\theta_j(\vec{a})]} \end{align*}$$
$\vec {a} \in M_{i_0}$
, we have
$\mathrm {FV}(B) = \mathrm {FV}([[B]^{i'}_j])$
and for all
$$ \begin{align*} {M_{i_0} \models_c [[B]^{i'}_j][\vec{x}/\vec{a}]} & \mathbin{\Leftrightarrow} {M_j \models_c [B]^{i'}_j[\vec{x}/\theta_j(\vec{a})]} \\ & \mathbin{\Leftrightarrow} {M_{i'} \models_c B[\vec{x}/\eta^j_{j i'}(\theta_j(\vec{a}))]} , \end{align*} $$
$\vec {a} \in M_{i_0}$
, by the induction hypothesis, and hence for all
$$\begin{align*}{M_{i_0} \models_c [[B]^{i'}_j][\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {M_{i'} \models_c B[\vec{x}/\eta_{i_0 i'}(\vec{a})]} \end{align*}$$
$\vec {a} \in M_{i_0}$
.
-
(iii): It follows from the induction hypothesis.
-
-
(5): Consider
$i' \in I$
with
$i \leq _I i'$
. Then either (i)
$i = i' = i_0$
; (ii)
$i = i_0$
and
$j \leq _I i'$
for some
$j \in J$
; or (iii)
$j \leq _I i$
for some
$j \in J$
.-
(i): It is trivial.
-
(ii): It suffices to show that if B is a
$\Sigma _0$
-formula, then for all
$$\begin{align*}{M_{i_0} \models_c B[\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {M_{j} \models_c B[\vec{x}/\theta_j(\vec{a})]} \end{align*}$$
$j \in J$
and
$\vec {a} \in M_{i_0}$
. This is the case, since
$M_j$
is a
$\Sigma _0$
-elementary extension of
$M_{i_0}$
.
-
(iii): It follows from the induction hypothesis.
-
We need a couple of technical lemmas in the language of
$\mathcal {L}(\mathbf {IQC})$
whose proofs are given in Appendix A.
Definition 4.10. Recall the definition of a schema in Definition 3.4. Then we define simultaneously classes
$\mathcal {A}$
,
$\mathcal {B}$
,
$\mathcal {C}$
, and
$\mathcal {D}$
of schemata as follows. Let P range over atomic formulae,
$\nu $
over expressions
$\nu _k(t_1 \ldots t_n)$
(
$\nu _k$
an n-ary place holder symbol),
$\alpha $
and
$\alpha '$
over
$\mathcal {A}$
,
$\beta $
and
$\beta '$
over
$\mathcal {B}$
,
$\gamma $
and
$\gamma '$
over
$\mathcal {C}$
, and
$\delta $
and
$\delta '$
over
$\mathcal {D}$
. Then
$\mathcal {A}$
,
$\mathcal {B}$
,
$\mathcal {C}$
, and
$\mathcal {D}$
are inductively generated by the clauses
$$ \begin{align*} & \bot, \alpha \land \alpha', \alpha \lor \alpha', \forall x \alpha, \gamma \mathbin{\rightarrow} \alpha \in \mathcal{A}; \\ & \alpha, P, \nu, \beta \land \beta', \beta \lor \beta', \forall x \beta, \exists x \beta, \gamma \mathbin{\rightarrow} \beta \in \mathcal{B}; \\ & \bot, P, \nu, \gamma \land \gamma', \gamma \lor \gamma', \exists x \gamma, \alpha \mathbin{\rightarrow} \gamma \in \mathcal{C}; \\ & \gamma, \delta \land \delta', \forall x \delta, \beta \mathbin{\rightarrow} \delta \in \mathcal{D}. \end{align*} $$
Lemma 4.11. Let
$\mathcal {E} = ((K,\leq ),f,(I,\leq _I))$
be an extended frame such that
$(K,\leq )$
is finite, and let
$\mathcal {K}_{\mathcal {E},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E},\mathcal {I}})$
be the induced IQC-Kripke model by an IQC-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
. Assume that for each
$i, i' \in I$
with
$i \leq i'$
and formula B, there exists a formula
$[B]^{i'}_{i}$
such that
$\mathrm {FV}([B]_{i}^{i'}) = \mathrm {FV}(B)$
and
$$\begin{align*}M_{i} \models_c [B]_{i}^{i'}[\vec{x}/\vec{a}] \mathbin{\Leftrightarrow} M_{i'} \models_c B[\vec{x}/\eta_{i i'}(\vec{a})] \end{align*}$$
for all
$\vec {a} \in M_{i}$
, where
$\vec {x}$
are the free variables of B. If
$\Gamma \subseteq \mathcal {D}$
and
$M_{f(k)} \models _c \Gamma $
for all
$k \in K$
, then
$\mathcal {K}_{\mathcal {E},\mathcal {I}} \Vdash \Gamma $
.
Definition 4.12. Let
$\Gamma $
be a class of formulae. Then
$\Gamma $
is closed under subformulae if:
-
1. if
$A \circ B \in \Gamma $
, then
$A \in \Gamma $
and
$B \in \Gamma $
, where
$\circ \in \{\land ,\lor ,\mathbin {\rightarrow }\}$
; -
2. if
$\forall x A \in \Gamma $
or
$\exists x A \in \Gamma $
, then
$A[x/t] \in \Gamma $
for all term t.
The class
$\exists (\Gamma )$
of formulae is inductively generated by the rules:
-
1.
$A \in \exists (\Gamma )$
for
$A \in \Gamma $
; -
2. if
$A, B \in \exists (\Gamma )$
, then
$A \land B, A \lor B \in \exists (\Gamma )$
; -
3. if
$A[x/t] \in \exists (\Gamma )$
for all term t, then
$\exists x A \in \exists (\Gamma )$
.
Remark 4.13. In the language
$\mathcal {L}_1$
of
$\mathbf {HA}$
, the classes of
$\Sigma _n$
-formulae and
$\Pi _n$
-formulae are closed under subformulae, and each
$\Sigma _{n+1}$
-formula belongs to a class
$ \exists (\Gamma ) $
of formulae, where
$\Gamma $
is the class of
$\Pi _n$
-formulae.
Lemma 4.14. Let
$ \mathcal {E} = ((K,\leq ),f,(I,\leq _I)) $
be an extended frame, let
$ \Gamma $
be a class of formulae closed under subformulae, and let
$ \mathcal {I} = (I,\leq _I,M,\eta ,\Vdash ) $
be an IQC-Kripke model such that if
$B \in \Gamma $
, then
$$\begin{align*}{M_i \models_c B[\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {M_j \models_c B[\vec{x}/\eta_{i j}(\vec{a})]} \end{align*}$$
for all
$i, j \in I$
with
$i \leq _I j$
and
$\vec {a} \in M_i$
. For the induced IQC-Kripke model
$ \mathcal {K}_{\mathcal {E},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E},\mathcal {I}}) , $
if
$B \in \exists (\Gamma )$
, then
$$\begin{align*}{k \Vdash_{\mathcal{E},\mathcal{I}} B[\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {M_{f(k)} \models_c B[\vec{x}/\vec{a}]} \end{align*}$$
for all
$k \in K$
and
$\vec {a} \in D_k = M_{f(k)}$
.
Definition 4.15. For each formula
$\varphi [p_1,\ldots ,p_m]$
of
$\mathcal {L}(\mathbf {IPC})$
and n, we define a set
$\Sigma _n\mbox {-}\varphi $
of
$\mathcal {L}_1$
-formulae by
$$\begin{align*}\Sigma_n\mbox{-}\varphi = \{ \varphi[A_1,\ldots,A_m] \mid A_1,\ldots,A_m\text{ are }\Sigma_n\text{-formulae} \}. \end{align*}$$
Proposition 4.16. Let
$\mathcal {E}_{\mathcal {K}} = ((K,\leq ),f_{\mathcal {K}},(I_{\mathcal {K}},\leq _{\mathcal {K}}))$
be the extended frame generated by a finite IPC-Kripke model
$\mathcal {K} = (K,\leq ,\Vdash )$
such that
$(I_{\mathcal {K}},\leq _{\mathcal {K}})$
is a rooted (and finite) tree, and let
$\varphi [p_1,\ldots ,p_n]$
be a formula of
$\mathcal {L}(\mathbf {IPC})$
. If
$ \mathcal {K} \not \Vdash \varphi , $
then
$$\begin{align*}\mathcal{K}_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \mathbf{HA} \quad\text{and}\quad \mathcal{K}_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \not\Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \Sigma_1\mbox{-}\varphi \end{align*}$$
for some
$\mathcal {L}_1$
-Kripke model
$ \mathcal {I} = (I_{\mathcal {K}},\leq _{\mathcal {K}},M,\eta ,\Vdash '). $
Proof Let
$i_0 \in I_{\mathcal {K}}$
be the root of the finite tree
$(I_{\mathcal {K}},\leq _{\mathcal {K}})$
. Then, by Lemma 4.9 with
$T_{0}=\mathbf {HA}$
, there exists a well-behaved set T of
$\mathcal {L}_1$
-sentences such that for each
$\Sigma _1$
-sentence
$C_{i_0}$
and
$\mathcal {L}_1$
-structure
$M_{i_0}$
, if
$$\begin{align*}M_{i_0} \models_c T + C_{i_0} , \end{align*}$$
there exist an
$\mathcal {L}_1$
-Kripke model
$(I_{\mathcal {K}},\leq _{\mathcal {K}},M,\eta ,\Vdash ')$
and a family
$\{ C_i \mid i \in I_{\mathcal {K}} \}$
of
$\Sigma _1$
-sentences satisfying that for each
$i \in I$
, (1)–(5) of Lemma 4.9. Let
$M_{i_0}$
be a model of T, and let
$C_{i_0} \equiv 0 = 0$
. Then
$ M_{i_0} \models _c T + C_{i_0} , $
and hence there exist an
$\mathcal {L}_1$
-Kripke model
$\mathcal {I} = (I_{\mathcal {K}},\leq _{\mathcal {K}},M,\eta ,\Vdash ')$
and a family
$\{ C_i \mid i \in I_{\mathcal {K}} \}$
of
$\Sigma _1$
-sentences satisfying that (1)–(5) for all
$i \in I_{\mathcal {K}}$
.
Let
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}}) $
be the induced
$\mathcal {L}_1$
-Kripke model by
$\mathcal {I}$
. We show that
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \mathbf {HA} $
and
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \not \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \varphi [B_1,\ldots ,B_n] $
for some
$\Sigma _1$
-sentences
$B_1,\ldots ,B_n$
. Since
$(K,\leq )$
is finite and the property (4) holds for all
$i \in I_{\mathcal {K}}$
, by Lemma 4.11, if
$\Gamma \subseteq \mathcal {D}$
and
$M_{f_{\mathcal {K}}(k)} \models _c \Gamma $
for all
$k \in K$
, then
$\mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \Vdash _{\mathcal {E},\mathcal {I}} \Gamma $
. Therefore, since the axioms and the axiom schema of
$\mathbf {HA}$
belong to the class
$\mathcal {D}$
and
$M_{f_{\mathcal {K}}(k)} \models _c \mathbf {HA}$
for all
$k \in K$
, we have
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \mathbf {HA}. $
For each
$m \in \{1,\ldots ,n\}$
, let
$B_m$
be a
$\Sigma _1$
-sentence such that
$$\begin{align*}\mathbf{HA} \vdash B_m \mathbin{\leftrightarrow} \bigvee_{i \in \{ [k]_{\mathcal{K}} \mid k \Vdash p_m \}} C_i. \end{align*}$$
Note that, by (1)–(3), we have
$ M_{i'} \models _c C_i \mathbin {\Leftrightarrow } i \leq _{\mathcal {K}} i' $
for all
$i, i' \in I_{\mathcal {K}}$
. Then, by (5) and Lemma 4.14, we have
$$ \begin{align*} {k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} B_m} & \mathbin{\Leftrightarrow} {\exists k' \in K ( k' \Vdash p_m \land k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} C_{[k']_{\mathcal{K}}} )} \\ & \mathbin{\Leftrightarrow} {\exists k' \in K ( k' \Vdash p_m \land M_{[k]_{\mathcal{K}}} \models_c C_{[k']_{\mathcal{K}}} )} \\ & \mathbin{\Leftrightarrow} {\exists k' \in K ( k' \Vdash p_m \land [k']_{\mathcal{K}} \leq_{\mathcal{K}} [k]_{\mathcal{K}} )} \mathbin{\Leftrightarrow} {k \Vdash p_m} \end{align*} $$
for all
$k \in K$
and
$m \in \{1,\ldots ,n\}$
. By Lemma 3.9, we have
$$\begin{align*}\mathcal{K}_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \not\Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \varphi[B_1,\ldots,B_n].\\[-37pt] \end{align*}$$
Now, we arrive at a separation theorem for
$\mathbf {HA}$
.
Theorem 4.17. Let
$\mathcal {K} = (K,\leq ,\Vdash )$
be a finite IPC-Kripke model such that
$(I_{\mathcal {K}},\leq _{\mathcal {K}})$
is a rooted
$($
and finite
$)$
tree, and let
$\varphi $
be a formula of
$\mathcal {L}(\mathbf {IPC})$
. If
$\mathcal {K} \not \Vdash \varphi $
and
$\mathcal {E}_{\mathcal {K}}$
is locally directed, then
$$\begin{align*}\mathbf{HA} + L(K,\leq)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}}) \not\vdash \Sigma_1\text{-}\varphi. \end{align*}$$
Proof Straightforward by Proposition 3.10, Proposition 3.14, Proposition 4.16, and the soundness theorem [Reference Troelstra and van Dalen33, Chapter 2, Section 5.10].
Example 4.18. By applying Theorem 4.17 to Example 2.10, we have
$$\begin{align*}\mathbf{HA} + L({K}_1,\leq_1)^\ast \not\vdash \Sigma_1\text{-}\mathrm{DNE} , \end{align*}$$
especially
$ \mathbf {HA} + \mathrm {WPEM}^\ast \not \vdash \Sigma _1\text {-}\mathrm {DNE}; $
to Example 2.11, we have
$$\begin{align*}\mathbf{HA} + L({K}_2,\leq_2)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_2}) \not\vdash \Sigma_1\text{-}\mathrm{WPEM} , \end{align*}$$
especially
$ \mathbf {HA} + \Sigma \text {-}\mathrm {DML} + \Sigma \text {-}\mathrm {DNE} \not \vdash \Sigma _1\text {-}\mathrm {WPEM}; $
to Example 2.12, we have
$$\begin{align*}\mathbf{HA} + L({K}_3,\leq_3)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_3}) \not\vdash \Sigma_1\text{-}\mathrm{DML} , \end{align*}$$
especially
$ \mathbf {HA} + \Sigma \text {-}\mathrm {DNE} \not \vdash \Sigma _1\text {-}\mathrm {DML}; $
to Example 2.13, we have
$$\begin{align*}\mathbf{HA} + L({K}_4,\leq_4)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_4}) \not\vdash \Sigma_1\text{-}\mathrm{WDML} , \end{align*}$$
especially
$ \mathbf {HA} + \Sigma \text {-}\mathrm {RPEM} \not \vdash \Sigma _1\text {-}\mathrm {WDML}; $
to Example 2.14, we have
$$\begin{align*}\mathbf{HA} + L({K}_2,\leq_2)^\ast \not\vdash \Sigma_1\text{-}\mathrm{RPEM}. \end{align*}$$
Note that
$\Sigma _1\mbox {-}\mathrm {DNE}$
,
$\Sigma _1\mbox {-}\mathrm {WPEM}$
,
$\Sigma _1\mbox {-}\mathrm {DML}$
,
$\Sigma _1\mbox {-}\mathrm {WDML}$
, and
$\Sigma _1\mbox {-}\mathrm {RPEM}$
correspond to
$\mathrm {MP}_{\mathrm {PR}}$
,
$\mathrm {WLPO}_{\mathrm {PR}}$
,
$\mathrm {LLPO}_{\mathrm {PR}}$
,
$\mathrm {MP}^\lor _{\mathrm {PR}}$
, and
$\Delta _1\mbox {-}\mathrm {PEM}_{\mathrm {PR}}$
, respectively.
Remark 4.19.
$\Sigma \text {-}\mathrm {DNE}$
(respectively,
$\Sigma \text {-}\mathrm {WPEM}$
,
$\Sigma \text {-}\mathrm {DML}$
,
$\Sigma \text {-}\mathrm {WDML}$
, and
$\Sigma \text {-}\mathrm {RPEM}$
) is stronger than
$\Sigma _1\text {-}\mathrm {DNE}$
(respectively,
$\Sigma _1\text {-}\mathrm {WPEM}$
,
$\Sigma _1\text {-}\mathrm {DML}$
,
$\Sigma _1\text {-}\mathrm {WDML}$
, and
$\Sigma _1\text {-}\mathrm {RPEM}$
) in
$\mathbf {HA}$
, and they are equivalent in many-sorted extensions of
$\mathbf {HA}$
with countable choice.
Figure 9 summarizes derivabilities among the omniscience principles in the introduction from which derivability between any pair of principles follows.
Figure 9 Derivabilities and underivabilities between omniscience principles.
We conclude the paper with discussing a possible relativization of the previous results and lifting Theorem 4.17 up to
$\Sigma _{n}$
-level.
Let
$\mathcal {L}_1^{Q}$
be an extension of
$\mathcal {L}_1$
by adding a unary predicate symbol Q.
$\Sigma ^{Q}_{0}$
- and
$\Sigma ^{Q}_{1}$
-formulae are similarly defined with extra atomic formulae of the form “
$Q(t)$
.”
$\mathbf {HA}^{*}$
denotes the set of
$\mathcal {L}_{1}^{Q}$
-sentences consisting of axioms and instances of the axiom schema of
$\mathbf {HA}$
. An
$\mathcal {L}_{1}^{Q}$
-structure is a pair
$(M,Q^{M})$
where M is an
$\mathcal {L}_{1}$
-structure and
$Q^{M}$
is an interpretation of Q on M.
For a set
$Q_0$
of natural numbers, we let
$$\begin{align*}\mathbf{HA}^{Q_{0}} = \mathbf{HA}^{*} \cup \{Q(\bar{n})\mid n\in Q_{0}\} \cup \{\neg Q(\bar{n})\mid n\notin Q_{0} \}. \end{align*}$$
Note that
$\mathbf {HA}^{Q_{0}}$
is
$\Sigma _{1}^{Q}$
-complete for
$(\omega ,Q_{0})$
, in other words,
$\mathbf {HA}^{Q_{0}}\vdash _{c}A$
if and only if
$(\omega ,Q_{0})\models _{c}A$
for all
$\Sigma _{1}^{Q}$
-sentence A. Consider a
$\Sigma _{1}^{Q}$
-formula
$\tau _{\mathbf {HA}}^{Q}(x)$
denoting
$$ \begin{align*} &"x\text{ is (a Gödel number of) an }\mathcal{L}_{1}^{Q}\text{-sentence"}\\ &\, \wedge[{"x\text{ is an axiom or an }\mathcal{L}_{1}^{Q}\text{-instance of the axiom schema of }\mathbf{HA}\text{"}}\\ &\, \quad\quad \vee \exists y("x\text{ is }Q(\bar y)"\wedge Q(y))\vee \exists y("x\text{ is }\neg Q(\bar y)"\wedge \neg Q(y))].\\ &\text{(Here, }\bar y\text{ denotes }y\text{-th numeral as in Remark 7.)} \end{align*} $$
Then,
$\tau _{\mathbf {HA}}^{Q}$
(uniformly) represents
$\mathbf {HA}^{Q_{0}}$
over
$\mathbf {HA}^{Q_{0}}$
in the sense that
$A\in \mathbf {HA}^{Q_{0}}$
if and only if
$\mathbf {HA}^{Q_{0}}\vdash _{c}\tau _{\mathbf {HA}}^{Q}(\lceil A\rceil )$
for all
$\mathcal {L}_{1}^{Q}$
-sentence A.
Definition 4.20. Let
$Q_{0}\subseteq \omega $
, and let T be a set of
$\mathcal {L}_1^{Q}$
-sentences. Then a
$\Sigma _{1}^{Q}$
-representation over
$Q_{0}$
of T is a
$\Sigma _{1}^{Q}$
-formula
$\tau (x)$
such that
$$ \begin{gather*} \mathbf{HA}^{*}\vdash_{c}\forall x[(\tau(x)\to "x\text{ is a sentence"})\wedge(\tau_{\mathbf{HA}}^{Q}(x)\to\tau(x))] , \text{ and} \\ A\in T\text{ if and only if }\mathbf{HA}^{Q_{0}}\vdash_{c}\tau(\lceil A\rceil)\text{ (or equivalently }(\omega,Q_{0})\models_{c}\tau(\lceil A\rceil)) \end{gather*} $$
for all
$\mathcal {L}_{1}^{Q}$
-sentence A. A set of
$\mathcal {L}_{1}^{Q}$
-sentences T is well-behaved over
$Q_{0}$
if T has a
$\Sigma _{1}^{Q}$
-representation over
$Q_{0}$
and
$\mathbf {HA}^{Q_{0}}\subseteq T\subseteq \mathrm {Th}(\omega ,Q_{0})$
. We then identify T (
$\supseteq \mathbf {HA}^{*}$
) with its
$\Sigma _{1}^{Q}$
-representation. Note that the condition
$T\subseteq \mathrm {Th}(\omega ,Q_{0})$
implies
$(\omega ,Q_{0})\models \mathrm {Con}(T)$
.
As same as the usual relativization in computability theory, the discussions and proofs in this section remain valid with the new predicate Q and its interpretation
$Q_{0}$
. In other words, for the extended language
$\mathcal {L}_{1}^{Q}$
, the arithmetized completeness theorem (Theorem 4.5), and its applications, Lemma 4.8, Lemma 4.9, and Proposition 4.16 are all relativizable in the sense that they still hold if we replace
$\mathcal {L}_{1}$
,
$\Sigma _{n}$
,
$\mathbf {HA}$
, and well-behavedness by
$\mathcal {L}_{1}^{Q}$
,
$\Sigma _{n}^{Q}$
,
$\mathbf {HA}^{Q_0}$
, and well-behavedness over
$Q_{0}$
, respectively. (We will see the relativization of Theorem 4.5 in Appendix B.)
As a typical application of relativization, we consider the case that Q denotes the
$\Sigma _{n}$
-satisfaction predicate. Then, we have the following generalization of Proposition 4.16.
Definition 4.21. A
$\Sigma _{n}$
-satisfaction predicate is a
$\Sigma _{n}$
-formula
$\mathrm {Sat}_{n}(e,x)$
such that
$$\begin{align*}\mathbf{HA} \vdash_{c}\forall \vec x[A \leftrightarrow \mathrm{Sat}_{n}(\lceil A\rceil,\langle \vec{x} \rangle)] \end{align*}$$
for all
$\Sigma _{n}$
-formula A with the free variables
$\vec {x} = x_1,\ldots ,x_n$
, where
$\langle \vec {x} \rangle = \langle x_1,\ldots ,x_n \rangle $
(see, e.g., [Reference Hájek and Pudlák13, Chapter I, Section 2, 2.55–2.57] for the definition of
$\Sigma _{n}$
-satisfaction predicates).
Proposition 4.22. Let
$\mathcal {E}_{\mathcal {K}} = ((K,\leq ),f_{\mathcal {K}},(I_{\mathcal {K}},\leq _{\mathcal {K}}))$
be the extended frame generated by a finite IPC-Kripke model
$\mathcal {K} = (K,\leq ,\Vdash )$
such that
$(I_{\mathcal {K}},\leq _{\mathcal {K}})$
is a rooted
$($
and finite
$)$
tree, and let
$\varphi [p_1,\ldots ,p_m]$
be a formula of
$\mathcal {L}(\mathbf {IPC})$
. If
$ \mathcal {K} \not \Vdash \varphi , $
then for each n
$$\begin{align*}\mathcal{K}_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \mathbf{HA} +\Sigma_{n}\text{-}\mathrm{PEM} \quad\mbox{and}\quad \mathcal{K}_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \not\Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} \Sigma_{n+1}\mbox{-}\varphi \end{align*}$$
for some
$\mathcal {L}_1$
-Kripke model
$ \mathcal {I} = (I_{\mathcal {K}},\leq _{\mathcal {K}},M,\eta ,\Vdash '). $
Proof (sketch)
Let
$Q_{0}\subseteq \omega $
be given by
$$\begin{align*}Q_{0}=\{a\in\omega \mid \omega\models_{c}\exists e\exists x (a=\langle e,x\rangle\wedge \mathrm{Sat}_{n}(e,x))\} , \end{align*}$$
and define a set
$T^{\mathrm {Sat}_{n}}$
of
$\mathcal {L}_{1}^{Q}$
-sentences by
$$\begin{align*}T^{\mathrm{Sat}_{n}} = \mathbf{HA}^{Q_{0}}\cup\{\forall y[Q(y)\leftrightarrow\exists e\exists x (y=\langle e,x\rangle\wedge \mathrm{Sat}_{n}(e,x))]\}. \end{align*}$$
Then
$T^{\mathrm {Sat}_{n}}$
is well-behaved over
$Q_{0}$
. We follow the proof of Proposition 4.16. Let
$i_0 \in I_{\mathcal {K}}$
be the root of the finite tree
$(I_{\mathcal {K}},\leq _{\mathcal {K}})$
. Then, by (the relativization of) Lemma 4.9 with
$T_{0}=T^{\mathrm {Sat}_{n}}$
, there exists a set T of
$\mathcal {L}_1^Q$
-sentences well-behaved over
$Q_0$
such that for each
$\Sigma _1^Q$
-sentence
$C_{i_0}$
and
$\mathcal {L}_1^Q$
-structure
$(M_{i_0},Q^{M_{i_0}})$
, if
$$\begin{align*}(M_{i_0},Q^{M_{i_0}}) \models_c T + C_{i_0} , \end{align*}$$
there exist an
$\mathcal {L}_1^Q$
-Kripke model
$(I_{\mathcal {K}},\leq _{\mathcal {K}},\{(M_i,Q^{M_i})\mid i \in I_{\mathcal {K}}\},\eta ,\Vdash ')$
and a family
$\{ C_i \mid i \in I_{\mathcal {K}} \}$
of
$\Sigma _1^Q$
-sentences satisfying that for each
$i \in I$
, (1)–(5) of (the relativization of) Lemma 4.9. Let
$(M_{i_0},Q^{M_{i_0}})$
be a model of T, and let
$C_{i_0} \equiv 0 = 0$
. Then
$ (M_{i_0},Q^{M_{i_0}}) \models _c T + C_{i_0} , $
and hence there exist an
$\mathcal {L}_1^Q$
-Kripke model
$\mathcal {I} = (I_{\mathcal {K}},\leq _{\mathcal {K}},\{(M_i,Q^{M_i})\mid i \in I_{\mathcal {K}}\},\eta ,\Vdash ')$
and a family
$\{ C_i \mid i \in I_{\mathcal {K}} \}$
of
$\Sigma _1^Q$
-sentences satisfying that (1)–(5) for all
$i \in I_{\mathcal {K}}$
.
Let
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}}) $
be the induced
$\mathcal {L}_1^Q$
-Kripke model by
$\mathcal {I}$
. Then, similar to the proof of Proposition 4.16, we have
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \mathbf {HA}. $
Moreover, for each
$\Sigma _n$
-formula B with the free variables
$\vec {x}$
, since
$$\begin{align*}M_i \models_c B[\vec{x}/\vec{a}] \mathbin{\Leftrightarrow} (M_i,Q^{M_i}) \models_c Q(\langle \lceil B \rceil, \langle \vec{a} \rangle \rangle) \end{align*}$$
for all
$i \in I$
, by the
$\Sigma _0^Q$
-elementarity of
$\eta _{i j}$
, we have
$$\begin{align*}M_i \models_c B[\vec{x}/\vec{a}] \mathbin{\Leftrightarrow} M_j \models_c B[\vec{x}/\eta_{i j}(\vec{a})] \end{align*}$$
for all
$i,j \in I_{\mathcal {K}}$
with
$i \leq _{\mathcal {K}} j$
. Therefore for each
$k \in K$
,
$\Sigma _n$
-formula B with the free variables
$\vec {x}$
and
$\vec {a} \in M_{f_{\mathcal {K}}(k)}$
, by Lemma 4.14, we have
$$ \begin{align*} {k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} B[\vec{x}/\vec{a}]} & \mathbin{\Leftrightarrow} M_{f_{\mathcal{K}}(k)} \models_c B[\vec{x}/\vec{a}] \\ & \mathbin{\Leftrightarrow} M_{f_{\mathcal{K}}(k')} \models_c B[\vec{x}/\eta_{f_{\mathcal{K}}(k) f_{\mathcal{K}}(k')}(\vec{a})] \\ & \mathbin{\Leftrightarrow} {k' \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} B[\vec{x}/\eta_{f_{\mathcal{K}}(k)f_{\mathcal{K}}(k')}(\vec{a})]} \end{align*} $$
for all
$k' \in K$
with
$k \leq k'$
. In particular, if
$k \not \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} B[\vec {x}/\vec {a}]$
, then
$k \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \lnot B[\vec {x}/\vec {a}]$
. Thus
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \Sigma _n\text {-}\mathrm {PEM}. $
Finally, we show that there exist
$\Sigma _{n+1}$
-sentences
$B_1,\ldots ,B_n$
such that
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \not \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \varphi [B_1,\ldots ,B_n]. $
As in the proof of Proposition 4.16,
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \not \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \varphi [A_1,\ldots ,A_n] $
for some
$\Sigma ^{Q}_{1}$
-sentences
$A_1,\ldots ,A_n$
. Hence it suffices to show that for each
$\Sigma _1^Q$
-sentence A there exists a
$\Sigma _{n+1}$
-sentence B such that
$ \mathcal {K}_{\mathcal {E}_{\mathcal {K}},\mathcal {I}} \Vdash _{\mathcal {E}_{\mathcal {K}},\mathcal {I}} A \mathbin {\leftrightarrow } B. $
For each
$\Sigma _1^Q$
-sentence A, since
$Q(y)$
is equivalent to a
$\Sigma _{n}$
-formula
$ \exists e\exists x (y=\langle e,x\rangle \wedge \mathrm {Sat}_{n}(e,x)) $
over
$T^{\mathrm {Sat}_{n}}$
, there exists a
$\Sigma _{n+1}$
-sentence B such that
$ T^{\mathrm {Sat}_{n}} \vdash _c A \mathbin {\leftrightarrow } B. $
Therefore for each
$k\in K$
, since
$(M_{f_{\mathcal {K}}(k)},Q^{M_{f_{\mathcal {K}}(k)}}) \models _c T^{\mathrm {Sat}_{n}}$
, by Lemma 4.14, we have
$$ \begin{align*} k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} A &\mathbin{\Leftrightarrow} (M_{f_{\mathcal{K}}(k)},Q^{M_{f_{\mathcal{K}}(k)}}) \models_c A \\ &\mathbin{\Leftrightarrow} (M_{f_{\mathcal{K}}(k)},Q^{M_{f_{\mathcal{K}}(k)}}) \models_c B \mathbin{\Leftrightarrow} k \Vdash_{\mathcal{E}_{\mathcal{K}},\mathcal{I}} B.\\[-37pt] \end{align*} $$
Theorem 4.23. Let
$\mathcal {K} = (K,\leq ,\Vdash )$
be a finite IPC-Kripke model such that
$(I_{\mathcal {K}},\leq _{\mathcal {K}})$
is a rooted
$($
and finite
$)$
tree, and let
$\varphi $
be a formula of
$\mathcal {L}(\mathbf {IPC})$
. If
$\mathcal {K} \not \Vdash \varphi $
and
$\mathcal {E}_{\mathcal {K}}$
is locally directed, then for each n
$$\begin{align*}\mathbf{HA} + \Sigma_{n}\text{-}\mathrm{PEM} + L(K,\leq)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}}) \not\vdash \Sigma_{n+1}\text{-}\varphi. \end{align*}$$
Example 4.24. By applying Theorem 4.23 to Example 2.10 with
$n\ge 0$
, we have
$$\begin{align*}\mathbf{HA} + \Sigma_{n}\text{-}\mathrm{PEM} + L({K}_1,\leq_1)^\ast \not\vdash \Sigma_{n+1}\text{-}\mathrm{DNE} , \end{align*}$$
especially
$ \mathbf {HA} + \Sigma _{n}\text {-}\mathrm {PEM} + \mathrm {WPEM}^\ast \not \vdash \Sigma _{n+1}\text {-}\mathrm {DNE}; $
to Example 2.11, we have
$$\begin{align*}\mathbf{HA} + \Sigma_{n}\text{-}\mathrm{PEM} + L({K}_2,\leq_2)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_2}) \not\vdash \Sigma_{n+1}\text{-}\mathrm{WPEM} , \end{align*}$$
especially
$ \mathbf {HA} + \Sigma _{n}\text {-}\mathrm {PEM} + \Sigma \text {-}\mathrm {DML} + \Sigma \text {-}\mathrm {DNE} \not \vdash \Sigma _{n+1}\text {-}\mathrm {WPEM}; $
to Example 2.12, we have
$$\begin{align*}\mathbf{HA} + \Sigma_{n}\text{-}\mathrm{PEM} + L({K}_3,\leq_3)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_3}) \not\vdash \Sigma_{n+1}\text{-}\mathrm{DML} , \end{align*}$$
especially
$ \mathbf {HA} + \Sigma _{n}\text {-}\mathrm {PEM} + \Sigma \text {-}\mathrm {DNE} \not \vdash \Sigma _{n+1}\text {-}\mathrm {DML}; $
to Example 2.13, we have
$$\begin{align*}\mathbf{HA} + \Sigma_{n}\text{-}\mathrm{PEM} + L({K}_4,\leq_4)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_4}) \not\vdash \Sigma_{n+1}\text{-}\mathrm{WDML} , \end{align*}$$
especially
$ \mathbf {HA} + \Sigma _{n}\text {-}\mathrm {PEM} + \Sigma \text {-}\mathrm {RPEM} \not \vdash \Sigma _{n+1}\text {-}\mathrm {WDML}; $
to Example 2.14, we have
$$\begin{align*}\mathbf{HA} + \Sigma_{n}\text{-}\mathrm{PEM} + L({K}_2,\leq_2)^\ast \not\vdash \Sigma_{n+1}\text{-}\mathrm{RPEM}. \end{align*}$$
Note that
$\Sigma \text {-}\mathrm {DNE}$
(respectively,
$\Sigma \text {-}\mathrm {WPEM}$
,
$\Sigma \text {-}\mathrm {DML}$
,
$\Sigma \text {-}\mathrm {WDML}$
, and
$\Sigma \text {-}\mathrm {RPEM}$
) implies
$\Sigma _{n+1}\text {-}\mathrm {DNE}$
(respectively,
$\Sigma _{n+1}\text {-}\mathrm {WPEM}$
,
$\Sigma _{n+1}\text {-}\mathrm {DML}$
,
$\Sigma _{n+1}\text {-}\mathrm {WDML}$
, and
$\Sigma _{n+1}\text {-}\mathrm {RPEM}$
) in
$\mathbf {HA}+\Sigma _{n}\text {-}\mathrm {PEM}$
.
5 Concluding remarks
In this paper, we have developed a general technique to separate omniscience principles over
$\mathbf {HA}$
by constructing a Kripke model of
$\mathbf {HA}$
from an IPC-Kripke model. Example 4.24 shows that all the separation results in [Reference Akama, Berardi, Hayashi, Kohlenbach and Ganzinger1] obtained by using several different kinds of functional interpretations can be proved uniformly by applying Theorem 4.23 to simple IPC-Kripke models; for some further separation results among weaker principles by using Theorem 4.17, see [Reference Fujiwara8].
On the other hand, our technique is not totally universal. According to the recent study of the hierarchical structure of the logical principles restricted to prenex formulae (including the principles studied in [Reference Akama, Berardi, Hayashi, Kohlenbach and Ganzinger1, Reference Fujiwara8, Reference Fujiwara, Ishihara and Nemoto9]) by Fujiwara and Kurahashi [Reference Fujiwara and Kurahashi11], some principles in the
$(n+1)$
-th hierarchy are mutually equivalent in the presence of
$\mathrm {DNE}$
or the double negation shift (
$\mathrm {DNS}$
):
$$\begin{align*}\forall x \lnot \lnot \nu(x) \to \lnot \lnot \forall x \nu(x), \end{align*}$$
in the n-th hierarchy. For example,
$\Sigma _{n+1}$
-
$\mathrm {DML}$
is equivalent to
$(\Pi _{n+1} \lor \Pi _{n+1})$
-
$\mathrm {DNE}$
in the presence of
$\Sigma _{n}$
-
$\mathrm {DNE}$
, but it is still open whether
$\Sigma _{n+1}$
-
$\mathrm {DML}$
implies
$(\Pi _{n+1} \lor \Pi _{n+1})$
-
$\mathrm {DNE}$
over
$\mathbf {HA}$
(cf. [Reference Fujiwara and Kurahashi11, Figure 3]). Since the relativized theory already contains
$\Sigma _{n}$
-
$\mathrm {PEM}$
(which is stronger than
$\Sigma _{n}$
-
$\mathrm {DNE}$
and
$\Sigma _{n}$
-
$\mathrm {DNS}$
), our Theorem 4.23 does not provide separations of equivalent principles, such as
$\Sigma _{n+1}$
-
$\mathrm {DML}$
and
$(\Pi _{n+1} \lor \Pi _{n+1})$
-
$\mathrm {DNE}$
, in the presence of
$\Sigma _{n}$
-
$\mathrm {PEM}$
.
Furthermore, our technique is available only for a separation of logical principles which are obtained from those in propositional logic by substituting propositional variables by predicate formulae, and therefore the fragments of
$\mathrm {DNS}$
(investigated in [Reference Fujiwara and Kohlenbach10]) are outside of the range of our technique.
It is also remarkable that separation of two propositional theories by an IPC-Kripke model does not necessarily induce a separation of their
$\Sigma _1$
-substitution instances in
$\mathbf {HA}$
. Consider the following propositional formulae:
$$ \begin{align*} \mathrm{LIN}[p,q] & \equiv (p\to q ) \lor (q \to p) ,\\ \mathrm{LIN}'[p,q] & \equiv (p\to \lnot q ) \lor (\lnot q \to p). \end{align*} $$
Example 5.1. We show the following.
-
1.
$ \mathrm {LIN}' \not \vdash _{\mathbf {IPC}} \mathrm {LIN};$
-
2.
$ \Sigma \text {-}\mathrm {LIN}' \nvdash _{\mathbf {IQC}} \Sigma \text {-}\mathrm {LIN};$
-
3.
$\mathbf {HA}+\Sigma _1\text {-}\mathrm {LIN}' \vdash \Sigma _1\text {-}\mathrm {LIN}.$
For (1) and (2), consider an IPC-Kripke model
$\mathcal {K}_6 = (K_6,\leq _6,\Vdash _6)$
given in Figure 10. Then
$\mathcal {K}_6 \not \Vdash _6 \mathrm {LIN}[p,q] $
. On the other hand,
$\mathrm {LIN}'$
is valid on the Kripke frame
$(K_6,\leq _6)$
. Therefore we have
$\mathrm {LIN}' \nvdash _{\mathbf {IPC}} \mathrm {LIN}$
. Furthermore, since the extended frame
$\mathcal {E}_{\mathcal {K}_6}$
generated by
$\mathcal {K}_6$
is locally directed (cf. Figure 10), we have
$$\begin{align*}L({K}_6,\leq_6)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_6}) \not\vdash_{\mathbf{IQC}} \Sigma\text{-}\mathrm{LIN} , \end{align*}$$
by Theorem 3.15. Since
$T(\mathcal {E}_{\mathcal {K}_6}) $
contains
$\mathrm {LIN'}[p,q]$
for all p and q, we have
$ \Sigma \text {-}\mathrm {LIN}' \nvdash _{\mathbf {IQC}} \Sigma \text {-}\mathrm {LIN}$
. Note that the Kripke frame
$(I_{\mathcal {K}_6}, \leq _{\mathcal {K}_6})$
generated by
$\mathcal {K}_6$
is not a tree, and Theorem 4.17 is not applicable.
Figure 10 The Kripke model and the extended frame in Example 5.1.
For (3), first note that, since an instance
$$\begin{align*}(p \mathbin{\rightarrow} \lnot p) \lor (\lnot p \mathbin{\rightarrow} p) \end{align*}$$
of
$\mathrm {LIN}'$
is equivalent to
$\mathrm {WPEM}[p]$
,
$\Sigma _1\text {-}\mathrm {LIN}'$
implies
$\Sigma _1\text {-}\mathrm {WPEM}$
. Assume that
$\Sigma _1\text {-}\mathrm {LIN}'$
. Then to show
$\Sigma _1\text {-}\mathrm {LIN}$
in
$\mathbf {HA}$
, it suffices to prove that
$$\begin{align*}(\exists x \,(s(x) = 0) \to \exists x \,(t(x) = 0)) \lor (\exists x \,(t(x) = 0) \to \exists x \,(s(x) = 0)) , \end{align*}$$
where s and t are (primitive recursive) terms of
$\mathbf {HA}$
. Consider terms s and t of
$\mathbf {HA}$
, and let
$A(x)$
and
$B(x)$
be the following formulae:
$$\begin{align*}\begin{array}{rl} A(x) \equiv & s(x)=0 \land \forall y \leq x\, (t(y) \neq 0),\\ B(x) \equiv & t(x)=0 \land \forall y \leq x \, (s(y) \neq 0). \end{array} \end{align*}$$
Then
$$\begin{align*}\mathbf{HA} \vdash \neg (\exists x A(x) \land \exists x B(x)). \end{align*}$$
Since
$\neg \exists x A(x) \lor \neg \neg \exists x A(x)$
and
$\neg \exists x B(x) \lor \neg \neg \exists x B(x)$
, by
$\Sigma _{1}\text {-}\mathrm {WPEM}$
, we have
$$\begin{align*}\neg \exists x A(x) \lor \neg \exists x B(x). \end{align*}$$
In the former case, if
$s(x)=0$
, then
$\neg \forall y \leq x \, (t(y) \neq 0)$
, that is,
$$\begin{align*}\exists y \leq x \, (t(y)=0); \end{align*}$$
hence
$\exists x \, (s(x) = 0) \to \exists x \, (t(x) = 0)$
. In the latter case, similarly we have
$\exists x \, (t(x) = 0) \to \exists x \, (s(x) = 0)$
.
Interestingly, our technique can be applied even to an IPC-Kripke model, which does not separate propositional principles, for separating their substitution instances in
$\mathbf {IQC}$
or
$\mathbf {HA}$
.
Example 5.2. We show the following.
-
1.
$ \mathrm {LIN} \vdash _{\mathbf {IPC}} \mathrm {LIN}';$
-
2.
$\Sigma \text {-}\mathrm {LIN} \nvdash _{\mathbf {IQC}} \Sigma \text {-}\mathrm {LIN}';$
-
3.
$\mathbf {HA}+\Sigma _1\text {-}\mathrm {LIN} \nvdash \Sigma _1\text {-}\mathrm {LIN}'.$
Note that, since
$\mathrm {LIN}'[p,q]$
is an instance of
$\mathrm {LIN}[p,q]$
, (1) is trivial.
For (2), let
$\mathcal {E}_{\mathcal {K}_7} = ((K_2,\leq _2),f_{\mathcal {K}_7},(I_{\mathcal {K}_7},\leq _{\mathcal {K}_7}))$
be the extended frame generated by the IPC-Kripke model
$\mathcal {K}_7 = (K_2,\leq _2,\Vdash _7)$
given in Figure 11, where
$(K_2,\leq _2)$
is the Kripke frame in Example 2.11. Then it is easy to see
$ \mathcal {K}_7 \not \Vdash _7 \mathrm {LIN'}[p,q] $
. Since the extended frame
$\mathcal {E}_{\mathcal {K}_7}$
is identical with
$\mathcal {E}_{\mathcal {K}_2}$
, which is locally directed, we have
$$\begin{align*}L({K}_2,\leq_2)^\ast + \Sigma\text{-}T(\mathcal{E}_{\mathcal{K}_7}) \not\vdash_{\mathbf{IQC}} \Sigma\text{-}\mathrm{LIN}' , \end{align*}$$
by Theorem 3.15. To prove that
$\Sigma \text {-}\mathrm {LIN} \nvdash _{\mathbf {IQC}} \Sigma \text {-}\mathrm {LIN}'$
, it suffices to show that
$T(\mathcal {E}_{\mathcal {K}_7})$
contains
$\mathrm {LIN}[p,q]$
for all p and q. Consider an IPC-Kripke model
$\mathcal {I} = (I_{\mathcal {K}_7},\leq _{\mathcal {K}_7},\Vdash ')$
.
Figure 11 The Kripke model and the extended frame in Example 5.2.
Then either
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} p$
,
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} q$
or
$0 \not \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} p, \,q$
. In the first and second cases, we have
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} q\to p$
and
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} p\to q$
, respectively. In the third case, either
$1 \not \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} p$
,
$1 \not \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} q$
or
$1 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} p, q$
; in the first and second cases, since
$2 \not \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} p, \,q$
, we have
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} p\to q$
and
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} q\to p$
, respectively; in the third case, we have
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} p\to q,\, q\to p$
. Therefore, in any case, we have
$0 \Vdash _{\mathcal {E}_{\mathcal {K}_7},\mathcal {I}} (p\to q) \lor (q\to p)$
.
For (3), since
$(I_{\mathcal {K}_7},\leq _{\mathcal {K}_7})$
is a rooted tree, applying Theorem 4.17, we have
$\mathbf {HA} + \Sigma _1\text {-}\mathrm {LIN} \nvdash \Sigma _1\text {-}\mathrm {LIN'}$
.
To conclude the paper, we briefly examine the following assumptions on a Kripke model
$\mathcal {K}=(K, \leq , \Vdash )$
in Theorem 4.17 and Theorem 4.23, respectively:
-
1. The Kripke frame
$(I_{\mathcal {K}}, \leq _{\mathcal {K}})$
generated by
$\mathcal {K}$
is a rooted finite tree. -
2. The extended frame
$\mathcal {E_K}$
generated by
$\mathcal {K}$
is locally directed.
The first and second assumptions are crucial for our constructions of Kripke models of
$\mathbf {HA}$
in Proposition 4.16 and of IQC-Kripke models in Lemma 3.13, respectively. Although, as we have seen in Examples 2.10–2.14 and 5.2, many useful IPC-Kripke models enjoy these assumptions, we cannot remove the first assumption from Theorem 4.17. In fact, if we omitted it in Theorem 4.17, since the locally directed extended frame
$\mathcal {E}_{\mathcal {K}_6}$
in Example 5.1 separates
$\mathrm {LIN}$
from
$\mathrm {LIN}'$
, we could have
$$\begin{align*}\mathbf{HA} + \Sigma_1\text{-}\mathrm{LIN}' \not\vdash \Sigma_1\text{-}\mathrm{LIN} , \end{align*}$$
which contradicts Example 5.1(3). Note that the Kripke frame
$(I_{\mathcal {K}_6}, \leq _{\mathcal {K}_6})$
generated by
$\mathcal {K}_6$
has a confluent point, and is not a tree. On the other hand, we still do not know whether the second assumption is essential or not for Theorem 4.17.
Appendix A. Proofs of Lemmas 4.11 and 4.14.
Lemma A.1. Let
$\mathcal {E} = ((K,\leq ),f,(I,\leq _I))$
be an extended frame such that
$(K,\leq )$
is finite, and let
$\mathcal {K}_{\mathcal {E},\mathcal {I}} = (K,\leq ,D,\epsilon ,\Vdash _{\mathcal {E},\mathcal {I}})$
be the induced IQC-Kripke model by an IQC-Kripke model
$\mathcal {I} = (I,\leq _I,M,\eta ,\Vdash )$
. Assume that for each
$i, i' \in I$
with
$i \leq i'$
and formula B, there exists a formula
$[B]^{i'}_{i}$
such that
$\mathrm {FV}([B]_{i}^{i'}) = \mathrm {FV}(B)$
and
$$\begin{align*}M_{i} \models_c [B]_{i}^{i'}[\vec{x}/\vec{a}] \mathbin{\Leftrightarrow} M_{i'} \models_c B[\vec{x}/\eta_{i i'}(\vec{a})] \end{align*}$$
for all
$\vec {a} \in M_{i}$
, where
$\vec {x}$
are the free variables of B. Then for each
$k\in K$
and formula A, there exists a formula
$\hat {A}_{k}$
such that
$\mathrm {FV}(\hat {A}_k) = \mathrm {FV}(A)$
and
$$\begin{align*}k \Vdash_{\mathcal{E},\mathcal{I}} A[\vec{x}/\vec{a}] \mathbin{\Leftrightarrow} D_{k} \models_c \hat{A}_{k}[\vec{x}/\vec{a}] \end{align*}$$
for all
$\vec {a} \in D_{k}$
, where
$\vec {x}$
are the free variables of A.
Proof Given a
$k \in K$
, define
$\hat {A}_{k}$
by induction on the complexity of a formula A as follows:
-
•
$ \hat {A}_{k} \equiv A $
for A prime; -
•
$ \hat {A}_{k} \equiv \hat {B}_{k} \land \hat {C}_{k} $
for
$A \equiv B \land C$
; -
•
$ \hat {A}_{k} \equiv \hat {B}_{k} \lor \hat {C}_{k} $
for
$A \equiv B \lor C$
; -
•
$ \hat {A}_{k} \equiv \bigwedge _{k' \geq k}([\hat {B}_{k'} \mathbin {\rightarrow } \hat {C}_{k'}]^{f(k')}_{f(k)}) $
for
$A \equiv B \mathbin {\rightarrow } C$
; -
•
$ \hat {A}_{k} \equiv \exists y \hat {B}_{k} $
for
$A \equiv \exists y B$
; -
•
$ \hat {A}_{k} \equiv \bigwedge _{k' \geq k}([\forall y \hat {B}_{k'}]^{f(k')}_{f(k)}) $
for
$A \equiv \forall y B$
.
Then it is straightforward to show that
$$\begin{align*}k \Vdash_{\mathcal{E},\mathcal{I}} A[\vec{x}/\vec{a}] \mathbin{\Leftrightarrow} D_{k} \models_c \hat{A}_{k}[\vec{x}/\vec{a}] , \end{align*}$$
for all
$k \in K$
and
$\vec {a} \in D_k$
, by induction on the complexity of A except the cases for
$\mathbin {\rightarrow }$
and
$\forall $
. For
$\mathbin {\rightarrow }$
, we have
$$ \begin{align*} k \Vdash_{\mathcal{E},\mathcal{I}} A[\vec{x}/\vec{a}] & \mathbin{\Leftrightarrow} \forall k' \geq k (k' \Vdash_{\mathcal{E},\mathcal{I}} B[\vec{x}/\epsilon_{k k'}(\vec{a})] \mathbin{\Rightarrow} k' \Vdash_{\mathcal{E},\mathcal{I}} C[\vec{x}/\epsilon_{k k'}(\vec{a})]) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k (D_{k'} \models_c \hat{B}_{k'}[\vec{x}/\epsilon_{k k'}(\vec{a})] \mathbin{\Rightarrow} D_{k'} \models_c \hat{C}_{k'}[\vec{x}/\epsilon_{k k'}(\vec{a})]) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k (D_{k'} \models_c (\hat{B}_{k'} \mathbin{\rightarrow} \hat{C}_{k'})[\vec{x}/\epsilon_{k k'}(\vec{a})]) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k (M_{f(k')} \models_c (\hat{B}_{k'} \mathbin{\rightarrow} \hat{C}_{k'})[\vec{x}/\eta_{f(k) f(k')}(\vec{a})]) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k (M_{f(k)} \models_c [\hat{B}_{k'} \mathbin{\rightarrow} \hat{C}_{k'}]^{f(k')}_{f(k)}[\vec{x}/\vec{a}]) \\ & \mathbin{\Leftrightarrow} M_{f(k)} \models_c \left( \bigwedge_{k' \geq k} [\hat{B}_{k'} \mathbin{\rightarrow} \hat{C}_{k'}]^{f(k')}_{f(k)} \right)[\vec{x}/\vec{a}] \\ & \mathbin{\Leftrightarrow} D_{k} \models_c \hat{A}_k[\vec{x}/\vec{a}] , \end{align*} $$
for all
$\vec {a} \in D_{k}$
. For
$\forall $
, we have
$$ \begin{align*} k \Vdash_{\mathcal{E},\mathcal{I}} A[\vec{x}/\vec{a}] & \mathbin{\Leftrightarrow} \forall k' \geq k \forall b \in D_{k'} (k' \Vdash_{\mathcal{E},\mathcal{I}} B[\vec{x},y/\epsilon_{k k'}(\vec{a}),b]) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k \forall b \in D_{k'} (D_{k'} \models_c \hat{B}_{k'}[\vec{x},y/\epsilon_{k k'}(\vec{a}),b]) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k (D_{k'} \models_c (\forall y \hat{B}_{k'})[\vec{x}/\epsilon_{k k'}(\vec{a})]) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k (M_{f(k')} \models_c (\forall y \hat{B}_{k'})[\vec{x}/\eta_{f(k) f(k')}(\vec{a})]) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k (M_{f(k)} \models_c [\forall y \hat{B}_{k'}]^{f(k')}_{f(k)}[\vec{x}/\vec{a}])\\ & \mathbin{\Leftrightarrow} M_{f(k)} \models_c \left( \bigwedge_{k' \geq k} [\forall y \hat{B}_{k'}]^{f(k')}_{f(k)} \right)[\vec{x}/\vec{a}] \\ & \mathbin{\Leftrightarrow} D_{k} \models_c \hat{A}_{k}[\vec{x}/\vec{a}] , \end{align*} $$
for all
$a \in D_{k}$
.
Recall the definition of the classes
$\mathcal {A}$
,
$\mathcal {B}$
,
$\mathcal {C}$
, and
$\mathcal {D}$
of schemata in Definition 4.10.
Lemma A.2. Let
$\mathcal {K} = (K,\leq ,D,\Vdash ,\epsilon )$
be an IQC-Kripke model. Assume that for each
$k\in K$
and formula A, there exists a formula
$\hat {A}_{k}$
such that
$\mathrm {FV}(\hat {A}_k) = \mathrm {FV}(A)$
and
$$\begin{align*}k \Vdash A[\vec{x}/\vec{a}] \mathbin{\Leftrightarrow} D_{k} \models_c \hat{A}_{k}[\vec{x}/\vec{a}] \end{align*}$$
for all
$\vec {a} \in D_{k}$
, where
$\vec {x}$
are the free variables of A. Then for each formula
$A^1, \ldots , A^n$
,
$k \in K$
, and
$\vec {a} \in D_k$
,
-
1. if
$\alpha \in \mathcal {A}$
, then
$$\begin{align*}\kern-15pt\exists k' \geq k (k' \Vdash (\alpha[A^1,\ldots,A^n])[\vec{x}/\epsilon_{k k'}(\vec{a})]) \mathbin{\Rightarrow} D_{k} \models_c (\alpha[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}] , \end{align*}$$
-
2. if
$\beta \in \mathcal {B}$
, then
$$\begin{align*}k \Vdash (\beta[A^1,\ldots,A^n])[\vec{x}/\vec{a}] \mathbin{\Rightarrow} D_{k} \models_c (\beta[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}] , \end{align*}$$
-
3. if
$\gamma \in \mathcal {C}$
, then
$$\begin{align*}D_{k} \models_c (\gamma[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}] \mathbin{\Rightarrow} k \Vdash (\gamma[A^1,\ldots,A^n])[\vec{x}/\vec{a}] , \end{align*}$$
-
4. if
$\delta \in \mathcal {D}$
, then
$$\begin{align*}\kern-20pt\forall k' \geq k (D_{k'} \models_c (\delta[\hat{A}^1_{k'},\ldots,\hat{A}^n_{k'}])[\vec{x}/\epsilon_{k k'}(\vec{a})]) \mathbin{\Rightarrow} k \Vdash (\delta[A^1,\ldots,A^n])[\vec{x}/\vec{a}] , \end{align*}$$
where
$\vec {x}$
are the free variables of
$\alpha [A^1,\ldots ,A^n]$
$($
respectively,
$\beta [A^1,\ldots ,A^n]$
,
$\gamma [A^1,\ldots ,A^n]$
and
$\delta [A^1,\ldots ,A^n])$
.
Proof By simultaneous induction on
$\mathcal {A}$
,
$\mathcal {B}$
,
$\mathcal {C}$
, and
$\mathcal {D}$
.
Basis. It is straightforward using the assumption.
Induction step. Since the cases for the propositional operators
$\land $
and
$\lor $
, and the quantifier
$\exists $
are straightforward, we review the propositional operator
$\mathbin {\rightarrow }$
and the quantifier
$\forall $
.
Case 1:
$ \forall y \alpha \in \mathcal {A}. $
Suppose that
$ k' \Vdash ((\forall y \alpha )[A^1,\ldots ,A^n])[\vec {x}/\epsilon _{k k'}(\vec {a})] $
for some
$k' \geq k$
. Then, since
$ k' \Vdash (\forall y (\alpha [A^1,\ldots ,A^n]))[\vec {x}/\epsilon _{k k'}(\vec {a})] , $
we have
$ k' \Vdash (\alpha [A^1,\ldots ,A^n])[\vec {x},y/\epsilon _{k k'}(\vec {a}),c] $
for all
$c \in D_{k'}$
, and hence
$$\begin{align*}k' \Vdash (\alpha[A^1,\ldots,A^n])[\vec{x},y/\epsilon_{k k'}(\vec{a}),\epsilon_{k k'}(b)] \end{align*}$$
for all
$b \in D_{k}$
. By the induction hypothesis, we have
$ D_{k} \models _c (\alpha [\hat {A}^1_k,\ldots ,\hat {A}^n_k]) [\vec {x},y/\vec {a},b] $
for all
$b \in D_{k}$
, and so
$ D_{k} \models _c (\forall y (\alpha [\hat {A}^1_k,\ldots ,\hat {A}^n_k]))[\vec {x}/\vec {a}]. $
Thus
$ D_{k} \models _c ((\forall y \alpha )[\hat {A}^1_k,\ldots ,\hat {A}^n_k])[\vec {x}/\vec {a}]. $
Case 2:
$ \gamma \mathbin {\rightarrow } \alpha \in \mathcal {A}. $
Suppose that
$ k' \Vdash ((\gamma \mathbin {\rightarrow } \alpha )[A^1,\ldots ,A^n])[\vec {x}/\epsilon _{k k'}(\vec {a})] $
for some
$k' \geq k$
. Then
$$\begin{align*}k' \Vdash (\gamma[A^1,\ldots,A^n])[\vec{x}/\epsilon_{k k'}(\vec{a})] \mathbin{\rightarrow} (\alpha[A^1,\ldots,A^n])[\vec{x}/\epsilon_{k k'}(\vec{a})]. \end{align*}$$
Assume that
$ D_{k} \models _c (\gamma [\hat {A}^1_k,\ldots ,\hat {A}^n_k])[\vec {x}/\vec {a}]. $
By the induction hypothesis, we have
$ k \Vdash (\gamma [A^1,\ldots ,A^n])[\vec {x}/\vec {a}], $
and hence
$ k' \Vdash (\gamma [A^1,\ldots ,A^n])[\vec {x}/\epsilon _{k k'}(\vec {a})]. $
Therefore
$ k' \Vdash (\alpha [A^1,\ldots ,A^n])[\vec {x}/\epsilon _{k k'}(\vec {a})]. $
By the induction hypothesis, we have
$$\begin{align*}D_{k} \models_c (\alpha[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}]. \end{align*}$$
Thus
$ D_{k} \models _c ((\gamma \mathbin {\rightarrow } \alpha )[\hat {A}^1_k,\ldots ,\hat {A}^n_k])[\vec {x}/\vec {a}]. $
Case 3:
$ \forall y \beta \in \mathcal {B}. $
Suppose that
$ k \Vdash ((\forall y \beta )[A^1,\ldots ,A^n])[\vec {x}/\vec {a}]. $
Then, since
$ k \Vdash \forall y ((\beta [A^1,\ldots ,A^n])[\vec {x}/\vec {a}]) , $
we have
$$\begin{align*}k \Vdash (\beta[A^1,\ldots,A^n])[\vec{x},y/\vec{a},b] \end{align*}$$
for all
$b \in D_{k}$
. By the induction hypothesis, we have
$ D_{k} \models _c (\beta [\hat {A}^1_k,\ldots ,\hat {A}^n_k]) [\vec {x},y/\vec {a},b] $
for all
$b \in D_{k}$
. Therefore
$$\begin{align*}D_{k} \models_c ((\forall y \beta)[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}]. \end{align*}$$
Case 4:
$ \gamma \mathbin {\rightarrow } \beta \in \mathcal {B}. $
Suppose that
$ k \Vdash ((\gamma \mathbin {\rightarrow } \beta )[A^1,\ldots ,A^n])[\vec {x}/\vec {a}]. $
Then
$$\begin{align*}k \Vdash (\gamma[A^1,\ldots,A^n])[\vec{x}/\vec{a}] \mathbin{\rightarrow} (\beta[A^1,\ldots,A^n])[\vec{x}/\vec{a}]. \end{align*}$$
Assume that
$ D_{k} \models _c (\gamma [\hat {A}^1_k,\ldots ,\hat {A}^n_k])[\vec {x}/\vec {a}]. $
By the induction hypothesis, we have
$ k \Vdash (\gamma [A^1,\ldots ,A^n])[\vec {x}/\vec {a}] , $
and hence
$ k \Vdash (\beta [A^1,\ldots ,A^n])[\vec {x}/\vec {a}]. $
By the induction hypothesis, we have
$ D_{k} \models _c (\beta [\hat {A}^1_k,\ldots ,\hat {A}^n_k])[\vec {x}/\vec {a}]. $
Thus
$$\begin{align*}D_{k} \models_c ((\gamma \mathbin{\rightarrow} \beta)[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}]. \end{align*}$$
Case 5:
$ \alpha \mathbin {\rightarrow } \gamma \in \mathcal {C}. $
Suppose that
$ D_{k} \models _c ((\alpha \mathbin {\rightarrow } \gamma )[\hat {A}^1_k,\ldots ,\hat {A}^n_k])[\vec {x}/\vec {a}]. $
Then
$$\begin{align*}D_{k} \models_c (\alpha[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}] \mathbin{\rightarrow} (\gamma[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}]. \end{align*}$$
Consider
$k' \geq k$
, and assume that
$ k' \Vdash (\alpha [A^1,\ldots ,A^n])[\vec {x}/\epsilon _{k k'}(\vec {a})]. $
By the induction hypothesis, we have
$ D_{k} \models _c (\alpha [\hat {A}^1_k,\ldots ,\hat {A}^n_k])[\vec {x}/\vec {a}] , $
and hence
$$\begin{align*}D_{k} \models_c (\gamma[\hat{A}^1_k,\ldots,\hat{A}^n_k])[\vec{x}/\vec{a}]. \end{align*}$$
By the induction hypothesis, we have
$ k \Vdash (\gamma [A^1,\ldots ,A^n])[\vec {x}/\vec {a}] , $
and so
$ k' \Vdash (\gamma [A^1,\ldots ,A^n])[\vec {x}/\epsilon _{k k'}(\vec {a})]. $
Thus
$$\begin{align*}k \Vdash ((\alpha \mathbin{\rightarrow} \gamma)[A^1,\ldots,A^n])[\vec{x}/\vec{a}]. \end{align*}$$
Case 6:
$ \forall y \delta \in \mathcal {D}. $
Suppose that
$ D_{k'} \models _c ((\forall y \delta )[\hat {A}^1_{k'},\ldots ,\hat {A}^n_{k'}])[\vec {x}/\epsilon _{k k'}(\vec {a})] $
for all
$k' \geq k$
. Then
$ D_{k'} \models _c (\delta [\hat {A}^1_{k'},\ldots ,\hat {A}^n_{k'}])[\vec {x},y/\epsilon _{k k'}(\vec {a}),c] $
for all
$k' \geq k$
and
$c \in D_{k'}$
. Therefore if
$k' \geq k$
and
$c \in D_{k'}$
, then
$$\begin{align*}D_{k"} \models_c (\delta[\hat{A}^1_{k"},\ldots,\hat{A}^n_{k"}])[\vec{x},y/\epsilon_{k' k"}(\epsilon_{k k'}(\vec{a})),\epsilon_{k' k"}(c)] \end{align*}$$
for all
$k" \geq k'$
. By the induction hypothesis, we have
$ k' \Vdash (\delta [A^1,\ldots ,A^n]) [\vec {x},y/\epsilon _{k k'}(\vec {a}),c]. $
Thus
$ k \Vdash ((\forall y \delta )[A^1,\ldots ,A^n])[\vec {x}/\vec {a}]. $
Case 7:
$ \beta \mathbin {\rightarrow } \delta \in \mathcal {D}. $
Suppose that
$ D_{k'} \models _c ((\beta \mathbin {\rightarrow } \delta )[\hat {A}^1_{k'},\ldots ,\hat {A}^n_{k'}])[\vec {x}/\epsilon _{k k'}(\vec {a})] $
for all
$k' \geq k$
. Then
$$\begin{align*}D_{k'} \models_c (\beta[\hat{A}^1_{k'},\ldots,\hat{A}^n_{k'}])[\vec{x}/\epsilon_{k k'}(\vec{a})] \mathbin{\rightarrow} (\delta[\hat{A}^1_{k'},\ldots,\hat{A}^n_{k'}])[\vec{x}/\epsilon_{k k'}(\vec{a})] \end{align*}$$
for all
$k' \geq k$
. Consider
$k' \geq k$
, and assume that
$$\begin{align*}k' \Vdash (\beta[A^1,\ldots,A^n])[\vec{x}/\epsilon_{k k'}(\vec{a})]. \end{align*}$$
Then
$ k" \Vdash (\beta [A^1,\ldots ,A^n])[\vec {x}/\epsilon _{k' k"}(\epsilon _{k k'}(\vec {a}))]. $
for all
$k" \geq k'$
. By the induction hypothesis, we have
$ D_{k"} \models _c (\beta [\hat {A}^1_{k"},\ldots ,\hat {A}^n_{k"}])[\vec {x}/\epsilon _{k' k"}(\epsilon _{k k'}(\vec {a}))] $
for all
$k" \geq k'$
. Therefore
$ D_{k"} \models _c (\delta [\hat {A}^1_{k"},\ldots ,\hat {A}^n_{k"}])[\vec {x}/\epsilon _{k' k"}(\epsilon _{k k'}(\vec {a}))] $
for all
$k" \geq k'$
. By the induction hypothesis, we have
$ k' \Vdash (\delta [A^1,\ldots ,A^n])[\vec {x}/\epsilon _{k k'}(\vec {a})]. $
Thus
$ k \Vdash ((\beta \mathbin {\rightarrow } \delta )[A^1,\ldots ,A^n])[\vec {x}/\vec {a}]. $
Proof of Lemma 4.11
Consider a schema
$\delta [\nu _1,\ldots ,\nu _n]$
in
$\Gamma $
. By Lemma A.1, for each
$k \in K$
and formulae
$A^1, \ldots , A^n$
, there exist formulae
$\hat {A}^1_k, \ldots , \hat {A}^n_k$
such that
$$\begin{align*}k \Vdash_{\mathcal{E},\mathcal{I}} A^i[\vec{x}/\vec{a}] \mathbin{\Leftrightarrow} M_{f(k)} \models_c \hat{A}^i_{k}[\vec{x}/\vec{a}] \end{align*}$$
for all
$i \in \{1,\ldots ,n\}$
and
$\vec {a} \in M_{f(k)}$
. Since
$$\begin{align*}M_{f(k)} \models_c (\delta[\hat{A}^1_{k},\ldots,\hat{A}^n_{k})[\vec{x}/\vec{a}] \end{align*}$$
for all
$k \in K$
and
$\vec {a} \in M_{f(k)}$
, by Lemma A.2, we have
$$\begin{align*}k \Vdash (\delta[A^1,\ldots,A^n])[\vec{x}/\vec{a}] \end{align*}$$
for all
$\vec {a} \in M_{f(k)}$
.
Proof of Lemma 4.14
It suffices to show that if
$B \in \Gamma $
, then
$$\begin{align*}{k \Vdash_{\mathcal{E},\mathcal{I}} B[\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {M_{f(k)} \models_c B[\vec{x}/\vec{a}]} \end{align*}$$
for all
$i \in I$
and
$\vec {a} \in M_{f(k)}$
. We proceed by induction on the complexity of B, and review only the cases for
$\mathbin {\rightarrow }$
and
$\forall $
. If
$B \equiv B' \mathbin {\rightarrow } B"$
, by the induction hypothesis and the assumption, we have
$$ \begin{align*} k \Vdash_{\mathcal{E},\mathcal{I}} B[\vec{x}/\vec{a}] & \mathbin{\Leftrightarrow} \forall k' \geq k ( k' \Vdash_{\mathcal{E},\mathcal{I}} B'[\vec{x}/\epsilon_{k k'}(\vec{a})] \mathbin{\Rightarrow} k' \Vdash_{\mathcal{E},\mathcal{I}} B"[\vec{x}/\epsilon_{k k'}(\vec{a})] ) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k ( M_{f(k')} \models_c B'[\vec{x}/\eta_{f(k) f(k')}(\vec{a})] \\ & \qquad\qquad\qquad\qquad\qquad \mathbin{\Rightarrow} M_{f(k')} \models_c B"[\vec{x}/\eta_{f(k) f(k')}(\vec{a})] ) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k ( M_{f(k')} \models_c B[\vec{x}/\eta_{f(k) f(k')}(\vec{a})] ) \\ & \mathbin{\Leftrightarrow} M_{f(k)} \models_c B[\vec{x}/\vec{a}]. \end{align*} $$
If
$B \equiv \forall y B'$
, again by the induction hypothesis and the assumption, we have
$$ \begin{align*} k \Vdash_{\mathcal{E},\mathcal{I}} B[\vec{x}/\vec{a}] & \mathbin{\Leftrightarrow} \forall k' \geq k \forall b \in D_{k'} ( k' \Vdash_{\mathcal{E},\mathcal{I}} B'[\vec{x},y/\epsilon_{k k'}(\vec{a}),b] ) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k \forall b \in M_{f(k')} ( M_{f(k')} \models_c B'[\vec{x},y/\eta_{f(k) f(k')}(\vec{a}),b] ) \\ & \mathbin{\Leftrightarrow} \forall k' \geq k ( M_{f(k')} \models_c B[\vec{x}/\eta_{f(k) f(k')}(\vec{a})] ) \\ & \mathbin{\Leftrightarrow} M_{f(k)} \models_c B[\vec{x}/\vec{a}].\\[-37pt] \end{align*} $$
Appendix B. The relativization of the arithmetized completeness theorem.
Recall that
$\mathcal {L}_1^{Q}$
is an extension of
$\mathcal {L}_1$
by adding a unary predicate symbol Q and an
$\mathcal {L}_{1}^{Q}$
-structure is a pair
$(M,Q^{M})$
where M is an
$\mathcal {L}_{1}$
-structure and
$Q^{M}$
is an interpretation of Q on M. Thanks to
$\mathcal {L}_1^{Q}$
-instances of the induction axiom schema in
$\mathbf {HA}^{*}$
, most proofs and discussions for
$\mathcal {L}_{1}$
-statements and structures within
$\mathbf {HA}$
can be carried out analogously for
$\mathcal {L}_{1}^{Q}$
within
$\mathbf {HA}^{*}$
.
Theorem B.1 (Arithmetized completeness theorem—relativized).
Let
$Q_{0} \subseteq \omega $
, let T be a set of
$\mathcal {L}_1^{Q}$
-sentences which is well-behaved over
$Q_{0}$
, and let
$(M,Q^{M})$
be an
$\mathcal {L}_1^{Q}$
-structure such that
$$\begin{align*}(M,Q^{M}) \models_c \mathbf{HA}^{Q_0} + \mathrm{Con}(T). \end{align*}$$
Then there exist a definable
$\mathcal {L}_1^{Q}$
-structure
$(\hat {M},Q^{\hat {M}})$
in
$(M,Q^{M})$
and a
$\Sigma _0^{Q}$
-elementary embedding
$\theta : M \to \hat {M}$
such that
$ (\hat {M},Q^{\hat {M}}) \models _c T. $
Moreover, for each formula B, there exists an
$\mathcal {L}_{1}^{Q}$
-formula
$[B]$
such that
$\mathrm {FV}([B]) = \mathrm {FV}(B)$
and
$$\begin{align*}{(M,Q^{M}) \models_c [B][\vec{x}/\vec{a}]} \mathbin{\Leftrightarrow} {(\hat{M},Q^{\hat{M}}) \models_c B[\vec{x}/\theta(\vec{a})]} \end{align*}$$
for all
$\vec {a} \in M$
, where
$\vec {x}$
are the free variables of B.
Note that a special case by letting
$Q_{0}=\omega $
and forgetting Q is the original arithmetized completeness theorem (Theorem 4.5).
Proof Let
$\tau (x)$
be a
$\Sigma _{1}^{Q}$
-representation over
$Q_{0}$
of T. By arithmetizing the usual argument within
$\mathbf {HA}^{*}$
, let
$\hat T$
be the Henkin extension of T. In other words, obtain
$\hat \tau (x)$
which represents a set of
$\mathcal {L}_{1}^{Q}\cup \mathcal {C}$
-sentences which extends
$\tau (x)$
together with Henkin axioms for
$\mathcal {L}_{1}^{Q}$
where
$\mathcal {C}$
is the set of Henkin constants (coded by numbers). Then
$\mathbf {HA}^{*}\vdash _{c} \forall x(\tau (x)\to \hat \tau (x))$
and
$\mathbf {HA}^{*}\vdash _{c} \mathrm {Con}(T)\to \mathrm {Con}(\hat T)$
. Apply the syntactic form of the arithmetized completeness theorem [Reference Smoryński31, Theorem 6.8] and obtain
$\chi (x)$
so that
$$ \begin{align*} \mathbf{HA}^{*}\vdash_{c} & \forall x[(\chi(x)\to "x\text{ is a sentence"})\wedge(\hat\tau(x)\to\chi(x))]\\ & \wedge [\mathrm{Con}(\hat T)\to "\chi(x)\text{ defines a complete set of }\mathcal{L}_{1}^{Q}\cup \mathcal{C}\text{-sentences"}]. \end{align*} $$
Now we see the semantic form of the arithmetized completeness theorem [Reference Smoryński31, Theorem 6.10] in our formulation. Let
$(M,Q^{M}) \models _c \mathbf {HA}^{Q_0} + \mathrm {Con}(T)$
. Then we have
$(M,Q^{M}) \models _c \mathrm {Con}(\hat T)$
. Hence, by arithmetizing the usual Henkin construction using the complete theory defined by
$\chi (x)$
, one may obtain a definable
$\mathcal {L}_{1}^{Q}$
-structure
$(\hat M,Q^{\hat M})$
in
$(M,Q^{M})$
such that for any
$\mathcal {L}_{1}^{Q}$
-sentence A,
$(M,Q^{M}) \models _c\chi (\lceil A\rceil )\mathbin {\Leftrightarrow }(\hat M,Q^{\hat M})\models _{c}A$
and thus
$(\hat M,Q^{\hat M})\models _{c}\mathbf {HA}^{*}$
. For a given
$\mathcal {L}_{1}^{Q}$
-formula B, one may obtain
$[B]$
by formalizing Tarski’s truth definition. Moreover, for each standard number
$m\in \omega $
, we have
$m\in Q_{0}\mathbin {\Leftrightarrow }(M,Q^{M}) \models _c Q(\bar m)\mathbin {\Leftrightarrow }(M,Q^{M})\models _{c}\tau (\lceil Q(\bar m)\rceil )\mathbin {\Leftrightarrow }(M,Q^{M})\models _{c}\chi (\lceil Q(\bar m)\rceil )\mathbin {\Leftrightarrow }(\hat M,Q^{\hat M})\models _{c}Q(\bar m)$
. Therefore
$(\hat M,Q^{\hat M})\models _{c}\mathbf {HA}^{Q_{0}}$
.
Now consider the canonical embedding
$\theta : M \to \hat {M}$
as in Remark 4.4, then M can be embedded onto an initial segment of
$\hat {M}$
by [Reference Smoryński31, Lemma 6.12]. Moreover, for each
$m\in M$
, we have
$(M,Q^{M}) \models _c Q(m)\mathbin {\Leftrightarrow }(\hat M,Q^{\hat M})\models _{c}Q(\bar m)\mathbin {\Leftrightarrow }(\hat M,Q^{\hat M})\models _{c}Q(\theta (m))$
, and hence
$\theta $
is
$\mathcal {L}_{1}^{Q}$
-homeomorphism. Therefore,
$\theta $
is
$\Sigma _{0}^{Q}$
-elementary by [Reference Smoryński31, Lemma 3.8].
See also [Reference Hájek and Pudlák13, Chapter I, Section 4, especially 4.27] and [Reference Wong36] for stronger forms of the arithmetized completeness theorem and a modern proof.
Acknowledgment
The authors thank Taishi Kurahashi for his useful comments.
Funding
The authors thank the Japan Society for the Promotion of Science (JSPS), Core-to-Core Program (A. Advanced Research Networks) for supporting the research. The first author was supported by JSPS KAKENHI Grant Numbers JP16H07289, JP18K13450, JP19J01239, and JP20K14354, the second author by JP16K05251, the third author by JP18K03392, the forth author by JP24540120, JP26245026, JP16K05252, JP20K03716, and JP21H00694, the fifth author by JP19K03601, and the first, second, third, and fifth authors by JP21KK0045.
