数理解析研究所講究録
927 巻 1995 年 140-156

140

Algebraic Kripke sheaf semantics forsuper-intuitionistic predicate logics
NoBu-Yu$\mathrm{K}\mathrm{I}$SUZUKI鈴木信行

Department of Computer and Information Sciences
Faculty of Engineering
Ibaraki University
akanarusawa, Hitachi 316
JAPAN$\mathrm{N}$Abstract
In so-called KIipke-type models, each sentence is assigned either to true or
to false at each possible world. In this setting, every possible world has thetwo-valued Boolean algebra as the set of the truth values. Instead, we take aas the set of the truth
collection of algebras each of which is attached to avalues at the world, and obtain an extended semantics based on the traditional
Kripke-type semantics, which we call here the algebraic Kripke semantics.
We introduce algebraic Kripke sheaf semantics for super-intuitionistic predicate logics, and discuss some basic properties. As application, we show a new
result on super-intuitionistic predicate logics. We prove that there exists a continuum of super-intuitionistic predicate logics each of which has both of the disjunction and existence properties and moreover the me propositional fragment
as the intuitionistic logic.
$\mathrm{w}\mathrm{o}\mathrm{I}\mathrm{l}\mathrm{d}$$\mathrm{s}\dot{\mathrm{a}}$Introduction
In so-called Kripke-type models, we assign true or false to each sentence at each possible world. In this setting, each possible world is supposed to have the two-valued
Boolean algebra $2=\{0,1\}$ as the set of the truth values. Instead of 2, we take an algebra $P(w)$ for each possible world as the set of the truth values at . In the case thata possible world is accessible from another world , it is desirable that computational
process in $P(w)$ can be traced in $P(v)$ . For this request, we arrange an apparatus in category theory, and obtain an extended semantics based on the traditional Kripke-type
semantics, which we call here the algebraic Kripke semantics. This kind of generalizasemantics in the sense of Skvortsov-Shehtman [13].
tion yields
$w$

$w$

$w$

$w$

$\mathrm{n}\mathrm{o}\mathrm{n}- \mathrm{K}\mathrm{r}\mathrm{i}\mathrm{P}^{\mathrm{k}-}\mathrm{e}\mathrm{t}\mathrm{y}\mathrm{P}\mathrm{e}$

$v$

141

In this article, we introduce algebraic Kripke sheaf semantics for super-intuitionistic
predicate logics based on the Kripke sheaf semantics, which is introduced by ShehtmanSkvortsov [11] as an extension of the Kripke frame semantics. In this case, each $P(w)$shall form a functor whose codomain
is a Heyting algebra, and the collection ofis an appropriate category with objects being Heyting algebras.
After this idea came to the author, Prof. Ono informed the author of that Nagai [8]introduced in 1973 an algebraic Kripke-type semantics based on the Kripke frame
are identical to each other. Our algebraic Kripke sheaf
semantics such that all
semantics contains his semantics as a special case, and is proved to be properly more
powerful than the Nagai semantics.
We discuss some basic properties and give a new result as application of this semantics. This result cannot be proved, at present, by using the Kripke sheaf semantics.
We present a new method of constructing a continuum of super-intuitionistic predicate logics. This method is obtained from the modified Jankov method in [15] by-modification. We show that there exists a continuum of super-intuitionistic predicate logics each of which has both of the disjunction and existence properties andmoreover the same propositional fragment as the intuitionistic logic. For this aim, wemust find a criterion for a logic to have both of the disjunction and existence properties. Our idea comes from an observation of the delta operation in super-intuitionistic
predicate logics.
$P(w)’ \mathrm{s}$$P(w)’ \mathrm{s}$$\mathrm{r}\mathrm{e}$In section 1, we repeat some basic definitions and properties of Kripke sheaf semantics for super-intuitionistic predicate logics. We introduce algebraic Kripke sheaf
semantics in section 2. Some concepts and results in the Kripke sheaf semantics can be
repeated for this semantics. An advantage of this semantics is that the set of formulas
valid in an algebraic Kripke sheaf is always closed under the rule of substitution. This
property fails to be possessed by extended Kripke-type semantics presented in Ghilardi $[2, 3]$ , Shehtman-Skvortsov [11], and Skvortsov-Shehtman [13]. We give in section
3 concrete application of the algebraic Kripke sheaf semantics stated above.

1

Starting from the Kripke sheaf semantics

Basic definitions and properties of the Kripke sheaf semantics are stated here to makethis article self-contained. We refer readers to $[14, 15]$ for details.
We fix a first-order language , which consists of logical connectives V (disjunc(existential(negation), and quantifiers(implication),tion), A (conjunction),quantifier) and (universal quantifier), a denumerable list of individual variables anda denumerable list of $m$ -ary predicate variables for each $m<\omega$ . As usual, -ary predicate variables are identified with propositional variables. Note that contains neither
individual constants nor function symbols. For each non-empty set , we denote by
the language obtained from by adding the name of each $u\in U$ . In what follows, we will sometimes use the same letter for the name of . We sometimes identify$\mathcal{L}$$\exists$$\neg$$\supset$$\forall$$0$$\mathcal{L}$$U$$\mathcal{L}[U]$$\mathcal{L}$$\overline{u}$

$u$

$u$

142

. For each super-intuitionistic propositionalwith the set of all sentences of,logic , we denote, by , the smallest predicate extension of , i.e.,
is the intuitionistic predicate logic.
where$\mathcal{L}[U]$$\mathcal{L}[U]$$\mathrm{J}_{*}=\mathrm{H}_{*}+\mathrm{J}$$\mathrm{J}$$\mathrm{J}$$\mathrm{J}_{*}$$\mathrm{H}_{*}$

iswith the least element
Definition 1.1 A partially ordered set
as a category in the usual
said to be a Ifripke base. We can regard a Kripke basefrom away. Let denote the category of all non-empty sets. A covariant functor
is,
M.
That
over
a
is
calledto
Kripke basedomain-sheaf$\mathrm{M}=\langle M, \leq\rangle$$0_{\mathrm{M}}$$\mathrm{M}$

$D$

$S$

$S$

$\mathrm{M}$is a non-empty set for every $a\in M$ ,for every $b\in M$ with $a\leq b$ , there exists a mappingis the identity mapping of $D(a)$ for every $\in M$ ,$c\in M$ with $a\leq b\leq c$ .
for every$\mathrm{D}\mathrm{S}1)D(a)$$\mathrm{D}\mathrm{S}2)$$a,$: $D(a)arrow D(b)$ ,$a$$\mathrm{D}\mathrm{S}3)D_{aa}$$a,$ $b,$$\mathrm{D}\mathrm{S}4)D_{ac}=D_{bc}\mathrm{o}D_{ab}$A pairKripke$D_{ab}$$\mathcal{K}=\langle \mathrm{M}, D\rangle$

of a Kripke base$\mathrm{M}$and a domain-sheaf

$D$

over

$\mathrm{M}$is called a.

$\mathit{8}heaf$

is said to be a Kripke
If every $D_{ab}(a\leq b)$ is the set-theoretic inclusion,$D(a)$
is the individual domain of the world
frame (for predicate logics). Intuitively, each$a\in M$ . For each $d\in D(a)$ and each $b\in M$ with $a\leq b,$ $D_{ab}(d)$ is said to be the inheritor
and each $b\in M$ with $a\leq b$ , the inheritor
of at . For each formula ofobtained from by replacing occurrences ofof at is a formula of$(u\in D(a))$ by the nameof the inheritor of at .
iseach $a\in M$ and each atomic sentence ofA binary relation
if for every $b\in M$ and every atomic sentence of
said to be a valuation on$a\leqb$$a\models A$ andto a relation between each
. We extend
imply$a\in M$ and each sentence of
inductively as follows:$\langle \mathrm{M}, D\rangle$$d$$A_{a,b}$

