A Note on Disjunction and Existence Properties in Predicate Extensions of Intuitionistic Logic—An Application of Jankov Formulas to Predicate Logics

Abstract

Predicate extensions of intuitionistic logic (PEI’s) are intermediate predicate logics having the same propositional part as intuitionistic logic. Intuitively, PEI’s must resemble intuitionistic logic. We discuss PEI’s from the viewpoint of disjunction property (DP) and existence property (EP). Note that DP and EP are regarded as “hallmarks” of constructivity of intuitionistic logic. There are, however, uncountably many PEI’s having both of DP and EP. Moreover, there are two continua of PEI’s: (1) each of which lacks both of DP and EP, and (2) each of which has EP but lacks DP. Now, a natural question arises: Do there exist uncountably many PEI’s each of which has DP and lacks EP? We answer this question affirmatively. Specifically, we construct uncountably many such PEI’s by making use of modified Jankov formulas. This result suggests that although PEI’s are living near to intuitionistic logic, the diversity of their nature seems rich. In other words, logics among PEI’s are fascinating from the logical point of view and yet to be explored.

1 Introduction

Predicate extensions of intuitionistic logic (PEI’s) are intermediate predicate logics having the same propositional part as intuitionistic logic. Intuitively, PEI’s must resemble intuitionistic logic. We discuss PEI’s from the viewpoint of disjunction property (DP) and existence property (EP). Note that DP and EP are regarded as distinguishing characteristics and features of constructivity of intuitionistic logic. However, Suzuki (1999) constructed a continuum of PEI’s having both of EP and DP. There exits a continuum of PEI’s without both of EP and DP as well. In 1983, Minari (1986) and Nakamura (1983) independently proved that some well-known PEI’s have DP and fail to have EP. Recently, in Suzuki (2021), a continuum of PEI’s having EP and lacking DP was constructed.¹

Now, a natural question arises: Do there exist uncountably many PEI’s each of which has DP and lacks EP? We answer this question affirmatively. Specifically, we construct uncountably many such PEI’s by giving a recursively enumerable sequence of concrete predicate axiom schemata. These axiom schemata are obtained by modifying the Jankov formulas (Jankov 1963, 1968, 1969).

Jankov created an invaluable research tool for the study of non-classical propositional logics²; the Jankov formulas provide us with a connection between algebraic property of Heyting algebras and inclusion relation among propositional logics. In this paper, we give an application of Jankov’s tool to non-classical predicate logics. Since Jankov’s method deals with propositional logics, its straightforward application to predicate logics inevitably yields logics having their propositional parts differing from intuitionistic logic. We introduce our formulas with an appropriate modification of Jankov’s to keep them having intuitionistic propositional part.

Accordingly, to show our main result, we prove three Lemmata 9.2, 9.6, and 9.9; Lemma 9.2 states that our modified Jankov formulas yield PEI’s lacking EP; Lemma 9.6 states that they yield PEI’s having DP; from Lemma 9.9, it holds that we can generate uncountably many PEI’s by using them. We show Lemma 9.2 by making use of algebraic semantics. Our idea for the proof of Lemma 9.6 comes from the above-mentioned idea of Minari (1986) and Nakamura (1983) based on Kripke frame semantics. Lemma 9.9 is proved by algebraic Kripke sheaf semantics introduced in Suzuki (1999).

We assume readers’ some familiarity with Heyting algebras and Kripke frames. To make this paper rather self-contained, we briefly explain some notions and definitions on these semantical tools needed in this paper. Algebraic Kripke sheaves are semantical framework obtained from integrating algebraic semantics into Kripke semantics. Since general algebraic Kripke sheaves are (as of now) not so simple to handle, we introduce restricted algebraic Kripke sheaves, called $\Omega$-brooms, and use them with a result in Suzuki (1999) for the proof of our main result.

In Sect. 9.2, brief explanation of intermediate (propositional and predicate) logics and some related definitions as well as DP and EP are given. In Sect. 9.3, we introduce Jankov formulas and modified Jankov formulas. Here, we prove that modified ones as axiom schemata yield PEI’s without EP (Lemma 9.2) . In Sects. 9.4 and 9.5, we prove that these axiom schemata enjoy DP (Lemma 9.6), and that they generate a continuum of PEI’s (Lemma 9.9), and we complete the proof of the main result (Theorem 9.4). In Sect. 9.6, we make some concluding remarks.

2 Preliminaries

Intermediate logics are logics falling intermediate between intuitionistic and classical logics. There are two types of intermediate logics: intermediate propositional logics and intermediate predicate logics. We refer readers to Ono (1987) for an information source.

We use a pure first-order language $\mathcal {L}$. Logical symbols of $\mathcal {L}$ are propositional connectives: $\vee$, $\wedge$, $\supset$, and $\lnot$ (disjunction, conjunction, implication, and negation, respectively), and quantifiers: $\exists$ and $\forall$ (existential and universal quantifiers, respectively). $\mathcal {L}$ has a denumerable list of individual variables and a denumerable list of m-ary predicate variables for each $m < \omega$. All 0-ary predicate variables are identified with propositional variables; thus, the propositional language $\mathcal {L}_{proposition}$ is contained in $\mathcal {L}$. Note that $\mathcal {L}$ contains neither individual constants nor function symbols.

The idea of introducing intermediate logics is the identification of each logic and the set of formulas provable in it. For example, intuitionistic propositional logic $\textbf{H}$ and intuitionistic predicate logic $\textbf{H}_*$ are identified with the sets of formulas provable in $\textbf{H}$ and $\textbf{H}_*$, respectively. Also, classical propositional and predicate logics, $\textbf{C}$ and $\textbf{C}_*$, are treated in the same way.

Definition 9.1

A set $\textbf{J}$ of formulas of propositional language $\mathcal {L}_{proposition}$ is said to be an intermediate propositional logic, if $\textbf{J}$ satisfies the conditions: (P1) $\textbf{H} \subseteq \textbf{J} \subseteq \textbf{C}$ and (P2) $\textbf{J}$ is closed under the rule of modus ponens (from A and $A \supset B$, infer B) and uniform substitution for propositional variable.

A set $\textbf{J}$ of formulas of $\mathcal {L}_{proposition}$ is said to be a super-intuitionistic propositional logic, if $\textbf{J}$ satisfies (P1’) $\textbf{H} \subseteq \textbf{J}$ and (P2). Let $\Psi _0$ be the set of all propositional formulas. The $\Psi _0$ is the only super-intuitionistic propositional logic that is not an intermediate propositional logic.

Definition 9.2

A set $\textbf{L}$ of formulas of $\mathcal {L}$ is said to be an intermediate predicate logic, if $\textbf{L}$ satisfies the three conditions: (Q1) $\textbf{H}_*\subseteq \textbf{L} \subseteq \textbf{C}_*$ and (Q2) $\textbf{L}$ is closed under the rule of modus ponens, the rule of generalization (from A, infer $\forall xA$), and uniform substitution³ for predicate variable.

A set $\textbf{L}$ of formulas of $\mathcal {L}$ is said to be a super-intuitionistic predicate logic, if $\textbf{L}$ satisfies (Q1’) $\textbf{H}_*\subseteq \textbf{L}$ and (Q2). There are uncountably many superintuitionistic predicate logics that are not intermediate predicate logics.

When $A \in \textbf{L}$, we sometimes write $\textbf{L} \vdash A$, and say “A is provable in $\textbf{L}$.” For a logic $\textbf{L}$ and a set $\Gamma$ of formulas, the smallest logic containing $\textbf{L}$ and $\Gamma$ (as sets) is denoted by $\textbf{L}+\Gamma$. Let $\textbf{L}$ be a predicate logic. Then, $\pi (\textbf{L})= \textbf{L} \cap \Psi _0$ is a propositional logic. It is called the propositional part of $\textbf{L}$.

For each propositional logic $\textbf{J}$, a predicate logic $\textbf{L}$ is called a predicate extension of $\textbf{J}$, if $\pi (\textbf{L})=\textbf{J}$. A predicate logic $\textbf{L}$ is said to be a predicate extension of intuitionistic logic (a PEI), if $\pi (\textbf{L})=\textbf{H}$.

Definition 9.3

(cf. Church 1956; Sect. 32) To each predicate variable p, we associate a unique propositional variable $\pi (p)$. For a given formula A of $\mathcal {L}$, we define the associated formula of the propositional calculus (afp) by (1) deleting all quantifiers $\forall x$ and $\exists x$ in A and (2) substituting $\pi (p)$ to $p(v_1, \dots , v_n)$ in A for each predicate variable⁴ p occurring in A. The afp of A is denoted by $\pi (A)$.

Proposition 9.1

Let $\textbf{L}$ be a predicate logic. It holds that $\pi (\textbf{H}_*+\Gamma )=\textbf{H}+\{ \pi (A) \mathrel {;} A \in \Gamma \}$.

Definition 9.4

A logic $\textbf{L}$ is said to have the disjunction property (DP), if for every A and every B, $\textbf{L} \vdash A \vee B$ implies either $\textbf{L} \vdash A$ or $\textbf{L} \vdash B$.

A formula A is said to be congruent to a formula B, if A is obtained from B by alphabetic change of bound variables which does not turn any free occurrences of variables newly bound (cf. Kleene 1952; p. 153). A predicate logic $\textbf{L}$ is said to have the existence property (EP),  if for every $\exists xA(x)$, $\textbf{L} \vdash \exists xA(x)$ implies that there exist a formula $\widetilde{A}(x)$ which is congruent to A(x) and an individual variable v such that v is free for x in $\widetilde{A}(x)$ and $\textbf{L} \vdash \widetilde{A}(v)$ (cf. Kleene 1962).

Formulas congruent to a formula A(x) are intuitionistically equivalent to each other. They are usually written by the same symbol A(x) for the sake of simplicity (cf. Gabbay et al. 2009; Sect. 2.3).

Definition 9.5

(cf. Jankov 1968) A sequence $\{ \textbf{L}_i \}_{i<\omega }$ of logics is said to be strongly independent, if $\textbf{L}_i \nsubseteq \bigcup _{j \ne i}\textbf{L}_j$ for each $i < \omega$, where $\bigcup _{j \ne i}\textbf{L}_j$ is the smallest logic containing all $\textbf{L}_j$ $(j \ne i)$.

Proposition 9.2

Let $\{ \textbf{L}_i \}_{i<\omega }$ be a strongly independent sequence of logics.

(1) For every $I, J \subseteq \omega$, $I=J$ if and only if $\bigcup _{i \in I}\textbf{L}_i = \bigcup _{i \in J}\textbf{L}_i$.