$A$

$b$

$A$

$\mathcal{L}[D(a)]$$A$$\mathcal{L}[D(b)]$

$b$

$b$

$u$

$v$

$\overline{v}$$\overline{u}$$\mathcal{L}[D(a)]$$\models \mathrm{b}\mathrm{e}\mathrm{t}_{\mathrm{W}}\mathrm{e}\mathrm{e}\mathrm{n}$$\langle \mathrm{M}, D\rangle$

$A$

$a,$

$b\models A_{a,b}$$\mathcal{L}[D(a)],$$\models$$\mathcal{L}[D(a)]$$\bullet$$\bullet$$a\models A$

A $B$ if and only if $a\models A$ and $a\models B$ ,$a\models AB$ if and only if $a\models A$ or $a\models B$

if and only if for every $b\in M$ with $a\leq b$ , either $b\# A_{a,b}$ or$\bullet$$a\models A\supset B$$\bullet$$a\models\neg A$$\bullet$$a\models\forall xA(x)$$b\models B_{a,b}$,

if and only if for every $b\in M$ with $a\leq b,$ $b\# A_{a,b}$ ,$b\models A_{a,b}(\overline{u})$$\bullet$,

if and only if for every $b\in M$ with $a\leq b$ and every $u\in D(b))$,$a\models\exists xA(x)$if and only if there exists $u\in D(a)$ such that$a\models A(\overline{u})$.

it is said to be a Ifripke-sheafof a Kripke sheaf and a
A pair,if
model
Kripke-sheaf
true
in
a
to
be
said
of
is
formulaA
model.
where is the universal closure of . A formula of is said to be valid in a Kripke. The set of formulas ofis true inonsheaf if for every valuation. The following propositions areoris denoted byvalid infundamental properties of Kripke-sheaf semantics.
$\mathcal{K}$$(\mathcal{K}, \models)$$A$$\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\models \mathrm{o}\mathrm{n}$$(\mathcal{K}, \models)$$\mathcal{L}$

$A$

$A$

$\overline{A}$$\mathcal{K}$$\models$$\mathcal{K}=\langle \mathrm{M}, D\rangle$$\mathcal{K},$$A$$L(\mathcal{K})$$0_{\mathrm{M}}\models\overline{A}$$\mathcal{L}$$(\mathcal{K}, \models)$$L\langle \mathrm{M}, D\rangle$$\mathcal{L}$143

Proposition 1.2 For every Kripke-sheaf model
every sentence$A\in \mathcal{L}[D(a)]$$(\langle \mathrm{M}, D\rangle, \models)$, if $a\models A$ and $a\leq b$ , then, every a, $b\in M_{f}$ and$b\models A_{a,b}$ ,all formulas, the set
Proposition 1.3 For each, and is closed under the modus $ponens_{f}$ the rule of generalization andprovable inNamely,is a super-intuitionistic predicate logic.
substitution.
the rule of$L(\mathcal{K})Contain\mathit{8}$$f\iota’ripke- \mathit{8}heaf\mathcal{K}$$\mathrm{H}_{*}$$L(\mathcal{K})$The Kripke sheaf semantics is properly more powerful than the Kripke frame semantics, which is stated in the following.
Theorem 1.4 ([14]) Let $Z$ be a formulaispredicate variable. The logic
complete.
$\mathrm{H}_{*}+\neg\neg Z$, where is a unary-sheaf complete, but not Kripke-frame$\exists xp(X)\supset\forall xp(X)$$I\mathrm{t}’ripke$$p$

We can introduce -morphisms between Kripke sheaves.
$p$

andDefinition 1.5 Let$N$$M$
is said to be a p–morphism ofofto$c\in N$ ,$\mathrm{M}=\langle M, \leq_{\mathrm{M}}\rangle$

$f$

(1)
(2) if$a\leq_{\mathrm{M}}b$

be Kripke bases. A mapping, if for every $b\in M$ , and every$\mathrm{N}=\langle N, \leq_{\mathrm{N}}\rangle$$\mathrm{M}$to$\mathrm{N}$,implies, that there exists a $c\in M$ such that$a,$$f(a)\leq_{\mathrm{N}}f(b)$$f(a)\leq_{\mathrm{N}}c’$$a\leq_{\mathrm{M}}c$

and $f(c)=c’$ .

sheaves. Suppose thatbeandLemma 1.6 Letacovariant functor from
below
to
Then
morphism ofdefined$i.e,$ , a
is a Kripke sheafj
domain-sheaf over M. Hence$\langle \mathrm{M}, D\rangle$$\mathrm{N}$$\mathrm{M}$$I\zeta ripke$$\langle \mathrm{N}, E\rangle$$E\mathrm{o}f$,$i_{\mathit{8}}$$f$is a pto ,$\mathrm{M}$$S$$\langle \mathrm{M}, E\mathrm{o}f\rangle$$(E\mathrm{o}f)(a)$$=$$E(f(a))$$(E\mathrm{o}f)_{ab}$$=$$E_{f(a)f}(b)$for every $a\in M$ ,for every a, $b\in M$ with$a\leq_{\mathrm{M}}b$.

of a pbe Kripke sheaves. A pairandDefinition 1.7 Let
is said to be a
and a natural transformation of totomorphism of$D(a)arrow(E\mathrm{o}f)(a)(a\inM)$
is surjective.
:
if eachtop–morphism of: $D(a)arrow(E\mathrm{o}f)(a)$ in such
That is, assigns to each $a\in M$ a surjective mappingyield the following commutative diagram:a way that every $b\in M$ with$\langle \mathrm{M}, D\rangle$$f$$\mathrm{M}$$(f, \tau)$$\langle \mathrm{N}, E\rangle$$\mathrm{N}$$\tau$$\langle \mathrm{N}, E\rangle$$\langle \mathrm{M}, D\rangle$$D$$E\mathrm{o}f$$\tau_{a}$$\tau$$\tau_{a}$$a\leq_{\mathrm{M}}b$$a,$$\tau_{a}$$D(a)$$arrow$$(E\mathrm{o}f)(a)$$\downarrow(E\circ f)ab$$D_{ab}\downarrow$$D(b)$$arrow$$\tau_{b}$$(E\circ f)(b)$.

Theorem 1.8 (the -morphism theorem for Kripke sheaves) Let, thento. If there exists a -morphism of
be Kripke$p$$\mathit{8}heaveS$$p$$\mathcal{K}_{1}$$\mathcal{K}_{2}$$\mathcal{K}_{1}$and.

$L(\mathcal{K}_{1})\subseteq L(\mathcal{K}_{2})$$\mathcal{K}_{2}$144

Let $CD$ be the sentence $\forall x(p(x)q)\supset(\forall xp(X)q)$ where is a unary predicate
is said to be withvariable and is a propositional variable. A Kripke frame. It is well-known that $CD$ is valid
constant domain, if $D(a)=D(0_{\mathrm{M}})$ for every
in a Kripke frame if and only if it is with constant domain.
$p$$\langle \mathrm{M}, D\rangle$$q$$a\in \mathrm{M}$Definition 1.9 A Kripke sheaf.
for every $b\in M$ with$\langle \mathrm{M}, D\rangle$

is said to be of type $CD$ , if

$D_{ab}$is surjective$a\leq_{\mathrm{M}}b$$a,$Lemma 1.10 The sentence $CD$ is valid in a Kripke sheaf if and only if it
type $CD$$i_{\mathit{8}}$of,, there exist a Kripke frame
Theorem 1.11 (1) For every
sheaf
.
to
and a
of
(2) For every Kripke sheafof type $CD$ , there exist a Kripke frameto .
with constant domain and a -morphism of$\mathcal{K}=\langle \mathrm{M}, D\rangle$$I\iota^{\mathit{7}}ripke$$\mathcal{K}^{*}$$p- m\mathit{0}r_{\mathrm{P}}hi_{\mathit{8}}m$$\mathcal{K}^{*}=\langle \mathrm{M}, D^{*}\rangle$$\mathcal{K}$$\mathcal{K}=(\mathrm{M},$$D\rangle$$\mathcal{K}^{*}=\langle \mathrm{M}, D^{*}\rangle$$\mathcal{K}^{*}$$p$$\mathcal{K}$Corollary 1.12 (1) For every intermediate propositional logic
sheaf complete if and only if is Kripke-frame complete.
islogic(2) For every intermediate
Ifripke-frame complete.
if and only if$\mathrm{J},$$\mathrm{J}_{*}$

is$I\iota^{\Gamma}ripke-$$\mathrm{J}_{*}$$prop_{\mathit{0}\mathit{8}itiona}l$$\mathrm{J},$$\mathrm{J}_{*}+CD$$I\iota^{F}ripke$-sheaf complete$\mathrm{J}_{*}+CDi_{\mathit{8}}$2Algebraic Kripke sheaf semantics, we can replace a relationa
In the definition of Kripke sheaf model
function whose codomain is the two-valued Boolean algebra $2=\{0,1\}$ . Namely,$(\langle \mathrm{M}, D\rangle, \models)$$\models \mathrm{b}\mathrm{y}$$V$$V(a, A)=\{$

1 if
if $a\# A$ .
$a\models A$$0$. In this setting, eachhas 2and every sentence
for everyas the set of the truth values. Instead of 2, we take an algebra $P(a)$ for eachas the set of the truth values at . It is natural that $P(a)$ coincides with an algebraic. Since we intend to provide semantics foris a singleton
semantics, whenevermust be Heyting algebras.
super-intuitionistic predicate logics,, computation in $P(a)$ is to be traced in $P(b)$ .
If is accessible from
For this request, we take a monomorphism1 of $P(b)$ into $P(a)$ . We design that thecollection $\{P(a) ; a\in \mathrm{M}\}$ forms a functor with domain , whose codomain shall be
an appropriate category with objects being Heyting algebras.
$a(\in \mathrm{M})$$A\in \mathcal{L}[D(a)]$$a\in \mathrm{M}$$a(\in \mathrm{M})$$a$$\{a\}$$\mathrm{M}$$P(a)’ \mathrm{s}$$b(b\leq_{\mathrm{M}}a)$$a$$\mathrm{M}$

1One might just as well try to take a homomorphism instead of a monomorphism. In the Kripke
frame semantics for super-intuitionistic predicate logics, we have a fundamental request that if is, thenis true at . In our semantics, this is translated into: if $V(b, A)=1$
true at and, then $V(a, A)=1$ . This request corresponds to the condition that each homomorphism
and$h:P(a)arrow P(b)$ satisfies that $h^{-1}(1)=\{1\}$ . This is equivalent to thatis a monomorphism.
$A$

$b$

$b\leq_{\mathrm{M}}a$

$A$

$a$

$b\leq_{\mathrm{M}}a$

$h$

145

Definition 2.1 Let
denote the category of all non-degenerate complete Heyting algebras with arrows being complete monomorphisms between complete Heyting
algebras. A contravariant functor from a Kripke baseto is called a$truth- value-_{She}af$ over M. That is,$\mathcal{H}$$P$$\mathrm{M}=\langle M, \leq\rangle$$\mathcal{H}$

TVSI) $P(a)$ is a non-degenerate complete Heyting algebra for every $a\in M$ ,TVS2) for every $b\in M$ with $a\leq b$ , there exists a complete monomorphism$P(b)arrow P(a)$ ,TVS3)
is the identity mapping of $P(a)$ for every $a\in M$ ,$c\in M$ with $a\leq b\leq c$ .
TVS4)for every$a,$$P_{ab}$:$P_{aa}$$P_{ac}=P_{ab^{\mathrm{O}}bc}P$$a,$ $b,$

A tripleof a Kripke base , a domain-sheaf $D$ over$P$value-sheaf is called an algebraic Kripke sheaf.
$\mathcal{K}=\langle \mathrm{M}, D, P\rangle$$\mathrm{M}$$\mathrm{M}$, and a truth-

Intuitively, each $P(a)(a\in M)$ is the set of truth values of the world . Since
we assume the existence of the least elementof , every $P(a)$ can be identified
with a complete subalgebra of. We write $P(a)= \langle P(a), \bigcap_{P}, Up,$or $P(a)=\langle P(a), \cap, \cup, arrow, 0,1\rangle$ for every, if there occurs no confusion. The$P(a)$
canonical order in(and also infor) is denoted byor simply by.
A mapping which assigns to each pair $(a, A)$ of $\in M$ and each atomic sentenceofan element of $P(a)$ is said to be a valuation on
if for every $b\in M$
and every atomic sentenceofimplies $V(a, A)\leq_{P}V(b, A_{a,b})$ . We
extend to a mapping which assigns to each pair $(a, A)$ of $a\in M$ and each sentenceofan element of $P(a)$ inductively as follows:$a$$\mathrm{M}$$0_{\mathrm{M}}$$P(0_{\mathrm{M}})$$arrow_{P}, 0_{PP}, 1\rangle$$a\in \mathrm{M}$$a\in \mathrm{M}$$P(0_{\mathrm{M}})$$\leq_{P}$$\leq$

$V$

$A$

$a$

$\mathcal{L}[D(a)]$$\langle \mathrm{M}, D, P\rangle$$A$$\mathcal{L}[D(a)],$$a,$$a\leq_{\mathrm{M}}b$

$V$

$A$

$\mathcal{L}[D(a)]$$\bullet$$\bullet$

$V$

(

$a,$

$A$

A $B$ ) $=V(a, A)\cap V(a, B)$ ,$V(a, AB)=V(a, A)\cup V(a, B)$ ,$\bullet$$V(a, A \supset B)=\bigcap_{b,a\leq b}(V(b, A_{a},b)arrow V(b, B_{a,b}))$$\bullet$$V(a, \neg A)=\bigcap_{b;a\leq b}(V(b, A_{a},b)arrow 0)$$\bullet$$\bullet$,,$V(a, \forall xA(X))=\mathrm{n}_{b};a\leq b\cap u\in D(b)V(b, Aa,b(\overline{u}))$$V(a, \exists xA(x))=\bigcup_{d\in D()}aV(a, A(\overline{u}))$,.

A pairof an algebraic Kripke sheaf
and a valuation
on it is said to be
an algebraic Kripke-sheaf model. A formula of is said to be true in an algebraic
Kripke-sheaf modelif. A formula of is said to be valid inan algebraic Kripke sheaf if for every valuationonis true in. The
set of formulas of valid in
is denoted byor. The
following propositions are fundamental properties of algebraic Kripke sheaf semantics.
$(\mathcal{K}, V)$

$A$

$A$

$V$