(2) The set $\{ \bigcup _{i \in I}\textbf{L}_i \mathrel {;} I < \omega \}$ has the cardinality $2^\omega$.

Proof

It suffices to show that $I \ne J$ implies $\bigcup _{i \in I}\textbf{L}_i \ne \bigcup _{i \in J}\textbf{L}_i$. Suppose $I \ne J$. Without loss of generality, we may assume that there exists a $k \in I \setminus J$. It is obvious that $\bigcup _{i \in J}\textbf{L}_i \subseteq \bigcup _{i \ne k}\textbf{L}_i$. By the assumption, we have $\textbf{L}_k \nsubseteq \bigcup _{i \ne k}\textbf{L}_i$. Thus, $\textbf{L}_k \nsubseteq \bigcup _{i \in J}\textbf{L}_i$. Therefore, we have $\bigcup _{i \in I}\textbf{L}_i \ne \bigcup _{i \in J}\textbf{L}_i$. $\square$

For a sequence $\{ X_i \}_{i < \omega }$ of formulas, we can define a sequence $\{ \textbf{H}_*+ X_i \}_{i < \omega }$ of logics. If $\{ \textbf{H}_*+ X_i \}_{i < \omega }$ is strongly independent, we say that $\{ X_i \}_{i < \omega }$ is strongly independent .

3 Modified Jankov Formulas—Learning Jankov’s Technique

In this section, we briefly explain Jankov formulas of finite subdirectly irreducible Heyting algebras. Then, we introduce a variant of Jankov formulas modified to achieve our aim. We show that these modified Jankov formulas as axiom schemata generate PEI’s without EP.

3.1 Heyting Algebras and Jankov Formulas

Let $\textbf{A}$ be a Heyting algebra. In what follows, we denote basic operations of $\textbf{A}$ by: $\cup _\textbf{A}$ (join), $\cap _\textbf{A}$ (meet), $\lnot _\textbf{A}$ (pseudo-complementation), and $\rightarrow _\textbf{A}$ (relative pseudo-complementation). We use the same letter $\textbf{A}$ to denote its underlying set. The partial order determined by the lattice structure of $\textbf{A}$ is denoted by $\le _\textbf{A}$. Also, $1_\textbf{A}$ and $0_\textbf{A}$ are the greatest and least element of $\textbf{A}$. We sometimes omit the subscript $\textbf{A}$. The two-element Boolean algebra is denoted by $\textbf{2}$ $(=\{1_\textbf{2}, 0_\textbf{2} \})$.

Definition 9.6

A Heyting algebra $\textbf{A}$ is said to be subdirectly irreducible, if $\textbf{A}\setminus \{1_\textbf{A} \}$ has the greatest element. This element is denoted by $\star _\textbf{A}$.

Example 9.1

A non-empty partially ordered set $\textbf{M}=(\textbf{M}, \le _\textbf{M})$ is said to be a Kripke base, if it has the least element $0_{\textbf{M}}$. A subset $S \subseteq \textbf{M}$ is said to be open, if S is upward-closed (i.e., for every $x \in S$ and every $y \in \textbf{M}$, $x \le _\textbf{M} y$ implies $y \in S$). Then the set $\mathcal {O}(\textbf{M})$ of all open subsets of $\textbf{M}$ is a subdirectly irreducible Heyting algebra with respect to the set-inclusion as its partial ordering. The second greatest element of $\mathcal {O}(\textbf{M})$ is $\textbf{M} \setminus \{ 0_{\textbf{M}}\}$.

Let $\textbf{A}$ be a Heyting algebra, PV the set of all propositional variables. A mapping $v: PV \rightarrow \textbf{A}$ is said to be an assignment on $\textbf{A}$. By the usual induction, we extend the v to the mapping $v : \Psi _0 \rightarrow \textbf{A}$. A propositional formula C is said to be valid in $\textbf{A}$, if $v(C) = 1_\textbf{A}$ for every assignment v on $\textbf{A}$. The set of all propositional formulas valid in $\textbf{A}$ is denoted by $E(\textbf{A})$.

Proposition 9.3

For every non-degenerate Heyting algebra $\textbf{A}$, the set $E(\textbf{A})$ is an intermediate propositional logic.

Let $\textbf{A}$ be a finite subdirectly irreducible Heyting algebra. For each $a \in \textbf{A}$, we can attach a unique propositional variable $p_a \in PV$. The diagram $\delta (\textbf{A})$ of $\textbf{A}$ is the finite set of propositional formulas defined by:

$$\begin{aligned} \delta (\textbf{A})&= \{ p_{a \cup _\textbf{A} b} \supset (p_a \vee p_b), (p_a \vee p_b) \supset p_{a \cup _\textbf{A} b} \mathrel {;} a, b \in \textbf{A}\} \\&\bigcup \{ p_{a \cap _\textbf{A} b} \supset (p_a \wedge p_b), (p_a \wedge p_b) \supset p_{a \cap _\textbf{A} b} \mathrel {;} a, b \in \textbf{A}\} \\&\bigcup \{ p_{a \rightarrow _\textbf{A} b} \supset (p_a \supset p_b), (p_a \supset p_b) \supset p_{a \rightarrow _\textbf{A} b} \mathrel {;} a, b \in \textbf{A}\} \\&\bigcup \{ p_{a \rightarrow _\textbf{A} 0_\textbf{A}} \supset (\lnot p_a), (\lnot p_a) \supset p_{a \rightarrow _\textbf{A} 0_\textbf{A}} \mathrel {;} a \in \textbf{A}\} . \end{aligned}$$

The Jankov formula $J(\textbf{A})$ of $\textbf{A}$ is the propositional formula defined by:

$$ J(\textbf{A}) \,\, : \,\, \big ( \bigwedge \delta (\textbf{A}) \big ) \supset p_{\star _\textbf{A}}, $$

where $\bigwedge \delta (\textbf{A})$ is the conjunction of all formulas in $\delta (\textbf{A})$. Then it is easy to see that $J(\textbf{A})$ is not valid in $\textbf{A}$ by taking the assignment $v_\textbf{A}$: $p_a \mapsto a$ for each $a \in \textbf{A}$. Since $v_\textbf{A}(\bigwedge \delta (\textbf{A}))=1_\textbf{A}$, we have $J(\textbf{A}) \not \in E(\textbf{A})$. Moreover, we have the following prominent result due to Jankov (1963), which provide us with a connection between validity of Jankov formula and algebraic property.

Lemma 9.1

(cf. Jankov 1963; 1968; 1969) Let $\textbf{A}$ be a finite subdirectly irreducible Heyting algebra. If $J(\textbf{A})$ is not valid in a Heyting algebra $\textbf{B}$, then there exists a quotient algebra $\textbf{B}'$ of $\textbf{B}$ such that $\textbf{A}$ is embeddable into $\textbf{B}'$.

For further discussion, we need a denumerable sequence $\{ \textbf{A}_i \}_{i < \omega }$ satisfying;

• (A1) for each $i < \omega$, $\textbf{A}_i$ is a finite subdirectly irreducible Heyting algebra;

• (A2) for every i, $j < \omega$, if $i \ne j$, then $\textbf{A}_i$ is not embeddable into any quotient algebra of $\textbf{A}_j$.

In fact, Jankov (1968) and Wroński (1974) constructed concrete sequences of Heyting algebras with the above properties. Let us fix one of these sequence. By the virtue of their construction, we have the following by Lemma 9.1.

Corollary 9.1

(cf. Jankov 1968 and Wroński 1974) $\{ J(\textbf{A}_i) \}_{i < \omega }$ is strongly independent.

Proof

Define $\textbf{L}_i=\textbf{H}_*+J(\textbf{A}_{i})$ for each $i<\omega$. Pick an arbitrary $i_0 \in \omega$. Then, for every $j \ne i_0$, $\textbf{A}_j$ is not embeddable into any quotient algebra of $\textbf{A}_{i_0}$. Thus, it holds that $J(A_j) \in E(\textbf{A}_{i_0})$ for every $j \ne i_0$. Therefore, we have $\bigcup _{j \ne i_0}\textbf{L}_j \subseteq E(\textbf{A}_{i_0}) \not \ni J(\textbf{A}_{i_0}) \in \textbf{L}_{i_0}$. Hence, $\textbf{L}_{i_0} \nsubseteq \bigcup _{j \ne i_0}\textbf{L}_j$.$\square$

Thus, by putting $\textbf{J}(I)=\bigcup _{i \in I}\textbf{L}_i$ for each $I \subset \omega$, we have a continuum $\{ \textbf{J}(I) \mathrel {;} J \subset \omega \}$ of logics by Proposition 9.2. Note that no logic in this continuum has the propositional part being identical to intuitionistic logic. We must modify the original $J(\textbf{A})$ so as to achieve our aim of this paper.

3.2 Modified Jankov Formulas for PEI’s Without EP

In this subsection, we introduce modified Jankov formulas. The idea of our modification comes from observation of behavior of the sentence the sentence F: $\exists x(p(x) \supset \forall yp(y))$, where p is a unary predicate variable. Clearly, F is provable in classical predicate logic $\textbf{C}_*$, but $p(v) \supset \forall yp(y)$ is not so for every individual variable v. Thus, this F is a typical counterexample to EP of $\textbf{C}_*$. Note that the afp $\pi (F)$ of F is $p \supset p$, and hence the propositional part $\pi (\textbf{H}_*+ F)$ of $\textbf{H}_*+ F$ equals $\textbf{H}$ by Proposition 9.1. This F also gives a counterexample to EP of $\textbf{H}_*+ F$ that is a PEI. Moreover, Minari (1986) and Nakamura (1983) independently proved that $\textbf{H}_*+ F$ has DP, and hence they showed that $\textbf{H}_*+ F$ is a PEI having DP and lacking EP. Our modified Jankov formulas play the same role as F and have a property similar to that of the original Jankov formula shown in Lemma 9.1 (see Lemma 9.12).

Let $\textbf{A}$ be a finite subdirectly irreducible Heyting algebra, $J(\textbf{A})$ the Jankov formula of $\textbf{A}$. Pick a fresh individual variable v. Let $\Delta (\textbf{A})$ be the finite set of sentences obtained from $\delta (\textbf{A})$ by replacing all occurrences of $p_{\star _\textbf{A}}$ by F. Define a formula $PJ(\textbf{A})(v)$ and a sentence $QJ(\textbf{A})$ by:

$$\begin{aligned} PJ(\textbf{A})(v) \,\,&: \,\, \bigwedge \Delta (\textbf{A}) \supset (p(v) \supset \forall yp(y)) , \\ QJ(\textbf{A}) \,\,&: \,\, \exists v PJ(\textbf{A})(v) . \end{aligned}$$