$\mathcal{K}$$\mathcal{L}$$\mathcal{L}$$V(0_{\mathrm{M}}, \overline{A})=1$$(\mathcal{K}, V)$$\mathcal{K}=\langle \mathrm{M}, D, P\rangle$$\mathcal{K},$$\mathcal{L}$$A$$(\mathcal{K}, V)$$L(\mathcal{K})$$L\langle \mathrm{M}, D, P\rangle$

Proposition 2.2 For every algebraic, every-sheaf model$b\in M$ , and every, if $a\leq b$ , then $V(a, A)\leq_{P}V(b, A_{a},b)$ .
$I\iota^{7}ripke$

$a,$

$V$

$\mathcal{K}$$\mathit{8}entenceA\in \mathcal{L}[D(a)]$$(\langle \mathrm{M}, D, P\rangle, V)$146

contains all forProposition 2.3 For each algebraic Kripke sheaf , the
the
rule
,
, and is closed under the modus
provable inof generalization-intuitionistic predicate logic.
a. Namely,
and the rule of$\mathcal{K}$$mula\mathit{8}$$\mathrm{H}_{*}$$\mathit{8}etL(\mathcal{K})$$ponen\mathit{8}$$sub_{\mathit{8}t}itution$$L(\mathcal{K})i_{\mathit{8}}$$\mathit{8}uper$

Ghilardi $[2, 3]$ , Shehtman-Skvortsov [11], and Skvortsov-Shehtman [13] presented
some extended Kripke-type semantics. The above proposition fails to hold for theirsemantics. For their semantical object, the set of formulas valid in it is not always
closed under the rule of substitution.
In 1973, Nagai [8] introduced an extended Kripke frame semantics for which theabove proposition holds. His semantics is a special case of our algebraic Kripke sheaf, if all $P(a)$is said to be a Nagai
semantics. An algebraic Kripke sheaf$(a\in M)$ are identical to the same Heyting algebra. A Nagai sheaf
is said to
is a Kripke frame. (cf. Nagai [8]). We can also introduce
be a Nagai frame, if
is said to be an algebraic
algebraicframes. An algebraic Kripke sheaf
is a Kripke frame.
Kripke frame, if
The algebraic Kripke sheaf semantics is properly more powerful than the Nagai
semantics. Let and $Lin$ be the following sentences;$\mathit{8}heaf$$\langle \mathrm{M}, D, P\rangle$$\langle \mathrm{M}, D, P\rangle$$\langle \mathrm{M}, D\rangle$$I\iota’ripke$$\langle \mathrm{M}, D, P\rangle$$\langle \mathrm{M}, D\rangle$$G$$G\equiv$$Lin$$\equiv$$\exists x\forall y(p(y)\supset_{\mathrm{P}(}x))$$(q\supset r)(r\supset q)$

where is a unary predicate variable, andhave the
$p$

$q$

and

$r$

,

,

are propositional variables. The we, but not algebraicICripke-8heaf
Theorem 2.4 (1) The logic
Ifripke-frame complete.
. On the other hand;
then
, if
(2) For every Kripke$CD\not\in
L(N)$
$G\in
L(N)$
and
that
a Nagai frame
there(3) For every Nagai sheaf $N$ , if $\mathrm{H}_{*}+Lin+G\subseteq L(N)$ then $CD\in L(N)$ . On thesuch that
other hand, there exists an algebraic Kripke.
and$c\mathit{0}mplete$$\mathrm{H}_{*}+\neg\neg Zi\mathit{8}$$\mathit{8}heaf\mathcal{K}$$exi\mathit{8}tS$$G\in L(\mathcal{K})$$CD\in L(\mathcal{K})$$N\mathit{8}uch$,$\mathit{8}heaf\mathcal{K}$$\mathrm{H}_{*}+Lin+G\subseteq L(\mathcal{K})$$CD\not\in L(\mathcal{K})$(1) : We can show that for every algebraic Kripke frame , if
.
then
which
(2) : In [17], Umezawa proved that there exists an algebraic frame$CD$(Model 9 in [17]). Since each algebraic frame is a special
validates but does not
Nagai frame, we have proved the latter half of (2).
(3) : Let $\mathrm{W}=\{0,1\}$ be a Kripke base with $0\leq 0,0\leq 1$ and $1\leq 1$ . Define adomain-sheaf $D$ and a truth-value-sheaf by.

$P\mathrm{r}oof$$\mathcal{F}$$\neg\neg Z\in L(\mathcal{F})$$Z\in L(\mathcal{F})$$(\mathrm{A}, U)$

$G$

$P$

$D(0)=U,$ $D(1)=\{0\}$ ,$D_{01}(u)=0$

for every $u\in U$,

147$P(0)=\mathrm{A},$$P(1)=2$ ,$P_{01}(0)=0,$ $P_{01}(1)=1$

Then

and

$\mathrm{H}_{*}+Lin+G\subseteq L\langle \mathrm{W}, D, P\rangle$.

$CD\not\in L\langle \mathrm{W}, D, P\rangle$.

$\square$We illustrate the situation in Figure 1. Until now, we have not found an appropriate
example to separate Nagai frames and algebraic Kripke frames (i.e., dotted linein1).
Figure$\cdots$

Figure 1
In the rest of this section, we state some basic results on the algebraic Kripke sheaf
semantics.

Definition 2.5 Let

be a Kripke
and a truth-value-sheafover, respectively. A mappingis said to be order-pre8erving, if:
for every $b\in M,$ $a\leq b$ implies $f(a)\leq_{P}f(b)$ . An order-preserving mapping is said
to be tame, if for every $a\in M,$ $f(a)\in P(a)$ . The set of all tame and order-preserving.
mappings is denoted by$\mathrm{M}=\langle M, \leq\rangle$$f$$\mathrm{M}$

and

$P$

$\mathrm{b}\mathrm{a}s\mathrm{e}$$\mathrm{M}arrow P(0_{\mathrm{M}})$

$f$

$a,$

$[P^{\mathrm{M}}]$

Proposition 2.6 (Cf. Ono-Nagai [9]) Let
be an algebraic Kripke
Then,
every
is a Heyting algebra.
propositional
forformulavalid in.
if and only if is valid in$\langle \mathrm{M}, D, P\rangle$$[P^{\mathrm{M}}]$$M_{\mathit{0}r}e\mathit{0}verf$$A$$\langle \mathrm{M}, D, P\rangle$.
is$\mathit{8}heaf$$A_{f}$$A$$[P^{\mathrm{M}}]$

Definition 2.7 Let
be algebraic Kripke sheaves. The
and-sheafover
is defined in a similar way that is used in the previous
section. Aoftois a tripleof a p-morphism(as Kripke sheaves) and a natural transformation ofof (toto . That is, assigns to each $a\in M$ a complete monomorphism (an arrow of )$\langle \mathrm{M}, D, P\rangle$$Q\mathrm{o}f$$\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{t}\mathrm{h}-_{\mathrm{V}\mathrm{a}}1\mathrm{u}\mathrm{e}$$p- m\mathit{0}rphi_{\mathit{8}}m$$(f, \tau)$$P$$\mathrm{M},$$D\rangle$$\sigma$$\langle \mathrm{N}, E\rangle$$\langle \mathrm{N}, E, Q\rangle$$\mathrm{M}$$\langle \mathrm{M}, D, P\rangle$$\langle \mathrm{N}, E, Q\rangle$$(f, \tau, \sigma)$$\sigma$$Q\mathrm{o}f$$\mathcal{H}$148: $(Q\mathrm{o}f)(a)arrow P(a)$ in such a way that every
following commutative diagram:$\sigma_{a}$$a,$$b\in M$with$a\leq_{\mathrm{M}}b$yield the$\sigma_{b}$$(Q\mathrm{o}f)(b)$$arrow$$P(b)$$(Q\mathrm{o}f)_{ab}\downarrow$$\downarrow P_{ab}$$(Q\mathrm{o}f)(a)$$arrow$$\sigma_{a}$$P(a)$.

Theorem 2.8 (the -morphism theorem for algebraic Kripke sheaves). If there exists a
be algebraic Kripke
and
Let
of to
then
$p$

$\mathcal{K}_{1}$$sheave\mathit{8}$$\mathcal{K}_{2}$$L(\mathcal{K}_{1})\subseteq L(\mathcal{K}_{2})$$p- m\mathit{0}rphi_{\mathit{8}}m$$\mathcal{K}_{1}$$\mathcal{K}_{2}$,,Definition 2.9 Let be an arbitrary non-zero cardinal. A Heyting algebra
and every subset
is said to be -distributive, if for every element, where Card $(s)$ is the, it holds thatwith Cardis said to be of type $CD$ , if
cardinality of . An algebraic Kripke sheaf
is a Kripke sheaf of type $CD$ and for every $a\in M,$ $P(a)$ is Card $(D(a))$ -distributive.
$\mathrm{P}=$$\lambda$$\lambda$$\langle P, \cap, \cup, arrow, 0,1\rangle$$a$$\bigcap_{s\in S}(s\cup a)=(\bigcap_{s\in S}s)\cup a$$(s)\leq\lambda$$S\subseteq P$$\in P$$S$$\langle \mathrm{M}, D, P\rangle$

Lemma 2.10 The sentence
it is of type $CD$ .

$CDi_{\mathit{8}}$$\langle \mathrm{M}, D\rangle$

valid in an algebraic Ifripke$\mathit{8}heaf$

if and only ifthere exist a
Theorem 2.11 (1) For every algebraic Kripke sheaf
to
.
and
a
Nagai frameof(2) For every algebraic Ifripke sheafof type $CD$ , there exist a Nagai
of type $CD$ and a -morphism of to .
frame$\mathcal{K}=\langle \mathrm{M}, D, P\rangle\rangle$$\mathcal{K}^{*}=\langle \mathrm{M}, D^{*}, P^{*}\rangle$$p- m\mathit{0}rphi_{\mathit{8}}m$$\mathcal{K}^{*}$$\mathcal{K}$$\mathcal{K}=\langle \mathrm{M}, D, P\rangle$$\mathcal{K}^{*}=\langle \mathrm{M}, D^{*}, P^{*}\rangle$$\mathcal{K}^{*}$$\mathcal{K}$$p$

Along lines with the above discussion, we can develop algebraic Kripke semantics based on extended Kripke-type semantics presented in Ghilardi $[2, 3]$ , ShehtmanSkvortsov [11], and Skvortsov-Shehtman [13]. E.g., algebraic Kripke bundles, algebraic
C-8ets and algebraic Kripke $metaframe\mathit{8}$ can be, in principle, introduced.

3

Application

As application of our algebraic Kripke sheaf semantics, we show here new results insuper-intuitionistic predicate logics. This result cannot be proved, at present, by using
the Kripke sheaf semantics. We present a new method of constructing a continuum of
super-intuitionistic predicate logics. This method is obtained from the modified Jankov
method in [15] by -modification with adopting a suitable subclass of algebraic Kripke
sheaves. We show that there exists a continuum of super-intuitionistic predicate logics
each of which has both of the disjunction and existence properties and moreover the$\mathrm{r}\mathrm{e}$149same propositional fragment as the intuitionistic logic. For this aim, we must finda criterion for a logic to have both of the disjunction and existence properties. Ouridea comes from an observation of the delta operation in super-intuitionistic predicate
logics.
We explain how to modify the Jankov method used in [15] by making use of algebraic
Kripke sheaf semantics. First, we give here a brief sketch of the original Jankov method([5]). We recall some terminology and notation mainly from [15]. The Jankov methodof logics.
is a method constructing a strongly independent$\mathit{8}equence$

Definition 3.1 A denumerable sequence
for each $i<\omega,$ wheredependent, if$\{\mathrm{L}_{i}\}_{i<\omega}$$\mathrm{L}_{\dot{l}}\not\in\bigcup_{j\neq i}\mathrm{L}_{\gamma}$

all$\mathrm{L}_{j}(j\neq i)$of logics is said to be strongly inis the smallest logic containing$\bigcup_{j\neq i}\mathrm{L}_{j}$.

of logics, we have that forIf there exists a strongly independent sequence. Hence the cardinality of$I=J$ if and only ifevery andequals that of a continuum.
A Heyting algebra A is said to be strongly compact if there exists the second greatest
element in A. The second greatest element of a strongly compact Heyting algebra A
be a finite and strongly
or simply by . Let A
is denoted bycompact Heyting algebra. Since its underlying set is finite, for each element $a\in A$ ,of A is defined by
we can attach a unique propositional variable . The diagram$\{\mathrm{L}_{i}\}_{i<\omega}$$I$$J\subseteq\omega,$$\bigcup_{i\in I}\mathrm{L}_{i}=\bigcup_{j\in J}\mathrm{L}_{\dot{J}}$$\{\bigcup_{i\in I}\mathrm{L}_{i} ; I\subseteq\omega\}$$\star$$\star_{\mathrm{A}}$$=\langle A, \cap, \cup, arrow, 0,1\rangle$$A$$P_{a}$$\delta(\mathrm{A})$$=$$\delta(\mathrm{A})$$\{P_{a\cap b}\supset(P_{a}\wedge P_{b}), (P_{a}\wedge P_{b})\supset P_{a\cap b} ; a, b\in A\}$$\cup\{P_{a\cup b}\supset(P_{a}P_{b}), (P_{a}P_{b})\supset P_{a\cup b} ; a, b\in A\}$$\cup\{P_{aarrow b}\supset(P_{a}\supset P_{b}), (P_{a}\supset P_{b})\supset P_{aarrow b} ; a, b\in A\}$$\cup\{P_{aarrow}0\supset\neg P_{a}, \neg P_{a}\supset P_{aarrow 0} ; a\in A\}$.

The Jankov formula of A is the formula$J(\mathrm{A})=(\wedge\delta(\mathrm{A}))\supset P_{\star}$,. Then it is easy to see thatis the conjunction of all formulas in
is not valid in A. The following Lemmas is the Key Lemma for the original
Jankov method.

where$\delta(\mathrm{A})$$\wedge\delta(\mathrm{A})$$J(\mathrm{A})$compact Heyting algebra. For eachLemma 3.2 Let A be a finite andHeyting algebra , the following two conditions are equivalent:is not valid in ,(1)
into a quotient algebra of B.
A
isembeddable(2)$\mathit{8}trongly$$\mathrm{B}$$J(\mathrm{A})$$\mathrm{B}$By this Lemma, Jankov established a relation between validity of a certain propositional formula and an algebraic property. We extend this to an appropriate relationin predicate logics.

150

of a Kripke baseis said to be open if for every $u\in A$ and every$v\in M,$ $u\leq v$ implies $v\in A$ . The setof all open subsets is a strongly compact, which we will denote by
Heyting algebra with the second greatest element. For each Heyting algebra , the setof all prime filters is a Kripke frame.
If A is strongly compact, thenis a Kripke base. The following facts and lemma
are well-known.
A subset$A$$\mathrm{M}$$\mathcal{O}(\mathrm{M})$$M\backslash \{0_{\mathrm{M}}\}$$P(\mathrm{A})$$\mathrm{A}$$\star_{\mathrm{M}}$$P(\mathrm{A})$Fact 3.3 (1) For each finite(2) For each finite and strongly compact Heyting algebra
to A.
$I\iota’ripkeba\mathit{8}e\mathrm{M},$isomorphic tois$P(\mathcal{O}(\mathrm{M}))i_{\mathit{8}}$$O(\mathcal{P}(\mathrm{A}))$$\mathrm{A},$$\mathrm{M}$,$i\mathit{8}om\mathit{0}rphic$

andLemma 3.4 Let
be Kripke.
thatfinite. Then, therea -morphism fromtoan embedding of
if and only if there.
into$\mathrm{M}$$exist\mathit{8}$$ba\mathit{8}e\mathit{8}$$\mathrm{N}$$\mathrm{M}$$p$$\mathrm{N}i_{\mathit{8}}$$Supp_{\mathit{0}\mathit{8}e}$$exi\mathit{8}t\mathit{8}$$\mathrm{N}$$\mathcal{O}(\mathrm{N})$$\mathcal{O}(\mathrm{M})$

Hence, we can identify finite Kripke bases with finite strongly compact Heyting
algebras. In the following we implicitly use the above fact and lemma in order to makeour exposition simple.

Definition 3.5 For a strongly compact Heyting algebra , there exists a Heyting, wheresuch that A is isomorphic tothe sum operation ofalgebraHeyting algebras. (See e.g., Troelstra [16].) For a strongly compact Heyting algebra A
and a Heyting algebra , we denote by
the Heyting algebra.
$\mathrm{A}$$\mathrm{A}^{-}\oplus 2$$\mathrm{A}^{-}$$\mathrm{B}$$\oplus \mathrm{i}\mathrm{s}$$\mathrm{A}^{-}\oplus \mathrm{B}$$\mathrm{A}\triangleleft \mathrm{B}$A$\mathrm{A}\triangleleft \mathrm{B}$$\mathrm{B}$Figure 2
Lemma 3.6 Every quotient algebra ofissomealgebra of A or toquotient
algebrafor$\mathrm{A}\triangleleft \mathrm{B}$$\mathrm{A}\triangleleft \mathrm{B}’$$i_{\mathit{8}omo}rphic$$\mathrm{B}’$either to a quotientof B.

Lemma 3.7 Suppose that a strongly compact Heyting algebra A contains at leastthree. If a finite and strongly compact Heyting algebra
the following
conditions:$element_{\mathit{8}}$$\mathrm{C}_{\mathit{8}}ati_{\mathit{8}}fies$151$(\neq \mathit{1})4\leq \mathrm{C}\mathrm{a}\mathrm{r}\mathrm{d}(\mathrm{c})$$(\neq \mathit{2})$,there are exactly three elements inand ),