Jankov (1968) and Wroński (1974) constructed a concrete sequence $\{ \textbf{H}_i \}_{i<\omega }$ of finite subdirectly irreducible Heyting algebras satisfying the conditions (A1) and (A2) in Sect. 9.3.1 together with the following (A3):

• (A3) for each $i < \omega$, there are exactly three elements in $\textbf{H}_i$ having no incomparable element (i.e., 0, 1 and $\star$).

Let us fix one of their sequences. Then, we can construct $QJ(\textbf{H}_i)$ ($i<\omega$) one by one concretely and in a recursively enumerable manner. To achieve our main aim, we use this sequence of Heyting algebras and show that $\{ QJ(\textbf{H}_i) \}_{i < \omega }$ satisfies the following three conditions:

• (cf. Lemma 9.2) for every $I \subseteq \omega$, $\textbf{H}_*+ \{ QJ(\textbf{H}_i) \, ; i \in I \}$ is a PEI lacking EP,

• (cf. Lemma 9.6) for every $I \subseteq \omega$, $\textbf{H}_*+ \{ QJ(\textbf{H}_i) \, ; i \in I \}$ has DP.

• (Lemma 9.9) $\{ QJ(\textbf{H}_i) \}_{i < \omega }$ is strongly independent.

In the rest of this subsection, we show that modified Jankov formulas axiomatize PEI’s lacking EP. Specifically, we show the

Lemma 9.2

Let $\mathcal {S}$ be a set of finite non-degenerate subdirectly irreducible Heyting algebras having at least three elements. Then, $\textbf{H}_*+ \{QJ(\textbf{A}) \mathrel {;} \textbf{A} \in \mathcal {S}\}$ is a PEI lacking EP.

Note that $QJ(\textbf{A})$ is provable in $\textbf{C}_*$. It is clear that $\pi (QJ(\textbf{A}))=\pi (\bigwedge \Delta (\textbf{A})) \supset (p \supset p)$ is provable in intuitionistic logic $\textbf{H}$. Hence, for every set $\mathcal {S}$ of finite subdirectly irreducible Heyting algebras, the intermediate predicate logic $\textbf{H}_*+\{ QJ(\textbf{A}) \mathrel {;} \textbf{A} \in \mathcal {S} \}$ is a PEI. It suffices to show the

Lemma 9.3

Let $\textbf{A}$ be a finite subdirectly irreducible Heyting algebra having at least three elements. Then, $PJ(\textbf{A})(v)$ is not provable in $\textbf{C}_*$.

We introduce algebraic semantics for predicate logics, and some definitions and propositions on Heyting algebras without proofs, and show this Lemma.

Definition 9.7

For each non-empty set U, the language obtained from $\mathcal {L}$ by adding the name $\overline{u}$ for each $u \in U$ is denoted by $\mathcal {L}[U]$. In what follows, we use the same letter u for the name $\overline{u}$ of u, when no confusion can arise. We sometimes identify $\mathcal {L}[U]$ with the set of all sentences of $\mathcal {L}[U]$.

A Heyting algebra $\textbf{A}$ is said to be $\kappa$-complete for some cardinal $\kappa$, if both of the supremum $\bigcup S$ and the infimum $\bigcap S$ exist in $\textbf{A}$ for every subset S of $\textbf{A}$ having the cardinality at most $\kappa$. A pair $\mathcal {A}=(\textbf{A},U)$ of a non-degenerate |U|-complete Heyting algebra $\textbf{A}$ and a non-empty set U is said to be an algebraic frame, where |U| is the cardinality of U.

A mapping V of the set of all atomic sentences of $\mathcal {L}[U]$ to $\textbf{A}$ is said to be an assignment on $\mathcal {A}$. We extend V to a mapping of $\mathcal {L}[U]$ to $\textbf{A}$ inductively as follows:

• $V(A \wedge B)=V(A) \cap V(B)$,

• $V(A \vee B)=V(A) \cup V(B)$,

• $V(A \supset B)=V(A) \rightarrow V(B)$,

• $V(\lnot A)=V(A) \rightarrow 0$,

• $V(\forall xA(x))= \bigcap _{u \in U}V(A(\overline{u}))$,

• $V(\exists xA(x))= \bigcup _{u \in U}V(A(\overline{u}))$.

Since $\textbf{A}$ is $\kappa$-complete, the right hand sides of the last two equalities are well-defined. A pair $(\mathcal {A}, V)$ of an algebraic frame $\mathcal {A}$ and an assignment V is said to be an algebraic model. A formula A of $\mathcal {L}$ is said to be true in an algebraic model $(\mathcal {A}, V)$, if $V(\overline{A})=1$, where $\overline{A}$ is the universal closure of A. A formula of $\mathcal {L}$ is said to be valid in an algebraic frame $\mathcal {A}$, if it is true in $(\mathcal {A}, V)$ for every assignment V on $\mathcal {A}$. The set of formulas of $\mathcal {L}$ valid in $\mathcal {A}$ is denoted by $L(\mathcal {A})$ or $L(\textbf{A},U)$.

Proposition 9.4

For each algebraic frame $\mathcal {A}$, the set $L(\mathcal {A})$ is a super-intuitionistic predicate logic.

It is well-known that $\textbf{C}_*\subseteq L(\textbf{2},\{0,1 \})$. To show Lemma 9.3, we construct an appropriate assignment V on $(\textbf{2},U)$ for each finite subdirectly irreducible Heyting algebra $\textbf{A}$ having at least three elements, and show that $V(\overline{PJ(\textbf{A})(v)})\ne 1_{\textbf{2}}$.

Lemma 9.4

Let $\textbf{A}$ be a finite subdirectly irreducible Heyting algebra having at least three elements. There exists a propositional assignment $\mu$ on $\textbf{2}$ such that $\mu (\bigwedge \delta (\textbf{A}))=\mu (p_{\star _\textbf{A}})=1_\textbf{2}$.

Proof

Take an assignment v such that $v(p_a)=a$ for every $a \in \textbf{A}$. Then, $v(\bigwedge \delta (\textbf{A}))=1$ and $v(p_{\star _\textbf{A}})=\star _\textbf{A}$. The set $\{ a \in \textbf{A} \mathrel {;} a= \lnot _\textbf{A} \lnot _\textbf{A} a \}$ forms a Boolean algebra with respect to the restriction of $\le _\textbf{A}$ to this set. We denote this Boolean algebra by $\textbf{A}^{\lnot \lnot }$. Since $\textbf{A}$ is non-degenerate, $\textbf{A}^{\lnot \lnot }$ is non-degenerate. Let $\lnot \lnot$ be the mapping of $\textbf{A}$ to $\textbf{A}^{\lnot \lnot }$ defined by $\lnot \lnot (a)= \lnot _\textbf{A} \lnot _\textbf{A} a$ for every $a \in \textbf{A}$. Then, $\lnot \lnot$ is a Heyting homomorphism. We have: $\lnot \lnot \circ v(\bigwedge \delta (\textbf{A})) =\lnot \lnot \circ v(p_{\star _\textbf{A}}) =1_{\textbf{A}^{\lnot \lnot }}$. Since, $\textbf{A}^{\lnot \lnot }$ is non-degenerate, there exists an ultrafilter $\mathcal {U}$ on this Boolean algebra such that $\textbf{A}^{\lnot \lnot }/\mathcal {U} \simeq \textbf{2}$. Let $\rho$ be the canonical projection of $\textbf{A}^{\lnot \lnot }$ onto $\textbf{2}$. Then, we have: $\rho \circ \lnot \lnot \circ v(\bigwedge \delta (\textbf{A})) =\rho \circ \lnot \lnot \circ v(p_{\star _\textbf{A}}) =1_\textbf{2}$. Putting $\mu =\rho \circ \lnot \lnot \circ v$, we have the conclusion.$\square$

Taking the assignment $\mu$ in Lemma 9.4, we define an assignment V on $(\textbf{2}, \{0,1\})$ by:

$$ V(A)= \left\{ \begin{array}{ll} \mu (a) &{} \text{ if } A \text{ is } p_a \text{ for } \text{ some } a \in \textbf{A},\\ 1_\textbf{2} &{} \text{ if } A \text{ is } p(\overline{1}),\\ 0_\textbf{2} &{} \text{ otherwise., } \end{array} \right. $$

for each atomic sentence A of $\mathcal {L}[U]$. It is easy to check that $V(F) =1_\textbf{2}$. Then, we have the

Lemma 9.5

Let X be a propositional formula having no propositional variable other than $\{ p_a \mathrel {;} a \in \textbf{A} \}$. By $X'$, we denote the formula obtained from X by replacing all occurrences of $p_{\star _\textbf{A}}$ by the sentence F. Then, we have $V(X')=\mu (X)$.

Proof

We can show this Lemma by induction on the length of X. Since $\rho \circ \lnot \lnot$ is a Heyting-homomorphism, it suffices to check the Basis-part. But it is obvious by the fact that $V(F)=\mu (p_{\star _\textbf{A}})=1_\textbf{2}$.$\square$

Note that $a=v_\textbf{A}(p_a)$ for each $a \in \textbf{A}$. Now, we show Lemma 9.3. By Lemma 9.5, we have $V(\bigwedge \Delta (\textbf{A})) = \mu (\bigwedge \delta (\textbf{A})) =1_\textbf{2}$. Thus we have $V(PJ(\textbf{A})(\overline{1}))=V(\bigwedge \Delta (\textbf{A}))\rightarrow _\textbf{2} ( V(p(\overline{1})) \rightarrow _\textbf{2} V(\forall yp(y))) =1_\textbf{2}\rightarrow _\textbf{2}( 1_\textbf{2} \rightarrow _\textbf{2} 0_\textbf{2}) =0_\textbf{2}$. Therefore, we have $V(\overline{PJ(\textbf{A})(v)})=0_{\textbf{2}} \ne 1_{\textbf{2}}$, i.e., $PJ(\textbf{A})(v) \not \in L(\textbf{2},\{ 0,1,\}) \supseteq \textbf{C}_*$. This completes the proofs of Lemmas 9.3 and 9.2.

4 Modified Jankov Formulas Preserve DP—Learning Minari’s and Nakamura’s Idea

In this section, we show that the modified Jankov formulas as axiom schemata preserve DP. More specifically, we show the

Lemma 9.6

Let $\mathcal {S}$ be a set of finite non-degenerate subdirectly irreducible Heyting algebras. Then, $\textbf{H}_*+ \{QJ(\textbf{A}) \mathrel {;} \textbf{A} \in \mathcal {S}\}$ has DP.