having no incomparable element $(i,e.,$ $0,1$$\mathrm{C}$$\star$then the following are equivalent:
embeddable into a quotient algebra ofis embeddable into a quotient algebra of A.
$(a)\mathrm{C}i_{\mathit{8}}$$\mathrm{A}\triangleleft \mathrm{B}_{f}$$(b)\mathrm{C}$Definition 3.8 An algebraic Kripke sheaf
is said to be a pendulum, if
for every $a\in M,$
implies $P(a)=2$ . A pendulum
is said to be$A$$V)$ isan -pendulum, if
A. An algebraic Kripke sheaf model
said to be a pendulum model (an $A$ -pendulum model), if
is a pendulum (anA-pendulum, respectively).
$\langle \mathrm{M}, D, P\rangle$$a\neq 0_{\mathrm{M}}$$\langle \mathrm{M}, D, P\rangle$$P(0_{\mathrm{M}})=$$(\langle \mathrm{M}, D, P),$$\langle \mathrm{M}, D, P\rangle$

Lemma 3.9 Let
be an $A$ -pendulum with Card(M)(1)
isomorphic to(2) Suppose a finite and strongly compact Heyting algebra
the conditions
andin Lemma 3.7. Then, for every pendulum, the following are
equivalent:is embeddable into a quotient algebra ofembeddable into a quotient algebra of.
$\geq 2$ ,$\langle \mathrm{M}, D, P\rangle$$[P^{\mathrm{M}}]i_{\mathit{8}}$$\mathcal{O}(\mathrm{M})\triangleleft \mathrm{A}$,$\mathrm{C}satisfie\mathit{8}$$(\neq \mathit{1})$$(\neq \mathit{2})$$\langle \mathrm{M}, D, P\rangle$$(a)\mathrm{C}$$[P^{\mathrm{M}}]_{f}$$(b)\mathrm{C}i_{\mathit{8}}$$\mathcal{O}(\mathrm{M})$Let
be a finite Kripke base. For each sentence of , we denote by $J(\mathrm{M};S)$ thesentence obtained fromby replacing all occurrences of by . We implicitly
assume that andcontain no propositional variables in common.
$S$$\mathrm{M}$$\mathcal{L}$$J(\mathcal{O}(\mathrm{M}))$

$S$

$S$

$J(\mathcal{O}(\mathrm{M}))$

Lemma 3.10 Let
be a finite Kripke
thatthe conditions
andin Lemma 3.7, For each pendulumwith Card(N),, thenis embeddable into a quotient algebra of.
$ba\mathit{8}e\mathit{8}uCh$$\mathrm{M}$$(\neq \mathit{1})$if$P_{\star}$$(\neq \mathit{2})$$J(\mathrm{M} ; S)\not\in L(\mathcal{K})$$\mathcal{O}(\mathrm{M})Sati_{Sfie\mathit{8}}$$\geq 2$$\mathcal{K}=\langle \mathrm{N}, D, P\rangle$$\mathcal{O}(\mathrm{M})$$\mathcal{O}(\mathrm{N})$We state our newly modified Jankov method as follows.
Lemma 3.11 (cf. Lemma 2.3 in [15]) Suppose
is a sequence of algebraic Kripke
models(0) each
is a pendulum,(1) eachis finite andtheandin Lemma 3.7,(2) for every $i,j<\omega,$ $i\neq j$ implies thatcannot be embedded into any quotient
algebra of,(3)
is not true in.
apredicate
logic
contained
in every,Ifthen theof super-intuitionistic predicate
defined bystrongly independent. In particular, theofpredicate logics defined. by
is strongly
independent.
$\{(\langle \mathrm{M}_{i}, D_{i}, P_{i}\rangle, V_{i})\}_{i<\omega}$$\mathit{8}heaf$$sati\mathit{8}fyingj$$\langle \mathrm{M}_{i}, D_{i}, Pi\rangle$$\mathcal{O}(\mathrm{M}_{i})$$satisfie\mathit{8}$$condit\dot{l}on\mathit{8}(\neq \mathit{1})$$(\neq \mathit{2})$$\mathcal{O}(\mathrm{M}_{i})$$\mathcal{O}(\mathrm{M}_{j})$$J(\mathrm{M}_{f} ; S)$$\mathit{8}uper_{-}intuiti_{\mathit{0}n}i\mathit{8}tiC$$\mathit{8}equence\{\mathrm{L}_{i}\}_{i<\omega}$$J(\mathrm{M}_{i} ; S)(i<\omega)i_{\mathit{8}}$$\mathit{8}uper- intuitioni_{\mathit{8}}tic$$(\langle \mathrm{M}_{i}, D_{i}, P_{i}\rangle, V_{i})$$\mathrm{L}i_{\mathit{8}}$$L\langle \mathrm{M}_{i}, D_{i}, P_{i}\rangle(i<\omega)$$iogic\mathit{8}$$\mathrm{L}_{:}=\mathrm{L}+$$\mathit{8}equence\{\mathrm{K}_{i}\}_{i<\omega}$$\mathrm{K}_{i}=\mathrm{H}_{*}+J(\mathrm{M}_{i} ; S)(i<\omega)$

152

By the virtue of this Lemma, we can present a concrete example of a continuum ofand sentence .
logics whenever we have appropriate sequence, all ofare provable inSince all of the additional axioms.
constructed above are locate below
of finite Kripke bases satisfyIn [18], Wrotski constructed a sequence
ing the conditions (1) and (2) in Lemma 3.11. We fix this sequence and use it toshow our results. The following Lemma provides a criterion for a sentence to haveandof domain-sheaves, truth-value-sheaves andsequencesand satisfy the conditions
valuations, respectively, such thatin Lemma 3.11.
$S$$\{(\langle \mathrm{M}_{i}, D_{i}, P_{i}\rangle, V_{i})\}_{i<\omega}$$J(\mathrm{M}_{\dot{t}} ; S)(i<\omega)$$\mathrm{H}_{*}+S$$\mathrm{K}_{l}’ \mathrm{s}$$\mathrm{H}_{*}+S$$\{\mathrm{M}_{i}\}_{\dot{\iota}<\omega}$$S$$\{D_{i}\}_{\dot{\iota}<\omega},$$\{V_{i}\}_{i<\omega}$$\{P_{i}\}_{i<\omega}$$S$$\{(\langle \mathrm{M}_{i}, D_{\dot{l}}, P_{i}\rangle, V_{i})\}_{i<\omega}$be a sentence. Suppose that there exists a pendulum model
Lemma 3.12 Let
such that $V(0, S)=0_{P}$ and $V(1, S)=1_{P}$ , wherewith Card(M)base. Then, for every finite Kripke
two-element
such that
not true in it.
therea pendulum model$S$$\mathrm{W}=\{0,1\}i_{\mathit{8}}a$$(\langle \mathrm{W}, D, P\rangle, V)$$ba\mathit{8}e\mathrm{M}$$I\iota’r\dot{\iota}pke$$exi\mathit{8}tS$

Let$W^{*}$$(\langle \mathrm{M}, D^{*}, P^{*}),$$p$$V^{*})$

be a sentence defined by:$W^{*}$

where$\geq 2_{f}$$J(\mathrm{M};S))i_{\mathit{8}}$$\equiv\forall x((p(_{X)\supset\forall}yp(y))\supset\forall yp(y))\supset\forall xp(x)$.

is a unary predicate variable.

Theorem 3.13 Thereandbetween$\mathrm{H}_{*}$$exi\mathit{8}t\mathit{8}$a continuum of $super- intuitioni_{\mathit{8}}ti_{C}$ predicate$logic\mathit{8}$$\mathrm{H}_{*}+W^{*}$ ,Define a sequence$\{\overline{\mathrm{P}_{n}}\}_{n<\omega}$$\overline{\mathrm{p}_{0}}$$\equiv$$\mathrm{P}_{n+1}^{-}$of sentences inductively by:$q\wedge\neg q$,$\equiv\forall x(p_{n+}1(X)(p_{n+1}(_{X})\supset\overline{\mathrm{P}_{n}}))$,

where is a propositional variable and each $p_{n}(n<\omega)$ is a unary predicate variable.
The following Theorem can be proved similarly.
$q$

Theorem 3.14 For each $n<\omega$ , there
and.
predicate logics between$\mathrm{H}_{*}$$exi\mathit{8}t\mathit{8}$a continuum of super-intuitionistic$\mathrm{H}_{*}+\overline{\mathrm{P}_{n}}$We make a remark here that theheight not greater than . By Lemma 1.11,
Kripke bases having height not greater than$\mathrm{s}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{e}\mathrm{n}\mathrm{C}\mathrm{e}\underline{\overline{\mathrm{p}}}n$$n$$\mathrm{P}_{n}$$n$is valid in every Kripke frames withis valid in every Kripke sheaves with.

Now we deal with the disjunction and existence properties.

Definition 3.15 (1) A super-intuitionistic predicate logic is said to have theand , eitheror
is provable inproperty, if for every formula
whenever $AB$ is provable in L.
(2) A super-intuitionistic predicate logic is said to have the existence property,, there exists such that $A(a)$ is provable in whenever
if for every formula$\mathrm{L}$

$B$

$A$

$di_{\mathit{8}}junCti_{\mathit{0}n}$

$A$

$B$

$\mathrm{L}$$\mathrm{L}$$\exists xA(x)$$\exists xA(x)$is provable in L.

$a$$\mathrm{L}$153

We would like to find a sufficient condition for alogic to have both of the disjunctionand existence properties. Our idea comes from an observation of the delta operationin super-intuitionistic predicate logics.

Definition 3.16 For each formula$A$, define$\triangle(A)\equiv p(P\supset A)$,

where is a propositional variable not occurring in . Let be a super-intuitionisticbypredicate logic. We define a super-intuitionistic predicate logic
$A$

$p$

$\mathrm{L}$$\triangle(\mathrm{L})$$\triangle(\mathrm{L})=\mathrm{H}*+\{\triangle(A) ; A\in \mathrm{L}\}$.

is originally defined on the set of super-intuitionistic propositional logics
The(see [4]). Some properties of on super-intuitionistic propositional logics can be rather
faithfully translated to those of the extended on super-intuitionistic predicate logics.
The following Fact can be shown in ways that are similar to those used for the case of
super-intuitionistic propositional logics.
$\triangle$$\triangle$$\triangle$.
predicate logic
Fact 3.17 (1) For every
and-intuitionistic predicate logics(2) For every.
predicate logic and every formula $A,$
if(3) For every.
and only if-intuitionistic predicate
is one-to-one as a mapping of the(4)of all.
to$\mathit{8}uper- intuitioni_{\mathit{8}}ti_{C}$$\mathrm{L},$$\mathrm{L}_{2},$$\mathrm{L}_{1}$$\triangle(\mathrm{L})\subseteq \mathrm{L}$$\mathrm{L}_{1}\subseteq \mathrm{L}_{2}implie\mathit{8}$$\mathit{8}uper$$\triangle(\mathrm{L}_{1})\subseteq\triangle(\mathrm{L}_{2})$$A\in \mathrm{L}$$\mathrm{L}$$\mathit{8}upe\gamma- intuitioni_{\mathit{8}}ti_{C}$$\triangle(A)\in\triangle(\mathrm{L})$$\mathit{8}et$$\triangle$$\mathit{8}uper$$it\mathit{8}elf$$logic\mathit{8}$As is often the case with logicians who try to extend things in propositional logics
to those in predicate logics, we can find contrast between propositional and predicate
logics. One of the most interesting results is the following.