We show this Lemma by making use of Kripke frame semantics. In Sect. 9.4.1, we introduce Kripke frame semantics for predicate logics. Next, in Sect. 9.4.2, a technique is given in a simplified form . A part of the result in Minari (1986) and Nakamura (1983) is presented to illustrate this technique.

4.1 Kripke Frame Semantics

Recall that a partially ordered set $\textbf{M}=(\textbf{M}, \le _\textbf{M})$ with the least element $0_\textbf{M}$ is said to be a Kripke base. For example,

Example 9.2

The set $\mathcal {P}(\textbf{A})$ of all prime filters of a subdirectly irreducible Heyting algebra $\textbf{A}$ together with its set-inclusion relation forms a Kripke base with the least element $\{ 1_\textbf{A} \}$.

Definition 9.8

Let S be a non-empty set. A mapping D of a Kripke base $\textbf{M}$ to $2^S$ is called a domain over $\textbf{M}$, if $\varnothing \ne D(a) \subseteq D(b)$ for all $a,b \in M$ with $a \le b$. A pair $\mathcal {K}=\langle \textbf{M}, D \rangle$ of a Kripke base $\textbf{M}$ and a domain D over $\textbf{M}$ is called a Kripke frame.

Intuitively, each D(a) is the individual domain of the world $a \in \textbf{M}$. For each $a \in \textbf{M}$ and each $b \in \textbf{M}$ with $a \le b$, every sentence of $\mathcal {L}[D(a)]$ is also a sentence of $\mathcal {L}[D(b)]$. A binary relation $\models$ between each $a \in \textbf{M}$ and each atomic sentence of $\mathcal {L}[D(a)]$ is said to be a valuation on $\mathcal {K}=\langle \textbf{M}, D \rangle$, if for every $a,b \in \textbf{M}$ and every atomic sentence A of $\mathcal {L}[D(a)]$, $a \models A$ and $a \le b$ imply $b \models A$. We extend $\models$ to the relation between each $a \in \textbf{M}$ and each sentence of $\mathcal {L}[D(a)]$ inductively as follows:

• $a \models A \wedge B$   if and only if    $a \models A$ and $a \models B$,

• $a \models A \vee B$   if and only if    $a \models A$ or $a \models B$,

• $a \models A \supset B$   if and only if    for every $b \in \textbf{M}$ with $a \le b$, either $b \not \models A$ or $b \models B$,

• $a \models \lnot A$   if and only if    for every $b \in \textbf{M}$ with $a \le b$, $b \not \models A$,

• $a \models \forall xA(x)$   if and only if    for every $b \in \textbf{M}$ with $a \le b$ and every $u \in D(b)$, $b \models A(\overline{u})$,

• $a \models \exists xA(x)$   if and only if    there exists $u \in D(a)$ such that $a \models A(\overline{u})$.

A pair $(\mathcal {K}, \models )$ of a Kripke frame $\mathcal {K}$ and a valuation $\models$ on $\mathcal {K}$ is said to be a Kripke-frame model. A formula A of $\mathcal {L}$ is said to be true in a Kripke-frame model $(\mathcal {K}, \models )$, if $0_{\textbf{M}} \models \overline{A}$ . A formula of $\mathcal {L}$ is said to be valid in a Kripke frame $\mathcal {K}$, if it is true in $(\mathcal {K}, \models )$ for every valuation $\models$ on $\mathcal {K}$. The set of formulas of $\mathcal {L}$ that are valid in $\mathcal {K}$ is denoted by $L(\mathcal {K})$. The following propositions are fundamental properties of Kripke semantics.

Proposition 9.5

For every Kripke-frame model $(\langle \textbf{M}, D \rangle , \models )$, every $a,b \in \textbf{M}$, and every sentence $A \in \mathcal {L}[D(a)]$, if $a \models A$ and $a \le b$, then $b \models A$.

Proposition 9.6

For each Kripke frame $\mathcal {K}$, the set $L(\mathcal {K})$ is a super-intuitionistic predicate logic.

It is well-known that $\textbf{H}_*$ is strongly complete with respect to Kripke frame semantics. That is,

Theorem 9.1

Let $\Gamma$ be a set of sentences of $\mathcal {L}$. If a formula $A(v_1, \dots , v_n)$ of $\mathcal {L}$ having no free variables other than $v_1, \dots , v_n$ is not provable from $\Gamma$ in $\textbf{H}_*$, then there exist a Kripke-frame model $(\langle \textbf{M}, D \rangle , \models )$ and elements $d_1, \dots , d_n \in D(0)$, where 0 is the least element of $\textbf{M}$, such that (1) $0 \models S$ for every $S \in \Gamma$ and (2) $0 \nvDash A(d_1, \dots , d_n)$.

4.2 Pointed Joins of Kripke-Frame Models

Let U and V be non-empty sets, $f : U \rightarrow V$ a mapping. The f induces the translation $\cdot ^f$ from $\mathcal {L}[U]$ to $\mathcal {L}[V]$; for each sentence A of $\mathcal {L}[U]$, the symbol $A^f$ denotes the sentence of $\mathcal {L}[V]$ obtained from A by replacing occurrences of $\overline{u}$ ($u \in U$) by the name $\overline{f(u)}$ of f(u).

Definition 9.9

Let $\mathcal {K}_1=\langle \textbf{M}_1, D_1 \rangle$ and $\mathcal {K}_2=\langle \textbf{M}_2, D_2 \rangle$ be Kripke frames with the least elements $0_1$ and $0_2$, respectively. Take a fresh element 0 and define a Kripke base $\{ 0 \} \uparrow (\textbf{M}_1 \oplus \textbf{M}_2)$ as the partially ordered set obtained from the disjoint union $\textbf{M}_1 \oplus \textbf{M}_2$ of $\textbf{M}_1$ and $\textbf{M}_2$ by adding 0 as the new least element. Then, we define a Kripke frame $0 \uparrow (\mathcal {K}_1\oplus \mathcal {K}_2)$ on $\{ 0 \} \uparrow (\textbf{M}_1 \oplus \textbf{M}_2)$ by associating the domain $D^\uparrow$:

$$ D^\uparrow (a)=\left\{ \begin{array}{ll} D_1(0_1) \times D_2(0_2)&{} \text{ if } a=0,\\ D_1(a) \times D_2(0_2) &{} \text{ if } a \in \textbf{M}_1,\\ D_1(0_1) \times D_2(a) &{} \text{ if } a \in \textbf{M}_2, \end{array} \right. $$

where $U \times V$ denotes the Cartesian product of U and V. The Kripke frame $0 \uparrow (\mathcal {K}_1\oplus \mathcal {K}_2) =(\{ 0 \} \uparrow (\textbf{M}_1\oplus \textbf{M}_2), D^\uparrow )$ is called the pointed join⁵ of $\mathcal {K}_1$ and $\mathcal {K}_2$.

Let $\pi _i:= \{ (\pi _i)_a : D^\uparrow (a) \rightarrow D_i(a) \mathrel {;} a \in \{ 0 \} \cup \textbf{M}_i \}$ $(i =1,2)$ be families of mappings defined by:

$$ (\pi _i)_a((d_1,d_2))=d_i \,\,\, \text{ for } (d_1,d_2) \in D^\uparrow (a) \text{ and } a \in \{ 0 \} \cup \textbf{M}_i. $$

Observe that $\pi _i$ induces translations of $\mathcal {L}[D^\uparrow (a)]$ to $\mathcal {L}[D_i(a)]$ ($a \in \textbf{M}$) or of $\mathcal {L}[D^\uparrow (0)]$ to $\mathcal {L}[D_i(0_i)]$; for every sentence $A \in \mathcal {L}[D^\uparrow (a)]$ (or $A \in \mathcal {L}[D^\uparrow (0)]$), the sentence translated by $\pi _i$ is denoted simply by $A^{\pi _i}$.

Let $\models _1$ and $\models _2$ be valuations on Kripke frames $\mathcal {K}_1=\langle \textbf{M}_1, D_1 \rangle$ and $\mathcal {K}_2=\langle \textbf{M}_2, D_2 \rangle$, respectively. A Kripke-frame model $(0 \uparrow (\mathcal {K}_1\oplus \mathcal {K}_2), \models )$ is said to be the pointed join model of $(\mathcal {K}_1, \models _1)$ and $(\mathcal {K}_2, \models _2)$, if for each $a \in \{0 \} \cup \textbf{M}_1 \oplus \textbf{M}_2$ and each atomic sentence $p((d^1_1,d^1_2), \dots , (d^n_1,d^n_2)) \in \mathcal {L}[D^\uparrow (a)]$,

$$\begin{aligned} a \models p((d^1_1,d^1_2), \dots , (d^n_1,d^n_2))&\\ \text{ if } \text{ and } \text{ only } \text{ if }&\left\{ \begin{array}{ll} a \in \textbf{M}_1 \text{ and } &{} a \models _1 p(d^1_1, \dots , d^n_1),\\ &{}\text{ or }\\ a \in \textbf{M}_2 \text{ and } &{} a \models _2 p(d^1_2, \dots , d^n_2). \end{array} \right. \end{aligned}$$

Then, the following Lemma clearly holds.

Lemma 9.7

Let $(0 \uparrow (\mathcal {K}_1\oplus \mathcal {K}_2), \models )$ be the pointed join model of $(\mathcal {K}_1, \models _1)$ and $(\mathcal {K}_2, \models _2)$. For each $i =1,2$ and each $a \in \textbf{M}_i$, it holds that

$$ \text{ for } \text{ every } A \in \mathcal {L}[D^\uparrow (a)], \,\,\, a \models A \, \text{ if } \text{ and } \text{ only } \text{ if } \, a \models _i A^{\pi _i}. $$

Definition 9.10

A formula A is said to be axiomatically true in a Kripke-frame model $(\mathcal {K},\models )$, if all of the substitution instances of A in the language $\mathcal {L}$ are true in $(\mathcal {K},\models )$.

A formula A is said to be pointed-join robust, if A is true in Kripke-frame models $(\mathcal {K}_1, \models _1)$ and $(\mathcal {K}_2, \models _2)$, then A is true in the pointed join model of them.

If the axiomatic truth of a formula A is preserved under the pointed-join construction of two Kripke models, then $\textbf{H}_*+A$ has DP. More precisely,

Theorem 9.2

(cf. Minari 1986 and Nakamura 1983) Let A be a formula of $\mathcal {L}$ satisfying:

$(*)$ every substitution instance of A is pointed-join robust.

Then $\textbf{H}_*+A$ has DP.

Proof

Suppose that $\textbf{H}_*+A \nvdash B_1$ and $\textbf{H}_*+A \nvdash B_2$. We show $\textbf{H}_*+A \nvdash B_1 \vee B_2$. Without loss of generality, we may assume that $B_1$ and $B_2$ contain no free variables other than $v_1, \dots , v_m$, and we write $B_i$ as $B_i(v_1, \dots , v_m)$ ($i=1,2$). By the strong completeness theorem of $\textbf{H}_*$ with respect to Kripke-frame models (i.e., Theorem 9.1), we have two Kripke-frame models $(\langle \textbf{M}_1, D_1 \rangle , \models _1)$ and $(\langle \textbf{M}_2, D_2 \rangle , \models _2)$, and elements $d^1_i, \dots , d^m_i \in D_i(0_i)$, where $0_i$ is the least element of $\textbf{M}_i$ ($i=1,2$), such that A is axiomatically true in both of them and $0_i \not \models _i B_i(d^1_i, \dots , d^m_i)$ ($i=1,2$). Take the pointed join model $(\mathcal {K}, \models )$ of them. By ($*$), we have that A is axiomatically true in $(\mathcal {K}, \models )$. By Lemma 9.7, we have $0_i \not \models B_i((d^1_1,d^1_2), \dots , (d^m_1, d^m_2))$ ($i=1,2$), and hence $0 \not \models B_i((d^1_1,d^1_2), \dots , (d^m_1, d^m_2))$ ($i=1,2$), where 0 is the least element of $\mathcal {K}$. Therefore, $0 \not \models (B_1 \vee B_2)((d^1_1,d^1_2), \dots , (d^m_1, d^m_2))$. Thus we have $\textbf{H}_*+A \nvdash B_1 \vee B_2$.$\square$

We can show the following in the same way as the above.

Corollary 9.2

Let $\Gamma$ be a set of formulas satisfying the condition $(*)$ in Theorem 9.2. Then $\textbf{H}_*+ \Gamma$ has DP.

Lemma 9.8

Let p be a unary predicate variable, S a sentence. Then, $\exists x(S \wedge p(x) \supset \forall yp(y))$ satisfies the condition $(*)$ in Theorem 9.2.

Proof

Suppose otherwise. Then, there exist a substitution instance I of $\exists x(S \wedge p(x) \supset \forall yp(y))$ and Kripke-frame models $(\langle \textbf{M}_1, D_1 \rangle , \models _1)$ and $(\langle \textbf{M}_2, D_2 \rangle , \models _2)$ such that I is true in both of them but I is not true in the pointed join model $(0 \uparrow (\langle \textbf{M}_1, D_1 \rangle \oplus \langle \textbf{M}_2, D_2 \rangle ), \models )$. We may assume that the I contains no free variables other than $v_1, \dots , v_n$, and these variables are distinct from x and y. There exist two formulas $B(v_1, \dots , v_n)$ and $C(w, v_1, \dots , v_n)$ of $\mathcal {L}$ having no free variables other than $v_1, \dots , v_n$ and $w, v_1, \dots , v_n$, respectively, such that I is obtained from $\exists x(S \wedge p(x) \supset \forall yp(y))$ by substituting $C(w, v_1, \dots , v_n)$ to all occurrences of p(w) (here w is a fresh variable) and replacing S by $B(v_1, \dots , v_n)$. Thus, I is of the form:

$$ \exists x(B(v_1, \dots , v_n) \wedge C(x, v_1, \dots , v_n) \supset \forall yC(y, v_1, \dots , v_n)). $$

For the sake of simplicity, we assume $n=1$. Since I is not true in the pointed join model, there exist an element $a \in \{ 0 \} \uparrow \textbf{M}_1 \oplus \textbf{M}_2$ and a $d \in D^\uparrow (a)$ such that $a \nvDash \exists x(B(d) \wedge C(x,d) \supset \forall yC(y, d))$. Suppose $a \in \textbf{M}_1$. Then, by Lemma 9.7, it holds that $a \nvDash _1 \exists x(B(\pi _1(d)) \wedge C(x,\pi _1(d)) \supset \forall yC(y, \pi _1(d)))$. This contradicts the assumption that I is true in $(\langle \textbf{M}_1, D_1 \rangle , \models _1)$. Therefore, $a \not \in \textbf{M}_1$. Similarly, we have $a \not \in \textbf{M}_2$, and hence $a =0$. Since $0_i \models _i \exists x(B(\pi _i(d)) \wedge C(x,\pi _i(d)) \supset \forall yC(y, \pi _i(d)))$ for $i=1,2$, there exist $s_1 \in D_1(0_1)$ and $s_2 \in D_2(0_2)$ such that $0_i \models _i B(\pi _i(d)) \wedge C(s_i,\pi _i(d)) \supset \forall yC(y, \pi _i(d))$ ($i=1,2$). Therefore, by Lemma 9.7, we have $0_i \models B(d) \wedge C((s_1,s_2),d) \supset \forall yC(y, d)$ ($i=1,2$).

Now we have two cases: $0 \not \models B(d) \wedge C((s_1,s_2),d)$ and $0 \models B(d) \wedge C((s_1,s_2),d)$. The former case implies $0 \models B(d) \wedge C((s_1,s_2),d) \supset \forall yC(y, d)$. That is, $0 \models \exists x( B(d) \wedge C(x,d) \supset \forall yC(y, d))$. Next, we assume the latter case where $0 \models B(d) \wedge C((s_1,s_2),d)$. Then, we have $0_i \models B(d) \wedge C((s_1,s_2),d)$, and hence $0_i \models \forall yC(y, d)$ ($i=1,2$). If it holds that $0 \models C(t, d)$ for every $t \in D^\uparrow (0)$, then we have that $0 \models \forall yC(y,d)$, and hence we trivially have $0 \models B(d) \wedge C((s_1,s_2),d) \supset \forall yC(y, d)$. That is, we have $0 \models \exists x( B(d) \wedge C(x,d) \supset \forall yC(y, d))$. Thus we have that there exists $t \in D^\uparrow (0)$ such that $0 \not \models C(t, d)$. Consider the sentence $B(d) \wedge C(t,d) \supset \forall yC(y, d)$. We have that $0 \not \models B(d) \wedge C(t,d)$, and that $m \models \forall yC(y, d)$ for every $m \ne 0$. Hence, we have that $0 \models B(d) \wedge C(t,d) \supset \forall yC(y, d)$. Therefore, it holds that $0 \models \exists x(B(d) \wedge C(x,d) \supset \forall yC(y, d))$. This contradicts the assumption.$\square$

We give here a proof of a result of Minari (1986) and Nakamura (1983) in this setting.

Corollary 9.3

(cf. Minari 1986 and Nakamura 1983) $\textbf{H}_*+\exists x(p(x) \supset \forall yp(y))$ has DP but lacks EP.

Proof

Take a fresh propositional variable q. Then, $\exists x(p(x) \supset \forall yp(y))$ is equivalent to $\exists x( (q \supset q) \wedge p(x) \supset \forall yp(y))$ in $\textbf{H}_*$. By Lemma 9.8, $\exists x(p(x) \supset \forall yp(y))$ satisfies the condition $(*)$ in Theorem 9.2, and hence we have the conclusion.$\square$

Now, we prove Lemma 9.6. Let $\mathcal {S}$ be a set of finite non-degenerate subdirectly irreducible Heyting algebras. Recall that $QJ(\textbf{A})$ ($\textbf{A} \in \mathcal {S}$) is of the form $\exists v (S \supset (p(v) \supset \forall yp(y)))$ with S being a sentence. Then, $QJ(\textbf{A})$ is equivalent to $\exists v (S \wedge p(v) \supset \forall yp(y))$. From Lemma 9.8, it follows that $QJ(\textbf{A})$ satisfies the condition $(*)$ in Theorem 9.2. By Corollary 9.2, it holds that $\textbf{H}_*+ \{QJ(\textbf{A}) \mathrel {;} \textbf{A} \in \mathcal {S}\}$ has DP. This completes the proof of Lemma 9.6.

5 Strongly Independent Sequence of Modified Jankov Formulas—Jankov’s Method for Predicate Logics

In this section, we show the following Lemma 9.9, and then the main Theorem (Theorem 9.4). Recall that $\{ \textbf{H}_i \}_{i<\omega }$ is the sequence of finite subdirectly irreducible Heyting algebras introduced in Sect. 9.3.2 and that $\{ \textbf{H}_i \}_{i<\omega }$ satisfies three conditions (A1), (A2) (in Sect. 9.3.1), and (A3) (in Sect. 9.3.2).

Lemma 9.9

$\{QJ(\textbf{H}_i) \}_{i<\omega }$ is strongly independent.

For the proof, we use algebraic Kripke sheaf semantics for super-intuitionistic predicate logics. The algebraic Kripke sheaf is a framework for extended semantics obtained from a Kripke base equipped with a domain-sheaf and a truth-value-sheaf. A domain-sheaf is a covariant functor which integrates interpretations of equality into Kripke semantics for predicate logics.⁶ A truth-value-sheaf is a contravariant functor which provides each possible world with an algebraic structure of “truth values” at the world.⁷ In this paper, we use a simplified version of algebraic Kripke sheaves, called $\Omega$-brooms, and apply a result in Suzuki (1999).

In Sect. 9.5.1, our simplified algebraic Kripke sheaf semantics is introduced. In Sect. 9.5.2, toolkit (a definition, lemmata, and notation) needed later is presented. In Sect. 9.5.3, we prove Lemma 9.9 and then Theorem 9.4.

5.1 Special Algebraic Kripke Sheaves

Definition 9.11

(cf. Suzuki 1999) A Kripke base $\textbf{M}$ can be regarded as a category in the usual way. A covariant functor D from a Kripke base $\textbf{M}$ to the category of all non-empty sets is called a domain-sheaf over $\textbf{M}$, if $D(0_\textbf{M})$ is non-empty. That is,

• (DS1) $D(0_\textbf{M})$ is a non-empty set,

• (DS2) for every $a, b \in \textbf{M}$ with $a\le _\textbf{M} b$, there exists a mapping $D_{ab} : D(a) \rightarrow D(b)$,

• (DS3) $D_{aa}$ is the identity mapping of D(a) for every $a \in \textbf{M}$,

• (DS4) $D_{ac}=D_{bc} \circ D_{ab}$ for every $a,b,c \in \textbf{M}$ with $a \le _\textbf{M} b \le _\textbf{M} c$.

Intuitively, D(a) is the set of individuals at the world $a \in \textbf{M}$. For each $d \in D(a)$ and each $b \in \textbf{M}$ with $a \le _\textbf{M} b$, the element $D_{ab}(d)$ $\in D(b)$ is said to be the inheritor of d at b. According to this intuition, each A ($\in \mathcal {L}[D(a)]$) with $a \le _\textbf{M} b$ has its unique inheritor $A^{D_{ab}}$ ($\in \mathcal {L}[D(b)]$). The $A^{D_{ab}}$ is denoted simply by $A_{a,b}$. In this paper, we deal only with domain-sheaves with the following additional condition:

• (DS5) for every $a \in \textbf{M}$, $D(a) = \left\{ \begin{array}{ll} \omega \, (=\{ 0,1, \dots \})&{} \text{ if } a=0_\textbf{M}, \\ \{0 \} &{} \text{ otherwise. } \end{array} \right.$

Thus, $D_{ab}$’s are trivially determined as follows:

$$D_{ab}(i)=\left\{ \begin{array}{ll} i &{} \text{ if } a=b=0_\textbf{M}, \\ 0 &{} \text{ otherwise, } \end{array} \right. $$

for every $i \in D(a)$. Then, for every $a \ne 0_\textbf{M}$, the inheritor $A_{a,b}$ of $A \in \mathcal {L}[D(a)]$ at b is identical to A.

The category $\mathcal {H}$ of all non-degenerate complete Heyting algebras with arrows being complete monomorphisms between complete Heyting algebras. A contravariant functor P from a Kripke base $\textbf{M}$ to the category $\mathcal {H}$ is called a truth-value-sheaf over $\textbf{M}$. That is,

• (TVS1) $P_a$ is a non-degenerate complete Heyting algebra: $P(a)=( P(a), \cap ^a, \cup ^a, \rightarrow ^a, 0^a, 1^a )$,

• (TVS2) for every $a, b \in \textbf{M}$ with $a\le _\textbf{M} b$, there exists a complete monomorphism $P_{ab} : P(b) \rightarrow P(a)$,

• (TVS3) $P_{aa}$ is the identity mapping of P(a) for every $a \in \textbf{M}$,

• (TVS4) $P_{ac}=P_{ab} \circ P_{bc}$ for every $a,b,c \in \textbf{M}$ with $a \le _\textbf{M} b \le _\textbf{M} c$.

A triple $\mathcal {K}=\langle \textbf{M}, D, P\rangle$ of a Kripke base $\textbf{M}$, a domain-sheaf D over $\textbf{M}$, and a truth-value-sheaf P over $\textbf{M}$ is called an algebraic Kripke sheaf. Intuitively, P(a) is the set of truth values at a. If $a \le _\textbf{M} b$ (i.e., b is accessible from a), the $P_{ab}$ sends computations of truth values in P(b) into P(a).

Let $\Omega$ be $\{ 1/n \mathrel {;} n =1,2,\dots \} \cup \{ 0 \}$. With the natural ordering, $\Omega$ is a complete Heyting algebra having the greatest element 1 and the least element 0. The lattice order on $\Omega$ is denoted by $\le _\Omega$ or simply $\le$. In this paper, we deal only with algebraic Kripke sheaves with the following condition:

• (TVS5) for every $a \in \textbf{M}$, $P(a) =\left\{ \begin{array}{ll} \Omega &{} \text{ if } a=0_\textbf{M}, \\ \textbf{2}&{} \text{ otherwise. } \end{array} \right.$

Thus, $P_{ab}$’s are essentially set-inclusions up to the identification: $1_\textbf{2}=1=1_\mathbf {\Omega }$ and $0_\textbf{2}=0=0_\mathbf {\Omega }$. Then, our algebraic Kripke sheaves are characterized by the Kripke base $\textbf{M}$. Moreover, by (DS5), we may regard our algebraic Kripke sheaf as a Kripke frame for propositional logics, except at the least element $0_\textbf{M}$ of its Kripke base. To make the difference clear, we will call an algebraic Kripke sheaf satisfying (DS5) and (TV5) an $\Omega$-broom. An $\Omega$-broom having $\textbf{M}$ as its Kripke base is denoted by $\mathcal {B}(\textbf{M})$.

A mapping V which assigns each pair (a, A) of an $a \in \textbf{M}$ and an atomic sentence $A \in \mathcal {L}[D(a)]$ to an element V(a, A) of P(a) is said to be a valuation on $\langle \textbf{M}, D, P \rangle$, if $a \le _\textbf{M} b$ implies $V(a,A) \le ^a P_{ab}(V(b,A_{a,b}))$, where $\le ^a$ is the lattice order of P(a). In our setting, P(a)’s are all trivial subalgebras of $\Omega =P(0_\textbf{M})$, and $P_{ab}$’s are set-inclusions. Thus, this condition can be written simply as: $a \le _\textbf{M} b$ implies $V(a,A) \le _\Omega V(b,A_{a,b})$. We extend V to the mapping which assigns to each pair (a, A) of an $a \in \textbf{M}$ and a sentence $A \in \mathcal {L}[D(a)]$ an element V(a, A) of P(a) as follows:

• $V(a, A \wedge B)=V(a, A) \cap V(a, B)$,

• $V(a, A \vee B)=V(a, A) \cup V(a, B)$,

• $V(a, A \supset B)=\bigcap _{b: a \le _\textbf{M} b}(V(b,A_{a,b}) \rightarrow V(b,B_{a,b}))$,

• $V(a,\lnot A)=\bigcap _{b: a \le _\textbf{M} b}(V(b,A_{a,b}) \rightarrow 0)$,

• $V(a,\forall xA(x))= \bigcap _{b: a \le _\textbf{M} b}\bigcap _{u \in D(b)}V(b,A_{a,b}(\overline{u}))$,

• $V(a,\exists xA(x))= \bigcup _{u \in D(a)}V(a,A(\overline{u}))$.

Note that operations of Heyting algebra in the right hand sides are those of $\Omega$. In the original definition in Suzuki (1999), these induction steps, especially of $\supset$, $\lnot$, and $\forall$, are slightly more complicated. However, by the virtue of (TV5), these simple steps work well.⁸

A pair $(\mathcal {B}, V)$ of an $\Omega$-broom $\mathcal {B}$ and a valuation V on it is said to be an $\Omega$-broom model (in the general case, an algebraic Kripke-sheaf model). A formula A of $\mathcal {L}$ is said to be true in an $\Omega$-broom model $(\mathcal {B}, V)$, if $V(0_{\textbf{M}}, \overline{A})=1$. A formula of $\mathcal {L}$ is said to be valid in an $\Omega$-broom $\mathcal {B}$, if it is true in $(\mathcal {B}, V)$ for every valuation V on $\mathcal {B}$. The set of formulas of $\mathcal {L}$ that are valid in $\mathcal {B}$ is denoted by $L(\mathcal {B})$ . The following propositions are fundamental properties of algebraic Kripke sheaf semantics (cf. Suzuki 1999).

Proposition 9.7

(cf. Proposition 9.5) For every $\Omega$-broom model $(\mathcal {B}(\textbf{M}), V)$, every $a,b \in \textbf{M}$, and every sentence $A \in \mathcal {L}[D(a)]$, if $a \le _\textbf{M} b$, then $V(a,A) \le _{\Omega } V(b,A_{a,b})$.

Proposition 9.8

(cf. Propositions 9.4 and 9.6) For each $\Omega$-broom $\mathcal {B}$, the set $L(\mathcal {B})$ is a super-intuitionistic predicate logic.

5.2 Toolkit for $\Omega$-Brooms

Definition 9.12

(cf. Suzuki 1999) Let $\textbf{M}$ be a finite Kripke base. Take the Jankov formula $J(\mathcal {O}(\textbf{M}))$ and replace all occurrences of $p_{\star _{\mathcal {O}(\textbf{M})}}$ in $J(\mathcal {O}(\textbf{M}))$ by F (i.e., $\exists x(p(x) \supset \forall yp(y))$). Then, we denote the resulting sentence by $J(\textbf{M};F)$.

The following Lemma gives the relationship between $QJ(\mathcal {O}(\textbf{M}))$ and $J(\textbf{M};F)$ in $\Omega$-brooms.

Lemma 9.10

In every $\Omega$-broom, the sentence $(q \supset \exists xr(x))\supset \exists x(q \supset r(x))$ is valid, where q and r are a propositional variable and a unary predicate variable, respectively.

Proof

Let C and D be $q \supset \exists xr(x)$ and $\exists x(q \supset r(x))$, respectively. Let V be an arbitrary valuation on an $\Omega$-broom $\mathcal {B}(\textbf{M})=\langle \textbf{M}, D,P \rangle$. Note that for each $b \ne 0_\textbf{M}$, we have that $V(b,\exists xr(x))=V(b,r(0))$ and that the inheritor $r(i)_{0_\textbf{M},b}$ of r(i) at b is r(0) for every $i \in \omega =D(0_\textbf{M})$. Then, for every $b \ne 0_\textbf{M}$, we have

$$\begin{aligned} V(b, C)&= \bigcap \{ V(c,q) \rightarrow V(c,\exists xr(x)) \mathrel {;} c \ge b \} \\&= \bigcap \{ V(c,q) \rightarrow V(c,r(0)) \mathrel {;} c \ge b \} \\&= V(b,q \supset r(0))\\&= V(b,\exists x(q \supset r(x)) )\\&= V(b,D) . \end{aligned}$$

Hence, it holds that $V(0_\textbf{M},C \supset D)= \bigcap \big [ \{V(0_\textbf{M},C) \rightarrow V(0_\textbf{M},D)\}\cup \{V(b,C) \rightarrow V(b,D )\mathrel {;} b \ne 0_\textbf{M} \} \big ] =V(0_\textbf{M},C) \rightarrow V(0_\textbf{M},D)$. Therefore, it suffices to show that $V(0_\textbf{M},C) \le V(0_\textbf{M},D)$. Let us check the value $V(0_\textbf{M}, C)$:

$$\begin{aligned}&{V(0_\textbf{M}, C)}\\&= V(0_\textbf{M}, q \supset \exists xr(x))\\&= \bigcap \{ V(a,q) \rightarrow V(a,\exists xr(x)) \mathrel {;} a \in \textbf{M}\}\\&= \bigcap \big [ \{V(0_\textbf{M},q) \rightarrow V(0_\textbf{M},\exists xr(x))\} \cup \{V(b,q) \rightarrow V(b,\exists xr(x))\mathrel {;} b \ne 0_\textbf{M} \} \big ] \\&= \bigcap \big [ \{V(0_\textbf{M},q) \rightarrow V(0_\textbf{M},\exists xr(x)) \cup \{V(b,q) \rightarrow V(b,r(0))\mathrel {;} b \ne 0_\textbf{M} \} \big ] . \end{aligned}$$

We have two cases: (1) $V(b, q) \rightarrow V(b,r(0))=0$ for some $b \ne 0_\textbf{M}$, and (2) $V(b, q) \rightarrow V(q,r(0))=1$ for every $b \ne 0_\textbf{M}$.

Suppose that (1) holds. Since 0 belongs to $\{ V(b,q) \rightarrow V(b,r(0))\mathrel {;} b \ne 0_\textbf{M} \}$, we have $V(0_\textbf{M},C) =0 \le V(0_\textbf{M},D)$. Next, suppose that (2) holds. Since $\{ V(b,q) \rightarrow V(b,r(0))\mathrel {;} b \ne 0_\textbf{M} \}=\{ 1 \}$, we have $V(0_\textbf{M},C)=V(0_\textbf{M},q) \rightarrow V(0_\textbf{M},\exists xr(x))$. Since $V(0_\textbf{M},\exists xr(x))=\max _{i \in \omega } \{V(0_\textbf{M},r(i))\}$, there exists an $i_0 \in \omega$ such that $V(0_\textbf{M},\exists xr(x))=V(0_\textbf{M},r(i_0))$. Hence, it holds that

$$ V(0_\textbf{M},C)= \left\{ \begin{array}{ll} V(0_\textbf{M},r(i_0)) &{} \text{ if } V(0_\textbf{M},r(i_0)) < V(0_\textbf{M},q),\\ 1 &{} \text{ if } V(0_\textbf{M},q)\le V(0_\textbf{M},r(i_0)). \end{array} \right. $$

To calculate $V(0_\textbf{M},D)$, we put

$$ v_i=V(0_\textbf{M},q \supset r(i)) $$

for each $i \in \omega$, and we have $V(0_\textbf{M},D)=\max _{i \in \omega }v_i$. Let us check the value $v_i$:

$$\begin{aligned} v_i&= V(0_\textbf{M}, q \supset r(i))\\&= \bigcap \{ V(a,q) \rightarrow V(a,r(i)_{0_\textbf{M},a}) \mathrel {;} a \in \textbf{M}\}\\&= \bigcap \big [ \{V(0_\textbf{M},q) \rightarrow V(0_\textbf{M},r(i))\} \cup \{V(b,q) \rightarrow V(b,r(0))\mathrel {;} b \ne 0_\textbf{M} \} \big ] . \end{aligned}$$

By the assumption (2), it holds that $\{V(b,q) \rightarrow V(b,r(0))\mathrel {;} b \ne 0_\textbf{M} \} =\{1 \}$. Therefore, we have $v_i=V(0_\textbf{M},q) \rightarrow V(0_\textbf{M},r(i))$. If $V(0_\textbf{M},r(i_0)) < V(0_\textbf{M},q)$, we have $V(0_\textbf{M},C)=V(0_\textbf{M},r(i_0))=v_{i_0}\le \max _{i\in \omega } v_i=V(0_\textbf{M},D)$. If $V(0_\textbf{M},q)\le V(0_\textbf{M},r(i_0))$, we have $v_{i_0}=1=V(0_\textbf{M},D) \ge V(0_\textbf{M},C)$.$\square$

From this Lemma and Proposition 9.8, it follows that $(A \supset \exists xB(x)) \supset \exists x(A \supset B(x))$ is valid in every $\Omega$-broom model, where A does not contain x as a free variable. Thus, we have the⁹

Lemma 9.11

In every $\Omega$-broom model, $J(\textbf{M};F) \supset QJ(\mathcal {O}(\textbf{M}))$ is valid.

Next we recall a Lemma in Suzuki (1999). We describe the Lemma in the setting of the present paper.¹⁰ This Lemma asserts that $QJ(\mathcal {O}(\textbf{M}))$ and $J(\textbf{M};F)$ have a property similar to that of the original Jankov formula shown in Lemma 9.1.

Lemma 9.12

(cf. Lemma 9.1 and Suzuki 1999; Lemma 4.10) Let $\textbf{M}$ be a finite Kripke base such that $\mathcal {O}(\textbf{M})$ satisfies the condition (A3) in Sect. 9.3.2. For each $\Omega$-broom $\mathcal {B}(\textbf{N})$ with $\textbf{N}$ having at least two elements, if $QJ(\mathcal {O}(\textbf{M})) \not \in L(\mathcal {B}(\textbf{N}))$, then $\mathcal {O}(\textbf{M})$ is embeddable into a quotient algebra of $\mathcal {O}(\textbf{N})$.

Proof

(Sketch) Suppose that $QJ(\mathcal {O}(\textbf{M})) \not \in L(\mathcal {B}(\textbf{N}))$. Then, by Lemma 9.11, we have $J(\textbf{M};F) \not \in L(\mathcal {B}(\textbf{N}))$. Since $J(\textbf{M};F)$ is obtained from $J(\mathcal {O}(\textbf{M}))$ by replacing $p_{\star _\textbf{M}}$ by the sentence F, the original Jankov formula $J(\mathcal {O}(\textbf{M}))$ is not valid in $\mathcal {B}(\textbf{N})$. This implies that $J(\mathcal {O}(\textbf{M}))$ is not valid in the Heyting algebra¹¹ $\big (\mathcal {O}(\textbf{M})/\star \big ) \oplus \Omega$. From Lemma 9.1, it follows that $\mathcal {O}(\textbf{M})$ is embeddable into a quotient algebra of $\big (\mathcal {O}(\textbf{M})/\star \big ) \oplus \Omega$. By (A3), we have that $\mathcal {O}(\textbf{M})$ is embeddable into a quotient algebra of $\mathcal {O}(\textbf{N})$.$\square$

Lemma 9.13

Let $\textbf{M}$ be a finite Kripke base. Then $QJ(\mathcal {O}(\textbf{M}))$ is not valid in $\mathcal {B}(\textbf{M})$.

Proof

Let $\mathcal {B}(\textbf{M})$ be $\langle \textbf{M},D,P\rangle$. Define a valuation V by

$$ V(a,p_O)=\left\{ \begin{array}{ll} 1 &{} \text{ if } a \in O,\\ 0 &{} \text{ if } a \not \in O, \end{array} \right. $$

for every $a \in \textbf{M}$ and every $O \in \mathcal {O}(\textbf{M})$, and

$$ V(a,p(i))= \left\{ \begin{array}{ll} 1 &{} \text{ if } a \ne 0_\textbf{M},\\ 1 / (i+1) &{} \text{ if } a = 0_\textbf{M}, \end{array} \right. $$

for every $a \in \textbf{M}$ and every $i \in D(a)$. Take an $a \ne 0_\textbf{M}$. Since $V(a, \forall yp(y))=\bigcap _{b \ge a} V(b, p(0)) =1$, we have that $V(a, F)= V(a, p(0) \supset \forall yp(y)) =\bigcap _{b \ge a } (1 \rightarrow V(b, \forall yp(y))\, ) = \bigcap _{b \ge a } V(b, \forall yp(y)) =1$. Thus, it holds that $V(a, p(0) \supset \forall yp(y))=V(a,F)= 1$ for every $a \ne 0_\textbf{M}$. Next, check that $V(0_\textbf{M},\forall yp(y))\le \bigcap _{i \in \omega }V(0_\textbf{M},p(i))=0$. For a fixed $i \in \omega$, we have that $V(0_\textbf{M}, p(i) \supset \forall yp(y)) =\bigcap _{a \in \textbf{M}} \{ V(a, p(i)_{0_\textbf{M},a}) \rightarrow V(a,\forall yp(y))\} \le V(0_\textbf{M}, p(i)) \rightarrow V(0_\textbf{M},\forall yp(y)) =1/(i+1) \rightarrow 0=0$. Thus, we have $V(0_\textbf{M},F)=0$.

Consider an assignment v on $\mathcal {O}(\textbf{M})$ defined by

$$ v(p_O)=\left\{ \begin{array}{ll} \{ a \mathrel {;} V(a,p_O)=1 \} &{} \text{ if } O \ne \textbf{M} \setminus \{ 0_\textbf{M}\},\\ \{ a \mathrel {;} V(a,F)=1 \} &{} \text{ if } O = \textbf{M} \setminus \{ 0_\textbf{M}\}, \end{array} \right. $$

for every $O \in \mathcal {O}(\textbf{M})$. Then, v is nothing but the assignment $v_\mathbf {\mathcal {O}(\textbf{M})}$ that makes the Jankov formula not true in $\mathcal {O}(\textbf{M})$.

Claim. Let X be a propositional formula having no propositional variable other than $\{ p_O \mathrel {;} O \in \mathcal {O}(\textbf{M}) \}$ . By $X'$ , we denote the formula obtained from X by replacing all occurrences of $p_{\star _{\mathcal {O}(\textbf{M})}}$ by the sentence F . Then, we have $V(a,X') \in \{ 0,1 \}$ for every $a \in \textbf{M}$ and that $v(X)=\{a \mathrel {;} V(a,X')=1 \}$ .

This Claim can be proved by induction on the length of X. The Basis-part is already clear by the discussion just after the definition of V. We check the Induction Steps. Suppose that X is of the form $Y \supset Z$. Take an arbitrary $a \in v(Y \supset Z)$. Then for every $b \ge a$, either $b \not \in v(Y)$ or $b \in v(Z)$. By the induction hypothesis, we have that $\{V(b,Y'), V(b,Z')\}\subseteq \{0,1\}$ for every $b \in \textbf{M}$, and $v(Y)=\{ c \mathrel {;} V(c, Y')=1 \}$ and $v(Z)=\{ c \mathrel {;} V(c, Z')=1 \}$. Thus, for every $b \ge a$, either $V(b,Y')=0$ or $V(b,Z')=1$. Therefore, we have $V(b,Y')\rightarrow V(b,Z')=1$ for every $b \ge a$, and hence $V(a, Y' \supset Z')=1$. Next take an arbitrary $b \not \in v(Y \supset Z)$. There exists $b \ge a$ such that $b \in v(Y)$ and $b \not \in v(Z)$. By the induction hypothesis, we have $V(b, Y')=1$ and $V(b, Z')=0$. Thus, $V(a, Y'\supset Z')=0$. Therefore, for every $a \in \textbf{M}$, we have $V(a, Y' \supset Z') \in \{0,1\}$ and $v(Y \supset Z)=\{ a \mathrel {;} V(a, Y' \supset Z')=1 \}$. Other cases can be proved similarly. This completes the proof of the Claim.

From this Claim, it follows that $\textbf{M}=1_{\mathcal {O}(\textbf{M})} =v(\bigwedge \delta (\mathcal {O}(\textbf{M}))) =\{a \mathrel {;} V(a, \bigwedge \Delta (\mathcal {O}(\textbf{M})))=1\}$. That is, we have $V(a,\bigwedge \Delta (\mathcal {O}(\textbf{M})))=1$ for every $a \in \textbf{M}$. Note that $V(0_\textbf{M},QJ(\mathcal {O}(\textbf{M}))= \max _{i \in \omega } \{ V(0_\textbf{M},\bigwedge \Delta (\mathcal {O}(\textbf{M})) \supset (p(i) \supset \forall yp(y))) \}$. Let us check for an $i \in \omega$:

$$\begin{aligned}&{V(0_\textbf{M},\bigwedge \Delta (\mathcal {O}(\textbf{M})) \supset (p(i) \supset \forall yp(y)))} \\&= \bigcap \{V(a, \bigwedge \Delta (\mathcal {O}(\textbf{M}))) \rightarrow V(a,(p(i) \supset \forall yp(y))_{0_\textbf{M},a}) \mathrel {;} a \in \textbf{M} \} \\&=\bigcap \{ V(a,(p(i) \supset \forall yp(y))_{0_\textbf{M},a}) \mathrel {;} a \in \textbf{M} \} \\&\le V(0_\textbf{M},p(i) \supset \forall yp(y)) \\&=0 \end{aligned}$$

Therefore, we have $V(0_\textbf{M},QJ(\mathcal {O}(\textbf{M}))=0$.$\square$

As we already mentioned in Examples 9.1 and 9.2, we have the correspondence between subdirectly irreducible Heyting algebras and Kripke bases. When they are finite, we have more exact correspondence:

Fact 9.3

(1) For each finite subdirectly irreducible Heyting algebra $\textbf{A}$, the $\mathcal {O}\mathcal {P}(\textbf{A})$ is isomorphic to $\textbf{A}$.

(2) For each finite Kripke base $\textbf{M}$, the $\mathcal {P}\mathcal {O}(\textbf{M})$ is isomorphic to $\textbf{M}$.

Thus, we may identify finite subdirectly irreducible Heyting algebras and finite Kripke bases. In the rest of this paper, we denote by $\textbf{N}_i$ the Kripke base corresponding to $\textbf{H}_i$ ($i < \omega$). That is, $\textbf{N}_i=\mathcal {P}(\textbf{H}_i)$ and $\textbf{H}_i=\mathcal {O}(\textbf{N}_i)$ for each $i< \omega$.

5.3 Proofs of Lemma 9.9 and the Main Theorem

The proof of Lemma 9.9 proceeds similarly to the proof of Corollary 9.1 by the virtue of the discussion of the previous subsection. Define $\textbf{L}_i=\textbf{H}_*+QJ(\textbf{H}_{i})$ for each $i<\omega$. We show that $\{ \textbf{L}_i \}_{i<\omega }$ is strongly independent. Pick an arbitrary $i_0 \in \omega$. Then, for every $j \ne i_0$, the $\textbf{H}_j$ is not embeddable into any quotient algebra of $\textbf{H}_{i_0}$. Thus, by Lemma 9.12, it holds that $QJ(\textbf{H}_j) \in L(\mathcal {B}(\textbf{N}_{i_0}))$ for every $j \ne i_0$. Therefore, $\bigcup _{j \ne i_0}\textbf{L}_j \subseteq L(\mathcal {B}(\textbf{N}_{i_0}))$. By Lemma 9.13, we have $QJ(\textbf{N}_{i_0}) \not \in L(\mathcal {B}(\textbf{N}_{i_0}))$. Hence, $\textbf{L}_{i_0} \nsubseteq \bigcup _{j \ne i_0}\textbf{L}_j$. This completes the proof of Lemma 9.9.

Theorem 9.4

(Main Theorem) There exits a continuum of PEI’s having disjunction property but lacking existence property.

Proof

By Lemma 9.2, for every $I \subseteq \omega$, the logic $\textbf{H}_*+ \{ QJ(\textbf{H}_i) \, ; i \in I \}$ is a PEI lacking EP. By Lemma 9.6, for every $I \subseteq \omega$, this logic has DP. By Lemma 9.9, $\{ QJ(\textbf{H}_i) \}_{i < \omega }$ is strongly independent. Thus, we have the conclusion.$\square$

By examining the definition of $\{QJ(\textbf{H}_i) \mathrel {;} i < \omega \}$, we have shown that $\{QJ(\textbf{H}_i) \mathrel {;} i < \omega \}$ is a recursively enumerable sequence of concrete predicate axioms schemata.

Corollary 9.4

There exits a continuum of PEI’s having none of DP and EP.

Let $Lin^*$ be $(q(x) \supset q(y))\vee (q(y) \supset q(x))$, where q is a fresh unary predicate variable. Then, it is obvious that $\textbf{H}_*+Lin^*$ is a PEI without DP. We have the

Lemma 9.14

$Lin^*$ is valid in every $\Omega$-broom $\mathcal {B}$.

Proof

Let V be a valuation on $\mathcal {B}(\textbf{M})$. If $a \in \textbf{M}$ and $a \ne 0_\textbf{M}$, the inheritors of $\forall y ((p(i)\supset p(y)) \vee (p(y) \supset p(i))$, $(p(i)\supset p(j)) \vee (p(j)\supset p(i))$, and $p(i)\supset p(j) \in \mathcal {L}[D(0_\textbf{M})]$ at a are $\forall y ((p(0)\supset p(y)) \vee (p(y) \supset p(0))$, $(p(0)\supset p(0)) \vee (p(0)\supset p(0))$, and $p(0) \supset p(0)$, respectively. Clearly, $V(a, p(0) \supset p(0))=1$, and hence for $a\ne 0_\textbf{M}$,

$$\begin{aligned}&{V(a, \forall y ((p(0)\supset p(y)) \vee (p(y) \supset p(0))))} \\&= \bigcap \{ V(b, (p(0)\supset p(0)) \vee (p(0)\supset p(0))) \mathrel {;} b \ge a \}\\&=1. \end{aligned}$$

And also,

$$\begin{aligned}&{V(0_\textbf{M}, p(i) \supset p(j))} \\&= \bigcap [ \{ V(b, p(0)) \rightarrow V(b, p(0))) \mathrel {;} b \ne 0_\textbf{M} \} \cup \{ V(0_\textbf{M}, p(i)) \rightarrow V(0_\textbf{M}, p(j)) \}]\\&=V(0_\textbf{M}, p(i)) \rightarrow V(0_\textbf{M}, p(j)). \end{aligned}$$

Therefore,

$$\begin{aligned} V(0_\textbf{M},Lin^*)&=V(0_\textbf{M}, (p(i) \supset p(j)) \vee (p(j) \supset p(i)))\\&=V(0_\textbf{M}, p(i) \supset p(j)) \cup V(0_\textbf{M}, p(j) \supset p(i))\\&=(V(0_\textbf{M}, p(i)) \rightarrow V(0_\textbf{M}, p(j)) ) \cup (V(0_\textbf{M}, p(j)) \rightarrow V(0_\textbf{M}, p(i))) \\&=1 . \end{aligned}$$

Thus, $Lin^*$ is valid in $\mathcal {B}(\textbf{M})$.$\square$

Let us consider the sequence $\{ Lin^*\wedge QJ(\textbf{H}_i) \}_{i< \omega }$ of sentences. Then, by putting $\textbf{K}_i=\textbf{H}_*+Lin^*\wedge QJ(\textbf{H}_i)$ ($i < \omega$), we can show that $\{ \textbf{K}_i \}_{i<\omega }$ is strongly independent. It is clear that for every non-empty subset $\mathcal {S}$ of $\{ \textbf{K}_i \mathrel {;} i<\omega \}$, the logic $\bigcup \mathcal {S}$ fails to have DP and EP. This completes the proof of Corollary 9.4.¹²

Note that the sequence $\{ Lin^*\wedge QJ(\textbf{H}_i) \}_{i< \omega }$ is recursively generated.

6 Concluding Remarks

We constructed a recursively enumerable set of concrete predicate axiom schemata. By adding these schemata to $\textbf{H}_*$, we obtained a strongly independent sequence of predicate extensions of intuitionistic; and this sequence yields a continuum of predicate extensions of intuitionistic logic each of which has DP but lacks EP.

This result suggests that although PEI’s are living near to intuitionistic logic, the diversity of their nature seems rich. In other words, logics among PEI’s are fascinating from the logical point of view and yet to be explored.

We have four types of continua of logics: “with EP and DP,” “without EP and DP,” “with DP but without EP,” and “with EP but without DP.” Other than the last one, three of them can be obtained by recursively enumerable construction of concrete axiom schemata. Recall that DP ad EP are regarded as “hallmarks” of constructivity of intuitionistic logic. It seems interesting that continua of logics with/without properties closely related to constructivity are constructively generated by sequences of axiom schemata. However, for the continuum: “with EP but without DP,” we do not have such a sequence of axiom schemata. So we pose a

Problem. Does there exist a recursively enumerable and strongly independent sequence of axiom schemata such that all the logics yield by this sequence are PEI’s, have EP, and fail to have DP?

We make two Remarks on the consideration of the Problem.

Remark 9.1

As shown in Suzuki (2021), if an intermediate logic $\textbf{L}$ has EP, then $\textbf{L}$ has DP, provided that $\textbf{L}$ has a very weak DP: $\textbf{L} \vdash A\vee (p(x) \supset p(y))$ implies $\textbf{L} \vdash A$ whenever A contains no occurrence of the symbols: p, x, and y. Note that this weak DP seems natural for reasonable logics such as logics complete with respect to a class of Kripke bases or to a class of complete Heyting algebras. (Even classical logic possesses it.) Thus, it is not straightforward to create semantically a logic that has EP and does not have DP

Remark 9.2

In Suzuki (2021), we gave a method to create a PEI with EP but without DP from a given logic with EP. Let $\textbf{H}^*$ be the superintuitionistic predicate logic $\textbf{H}+ \exists xp(x) \supset \forall xp(x)$, where p is a unary predicate variable. Then, $\textbf{H}^*$ is the greatest superintuitionistic predicate logic having the same propositional part as $\textbf{H}$. If $\textbf{L}$ is an intermediate predicate logic having EP, then $\textbf{L} \cap \textbf{H}^*$ has EP but lacks DP, provided that $\textbf{L}$ is NOT a PEI.

If we try to use this method to solve the problem affirmatively, we need appropriate logics with EP. Ferrari and Miglioli (1993) gave a continuum of intermediate predicate logics having both of EP and DP. These logics are all not PEI’s. However, their logics are non-recursively generated. Hence, the resulting logics by this method are not recursively generated. We cannot use their logics to solve the Problem. On the other hand, (Suzuki 1999)’s strongly independent sequence are recursively generated, but we cannot apply the method to them, because these logics are PEI’s (they are fixed points of the $\Delta$-operation. cf. Suzuki 1996). Hence, we cannot use these logics neither.