Fact 3.18 (Propositional) For every propositional logic
if and only if
is the intuitionistic $propo\mathit{8}itional$ logic. That is, the intuitionistic logic is the uniquefixed point of .
-intuitionistic predicate logica(Predicate) There.
which not identical to$\mathrm{J},$$\triangle(\mathrm{J})=\mathrm{J}$$\mathrm{J}$$\triangle$$exist\mathit{8}$$\mathrm{L}\mathit{8}atisfying\triangle(\mathrm{L})=\mathrm{L}$$\mathit{8}uper$$\mathrm{H}_{*}$$i_{\mathit{8}}$are fixed points of , whereandFor example,$\neg p(x))$ withbeing a unary predicate variable. These non-trivial fixed points ofhave interesting properties from the logical point of view.
$\mathrm{H}_{*}+K$$\mathrm{H}_{*}+W^{*}$$\triangle$$I\mathrm{f}\equiv\neg\neg\forall x(p(x)$$\triangle$$p$Lemma 3.19 If$\triangle(\mathrm{L})=\mathrm{L}$, then$\mathrm{L}ha\mathit{8}$the disjunction and$exi\mathit{8}tenCepropertie\mathit{8}$

.

154

, then has both of the disjunction and existence properties andHence, if
the same propositional fragment as the intuitionistic logic. Now we show the existenceof a continuum of such logics. For this purpose, it suffices to show the following lemma,$\mathrm{L}$$\triangle(\mathrm{L})=\mathrm{L}$which implies the existence of a continuum of fixed points of$\triangle$.

Lemma 3.20 We can construct a denumerable $\mathit{8}equenCe\{X_{i} ; i<\omega\}$ ofsuch thatis a fixed point of(1) for eachis strongly independent.
(2)$sub_{\mathit{8}e}tS\subseteq\omega,$$\mathrm{H}_{*}+\{X_{i} ; i\in S\}$$\triangle$$axiom\mathit{8}$,$\{\mathrm{H}_{*}+X_{\dot{l}}\}\dot{\iota}<\omega$

The methods in [15] do not provide the axioms satisfying (1) and (2) of Lemma 3.20.
The Wajsberg method generates axioms of the form $W_{i}S(?<\omega)$ . Here each$(i<\omega)$ is a special axiom not provable in
is a fixed. Hence, if
by the disjunction property. Then
is not provable inpoint of , then$i<\omega$for each. The Jankov method gives axioms each of which
is not valid in some Kripke sheaf with finite Kripke base. On the other hand we have
$W_{\dot{l}}$$\mathrm{H}_{*}+W_{\dot{l}}S$$\mathrm{C}_{*}$$\triangle$$S$$\mathrm{H}_{*}+W_{i}$$\mathrm{H}_{*}+W_{i}\vee S=\mathrm{H}_{*}+S$

Proposition 3.21 If
sheaf with finite Kripke$\mathrm{H}_{*}+S$$ba\mathit{8}e$.

is a fixed point of$\triangle$, then$Si_{\mathit{8}}$valid in every Kripke

Hence we cannot apply methods in [15]. We shall use our newly modified method.
Lemma 3.22 For every sentence $A,$$\mathrm{H}_{*}+A\supset W^{*}$

is a fixed point of$\triangle$.

is of the form $A\supset W^{*}$ , the sequence $\{J(\mathrm{M}_{i} ; W^{*}) ; i<\omega\}$Sincesatisfies the condition (1) of Lemma 3.20. In Theorem 3.13, we have already provedthat this sequence satisfies the condition (2) of Lemma 3.20, and hence, we have$J(\mathrm{M}_{i} ; W^{*})$a continuum of $super- intuitioni_{\mathit{8}}ti_{C}$ predicate
Theorem 3.23 Thereand moreover theboththeand existence
which
has
each ofof
logic.
thefragment$exist\mathit{8}$$logic\mathit{8}$$propertie\mathit{8}$$di_{\mathit{8}}junCti_{\mathit{0}n}$$\mathit{8}ame_{\mathrm{P}^{r}}opo\mathit{8}itional$$a\mathit{8}$$intuitioni_{\mathit{8}}tic$

Ferrari and Miglioli [1] constructed a continuum of logics with both of the disjunction and existence properties by highly transcendental manner. In fact, none of theirlogics have the same propositional fragment as the intuitionistic logic, and are finitely
axiomatizable. On the other hand, we have here infinitely many finitely axiomatizable
logics with these properties and the same propositional fragment as the intuitionistic
logic.
In [15], we presented the following problem:(Problem 3 in [15]) How many$logic\mathit{8}$are there between$\mathrm{H}_{*}$

and$\mathrm{H}_{*}+K$?

Unfortunately, our method developed here cannot be applied to this problem, either.
In fact, $K$ is valid in every pendulum with finite Kripke base. Hence, the above problem
still remains open. We know only that there exist at least infinitely many logics between.
and$\mathrm{H}_{*}$$\mathrm{H}_{*}+K$

155

References[1] M. Ferrari and P. Miglioli, Counting the maximal intermediate constructive logics,
Journal of Symbolic Logic 56(1993), pp. 1365-1401.
[2] S. Ghilardi, Presheaf semantiC8 and independence
for some non-classical125-136.
(1989),
pp.
Logic
Mathematicalfor
Archive
logics,first-order$result_{\mathit{8}}$[3] S. Ghilardi, Incompleteness results in Kripke semantics, Journal of Symbolic Logic(1991), pp. 517-538.
[4] T. Hosoi, On intermediate logics I and II, Journal of Faculty of Science, Universityof Tokyo, section I 14(1967), 293-312, and 16(1969), 1-12.

[5] V. A. Jankov, Constructing a 8equence of 8trongly independent 8uperintuiti0ni8tiC
propositional calculi, Soviet Mathematics Doklady 9(1968), 806-807.
[6] S. Mac Lane, Categories for the Working Mathematician, Springer-Verlag,
New York Heidelberg Berlin 1971.

property for some intermediate predicate $logi_{C}s$ , Reports[7] T. Nakamura,on Mathematical Logic 15(1983), pp. 33-39.
$Di_{\mathit{8}}junCti_{\mathit{0}n}$[8] S. Nagai, On afor non-cla88ical logics, Proceedings of the Japan
Academy 49(1973), pp. 337-340.
$\mathit{8}emanti_{CS}$[9] H. Ono and S. Nagai, Application of general
Journal of Tsuda College 6(1974), 9-21.

$I\zeta ripkemodel_{\mathit{8}}$to intermediate logic8,[10] H. Ono, Some problems in intermediate predicate logic8, Reports on Mathematical
Logic 12(1987), 55-67.
[11] V. B. Shehtman and D. P. Skvortsov, Semantics of non-classical first-order predicate logiC8, in Mathematical Logic, edited by P. P. Petkov, Plenum Press, New
York, 1990, pp. 105-116.

[12] T. Shimura and N.-Y. Suzuki, Some super-intuitionistic logics as the logical fragment8 of equational theories, Bulletin of the Section of Logic 22(1993), pp. 106112.

[13] D. P. Skvortsov and V. B. Shehtman, Maximal Kripke-type 8emantiCS formodal and 8uperintuitioniStiC predicate logics, Annals of Pure and Applied Logic
63(1993), pp. 69-101.
[14] N.-Y. Suzuki, Some re8ults on the Kripke sheaf semantics for super-intuitionistic
predicate logic8, Studia Logica 52(1993), pp. 73-94.

156[15] N.-Y. Suzuki, Constructing a continuum of predicate
diate propositional logic\rangle Studia Logica 54(1995), pp. 173-198.

$exten\mathit{8}i_{onS}$of each interme-[16] A. S. Troelstra, On intermediate propositional logics, Indagationes Mathematicae27(1965), 141-152.
[17] T. Umezawa, On logics intermediate between
logic, Journal of Symbolic Logic, 24(1956), 141-153.

$intuitioni_{\mathit{8}}tic$

and classical predicate[18] A. Wrotski, The degree of completene8s of 8ome fragments of the intuiti0l8tic
propositional logic, Reports on Mathematical Logic 2(1974), 55-62.

Nobu-Yuki SUZUKI

Department of Computer and Information Sciences
Faculty of Engineering
Ibaraki University
Nakanarusawa, Hitachi 316
JAPAN