数理解析研究所講究録 1301 巻 2003 年 92-121

92
A Proof-Theoretical Study on Logics with
Constructible Falsity
HASUO Ichiro

蓮尾一郎

鹿島 亮

KASHIMA Ryo

東京工業大学大学院数理・計算科学専攻
Department of Mathematical and Computing Sciences
Tokyo Institute of Technology
O-okayama, Meguro, Tokyo 152-8552, JAPAN{hasu02, kashima}@is.titech.ac.jp
http: //www.is. t itech. ac.jp/\sim { hasuo2, kashima}

November 26, 2002
Abstract

also called strong negation, is an alternative to HeytConstructible
in intuitionistic logics. In this paper we give theing’s negation
proofs for Kripke completeness of the basic logic
and its five variations. Amongthem the most ffesh results are about the logics with what we call omniscienceaxiom, $\neg\neg(A\vee\sim A).$ We present two different proofs based on tree-sequents: one
is by an embedding of classical logic, and the other is by an extended version of$\mathrm{f}\mathrm{a}\mathrm{k}\mathrm{i}\mathrm{t}\mathrm{y}\sim A,$$\neg A(rightarrow(Aarrow[perp]))$$\mathrm{N}_{\neg}$tree-sequent.

1

Introduction

introduced by Heyting is a realization as aformal system ofIntuitionistic logic
Brauwer’s intuitionism as to mathematics. However, its negation
which is equivcalled Heyting’s negation to make distinct
alent tois subject
to criticisms that it is not constructive enough. For instance, it seems a natural de, we must know
mand from constructivists’ point of view that in order to show
aconcrete object such that $\neg A[t/x]$ holds. But this is not the case with Heyting’s$\mathrm{l}\mathrm{n}\mathrm{t}$$\neg A,$

$Aarrow[perp] \mathrm{a}\mathrm{n}\mathrm{d}$$\mathrm{f}\mathrm{r}\mathrm{o}\mathrm{m}\sim A,$$\neg\forall xA$$t$

negation.
, called construclible falsity or strong negation, was introduced independently
is axiomatized in the Hilbert-style system
by Nelson [Ne149] and Markov [Mar50].
as follows:$\sim A$$\sim A$

$Aarrow(\sim Aarrow B)$$\sim(A\Lambda B)rightarrow\sim A\vee\sim B$$\sim(Aarrow B)rightarrow A\Lambda\sim B$$\sim\forall xArightarrow\exists x\sim A$

It is easy to verify that$\sim \mathrm{i}\mathrm{s}$$\sim(A\vee B)rightarrow\sim A\wedge\sim B$$\sim\sim Arightarrow A$$\sim\neg Arightarrow A$$\sim\exists xArightarrow\forall x\sim A$

free ffom such criticisms as stated above.

93
The logic*( stands for Nelson’s logic) is the -free fragment ofplus constructible falsity
as above. The basic logic considered in this paper isthe logic
plus HeyCing’s negation .
We will also consider the variations ofwhich are obtained by adding some of
the following characters:$\mathrm{N}$$\mathrm{N}$$\mathrm{l}\mathrm{n}\mathrm{t}$$\neg$$\sim \mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{z}\mathrm{e}\mathrm{d}$$\mathrm{N}_{\neg},$$\mathrm{N}$$\neg$$\mathrm{N}_{\neg}$$\mathrm{D}$Constant domain Ctziom, $\forall x(A(x)\vee B)arrow\forall xA(x)\vee B$ . Here have no freeoccurrences in . Its name comes from the fact that aKripke model for Int
which makes this axiom valid has aconstant domain, i.e. the same domain forevery possible world. This is one of the axioms which characterize intermediate
$x$

$B$

(or super-intuitionistic) logics.

, which the authors would like to call omniscience ctziom. This axiom
is needless to say peculiar to the logics with both, and as we shall show
later, it is interpreted as a reference to Kripke model that every possible world
has an omniscient world which approves it. This axiom may also be considered
as one of the weaker versions of the law of excluded middle,.

$\mathrm{O}\neg\neg(A\vee\sim A)$$\sim \mathrm{a}\mathrm{n}\mathrm{d}$$\neg$$A\vee\sim A\dagger$$\mathrm{P}$This indicates omitting the axiom $Aarrow(\sim Aarrow B)$ , and as aresult we haveparaconsistency.

With these three characters we obtain $8(=2^{3})$ variations oflattice (the upperright the stronger) presented below (Fig. 1).

$\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{N}_{\neg}$, which form the$\mathrm{N}_{\neg}$$-\mathrm{P}$Fig. 1:In the literature [AN84]
is referred to asor$\mathrm{N}^{+},$$\mathrm{N}^{-}$$\mathrm{N}\mathrm{D},$$\mathrm{N}^{+-}$$\mathrm{N}\mathrm{P}$$\mathrm{N}_{\neg}$-family

or NDP ( -free fragment of$\neg$$\mathrm{N}_{\neg}\mathrm{D},$$\mathrm{N}_{\neg}\mathrm{P}$or$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$), respectively.

’In this paper the word logic is used for apair of aformal language and the set of formulas of that
language which are admitted as theorems. To define the set of theorems, we will adopt Gentzen-stylesequent systems.
is said to be the weak law of excluded middle and characterizes intermediate logics.
$\uparrow\neg A\vee\neg\neg A$

94
In this paper we prove Kripke completeness of logics
DO.
andFor each logic we introduce a Gentzen-style sequent calculus, Kripke-type possible
world semantics, and give the correspondence between them, i.e. the completenesstheorem. For the proof of completeness, we adopt the general method tree-sequent.
Roughly stated, atree-sequent is finite tree each of whose nodes are associated with asequent. Since it simulates the shape of Kripke models for variations oflnt, we can easily
obtain acounter-model for an unprovable sequent by expanding the corresponding tree,
sequent, hence the proof of completeness. In the literature [Kas99] applications forpresented.
logicsarerelevant
andlogics,some intermediate logics, modal
DO, we can hardly prove their Kripke completeness byandFor the logics
simply applying the tree-sequent method, because omniscience axiom may be regarded
as areference to “upper bounds” of Kripke models. Fkesh results in this paper lie inthe proofs for them; we present two different methods to consider the logics with O.
and its idea is that an omniscient
One uses an embedding of classical logic into
) The
(whichusually called aisCI-modelbyapossible world can be induced
other proof is by an extended version of tree-sequent which the authors would like tocall tree-sequent with guardians.
orremain unconsidered in thisKripke completeness of the logic
logic
into
classical
those two logics, so that
paper. It is hard to find an embedding of
our first method fails. And the method of tree-sequent with guardians also fails, while
in fact, the authors are not certain
andtree-sequent can treat the logics
is complete. In any case, they requireor
as to which type of models
more inspection .
$\mathrm{N}_{\neg},$$\mathrm{N}_{\neg}\mathrm{D},$$\mathrm{N}_{\neg}\mathrm{P},$$\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P},$$\mathrm{N}_{\neg}$$\mathrm{a}$$\mathrm{l}\mathrm{n}\mathrm{t}$$\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{N}_{\neg}$$\mathrm{C}1$$\mathrm{N}_{\neg}\mathrm{O},$$st_{7\mathrm{U}C}ture$$.$$\mathrm{N}_{\neg}\mathrm{O}\mathrm{P}$$\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{O}\mathrm{P}$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P};$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{O}\mathrm{P}$$\mathrm{N}_{\neg}\mathrm{O}\mathrm{P}$We describe the notations used in this paper.
areandsyntactical equivalence. For example,
The relation
However,.
paper.
A
logically equivalent in those logics considered in this$A[y/x]$ is asubstitution, i.e. a formula obtained by substituting every free occurIt is not preferable that by substituting by a new boundrence of in byvariable comes to existence, which is the case when a free occurrence of is in ascopeof . We avoid such cases by taking variants, i.e. substituting bound variables.
As we do in the Tarski-type semantics for CI, in defining semantics we will introduce
constants each of which designates a certain individual $u.$ This kind of constant is said
to be the name of $u,$ and denoted by .
We will sometimes denote a formula by $A(x)$ to emphasize that has free occurrences only in $A,$ as we just did to demonstrate constant domain axiom. However,more often we do not add (x) but do put explicitly as “ has no free occurrence in. . .”.
(or) is defined as
For afinite set of formulas $\Gamma=\{A_{1}, \ldots, A_{m}\},$ the, then it is (or 1), which is an abbreviation
). If
(or
$AarrowA$$\neg(AarrowA)$
respectively).
,(orof$A$ $\Lambda B$$\equiv \mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\mathrm{s}$$B\Lambda$$A$$\Lambda B\not\equiv B\Lambda A$

$x$

$A$

$x$

$y.$

$y$

$x$

$\forall y$$\underline{u}$

$x$

$x$

$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{a}\wedge\Gamma$$A_{1}\Lambda\ldots\Lambda A_{m}$$A_{1}\vee\ldots\vee A_{m}$$\Gamma=\emptyset$$\Gamma$$\mathrm{T}$ISome other cut-free sequent systems are presented by Ishimoto [Ish70], and Kripke completenessplus constants) is presented by Tanaka [Tan80] whose proof is done differently from ours.
it, it seems reasonable to admit
as an\S When we consider alogic with both and$\neg Aarrow(\sim\neg Aarrow B)$ is provable even without
formula
fact
that
the
in
the
results
However,
thisaxiom.
can have only
the axiom $Aarrow(\sim Aarrow B)$ , which designates that any paraconsistent variation oflimited paraconsistency.

of$\Sigma$($\mathrm{N}$$\neg$$\sim \mathrm{i}\mathrm{n}$$\sim\neg Arightarrow A$$\mathrm{N}_{\neg}$

95
2Logic2.1$\mathrm{N}_{\neg}$Sequent System$\mathrm{G}\mathrm{N}_{\neg}$

Here we introduce the Gentzen-style sequent system for the logic
The language of the logic -consists of the following symbols:$\mathrm{N}_{\neg}$.

$\mathrm{N}$$\bullet$$\bullet$$\bullet$countably many variables,$x_{1},$$x_{2},$;$\ldots$

countably many m-ary predicate symbols for each

logical connectives,$\vee \mathrm{a}\mathrm{n}\mathrm{d}$$\Lambda,$$\neg,$$arrow,$$\forall$$\sim,$$m\in \mathrm{N},$$p_{m}^{1},$$p_{m}^{2},$$\ldots$;.

are introduced as defined symbols:$\exists$$\exists xA\equiv\sim\forall x\sim A$$A\vee B\equiv\sim(\sim A\Lambda\sim B)$

is an abbreviation of $(Aarrow B)\Lambda(Barrow A)$ .
We do not consider constants or function symbols, which makes the arguments
simpler without essential loss of generality.
are composed in the same way as those of Cl, and noteTerms and formulas ofunary.
that
Asequent is defined as an ordered pair of finite sets of formulas, therefore the ruleof exchange or contraction is omitted.
Now we present the axioms and the inference rules of the Gentzen-style sequent:systemfor the logic$Arightarrow B$$\mathrm{N}_{\neg}$$\sim \mathrm{i}\mathrm{s}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}$$\overline{A\Rightarrow A}$(axiom 1)$\overline{A,\sim A\Rightarrow}(\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m} 2)$$\frac{\Gamma\Rightarrow\Delta}{\Sigma,\Gamma\Rightarrow\Delta,\Pi}$(weakening)$\frac{\Gamma\Rightarrow\Delta,AA,\Sigma\Rightarrow\Pi}{\Gamma,\Sigma\Rightarrow\Delta,\Pi}$$\frac{A,B,\Gamma\Rightarrow\Delta}{A\Lambda B,\Gamma\Rightarrow\Delta}(\Lambda \mathrm{L})$$\frac{\Gamma\Rightarrow\Delta,A\Gamma\Rightarrow\Delta,B}{\Gamma\Rightarrow\Delta,A\Lambda B}(\Lambda \mathrm{R})$$\frac{A,\Gamma\Rightarrow B}{\Gamma\Rightarrow Aarrow B}(arrow \mathrm{R})_{\mathrm{S}}$$\frac{\Gamma\Rightarrow\Delta,AB,\Sigma\Rightarrow\Pi}{Aarrow B,\Gamma,\Sigma\Rightarrow\Delta,\square }(arrow \mathrm{L})$$\frac{A,\Gamma\Rightarrow}{\Gamma\Rightarrow\neg A}(\neg \mathrm{R})_{\mathrm{S}}$$\frac{\Gamma\Rightarrow\Delta,A}{\neg A,\Gamma\Rightarrow\Delta}(\neg \mathrm{L})$$\frac{A[y/x],\Gamma\Rightarrow\Delta}{\forall xA,\Gamma\Rightarrow\Delta}(\forall \mathrm{L})$$\frac{\Gamma\Rightarrow A[z/x]}{\Gamma\Rightarrow\forall xA}(\forall \mathrm{R})_{\mathrm{S},\mathrm{V}\mathrm{C}}$$\frac{\sim A,\Gamma\Rightarrow\Delta\sim B,\Gamma\Rightarrow\Delta}{\sim(A\Lambda B),\Gamma\Rightarrow\Delta}(\sim\Lambda \mathrm{L})$$\frac{A,\sim B,\Gamma\Rightarrow\Delta}{\sim(Aarrow B),\Gamma\Rightarrow\Delta}(\simarrow \mathrm{L})$$\frac{A,\Gamma\Rightarrow\Delta}{\sim\neg A,\Gamma\Rightarrow\Delta}(\sim\neg \mathrm{L})$$\frac{A,\Gamma\Rightarrow\Delta}{\sim\sim A,\Gamma\Rightarrow\Delta}(\sim\sim \mathrm{L})$(cut)$\frac{\Gamma\Rightarrow\Delta,\sim A,\sim B}{\Gamma\Rightarrow\Delta,\sim(A\Lambda B)}(\sim\Lambda \mathrm{R})$$\frac{\Gamma\Rightarrow\Delta,A\Gamma\Rightarrow\Delta,\sim B}{\Gamma\Rightarrow\Delta,\sim(Aarrow B)}(\simarrow \mathrm{R})$$\frac{\Gamma\Rightarrow\Delta,A}{\Gamma\Rightarrow\Delta,\sim\neg A}(\sim\neg \mathrm{R})$$\frac{\Gamma\Rightarrow\Delta,A}{\Gamma\Rightarrow\Delta,\sim\sim A}(\sim\sim \mathrm{R})$96$\frac{\Gamma\Rightarrow\Delta,\sim A[y/x]}{\Gamma\Rightarrow\Delta,\sim\forall xA}(\sim\forall \mathrm{R})$$\frac{\sim A[z/x],\Gamma\Rightarrow\Delta}{\sim\forall xA,\Gamma\Rightarrow\Delta}(\sim\forall \mathrm{L})_{\mathrm{V}\mathrm{C}}$

Here the subscript indicates the condition that the succedent of the conclusion consist
the eigenvariable condition, i.e. the eigenvariable mustof only one formula, andnot appear in the conclusion.
if.
Aformula is provable inwhich require some remarks.
Now we consider logical equivalence in$\mathrm{S}$$\mathrm{V}\mathrm{C}$

$A$

$z$

$\mathrm{G}\mathrm{N}_{\neg},$$\mathrm{G}\mathrm{N}_{\neg}\vdash\Rightarrow A$$\mathrm{G}\mathrm{N}_{\neg}\vdash A,$$\mathrm{N}_{\neg}$)
DEFINITION 2.1 (LOGICAL EQUIVALENCE IN.
and $B$ are logically equivalent,Let
and $B$ be formulas of.
and$\mathrm{N}_{\neg}$$A$$\mathrm{N}_{\neg}$$A$$A\cong_{\mathrm{N}_{\neg}}B$

THEOREM 2.2 (THE EQUIVALENCE THEOREM)
where the special atomic fomula
Let $C[]$ be a formula ofand $C[A]$ a formula obtained by substituting every occurence of.
, Then$[]$$\mathrm{N}_{\neg}$$[]$is alloeved to appear,by the formula A. If$C[A]\cong_{\mathrm{N}_{\neg}}C[B]$$A\cong \mathrm{N}_{\neg}B$1

By the induction on the construction of $C[]$ .

Proof.

, if$\mathrm{G}\mathrm{N}_{\neg}\vdash\sim Arightarrow\sim B$$\mathrm{G}\mathrm{N}_{\neg}\vdash Arightarrow B$

REMARK 2.3
define the logical equivalence
It is common in alogic which does not
However,
this is not enough to allow the equivalence theorembywe shall see in lemma 2.8.
for the logics with$\mathrm{h}\mathrm{a}\mathrm{v}\mathrm{e}\sim \mathrm{t}\mathrm{o}$$\mathrm{L}$$A\cong\llcorner B$$\mathrm{L}\vdash Arightarrow B.$$\sim \mathrm{a}\mathrm{s}$It is required naturally that the meaning of a formulation of bound variables.
LEMMA 2.4
If has no free occurrences in $A,$ then.
equivalent in
$z$

$A$

$\forall zA[z/x]\cong_{\mathrm{N}_{\neg}}\forall xA,$

is invariant as to substitu-$i.e$. variants are logically$\mathrm{N}_{\neg}$

2.2

Kripke-Type Semantics for$\mathrm{N}_{\neg}$

The Kripke-type possible world semantics foris introduced as anatural extensionof that for Int, which is one of the reasons why logics with constructible falsity areworthy of consideration.
, satisfying
Let $(M, \leq)$ be aposet, $W$ a non-empty set, $U$ be a map of $M$ into$\mathrm{N}_{\neg}$$\mathfrak{P}W$$\bullet$$\bullet$$U(a)\neq\emptyset$$a\leq b$

for all $a\in M$ ;implies $U(a)\subseteq U(b)$ .

For every predicate symbol
in $a\in M,$
and

$p$

$\bullet$$a\leq b$$p$(we assumeis m-ary), we define two interpretations of, as subsets of $U(a)^{m}$ , satisfying$p^{I^{+}(a)}$$p^{I^{-}(a)}$implies$p^{I^{+}(a)}\subseteq p^{I^{+}(b)}$$\bullet p^{I^{+}(a)}\cap p^{I^{-}(a)}=\emptyset$

.

and

$p$

$p^{I^{-}(a)}\subseteq p^{I^{-}(b)}$;97Then the quintuple $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ is said to be an-model.
An element in $M$ is said to be apossible world, and can be thought of as astageof our knowledge. $a\leq b$ can be read as is more advanced, knows more than . $U(a)$is called adomain of , being the set of individuals recognized by .
, we can obtain the two relations between $a\in M$ and aGiven anclosed formula $A,$
and $a\models^{-}A$ , by extending two interpretations
andin the procedure shown below.
may be interpreted as “a verifies
or”or “a refutes ”respectively (this terminology the authors hope reflects the ideaof constructivism).
andare defined inductively on the construction of the closed
formula :$\mathrm{N}_{\neg}$

$a$

$b$

$a$

$a$

$a$

$\mathrm{N}_{\neg}-\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1\mathfrak{M}$$a\models^{+}$$A$$I^{+}$$a\models^{+}$

$A$

$A$

$a\models^{-}$$I^{-}$$A$$A$$a\models^{+}$$A$$a\models^{-}$

$A$

$A$

$a\models^{+}p(\underline{u_{1}}, \ldots,\underline{u_{m}})$$\Leftrightarrow$$(u_{1}, \ldots, u_{m})\in p^{I^{+}(a)}$;$a\models^{-}p(\underline{u_{1}}, \ldots,\underline{u_{m}})$$\Leftrightarrow$$(u_{1}, \ldots, u_{m})\in p^{I^{-}(a)}$;$\Lambda B$$\Leftrightarrow$$a\models^{+}A$and$a\models^{-A\Lambda B}$$\Leftrightarrow$$a\models^{-A}$or$a\models^{+}A$$a\models^{+}Aarrow B$$\Leftrightarrow$$a\models^{-A}arrow B$$\Leftrightarrow$$\Leftrightarrow$$a\models^{+}A$;$a\models^{+}\sim A$$\Leftrightarrow$$a\models^{-}A$;$a\models^{-}\sim A$$\Leftrightarrow$$a\models^{+}A$;$\Leftrightarrow$;

implies$b\models^{+}A$$b\models^{+}B$;

and $a\models^{-B}$ ;for every $b\geq a$ , $b\#^{+}A$ ;$a\models^{-}\neg A$$a\models^{-}\forall xA$;$a\models^{+}A$$\Leftrightarrow$$\Leftrightarrow$$a\models^{-}B$for every $b\geq a$ ,$a\models^{+}\neg A$$a\models^{+}\forall xA$$a\models^{+}B$for every $b\geq a$ and every $u\in U(b)$ ,for some $u\in U(a)$ ,.

$b\models^{+}A[\underline{u}/x]$;$a\models^{-}A[\underline{u}/x]$

The case where neithernorholds is interpreted as “a cannot tell
the tmth of ”and denoted by $a\#^{+-}A$ .
, if
Aformula ofis valid in an-model $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ ,$a\inM$, wherefor every
is valid,
is auniversal closure of A.
, if is valid in every-model.
A sequent),ofis valid (or valid in ),(or
if the formula $(\wedge\Gamma)arrow(\Delta)$ is valid (or valid in ).
The result of the following lemma is necessary for $a\in M$ to be considered as astageof knowledge, and is verified easily by the induction on the construction of aformula$a\models^{+}$$A$$a\models^{-}$

$A$

$A$

$A$

$\mathrm{N}_{\neg}$$A$$\forall\vec{x}A$$a\models^{+}\forall\vec{x}A$$\mathrm{N}_{\neg}\models A$$\mathfrak{M}\models A$$\mathrm{N}_{\neg}$$A$$\mathrm{N}_{\neg}$$\Gamma\Rightarrow\Delta$$\mathfrak{M}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\models\Gamma\Rightarrow\Delta$$\mathfrak{M}\models\Gamma\Rightarrow\Delta$$\mathfrak{M}$$A$.

LEMMA 2.5$\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ be anLeta formula ofThen(or $a\models^{-A}$ ) implies(or$A$-model, $a,$ $b\in M$ and $a\leq b$ .
$b\models^{-A}$ , respectively).

$\mathrm{N}_{\neg},$$a\models^{+}A$$b\models^{+}A$$\mathrm{N}_{\neg}$

The next lemma is proved by the induction on the construction of aformula , theThisbase case of which is verified by the condition of an -model
is not the case for the logics with the letter , i.e. those which allow paraconsistency.
$A$$\mathrm{N}_{\neg}$$p^{I^{+}(a)}\cap p^{I^{-}(a)}=\emptyset.$$\mathrm{P}$LEMMA 2.6$\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ be an
Let a formula of
impossible that both $a\models^{+}A$ and $a\models^{-A}$ hold.
$A$$\mathrm{N}_{\neg},$$\mathrm{N}_{\neg}$-model and $a\in M.$ Then it is98with respect to the Kripke-type semantics
The soundness of the sequent system.
defined above is also easily proved by the induction on the derivation in$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}$

THEOREM 2.7 (KRIPKE s0UNDNESS OF.
, thenIf$\mathrm{G}\mathrm{N}_{\neg}\vdash\Gamma\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg}$)$\mathrm{N}_{\neg}\models\Gamma\Rightarrow\Delta$

From the soundness theorem we can obtain the following result which justifies the(see remark 2.3).
definition of logical equivalence in$\mathrm{N}_{\neg}$

COROLLARY 2.8
does not necessarily imply$\mathrm{G}\mathrm{N}_{\neg}\vdash\sim Arightarrow\sim B$$\mathrm{G}\mathrm{N}_{\neg}\vdash Arightarrow B$

Proof.

Let

$p$

and

$q$

.

be distinct 0-ary predicate symbols, then it is easy to verify.

$\mathrm{G}\mathrm{N}_{\neg}\vdash(p\Lambda\sim p)rightarrow(q\Lambda\sim q)$-model where $M=\{0\},$Here let $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ be an
hence
Then
contraposition of the theorem.
$\mathrm{N}_{\neg}$$\mathfrak{M}\#\sim(p\Lambda\sim p)rightarrow\sim(q\Lambda\sim q),$Now we can give some examples oforpresent them in comparison withCl or Int.
by$\mathrm{C}1$$0\models^{+}p,$$0\#^{+-}q$$\mathrm{G}\mathrm{N}_{\neg}\forall\sim(p\Lambda\sim p)rightarrow\sim(q\Lambda\sim q)$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}/\mathrm{u}\mathrm{n}\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}$$\mathrm{l}\mathrm{n}\mathrm{t}.$.

by$\mathrm{t}\mathrm{h}\mathrm{e}|$formulas in

In the table presented below,$\neg$$\mathrm{G}\mathrm{N}_{\neg}.$We

is denoted$\sim \mathrm{f}\mathrm{o}\mathrm{r}$2.3

Tree-Sequent System$\mathrm{T}\mathrm{N}_{\neg}$, and consider the relation, the tree-sequent system for
Here we introduce.
and the Gentzen-style system
betweenKripkecompleteness of
prove
subsection,using treeweshall
In the next
sequents. In general, aformal deductive system (of Hilbert-style, Gentzen-style, tableau
method, or else) is designed to derive a formula which is valid in any model of the corresponding semantics. This request can be stated differently, as “a formal deductive
system should derive aformula for which we have no counter models”. This may help
us understand how the idea of tree-sequents is obtained or justified.
we can assume a Kripke model to form atree by taking every
In variations ofmodel
as anew node. Thus if we would like aunit of deduction topath in an original
simulate the shape of Kripke models, its shape should be atree.
$\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{l}\mathrm{n}\mathrm{t},$Atree-sequent ofis finite tree each of whose nodes is associated with its
finite set of variables, and the, whereis asequent ofown
following conditions are satisfied:$\mathcal{T}$$\Gamma \mathrm{g}\Delta$$\bullet$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{a}$$\Gamma\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg},$

Let be an arbitrary node of
associated to
0of to , and$a$$\mathcal{T}$$\mathcal{T},$$a$$\Gamma_{i}\Rightarrow\alpha_{i}\Delta_{i}$$a\mathrm{o}(=0),$$\alpha \mathrm{a}$$a_{1},$$a_{i}.$$\ldots,$$a_{n}(=a)$

Then$\alpha 0,$$\alpha_{1},$apath from the root
are disjoint.
$\ldots,$$\alpha_{n}$99
The (disjoint) unionat the node a.
$\bullet$$\alpha_{0}\cup\alpha_{1}\cup\cdots\cup\alpha_{n}$is said to be the set of available variables

Every free variable which appears in the sequent associated to$a$is available at .
$a$), then isIf
is associated to anode (we will denote this by :the set of variables which are available at for the first time in tracing from the root.
:
We present an example of atree-sequent of$\Gamma\Rightarrow\alpha\Delta$$\Gamma\Rightarrow\alpha\Delta$

$a$

$a$

$\alpha$$a$$\mathrm{T}\mathrm{N}_{\neg}$$\neg(p(x)\vee\sim p(x))$

This tree-sequent can also be denoted in the following styles:$\{z\}\Rightarrow r(z, y)$$\underline{\neg(p(x)\vee\sim p(x))4p(x)\vee\sim p(x)\forall z(q(y)\vee r(z,y))\Rightarrow q(y)\vee\forall zr(z,y)\{y\}}$$\{x\}\Rightarrow\neg\neg(p(x)\vee\sim p(x))$

or$[$$\{x\}\Rightarrow\neg\neg(p(x)\vee\sim p(x))|[\neg(p(x)\vee\sim p(x))\Rightarrow^{\emptyset}p(x)\vee\sim p(x)]$$[\forall z(q(y)\vee r\langle z, y))\{y\}\Rightarrow q(y)\vee\forall zr(z, y)|\{z\}\Rightarrow r(z, y)]$$]$We will adopt the last one for the economy of space, i.e.
$\mathcal{T}_{m}$$\mathcal{T}_{1}$is denoted by$[\Gamma 3\Delta|\mathcal{T}_{1}\ldots \mathcal{T}_{m}]$.

$\Gamma\Rightarrow\Delta$

However, this style hardly clarify the structure of atree-sequent. It will help us understand better to rewrite in the first style.

The
inference rules:$\mathrm{t}\mathrm{r}\mathrm{e}\triangleright \mathrm{s}\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{e}\mathrm{n}\mathrm{t}$system$\mathrm{T}\mathrm{N}_{\neg}$derives tree-sequents using the following axioms and(axiom 2)–(axiom 1). . . [A$\overline{\ldots[A,\sim A\xi_{1}\ldots}$$\mathrm{g}A|\cdots$

For instance, (axiom 1) is interpreted that if asequent of the form.
to any node of , then$\mathcal{T}$$A\Rightarrow A$

is associated$\mathrm{T}\mathrm{N}_{\neg}\vdash \mathcal{T}$$\ldots\cdots\frac{[\Gamma\Rightarrow\Delta|}{[\Sigma,\Gamma\xi\Delta,\Pi|}\ldots\ldots$(weakening)This is interpreted as we can add any formula to the antecedent or the succedent of asequent associated to any node.

.

. . [ $A,$ $\Sigma\Rightarrow\Pi|\cdots$$\underline{\ldots[\Gamma\xi\Delta,A|\cdots}$...

$[\Gamma,$$\Sigma\Rightarrow\Delta,$$\Pi|\cdots$

(cut)

100
Here the tree-structure and the nodes not displayed are the same among the conclusion
and the two hypotheses .
$\underline{\ldots[\Gamma\Rightarrow\Delta|\alpha\ldots[A,\Sigma\Rightarrow\Pi|\cdots]\cdots]\beta\ldots}$...

(drop L)$[A, \Gamma\Rightarrow\Delta|\cdots[\Sigma\Rightarrow\Pi|\beta\ldots]\cdots]\cdots$

Here aformula in the antecedent of a node $b:A,$of asequent associated to the mother of .
$A$$\beta$$\Sigma\Rightarrow\Delta$

is dropped to the antecedent$b$$\underline{\ldots[A,B,\Gamma\Rightarrow\Delta|\cdots}(\Lambda \mathrm{L})$. . . [A$\Lambda B$,I$\epsilon\Delta|\cdots$ofis applied to one node (more precisely, a sequent associatedHere the rule
to one node), and the tree-structure and the nodes not displayed are the same between
the hypothesis and the conclusion.
$(\Lambda \mathrm{L})$$\mathrm{G}\mathrm{N}_{\neg}$$\ldots\ldots\frac{[\Gamma\epsilon\Delta,A|\cdots\cdots[\Gamma\epsilon\Delta,B|}{[\Gamma 3\Delta,A\wedge B|}\ldots\cdots(\Lambda \mathrm{R})$Here the tree-structure and the nodes not displayed are the same among the conclusion
and the two hypotheses. This kind of remark is to be attached to every inference rulepresented below.

...

$[B,$
$\underline{\ldots[\Gamma\xi\Delta,A|\cdots}$$\Sigma@\Pi|\cdots(arrow \mathrm{L})$. . . $[Aarrow B,$$\Gamma,$$\Sigma\xi\Delta,$ $\Pi|\cdots$$\underline{\ldots[\Gamma\epsilon\Delta|\cdots[A\Rightarrow B]\cdots]\emptyset\cdots}(arrow \mathrm{R})_{\mathrm{t}}$... [I$\xi\Delta,$$Aarrow B|\cdots$(which must be a leaf) of the nodein the hypothesis
Here the daughteris trimmed. The subscript will be added to the rules of this type, i.e. a leaf is trimmed.
$A\Rightarrow B\emptyset$$\Gamma\in\Delta$$\mathrm{t}$$\ldots\ldots\frac{[\Gamma\Rightarrow\Delta|\cdots[A4]\cdots]}{[\Gamma \mathrm{g}\Delta,\neg A|}\ldots\cdots(\neg \mathrm{R})_{\mathrm{t}}$$. \cdot\cdot\cdot\cdot\cdot\frac{[\Gamma 3\Delta,A|}{[\neg A,\Gamma 3\Delta|}..\cdot\cdot\cdot\cdot(\neg \mathrm{L})$$\underline{\ldots[A[y/x],\Gamma 3\Delta|\cdots}(\forall \mathrm{L})$.. . [$\forall xA$, I $\xi\Delta|\cdots$$\underline{\ldots[\Gamma\Rightarrow\Delta|\cdots[\Rightarrow A[z/x]]\cdots]\{z\}\ldots}(\forall \mathrm{R})_{\mathrm{t}}$. . . [I$\Rightarrow\Delta,\forall xA|\cdots$

is not available at the node associated with.
variable in$z$$\Gamma\xi\Delta,$

thus

$z$

does not appear as afree$\Gamma\Rightarrow\Delta$

rule is necessary for the proofs of lemma 2.9 and its counterparts for other logics, which areused only when omniscience axiom is involved. Hence just to prove the completeness of the logics
without the letter , we do not need cut rule.
Moreover, if the Gentzen-style system is proved to be cut-free, then cut rule of the tree-sequentsystem can also be omitted.
$\tau_{\mathrm{C}\mathrm{u}\mathrm{t}}$$\mathrm{O}$101$\ldots\ldots\frac{[\sim A,\Gamma\Rightarrow\Delta|\alpha[\sim B,\Gamma\Rightarrow\Delta|\alpha}{[\sim(A\Lambda B),\Gamma\Rightarrow\Delta|\alpha}\ldots\ldots\ldots\cdots(\sim\Lambda \mathrm{L})$$. \cdot\cdot\cdot\cdot\cdot\frac{[\Gamma 3\Delta,\sim A,\sim B|}{[\Gamma\Rightarrow\Delta,\sim(\alpha A\Lambda B)|}..\cdot\cdot\cdot\cdot(\sim\Lambda \mathrm{R})$$\underline{\ldots[A,\sim B,\Gamma\Rightarrow\Delta|\cdots}(\simarrow \mathrm{L})$. . . $[\sim(Aarrow B),$$\ldots\ldots\frac{[\Gamma 3\Delta,A|\cdots\cdots[\Gamma\Rightarrow\Delta,\sim B|}{[\Gamma\epsilon\Delta,\sim(Aarrow B)|}\ldots\cdots(\simarrow \mathrm{R})$$\Gamma 3\Delta|\cdots$.

$. \cdot\cdot\cdot\cdot\frac{[A,\Gamma\Rightarrow\Delta|}{[\sim\neg A,\Gamma\Rightarrow\Delta|}...\cdot\cdot\cdot(\sim\neg \mathrm{L})$$. \cdot\cdot\cdot\cdot\frac{[\Gamma\xi\Delta,A|}{[\Gamma\xi\Delta,\sim\neg A|}...\cdot\cdot\cdot(\sim\neg \mathrm{R})$$. \cdot\cdot\cdot\cdot\frac{[A,\Gamma 3\Delta|}{[\sim\sim A,\Gamma\xi\Delta|}...\cdot\cdot\cdot(\sim\sim \mathrm{L})$$. \cdot\cdot\cdot\cdot\frac{[\Gamma\xi\Delta,A|}{[\Gamma\Rightarrow\Delta,\sim\sim A|}...\cdot\cdot\cdot(\sim\sim \mathrm{R})$

.

.

.

.
$\ldots\ldots\frac{[\sim A[z/x],\Gamma 4^{z\}}\alpha\cup\Delta|}{[\sim\forall xA,\Gamma\Rightarrow\Delta|}\ldots\cdots(\sim\forall \mathrm{L})_{\mathrm{V}\mathrm{C}}$$.. \cdot..\frac{[\Gamma\Rightarrow\Delta,\sim A[y/x]|}{[\Gamma\Rightarrow\Delta,\sim\forallxA|}$$.\cdot\cdot\cdot\cdot(\sim\forall\mathrm{R})$.

, an abbreviation for the variable condition, is that the eigenvariable must notappear in any node of the conclusion.
Now we will consider the relation between, through the following
andtwo lemmas.
$\mathrm{V}\mathrm{C}$$z$$\mathrm{T}\mathrm{N}_{\neg}$

LEMMA 2.9
Let be a tree-sequent ofthen.
$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$. If$\mathcal{T}$has a node

$a$

:I4

$\mathrm{G}\mathrm{N}_{\neg}$$\Delta$such that$\mathrm{G}\mathrm{N}_{\neg}\vdash\Gamma\Rightarrow\Delta$,$\mathrm{T}\mathrm{N}_{\neg}\vdash \mathcal{T}$Proof.

By the induction on the derivation of. It is easy to checkinthe case where the rule or the axiom applied at last is other thani.e. thosewhich demand the succedent of the conclusion consist of only one formula. We will
only present the case for.
or, we have inFor$\Gamma\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg}$$($$(arrow \mathrm{R})_{\mathrm{S}},$$(arrow \mathrm{R})_{\mathrm{S}}$$(\neg \mathrm{R})_{\mathrm{S}}$$(\forall \mathrm{R})_{\mathrm{S},\mathrm{V}\mathrm{C}}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{i}\mathrm{n}\mathrm{d}$.

$\mathrm{h}\mathrm{y}\mathrm{p}$.

$.. \cdot.\cdot.\ldots\frac{\underline{[4|\cdots[\Gamma,A\Rightarrow B]\cdots]\emptyset}}{\frac{[\Gamma 3|\cdots[A\Rightarrow B]\cdots]0}{[\Gamma\Rightarrow Aarrow B|\alpha}}\ldots\cdot..\cdot.\cdot(\mathrm{d}\mathrm{r}\mathrm{o}\mathrm{p}\mathrm{L})(arrow \mathrm{R})$For$(\neg \mathrm{R})_{\mathrm{S}}$,$\mathrm{i}\mathrm{n}\mathrm{d}$.

$\mathrm{h}\mathrm{y}\mathrm{p}$.

$.. \cdot.\cdot.\ldots\frac{\underline{[3|\cdots[\Gamma,A\Rightarrow]\cdots]\emptyset}}{\frac{[\Gamma\Rightarrow|\cdots[\alpha A\Rightarrow]\cdots]\emptyset}{[\Gamma\Rightarrow\neg A|}}\ldots\cdot..\cdot.\cdot(\mathrm{d}\mathrm{r}\mathrm{o}\mathrm{p}(\neg \mathrm{R}) \mathrm{L})$$)_{\mathrm{S}}$

102
For

$(\forall \mathrm{R})_{\mathrm{S},\mathrm{V}\mathrm{C}}$,$\mathrm{i}\mathrm{n}\mathrm{d}$.

$\mathrm{h}\mathrm{y}\mathrm{p}$.
.

$. \cdot...\cdot\ldots\frac{[\alpha\Rightarrow|\cdots[\Gamma\Rightarrow A[z/x]]\cdots][\Gamma\Rightarrow|\cdots[\Rightarrow A[z/x]]\cdots]\{z\}\overline{\overline{\{z\}}}}{[\Gamma\Rightarrow\forall xA|}\ldots\cdot..\cdot\cdot$$(\forall \mathrm{R})(\mathrm{d}\mathrm{r}\mathrm{o}\mathrm{p} \mathrm{L})$I
A pre-tree-sequent ofsatisfies all the conditions of a tree-sequent except theone that if has ffee occurrence in :then is available atThis concept
is necessary for the proof of the next lemma which is done by an induction.
The translation into a fomula of a pre-tree-sequent of, isdenoted bydefined inductively on the height of ;$\mathcal{T}$$x$$\mathrm{T}\mathrm{N}_{\neg}$$\Gamma\Rightarrow\Delta$$a$$\mathrm{a}$

$x$

$a.$

$\mathcal{T}$$\mathcal{T}^{f}$$\mathrm{T}\mathrm{N}_{\neg},$$\mathcal{T}$$[\Gamma \mathrm{s}\Delta|\mathcal{T}_{1}\ldots \mathcal{T}_{m}]^{f}:\equiv\forall\not\supset((\wedge\Gamma)arrow(\vee\Delta)\vee \mathcal{T}_{1}^{f}\vee\cdots\vee \mathcal{T}_{m}^{f})$ofThen the next important lemma is proved, which approves so called the soundness$\mathrm{T}\mathrm{N}_{\neg}$.

LEMMA 2.10

If$\mathrm{T}\mathrm{N}_{\neg}\vdash \mathcal{T},$ihen$\mathrm{G}\mathrm{N}_{\neg}\vdash \mathcal{T}^{f}$.

To prove this lemma we will prepare a couple of sublemmas.

SUBLEMMA 2.11
be a tree-sequent ofLeta node ofa pre-tree-sequent which consists
pre-tree-sequents of, andbeof all the descendants oftree-sequent obtained by substitutingbyrespectively (Fig. 2).
$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg},$

$a,$

$a$

$\mathcal{T}_{1}’,$$\mathcal{T},$$\mathcal{T}’$$\mathrm{T}\mathrm{N}_{\neg}$$\mathcal{T}_{k}’$$\mathcal{T}_{1},$$\ldots,$$a$$\mathcal{T}_{k}$$\ldots,$$\mathcal{T}’$$\mathcal{T}_{1}’,$$\mathcal{T}_{k}’,$$\ldots,$

Fig. 2:Then$\mathrm{G}\mathrm{N}_{\neg}\vdash \mathcal{T}_{1}^{\prime f},$$\mathcal{T}_{k}^{\prime f}\Rightarrow \mathcal{T}^{\prime f}$$\ldots,$$\mathcal{T},$implies$\mathcal{T}_{1},$$\mathcal{T}_{k}$$\ldots,$$\mathrm{G}\mathrm{N}_{\neg}\vdash \mathcal{T}_{1}^{f},$$\mathcal{T}_{k}^{f}\Rightarrow \mathcal{T}^{f}$$\ldots,$.

$\mathrm{S}_{\mathrm{U}\mathrm{B}\mathrm{L}\mathrm{E}\mathrm{M}\mathrm{M}\mathrm{A}}2.12$

Let$\mathcal{T}$and$\mathrm{G}\mathrm{N}_{\neg}\vdash \mathcal{T}^{f}$$\mathcal{T}’$the same as those in the sublemma above. Then

implies$\mathrm{G}\mathrm{N}_{\neg}\vdash \mathcal{T}^{\prime f}$.

Proof. Both sublemmas are proved easily by the induction on the height of

$a$

in

.

$\mathcal{T}_{-}$

103
Proof of lemma 2.10

By the induction on the derivation of in. For the base case, i.e. when is anaxiom, use sublemma
step cases whereis derived by an inference rullwith ahypothesis (or hypotheses), use sublemma 2.11.
$\mathcal{T}$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$

2.12.teForthe

2.4$\mathcal{T}$$\mathrm{e}$Kripke Completeness of$\mathrm{G}\mathrm{N}_{\neg}$

Here we present the way how we can construct what we may call acounter-model. Then, hence Kripke completeness offor an unprovable tree-sequentof
Kripke completeness ofis obtained immediately by lemma 2.10.
, then we cantree-sequent of
The sketch is as follows. Let be an unR-saturated(we shall define
extend to obtain an infinite tree-sequent which is(here the-modelthis concept later). A-saturated tree-sequent induces an
set of available variables at is used as the seed of the domain of ), and this is what
we would like to obtain, i.e. acounter-model for .
-saturatedness, which is anatural extension
We start with defining the concept. Here an infinite tree-sequent ofof that for
is apossibly infinite tree each of, where andwhose node is associated with its own
are sets of apossibly, and is aset of apossibly infinite number of variinfinite number of formulas ofables, and satisfies the same conditions as those of atree-sequent, as to the availabilityof variables.
$\mathrm{N}_{\neg}$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathcal{T}$$\mathcal{T}$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathfrak{M}$$\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$

$a$

$a$

$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{L}\mathrm{K}$$\mathrm{T}\mathrm{N}_{\neg}$$\Gamma \mathrm{g}\Delta$$\mathrm{N}_{\neg}$

DEFINITION 2.13
An infinite tree-sequent
tions:$\Delta$$\Gamma$$\alpha$$(\mathrm{T}\mathrm{N}_{\neg}- \mathrm{S}\mathrm{A}\mathrm{T}\mathrm{U}\mathrm{R}\mathrm{A}\mathrm{T}\mathrm{E}\mathrm{D}\mathrm{N}\mathrm{E}\mathrm{S}\mathrm{S})$1. Let$a$$\Gamma\subseteq\Sigma$: I4;$\Delta$

2. For every node$(\Lambda \mathrm{L})$(b)$(\Lambda \mathrm{R})$(c)$(arrow \mathrm{L})$

(f)

$b$

:

$\Sigma\Rightarrow\beta$of$a:\mathrm{I}\Rightarrow\Delta$is$\mathrm{T}\mathrm{N}_{\neg}$-saturated if it satisfies the following condi-

II be nodes of$\mathcal{T}$$\mathcal{T}$

. If

$b$

is adescendant of , then$a$,$B\in\Gamma$$A\in\Gamma$$\Lambda B\in\Delta$-saturated:If $Aarrow B\in\Gamma$ , then $A\in\Delta$ or$B\in\Gamma$;-saturated:If $Aarrow B\in\Delta$ , then there exists adescendantsuch thatand $B\in\Pi$ ;, then $A\in\Delta$ ;-saturated:If$b:\Sigma\Rightarrow\Pi\beta$$(arrow \mathrm{R})_{\mathrm{t}}$

of
(e)

and

$\mathrm{T}\mathrm{N}_{\neg}$;and-saturated:If $A\wedge B\in\Gamma$ , then
, then $A\in\Delta$ or $B\in\Delta$ ;-saturated:If A

(a)

(d)

of

$\mathcal{T}$$A\in\Sigma$$a$$(\neg \mathrm{L})$$\neg A\in\Gamma$-saturated:If;such that$(\neg \mathrm{R})_{\mathrm{t}}$

of

$a$

, then $A[y/x]\in\Gamma$ for every available variable$y$$\neg A\in\Delta$, then there exists adescendant:$b$$\Sigma\Rightarrow\Pi\beta$$A\in\Sigma$

(g)

(h)

$(\forall \mathrm{L})$-saturated

at

;

$a$

If

, then there exists adescendant-saturated:If
and avariable such that $A[y/x]\in\Pi$ ;;or-saturated:;-saturated:;then-saturated:$b:\Sigma\Rightarrow\Pi\beta$$\forall xA\in\Delta$$(\forall \mathrm{R})_{\mathrm{t}}$$a$$\forall xA\in\Gamma$

$y$

(i)

$(\sim\Lambda \mathrm{L})$$\mathrm{I}\mathrm{f}\sim(A\Lambda B)\in\Gamma,$(j)$(\sim\Lambda \mathrm{R})$$\mathrm{I}\mathrm{f}\sim(A\Lambda B)\in\Delta,$(k)$(\simarrow \mathrm{L})$$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\sim A\in\Gamma$$\sim B\in\Gamma$$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\sim A\in\Delta \mathrm{a}\mathrm{n}\mathrm{d}\sim B\in\Delta$$\mathrm{I}\mathrm{f}\sim(Aarrow B)\in\Gamma,$$A\in\Gamma \mathrm{a}\mathrm{n}\mathrm{d}\sim B\in\Gamma$

of

104
(1)

$(\simarrow \mathrm{R})$-saturated:-saturated:-saturated:(m)$(\sim\neg \mathrm{L})$(n)$(\sim\neg \mathrm{R})$-saturated:-saturated:(p)(q)-saturated:(r):variable at .
(o)

then

$\mathrm{I}\mathrm{f}\sim\neg A\in\Gamma,$$\mathrm{I}\mathrm{f}\sim\neg A\in\Delta,$$(\sim\sim \mathrm{L})$$\mathrm{I}\mathrm{f}\sim\sim A\in\Gamma,$$(\sim\sim \mathrm{R})$$\mathrm{I}\mathrm{f}\sim\sim A\in\Delta$$(\sim\forall \mathrm{L})$then$\mathrm{I}\mathrm{f}\sim(Aarrow B)\in\Delta,$

then $A\in\Delta$ ;$A\in\Gamma$;$A\in\Delta$;

for some variable ;for every available$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\sim A[y/x]\in\Gamma$$\mathrm{I}\mathrm{f}\sim\forall xA\in\Delta,$$(\sim\forall \mathrm{R})- \mathrm{s}\mathrm{a}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d}$;;$A\in\Gamma$then, then$\mathrm{I}\mathrm{f}\sim\forall xA\in\Gamma,$$A\in\Delta \mathrm{o}\mathrm{r}\sim B\in\Delta$$y$$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\sim A[y/x]\in\Delta$

$a$

$y$

Note that for the rules$($$)_{\mathrm{t}}$, descendants are involved.

a tree-sequent ofsuch that there is at least one variable available
Now letroot,
We
the way
describe
is extended to aat itsand-saturated
infinite tree-sequent.
By our definition of the language ofthere are only countably many formulas
We arrange this to obtain anew
hence we can enumerate them asofsequence,$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}\forall \mathcal{T}.$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{N}_{\neg},$$B_{1},$ $B_{2},$$\mathrm{N}_{\neg},$$\ldots.$$B_{1}|B_{1},$ $B_{2}|B_{1},$ $B_{2},$ $B_{3}|\ldots$

The point is that every formula ofappears infinitely
which we denote by
Again by definition, a term of
many times in
is to be avariable and.
we can enumerate them as
step by step and obtain a sequence of (finite) tree-sequents
We extend
is for the reduction of the formula , described.The step fromtobelow in detail. It should be paid attention to that each operation preserves theunprovability of the tree-sequent.
$A_{1},$ $A_{2},$$A_{1},$ $A_{2},$$\mathrm{N}_{\neg}$$\ldots.$$\mathrm{N}_{\neg}$$\ldots.$$x_{1},$ $x_{2},$$\ldots$$\mathcal{T}_{0}(:\equiv \mathcal{T})$$\mathcal{T}_{1},$$\mathcal{T}_{i-1}$$\mathcal{T}_{2},$$A_{i}$$\mathcal{T}_{i}$$\ldots$

1. (inheritance) For every node $a:\Gamma\xi\Delta$ of, addsuch thatto theantecedent of each descendant of This operation is called an inheritance, andpreserves unprovability because of the rule (drop );$A_{i}\in\Gamma$$\mathcal{T}_{i-1}$$A_{i}$$a.$$\mathrm{L}$

2. (reduction) According to the shape of:
executed for each node :I3 of$A_{i},$$\Delta$$a$(a)one of the following operations is$\mathcal{T}_{i-1}$

C. If
then add $B$ and $C$ to
This operation preserves
unprovability because of the ruleofIfthen at least one$B$$C$of the tree-sequents obtained by adding or to is unprovable becauseof the ruleTake the unprovable one as a resulting tree-sequent ;$A_{i}\equiv B\Lambda$$A_{i}\in\Gamma,$$\Gamma.$$A_{i}\in\Delta,$$\mathrm{T}\mathrm{N}_{\neg}.$$(\Lambda \mathrm{L})$$\Delta$$(\Lambda \mathrm{R}).$(b) $A_{i}\equiv Barrow C.$ Ifthen add $B$ totree-sequent remains unprovable. If;(which is aleaf) of$A_{i}\in\Gamma,$$\Delta,$or$A_{i}\in\Delta$toso that the resulting, then make anew daughter$C$$\Gamma,$$b:B\Rightarrow^{\emptyset}C$

$a,$

(c)

$A_{i}\equiv\neg B.$$b:B4$
(d)

If
of ;

$a$

then add $B$ to$\Delta.$If$A_{i}\in\Delta,$

then make anew daughter$a$Ifand is in$A_{i}\equiv\forall xB.$at

$A_{i}\in\Gamma,$$A_{i}\in\Gamma,$

then add $B[y/x]$ tofor every which is available
Ifthen take affesh variable
and$\Gamma,$$\{x_{1}, \ldots, x_{i}\}.$

make anew daughter$b$:$A_{i}\in\Delta,$$\{x_{m}\}\Rightarrow B[x_{m}/x]$$y$$x_{m}$

of ;
$a$

105
(e) $A_{i}\equiv\sim(B\Lambda C)$ . If
, add
to , so that the resulting
to ;tree-sequent remains unprovable. If
add
If
, add
(f) $A_{i}\equiv\sim(Barrow C).$ If
to;unprovabletotree-sequent
so that the resulting
remains. If(g)or(or ), add $B$ to (or , respectively) ;to ,, then take afresh variable. If(h)for every which istoand also add
to . If.
available at and in$\sim B\mathrm{o}\mathrm{r}\sim C$$A_{i}\in\Gamma$$A_{i}\in\Delta,$$A_{i}\in\Gamma$$\Gamma$$\Delta$$\mathrm{a}\mathrm{d}\mathrm{d}\sim B\mathrm{a}\mathrm{n}\mathrm{d}\sim C$$B\mathrm{a}\mathrm{n}\mathrm{d}\sim C$$B\mathrm{o}\mathrm{r}\sim C$$A_{i}\in\Delta,$$\Gamma.$$\Delta$$A_{i}\equiv\sim\sim B$$A_{i}\equiv\sim\neg B$$A_{i}\equiv\sim\forall xB$$A_{i}\in\Gamma$$\Delta$$A_{i}\in\Gamma$$x_{m}$$\Delta$$\Gamma$$\mathrm{a}\mathrm{d}\mathrm{d}\sim B[x_{m}/x]$$x_{m},$$A_{i}\in\Delta,$$\alpha$$\Delta$$\mathrm{a}\mathrm{d}\mathrm{d}\sim B[y/x]$$\Gamma$$y$$\{x_{1}, \ldots, x_{i}\}$$a$i.e. the treeTake an infinite tree-sequentof-as aunion of, and the infinite sequent or the set ofstructure of is aunion of those of.
variables associated to each node is again aunion of those ofThen it is easily verified that is-saturated.
$\mathfrak{M}=(M,\leq, U, I^{+}, I^{-})$ from
. Let $(M, \leq)$ be
Now we will construct an-modelatree-structure of and $U(a)$ be the set of available variables at (here the condition
for every $a\in M$ ).
that one variable is available at the root of assures that
For anode $a:\Gamma\xi\Delta$ of and an m-ary predicate symbol ,$\overline{\mathcal{T}}$$\mathrm{T}\mathrm{N}$$\mathcal{T}_{0},$$\mathcal{T}_{1},$$\ldots,$$\overline{\mathcal{T}}$$\mathcal{T}_{0},$$\mathcal{T}_{1},$$\ldots$$\mathcal{T}_{0},$$\mathcal{T}_{1},$$\ldots$$\tilde{\mathcal{T}}$$\mathrm{T}\mathrm{N}_{\neg}$$\tilde{\mathcal{T}}$$\mathrm{N}_{\neg}$$\tilde{\mathcal{T}}$$a$$U(a)\neq\emptyset$$\mathcal{T}$$\tilde{\mathcal{T}}$$p$$p^{I^{+}(a)}:=\{(y_{1}, \ldots, y_{m})|p(y_{1}, \ldots, y_{m})\in\Gamma\}$$p^{I^{-}(a)}:=\{(y_{1}, \ldots, y_{m})|\sim p(y_{1}, \ldots, y_{m})\in\Gamma\}$-models;for
The model
defined above certainly satisfies the conditions of
example, the conditionis satisfied since every finite sub-tree-sequent
unprovable
in
and
of is
has an axiom$\mathrm{N}_{\neg}$$\mathfrak{M}$$p^{I^{+}(a)}\cap p^{I^{-}(a)}=\emptyset$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$$-(\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}2)$...

$[p(\vec{x}),$ $\sim p(\vec{x})\Rightarrow|\cdots$

Then the following fact is again easily verified by the induction on the construction$A\in\Gamma$ implies
inof aformula :for eevveerryy node :of-saturated.
. Here we used the fact that is
and $A\in\Delta$ implies
With the fact thatis asub-tree-sequent of , we have proved the following
theorem:$A$$\Gamma\xi\Delta$$a$$a\models^{+}A[\vec{\underline{x}}/\vec{x}]$$\overline{\mathcal{T}},$$\mathfrak{M}$$\overline{\mathcal{T}}$$a\#^{+}A[\vec{\underline{x}}/\vec{x}]$$\mathrm{T}\mathrm{N}_{\neg}$$\overline{\mathcal{T}}$$\mathcal{T}$)THEOREM 2.14 (KRIpKE COMPLETENESS OF
at whose root at least one variable is available, andLet
be a tree-sequent ofthat is:. Then there exists a counter -model $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ for$\mathrm{T}\mathrm{N}_{\neg}$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$

The tree-structure of$\bullet$$\bullet$$\mathcal{T},$$\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}\forall \mathcal{T}$$\mathcal{T}$can be embedded in $(M, \leq)$ ;For each node $a:\Gamma\xi\Delta$ of.
implies$\mathcal{T},$$A\in\Gamma$

implies$a\models^{+}A[\vec{\underline{x}}/\vec{x}]$in$\mathfrak{M},$and $A\in\Delta$$a\#^{+}A[\vec{\underline{x}}/\vec{x}]$From this we immediately obtain Kripke completeness of
COROLLARY 2.15 (KRIPKE COMPLETENESS OF
implies
For every formula of$A$$\mathrm{N}_{\neg},$$\mathrm{N}_{\neg}\models A$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}$.

)$\mathrm{G}\mathrm{N}_{\neg}\vdash A$.

, and be anonempty finite set of variables which includes allLetand the contraposition of lemma
the ffee variables of . Then by$[3A]$ . The theorem shows that there exists an -model such
2.10,

Proof.

$\mathrm{G}\mathrm{N}_{\neg}\forall A$$A$$\mathrm{T}\mathrm{N}_{\neg}\forall$$\alpha$$[\xi A]^{f}\cong_{\mathrm{N}_{\neg}}\forall\partial A$$\mathrm{N}_{\neg}$$\mathfrak{M}$$\mathrm{t}\mathrm{h}\underline{\mathrm{a}\mathrm{t}}$

106
Logic

3

$\mathrm{N}_{\neg}\mathrm{D}$obtained by adding constanta variation of
In this section we consider the logic
domain axiom $\forall x(A(x)\vee B)arrow\forall xA(x)\vee B.$ This axiom corresponds to the reference
to Kripke models that every possible world has the same domain in common, as we
the Gentzen-style sequent system forshall show later. Kripke completeness oftree-sequents.
using, is shown just as that for$\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\mathrm{D},$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D},$$\mathrm{G}\mathrm{N}_{\neg},$$\mathrm{N}_{\neg}\mathrm{D}$DEFINITION 3.1 (SEQUENT SYSTEM
plus the following axiom:
is$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$)$\mathrm{G}\mathrm{N}_{\neg}$(axiom D)$\overline{\Rightarrow\forall x(A(x)\vee B)arrow\forall xA(x)\vee B}$

The following is a well-known result in the intermediate logic
verified.
LEMMA 3.2
be the system obtained fromLet$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}’$$\mathrm{G}\mathrm{N}_{\neg}$by substituting the$\mathrm{C}\mathrm{D}$and also easily$mle(\forall \mathrm{R})\mathrm{s}$,vc by$\frac{\Gamma\Rightarrow\Delta,A[z/x]}{\Gamma\Rightarrow\Delta,\forall xA}(\forall \mathrm{R})_{\mathrm{V}\mathrm{C}}$$i.e$. allow plrral fomulas in the succedent. Then

DEFINITION 3.3
An -model $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ is an$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}’$is equivalent to$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$.

$(\mathrm{N}_{\neg}\mathrm{D}- \mathrm{M}\mathrm{O}\mathrm{D}\mathrm{E}\mathrm{L})$$\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\mathrm{D}$-model if

just like that of
We define the validity,
is shown by the induction on the derivation.
$\mathrm{N}_{\neg}\mathrm{D}\models A,$

THEOREM 3.4 (KRIPKE SOUNDNESS OF.
, thenIf$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash\Gamma\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{N}_{\neg}.$

is a constant map.

$U$

Then the soundness of$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$)$\mathrm{N}_{\neg}\mathrm{D}\models\Gamma\Rightarrow\Delta$of
A toee-sequent
the tree-sequent system for
Now we introduce
sequentwithaof
is afinite tree each of whose nodes is associated. Each will do since they have the same language in common). This definition(orin that the indication of a set of variables is omitted here,
is different from that of
we need not consider whether a variable is available or not, which
because inadomain in the proofs above.
of
aseed
worked as
except thatare the same as those of
The axioms and inference rules ofvariables,(whichandtheruleavailability
ofabout
they have no consideration
is substituted bytrims aleaf) of$\mathcal{T}$$\mathrm{N}_{\neg}\mathrm{D}.$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D},$$\Gamma\Rightarrow\Delta$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{T}\mathrm{N}_{\neg},$$(\forall \mathrm{R})_{\mathrm{t}}$$\mathrm{T}\mathrm{N}_{\neg}$$... \cdot..\frac{[\Gamma\Rightarrow\Delta,A[z/x]|}{[\Gamma\Rightarrow\Delta,\forall xA|}..\cdot\cdot\cdot\cdot(\forall \mathrm{R})_{\mathrm{V}\mathrm{C}}$. The rule adopted here may be justified by lemma 3.2.
andNext we consider the relation between.
andjust as that between

LEMMA 3.5
Let be a tree-sequent.
thensuch that$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D},$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathcal{T}$$of\mathrm{T}\mathrm{N}_{\neg}$

D. If$\mathcal{T}$has a node

$a:\Gamma\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash\Gamma\Rightarrow\Delta$,$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}\vdash \mathcal{T}$Proof. Just like the case of$\mathrm{T}\mathrm{N}_{\neg},$i.e. lemma 2.9.

1

107
DEFINITION 3.6 (TRANSLATION)
denoted by
Atranslation into a formula of a tree-sequent of, which in turn is defined inductively on the height of ;closure of$\mathcal{T}$$\mathcal{T}^{f},$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D},$is a universal$\mathcal{T}$$\mathcal{T}^{p}$$[\Gamma\Rightarrow\Delta|\mathcal{T}_{1}\ldots \mathcal{T}_{m}]^{p}:\equiv(\wedge\Gamma)arrow(\vee\Delta)\vee \mathcal{T}_{1}^{p}\vee\cdots\vee \mathcal{T}_{m}^{p}$

Here the concept pre-tree-sequent is not necessary because it was for considering availability of variables.
LEMMA 3.7

If$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}\vdash \mathcal{T}$, then$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash \mathcal{T}^{f}$.

Again we prepare acouple of sublemmas, the proofs for which are easy by induction
just like those for lemmas 2.11 and 2.12.
SUBLEMMA 3.8
Let$\mathcal{T}’,$$\mathcal{T},$$\mathcal{T}_{1}’,$$\ldots,$$\mathcal{T}_{k}^{\prime p}\Rightarrow \mathcal{T}^{\prime p}$$\mathcal{T}_{1}^{\prime p},$$\ldots,$

andimplies$\mathcal{T}_{k}’$$\mathcal{T}_{k}$$\mathcal{T}_{1},$$\ldots,$

be just as those of lemma 2.11. Then$\mathcal{T}_{k}^{p}\Rightarrow \mathcal{T}^{p}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash \mathcal{T}_{1}^{p},$$\ldots,$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash$.

SUBLEMMA 3.9
the same as those in the sublemma above. Then
Let
and
.

$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash \mathcal{T}^{\prime f}$$\mathcal{T}’$$\mathcal{T}$implies$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash \mathcal{T}^{f}$

Proof of lemma 3.7

D. The proof is carried out just likeBy the induction on the derivation of in
is inferred by the rulethat of lemma 2.10, and it suffices to check the case where
D. In fact, we can not apply sublemma 3.8 which was used in the caseofinstead.
, therefore we will make use of the character ofofas an induction hypothesis. Then
Supposeis in the form$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$(\forall \mathrm{R})_{\mathrm{V}\mathrm{C}}$$\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash(\cdots[\Gamma\Rightarrow\Delta, A[z/x]|\cdots)^{f}$$(\cdots[\Gamma\Rightarrow\Delta, A[z/x]|\cdots)^{f}$$\forall\vec{x}\forall z(B_{1}arrow C_{1}\vee(B_{2}arrow C_{2}\vee(\cdots\vee(B_{n}arrow C_{n}\vee A[z/x])\cdots)))$or . Then we repeatedly apply the, where has no free occurrence in any offollowing logical equivalences which are easily verified:$B_{i}$$z$$\forall x(Barrow C(x))\cong \mathrm{N}_{\neg}\mathrm{D}Barrow\forall xC(x)$$C_{i}$$\forall x(C\vee D(x))\cong_{\mathrm{N}_{\neg}}{}_{\mathrm{D}}C\vee\forall xD(x)$The second one is unique to logics with constant domain axiom. Thus we have thelogical equivalence,$(\cdots[\Gamma\Rightarrow\Delta, A[z/x]|\cdots)^{f}$$\equiv\forall\vec{x}\forall z(B_{1}arrow C_{1}\vee(B_{2}arrow C_{2}\vee(\cdots\vee(B_{n}arrow C_{n}\vee A[z/x])\cdots)))$$\cong_{\mathrm{N}_{\neg}\mathrm{D}}\forall\vec{x}(B_{1}arrow C_{1}\vee(B_{2}arrow C_{2}\vee(\cdots\vee(B_{n}arrow C_{n}\vee\forall xA)\cdots)))$$\equiv(\cdots[\Gamma\Rightarrow\Delta,\forall xA|\cdots)^{f}$

By the induction hypothesis and the cut rule, we obtain$\ldots)^{f}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash(\cdots[\Gamma\Rightarrow\Delta,\forall xA|\mathrm{I}$.

D-SATURATEDNESS)
DEFINITION 3.10 (-saturated if satisfies the conditions ofisAn infinite tree-sequent of-saturatedness(see definition 2.13) where the word available is omitted and the-saturated is substituted by:condition$\mathrm{T}\mathrm{N}_{\neg}$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$(2\mathrm{h})(\forall \mathrm{R})_{\mathrm{t}}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathcal{T}$108$(\forall \mathrm{R})$-saturated:If$\forall xA\in\Delta,$

then $A[y/x]\in\Delta$ for some variable ;$y$

Now we can prove Kripke completeness extending an unprovable tree-sequent of.
into saturation to obtain a counter model, as we did inandArrange all the formulas and variables to obtain sequences.
a tree-sequent ofsuch that
as we did in the last section. Let
where each steptois for the
We extend step by step and obtain
The operation carried out at each step is almost the same as that in
reduction of, being different in the following points:$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$A_{1},$ $A_{2},$$\mathcal{T}$$x_{1},$ $x_{2},$$\ldots$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathcal{T}$$\mathcal{T}_{i-1}$$\mathcal{T}_{1},$$\mathcal{T}_{0},$$\ldots$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}\forall \mathcal{T}$$\mathcal{T}_{i}$$\ldots,$$A_{i}.$$\mathrm{T}\mathrm{N}_{\neg}$$\bullet$$\bullet$

The word available is omitted;

The caseis substituted by:$(2\mathrm{d})$. If$B[x_{i}/x]$ to, then add all of $B[x_{1}/x],$
If $A:\in$This operation$4$ then take a fresh variable
and add $B[x_{m}/x]$ to;ofpreserves unprovability because of the rule$(2\mathrm{d})A_{i}\equiv\forall xB$$\Gamma.$$A_{i}\in\Gamma$$\ldots,$$\Delta.$$x_{m}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$(\forall \mathrm{R})$-saturated.
Then isLet be aunion of
as follows: let,
we can construct an
From$U(a)$ the set of all the variables for every $a\in M$$(M, \leq)$ be atree-structure of
D-model, i.e. has the constant domain), and interpretations
and(henceis.
just the same as those for
and we obtain the following theorem:
is acounter model for
Then$\overline{\mathcal{T}}$$\overline{\mathcal{T}}$$\mathcal{T}_{0},$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathcal{T}_{1},$$\ldots.$$\tilde{\mathcal{T}}$$\mathrm{N}_{\neg}\mathrm{D}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$$\tilde{\mathcal{T}},$$\mathfrak{M}$$I^{+}$$\mathrm{N}_{\neg}$$I^{-}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathfrak{M}$$\mathcal{T},$THEOREM 3.11 (KRIPKE COMPLETENESS OF
such thatbe a tree-sequent ofLet-model $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ for , that is:$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathcal{T}$$\bullet$. Then there exists a counter$\mathcal{T}$$\mathrm{N}_{\neg}\mathrm{D}$$\bullet$)$\mathrm{T}\mathrm{N}_{\neg}\forall \mathcal{T}$The tree-structure of
For each node
impliescan be embedded in $(M, \leq)$ ;$\mathcal{T}$$a:\Gamma\Rightarrow\Delta$$a\#^{+}A[\vec{\underline{x}}/\vec{x}]$.

of$\mathcal{T},$$A\in\Gamma$

implies$a\models^{+}A[\vec{\underline{x}}/\vec{x}]$Kripke completeness of the Gentzen-style systemacorollary:
COROLLARY 3.12 (KRIPKE COMPLETENESS 0F
implies
For every formula of$A$

Proof. Let$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\forall$tion of lemma 3.7,.
such that$\mathrm{N}_{\neg}\mathrm{D},$

and

$A$

$\mathrm{N}_{\neg}\mathrm{D}\models A$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$$\mathfrak{M},$and $A\in\Delta$

is derived immediately as)$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\vdash A$

.

Since
and the contraposithat
there
The theorem shows
exists an
D-model$\mathcal{T}:\equiv[ \Rightarrow A].$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}\psi \mathcal{T}.$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$in$\mathcal{T}^{f}\cong_{\mathrm{N}_{\neg}\mathrm{D}}\forall\vec{x}A$$\mathrm{N}_{\neg}$$\mathfrak{M}1$$\mathfrak{M}\# A$

4Logics$\mathrm{N}_{\neg}\mathrm{P},$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$andobtained by omitting the axiom
In this section we consider the logics$Aarrow(\sim Aarrow B)$ in
which results in paraconsistency.
andthe Gentzen-style system for
Alogic is explosive if in
adopt, and in fact we use(it depends on the language of which one of
explosive.
paraconsistent if it is not
and
are
all
is
. For instance,$\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{L}$$\mathrm{G}\mathrm{L},$$\mathrm{L},$$\mathrm{L}$$\sim \mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e})$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P},$$\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{N}_{\neg}$$\mathrm{C}1,$$\mathrm{l}\mathrm{n}\mathrm{t}$$\neg \mathrm{o}\mathrm{r}\sim \mathrm{w}\mathrm{e}$$\mathrm{N}_{\neg}$$\mathrm{L}$$\mathrm{G}\mathrm{L}\vdash A,$$\neg A\Rightarrow B$

109
Paraconsistent logics are certainly of considerable use as tools to formalize theories
which have some contradiction but are non-trivial. We can give some examples of suchtheories; the Newton-Leibniz version of calculus, Cantor’s naive set theory, or early
quantum mechanics. The history and some approaches other than we present in thispaper are in the literature [PR84] by Priest and Routley, who adopt relevant logics as
an approach to paraconsistency. Whether
is useful with respect to theormotivation stated above is to be inspected further.
The proof of Kripke completeness ofis exactly the same as thator
, respectively.
ofor
The Gentzen-style sequent systemor-DP is defined by omitting theaxiom$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$$\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{G}\mathrm{N}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{P}$$\overline{A,\sim A\Rightarrow}(\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}2)$or, respectively.
-model)if it satisfies all theis an-model(or a.
-model)except the one
conditions of -model(or aThe tree-sequent systemoris obtained by omitting the axiom

in$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$$\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$$\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$$p^{I^{+}(a)}\cap p^{I^{-}(a)}=\emptyset$$\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$$-(\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}2)$. .. $[A,$inor$\sim A\doteqdot|\cdots$, respectively.
or
Then we can prove Kripke completeness of$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{P}$or$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$just like that of$\mathrm{G}\mathrm{N}_{\neg}$, respectively.

THEOREM 4.1 (KRIPKE SOUNDNESS AND COMPLETENESS OF
AND, and $A$ an arbitrary formula of L. Then
Let be eitheror
only if.
$\mathrm{G}\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{L}$

)
and
if

$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$$\mathrm{L}\models A$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$$\mathrm{N}_{\neg}\mathrm{P}$$\mathrm{G}\mathrm{L}\vdash A$

Rom the soundness, we can assure that
COROLLARY 4.2
Let be either$\mathrm{L}$in$\mathrm{G}\mathrm{L}$$\mathrm{N}_{\neg}\mathrm{P}$or$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$, in general.

$\mathrm{N}_{\neg}$Pand$\mathrm{N}_{\neg}\mathrm{D}\mathrm{P}$. Then sequents of the form $A,$

are both paraconsistent:$\sim A\Rightarrow B$

are not provable

Let and $q0$ -ary predicate symbols, $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ be an L-model, and 0 $\#^{+-}q$ . Thensuch that $M=\{0\},$and by the.
soundness we have

Proof.

$p$$0\models^{+}p,$ $0\models^{-}p$$\mathfrak{M}\# p\Lambda\sim parrow q$$\mathrm{I}$$\mathrm{G}\mathrm{L}\mu p,$$\sim p\Rightarrow q$

5

Logics5.1

First Proof-Kripke Completeness of$\mathrm{N}_{\neg}\mathrm{O},$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{O}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$In this subsection we consider the logic( for omniscience crxiom, $\neg\neg(A\vee\sim A)$ ),whose Kripke completeness we can hardly prove by only aPPlying the tree-sequent
method we used above. Here we use some fresh result about the relation to classicallogic.
plus the axiom, is, the Gentzen-style sequent system for$\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{O}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{N}_{\neg}\mathrm{O}$$\overline{\Rightarrow\neg\neg(A\vee\sim A)}$(axiom O)

An-model $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ is anexists $a’(\geq a)$ such that:$\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\mathrm{O}$-rnodel if for every $a\in M$ , there

110
$a’$

$\bullet$$\bullet$is maximal in the poset $(M, \leq)$ ;for every predicate symbol $p,$ where $m$ is the arity of$p^{I^{+}(a’)}\cup p^{I^{-}(a’)}=U(a’)^{m}$$p$.

From the condition
disjoint.

$p^{I^{+}(a’)}\cap p^{I^{-}(a’)}=\emptyset$of an$\mathrm{N}_{\neg}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1,$

the union$p^{I^{+}(a’)}\cup p^{I^{-}(a’)}$is

LEMMA 5. 1
-model, $a’\in M$ satisfy the two conditions itemized
Let $\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$ be anThenor $a’\models^{-}A,$ andabove, andbe an arbitrary closed fomula ofby lemma 2.6 exactly one of them holds.
$\mathrm{N}_{\neg}$$A$$a’\models^{+}$$\mathrm{N}_{\neg}.$$A$

The proof is easy by the induction on the construction of $A,$ a formula ofwhere , aname of an individual, is allowed to occur. We present here only the step.
cases where $A\equiv Barrow C$ or$A\equiv
BarrowC$, assume $a’\#^{+}$ A. We shall show that
holds. If
When$a’\models^{-}B$ , by lemma 2.5 for every $c\geq a’c\models^{-}B,$ which in turn implies $c\#^{+}B$ bylemma 2.6. Hence $a’\models^{+}Barrow C,$ which is a contradiction. So we must have $a’\#^{-}B$ ,which is equivalent to $a’\models^{+}B$ by the induction hypothesis. Now $a’\models^{+}C$ leads tocontradiction in the same way, so we must have $a’\models^{-}C$ by the induction hypothesis.
, assume $a’\#^{+}A.$ Since $a’$ is maximal, there exists $u\in U(a’)$ suchWhenby the induction hypothesis. Hence
that $a’\#^{+}B[\underline{u}/x],$ which implies
I.
we have

Proof.

$\mathrm{N}_{\neg}$$\underline{u}$$A\equiv\forall xA$$a’\models^{-}$$A$$\mathrm{a}$$A\equiv\forall xB$$a’\models^{-}B[\underline{u}/x]$$a’\models^{-}\forall xB$

may be regarded as apossible world which is omniscient, in the sence of lemma 5.1.
This is the origin of the name of the axiom.
$a’$

In order to prove Kripke soundness of$\neg\neg(A\vee\sim A)$ is valid in every

THEOREM 5.2 (KRIPKE SOUNDNESS OF
.
then
If

$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{V}\mathrm{e}\mathrm{r}\mathrm{i}\mathfrak{h}r$)$\mathrm{N}_{\neg}\mathrm{O}\models\Gamma\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\Gamma\Rightarrow\Delta,$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}$

we have only tothat the formulawhich is obvious by lemma 5.1.

$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O},$$\mathrm{N}_{\neg}\mathrm{O}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1,$, the tree-sequent system for the logic$\mathrm{N}_{\neg}\mathrm{O},$an axiom$\overline{\ldots[=5\neg\neg(A\vee\sim A)|\cdots}$. Then the same relations as those between, as we shall see in the following lemmas.

$\mathrm{G}\mathrm{N}_{\neg}$

is obtained ffom$\mathrm{T}\mathrm{N}_{\neg}$by adding(axiom O)

and$\mathrm{T}\mathrm{N}_{\neg}$hold between$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$and$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}$LEMMA 5.3
Let be a tree-sequent.
then$\mathcal{T}$$of\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}.$If has a node$\mathcal{T}$$a:\Gamma\Rightarrow\Delta$

such that$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\Gamma\Rightarrow\Delta$,$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}\vdash \mathcal{T}$Proof.

By the induction on the derivation of$\Gamma\Rightarrow\Delta$in$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$We define the translation into a formula of a tree-sequent.
same one as that of1.

$\mathcal{T}$of$\mathcal{T}^{f}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O},$, as the$\mathrm{T}\mathrm{N}_{\neg}$

LEMMA 5.4

If
Proof.

$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}\vdash \mathcal{T},$then$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash \mathcal{T}^{f}$.

Similarly to the proof of lemma 2.10.

1

111
can be introduced
We make aremark about the language of Cl. All ofas defined symbols in ;however in this paper we assume the logical connectives of Cl.
make correspondence with
be not only
and but include
In this paper astructure in Tarski-type semantics for Cl is often said to be aCland the interpretation
model. For aCl-model we denote the domain of by
in orderbyof apredicate symbol by . We will often denote a formula ofwhich is obtained by.
to make clear that
contains no-isaformula ofby .
inreplacing some (possibly all or no)
Now we prepare alemma which is abasic idea for the proof of Kripke completeness; that is, a -model induces an omniscient possible utorld.
of$\vee,$$arrow \mathrm{a}\mathrm{n}\mathrm{d}$$\exists$$\mathrm{C}1$$\forall$$\neg$$\Lambda,$$\mathrm{N}_{\neg}\mathrm{O}$$arrow \mathrm{t}\mathrm{o}$$\mathfrak{U}$$\mathfrak{U}$$|\mathfrak{U}|,$$A_{\neg},$$\mathrm{C}1$$p$$p_{\mathfrak{U}}$$A$$A_{\sim}$$\sim’ \mathrm{s}$$\mathrm{N}_{\neg}$$A$$\neg’ \mathrm{s}$$\sim$$\mathrm{C}1$$\mathrm{G}\mathrm{N}_{\neg}$

LEMMA 5.5
Let be a -model, and$U(0)=|\mathfrak{U}|,$
and
Cl,
of
iff
5.1, ate also haveiff$p^{I^{+}(0)}=p_{\mathfrak{U}}$$A_{\neg}$-model such that $M=\{0\}$ ,an. Then for an arbitrary closed formula$\mathfrak{M}_{\mathfrak{U}}=(M, \leq, U, I^{+}, I^{-})$$\mathrm{C}1$$\mathfrak{U}$$p^{I^{-}(0)}=U(0)^{m}\backslash p_{\mathfrak{U}}$$0\models^{+}A_{\sim}$$21\models A_{\neg}$$\mathfrak{U}\# A_{\neg}$-(or equivalently$0\models^{-A}\sim\neg$$\mathfrak{M}\models A_{\sim_{\neg}}$)$.$

From this and lemma.

By the induction on the construction of

Proof.

$\mathrm{N}_{\neg}\mathrm{O}$$A_{\neg}.$

We only present the step case

.
where
.
or
is syntactically equivalent to
Whenby the induction hypothesis. This
, which is equivalent to 0
iff 21descendants,
and is also equivalent toequivalentnoistosince 0has
by lemma 5.1.
$A_{\neg}\equiv\neg B_{\neg}$$A_{\neg}\equiv\neg B_{\neg},$$\sim B\sim\neg$$\neg B_{\sim_{\neg}}$$A_{\sim_{\neg}}$$\mathfrak{U}\models A_{\neg}$$\#^{+}B_{\sim}\neg$$\# B_{\neg}$$0\models^{+}\neg B_{\sim}\neg$$\mathrm{I}$$0\models^{+}\sim B\sim\neg$)
THEOREM 5.6 (MAIN THEOREM 1. KRIPKE COMPLETENESS OF
.
then
If
Proof. We describe the sketch of the proof here, and the details shall be shown lateras lemmas.
, and be afinite set of variables which is nonempty and includes
Let
Now weevery ffee variable of . By lemma 5.4 and
$[\xi
A]$
. Becauseandextendinto-saturation in the same way as we do inhave the same inference rules in common, the procedure of extension preserves. Hence as aresult we obtain an infinite
theof the tree-sequent in-saturated, and every finite sub-tree-sequent of which istree-sequent
which isunprovable in. A-saturated induces anwhich makes not valid.
We are to add an omniscient world to each possible world of , in the following
way.
world of . Then
which induces an
Let : I
the node offorby lemma 5.3 and that every finite sub-tree-sequent of is unprovable ininfinitei.e. theevery finite subsets
we haveandsequent-consistent. It is the result of corollary 5.10 thatofis
, i.e. every finite subsequent offfom
we have a -consistent sequent. Then by lemma 5.11 we can construct aCl-model 21 which
which is unprovable invalid. We
has alarge domain enough to include $U(a)$ and makes every formula inin lemma 5.5. Then is an omniscient possible world,
construct from as 0ofdaughterof .
as anew
and we add it to
we obtain an
By carrying out this procedure for every node of
It shall be shown in lemmaof, hence Kripke completenesssuch that1is acounter model for in fact.
5.13 that$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash A$$\mathrm{N}_{\neg}\mathrm{O}\models A,$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\forall A$$\alpha$$[4 A]^{f}\equiv\forall\partial A,$$A$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}\psi[4A].$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{u}\mathrm{n}\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{a}\mathrm{b}\underline{\mathrm{i}\mathrm{l}}\mathrm{i}\mathrm{t}\mathrm{y}$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{N}_{\neg}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$$\mathcal{T}$$\mathrm{T}\mathrm{N}_{\neg}$

$A$

$a’$

$\mathrm{g}\Delta$

$a$

$a$

$\mathfrak{M}$$\overline{\mathcal{T}}$$\mathrm{p}\underline{\mathrm{o}}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{b}\mathrm{l}\mathrm{e}$$\mathfrak{M}$$a$$\mathcal{T}$$\Delta’\subseteq\Delta$$\Gamma’\subseteq\Gamma$$\Gamma\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\Gamma\Rightarrow\Delta$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O},$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\forall\Gamma’\Rightarrow\Delta’,$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\Gamma_{\neg}\Rightarrow$$\mathrm{L}\mathrm{K}$$\mathrm{L}\mathrm{K}$$\Gamma_{\neg}$$a’$$\mathfrak{U}$$a’$$\mathfrak{M}_{\mathfrak{U}}$$\mathfrak{M}$$a$$\mathfrak{M},$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}.$$\mathfrak{M}’\# A$$\mathfrak{M}’$$A$$\mathrm{N}_{\neg}\mathrm{O}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1\mathfrak{M}’$112First we present some derivations which are only allowed in the logics with omniscience axiom, and some related results.
LEMMA 5.7
In the system$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$, the following$de7\dot{\mathrm{v}}vations$are allouted:$\frac{\sim A,\Gamma\Rightarrow}{\neg A,\Gamma\Rightarrow}(\phi 2)$$\overline{Aarrow B\Rightarrow\neg\neg(\sim A\vee B)}(\mathrm{J}3)$$\overline{\neg\sim A,\neg A\Rightarrow}(l1)$

as follows. Here it is notable
The derivations above can be simulated in$A,$hence these are also allowed in the systems
that we do not use (axiom 2)DO).
say(needless
to
in
and

Proof.

$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\sim A\Rightarrow,$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\mathrm{O}\mathrm{P}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\mathrm{P}$$(l1)$$\frac{\frac(\mathrm{w}\mathrm{e}\mathrm{a}\mathrm{k}\mathrm{e}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g},\neg \mathrm{L})\frac{\sim A\Rightarrow\sim A}{\overline{\sim A,\neg\sim A,\neg A\Rightarrow}}A,\neg\sim A,\neg A\Rightarrow\underline{A\Rightarrow A}}{\frac{\underline{A\vee\sim A,\neg\sim A,\neg A\Rightarrow}}{\neg\neg(A\vee\sim A),\neg\sim A,\neg A\Rightarrow}(\neg \mathrm{R},\mathrm{L})}(\vee \mathrm{L})$$\Rightarrow\neg\neg(A\vee\sim A)\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}\mathrm{O}$$\overline{\neg\sim A,\neg A\Rightarrow}$ (cut)$(l2)$$\frac{\frac{\overline{\neg A,\neg\sim A\Rightarrow}}{\neg A\Rightarrow\neg\neg\sim A}(\neg \mathrm{R})(l1)\overline{\overline{\neg\neg\sim A,\Gamma\Rightarrow}}\overline{\sim A,\Gamma\Rightarrow}}{\neg A,\Gamma\Rightarrow}(\mathrm{c}\mathrm{u}.\mathrm{t})\mathrm{h}\mathrm{y}\mathrm{p}(\neg \mathrm{R}, \mathrm{L})$$(\phi 3)$$\frac{\Rightarrow\neg\neg(A\vee\sim A)\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}\mathrm{O}\frac{\frac{\frac{\underline{A\Rightarrow AB\Rightarrow B}}{Aarrow B,A\Rightarrow\sim A\vee B}(}{}(\neg \mathrm{L})Aarrow B,A,\neg(\sim A\vee B)\Rightarrow}{Aarrow B,\neg\neg(A\vee\sim A)Aarrow B,A\vee\sim A,\neg}arrow \mathrm{L})\Rightarrow}{Aarrow B\Rightarrow\neg\neg(\sim A\vee B)}\frac{\overline{\overline{Aarrow B,\sim A\Rightarrow\sim A\vee B}}\sim A\sim A}{\Rightarrow\neg\neg(\sim A\vee B)\underline{\underline{(\sim A\vee B)\Rightarrow Aarrow B,\sim A,\neg(}}\sim A\vee B)\Rightarrow(\neg \mathrm{R},\mathrm{L},\mathrm{R}),(\mathrm{c}\mathrm{u}\mathrm{t})}(\neg \mathrm{L})(\vee \mathrm{L})$I
LEMMA 5.8
Let the sequent system$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}’$be$\mathrm{G}\mathrm{N}_{\neg}$plus an inference $mle$$\frac{\sim A,\Gamma\Rightarrow}{\neg A,\Gamma\Rightarrow}(l2)$. Thenand$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}’\vdash\Rightarrow\neg\neg(A\vee\sim A),$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}’$.

and with lemma 5.7 we obtain the equivalence ofProof.
$\frac{\overline{\sim A,\sim\sim A\Rightarrow}}{\sim(A\vee\sim A)\Rightarrow}(\sim\vee \mathrm{L})(\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}2)$$\frac{\overline{\neg(A\vee\sim A)\Rightarrow}}{\Rightarrow\neg\neg(A\vee\sim A)}(\neg \mathrm{R})(\phi 2)$

113
Using lemma 5.7 we can prove the main lemma, which is an embedding of LK into.
. Againis obtained by substituting some ’s by$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}^{||}$$\Gamma_{\sim_{\neg}}$$\sim \mathrm{i}\mathrm{n}$$\neg$LEMMA 5.9 (MAIN LEMMA)-if and only ifto.
$\mathrm{L}\mathrm{K}\vdash\Gamma_{\neg}\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\Gamma_{\sim}\neg’\sim\Delta_{\sim}\neg\Rightarrow$$\Gamma$. Moreover, it is also equivalent$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\Gamma_{\sim}\neg’\neg\Delta_{\sim}\neg\Rightarrow$.
andWe consider the first equivalence. The only if part of the lemma is shown semanti,cally; Let an arbitrary -model. By the soundness ofThen by com, hence
and by lemma 5.5 we havepleteness of.
We now consider the if part. First note that we may restrict axioms (or initial
sequents) of
to the form
. The proof is carried out through the.
induction on the derivation in
In the following
is denoted by $A’$ to avoid the proof being too wide.
applied at last is presented in the left, and the correspondThe inference rule ofproof figure inin the right:

Proof. The second equivalence is obvious by$(\phi 2)$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\sim A\Rightarrow\neg A$$\mathrm{C}1$$\mathfrak{U}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\mathfrak{M}_{\mathfrak{U}}\models\Gamma_{\sim_{\neg}},$$\mathfrak{U}\models\Gamma_{\neg},$$\mathrm{L}\mathrm{K},$$\neg\Delta_{\neg}\Rightarrow$$\sim\Delta\sim\neg\Rightarrow$$21\models\Gamma_{\neg}\Rightarrow\Delta_{\neg}.$$\mathrm{L}\mathrm{K}\vdash\Gamma_{\neg}\Rightarrow\Delta_{\neg}$$p(\vec{x})\Rightarrow p(\vec{x})$$\mathrm{L}\mathrm{K}$$\mathrm{L}\mathrm{K}$$A_{\sim_{\neg}}$$\mathrm{L}\mathrm{K}$$\mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\overline{p(\vec{x})\Rightarrow p(\vec{x})}$(axiom)$\overline{p(\vec{x}),\sim p(\vec{x})\Rightarrow}(\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m} 2)$$\mathrm{i}\mathrm{n}\mathrm{d}$$\frac{\Gamma\Rightarrow\Delta}{\Sigma,\Gamma\Rightarrow\Delta,\Pi}$.

$\mathrm{h}\mathrm{y}\mathrm{p}$, ,(weakening)$\frac{\Gamma’,\sim\Delta’\Rightarrow}{\Sigma,\Gamma,\sim\Delta’,\sim\Pi\Rightarrow},(\mathrm{w}\mathrm{e}\mathrm{a}\mathrm{k}\mathrm{e}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g})$$\mathrm{i}\mathrm{n}\mathrm{d}$$\Lambda$.

$\mathrm{h}\mathrm{y}\mathrm{p}$.

$\frac{A’,\Gamma’,\Delta’\Rightarrow}{A’\Lambda B,\Gamma’,\sim\Delta\Rightarrow},,(\Lambda \mathrm{L})$$\frac{A,\Gamma\Rightarrow\Delta}{A\Lambda B,\Gamma\Rightarrow\Delta}(\Lambda \mathrm{L})$For the rules introducing.

or , the proof is similar to that of$\forall$$\mathrm{i}\mathrm{n}\mathrm{d}$.

$\mathrm{h}\mathrm{y}\mathrm{p}$.
$\mathrm{i}\mathrm{n}\mathrm{d}$$\frac{\Gamma\Rightarrow\Delta,A}{\neg A,\Gamma\Rightarrow\Delta}(\neg \mathrm{L})$and$\frac{\Gamma’,\sim\Delta’,\sim A’\Rightarrow}{\neg A’,\Gamma’,\sim\Delta\Rightarrow},(\phi 2)$$\mathrm{i}\mathrm{n}\mathrm{d}$$\frac{A,\Gamma\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,\neg A}(\neg \mathrm{R})$For the rule of LK$(\Lambda \mathrm{L})$.

$\mathrm{h}\mathrm{y}\mathrm{p}$$\sim A’,$.

.

$\mathrm{h}\mathrm{y}\mathrm{p}$$\Gamma’,$.

$\sim\Delta’\Rightarrow$.
or$\frac{\Gamma’,\sim\Delta’,A’\Rightarrow}{\Gamma’,\sim\Delta’,\sim\neg A’(\mathrm{o}\mathrm{r}\sim\sim A’)\Rightarrow}(\sim\neg \mathrm{L})$$\frac{\Gamma\Rightarrow\Delta,AB,\Sigma\Rightarrow\Pi}{Aarrow B,\Gamma,\Sigma\Rightarrow\Delta,\Pi}(arrow \mathrm{L}),$$(\sim\sim \mathrm{L})$we have in””$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\frac{A’arrow B’\Rightarrow\neg\neg(\sim A’\vee B’)(l3)\frac{\frac{\sim A’,\Gamma’,\sim\Delta’\Rightarrow B’,\Sigma\prime,\sim\Pi\prime.\Rightarrow \mathrm{i}\mathrm{n}\mathrm{d}.\mathrm{h}\mathrm{y}\mathrm{p}.\mathrm{i}\mathrm{n}\mathrm{d}.\mathrm{h}\mathrm{y}\mathrm{p}}{\sim A’\vee B’,\Gamma’,\Sigma\prime,\sim\Delta,\sim\Pi\Rightarrow}}{\overline{\neg\neg(\sim A’\vee\Sigma,\sim\Delta,\sim\Pi^{B’}\Rightarrow),\Gamma,\Sigma\prime,\sim\Delta’,\sim\Pi\prime\Rightarrow}}}{A’arrow B’,\Gamma’’’},$$\mathrm{i}\mathrm{n}\mathrm{d}$$\frac{A,\Gamma\Rightarrow\Delta,B}{\Gamma\Rightarrow\Delta,Aarrow B}(arrow \mathrm{R})$$||_{\mathrm{I}\mathrm{n}}$.

$\mathrm{h}\mathrm{y}\mathrm{p}$$(\mathrm{c}\mathrm{u}\mathrm{t})(\vee \mathrm{L})(\neg \mathrm{R}, \mathrm{L})$.

$\frac{\Gamma’,\sim\Delta’,A’,\sim B’\Rightarrow}{\Gamma’,\sim\Delta’,\sim(Aarrow B’)\Rightarrow},(\simarrow \mathrm{L})$the literature [Tan80] an embedding of the$arrow$-free fragment of Cl into$\mathrm{N}$is presented.

114

COROLLARY5.10
be a formula ofLet
Then for every sequent$A_{\neg}$

Proof.

$\mathrm{C}1$

obtained by replacing $every\sim’ s$ by in a formula.
impliesof$\Gamma\Rightarrow\Delta$

Take the emptyset as$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\forall\Gamma\Rightarrow\Delta$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O},$LEMMA 5.11
be an infiniie sequent ofLet
we haveandsubsetssuch that:$\Gamma\Rightarrow\Delta$

1.

$|\mathfrak{U}|$of$\mathrm{N}_{\neg}$$\Delta’\subseteq\Delta$$\mathrm{C}1$.

$\mathrm{L}\mathrm{K}\forall\Gamma_{\neg}\Rightarrow$and use the lemma.

$\Delta_{\sim}\neg$

The next lemma certifies that we can construct aof an omniscient possible world.

$\Gamma’\subseteq\Gamma$$A$$\neg$$\mathrm{I}$-model which will be the seed

which is consistent, that is, for every finite
Then there exists a Cl-model$\mathrm{L}\mathrm{K}$$\mathrm{L}\mathrm{K}\forall\Gamma’\Rightarrow\Delta’.$$\mathfrak{U}$includes the set of all variables;2.

$\mathfrak{U}\models A[\vec{\underline{x}}/\vec{x}]$3.

$\mathfrak{U}\# B[\vec{\underline{x}}/\vec{x}]$for every
for every;$A\in\Gamma$$B\in\Delta$.

for each original variable . Then an
which is a sequent
have no occurrence ininfinite number of variables
thatis consistent weof the o.riginal formal language. Now with thewhich induces a Cl-model 2
can extend it to a -saturated infinite sequentand the conditions 1. and 2. are satisfied. Hence iswhere
1what we would like to obtain.

Proof. First increase variables twofold, adding$x_{1}’,$ $x_{2}’,$$x_{i}’$$x_{i}$$\Gamma\Rightarrow\Delta,$$\ldots$$\Gamma\Rightarrow\Delta$$\mathrm{c}\underline{\mathrm{o}\mathrm{n}}\mathrm{d}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$\Gamma\Rightarrow\tilde{\Delta},$$\mathrm{L}\mathrm{K}$$[$$\mathfrak{U}$$|\mathfrak{U}|=\{x_{1},x_{1}’, x_{2}, x_{2}’, \ldots\}$

REMARK 5.12
lies in the lemma
The reason why we cannot aPPly our method to the logic
we must have infinitely many
above. Given an infinite consistent sequent
LK-saturation,in the extension of thewhichresultittoextra variables to extend
domain.
$\mathrm{N}_{\neg}\mathrm{D}\mathrm{O}$$\Gamma\Rightarrow\Delta,$

Now we prove the last lemma.
LEMMA 5.13
$a’,$and so on be the same as in the proof of theorem 5.6. Then
Let $A,$$ce\hslash
ainly$.
-model andanis
As we saw in lemma 5.11, $U(a)\subseteq U(a’)$ .
Proof. First we show that is an
is in whereby the definition of,orIf
Now by the definition of which is a counter model foris anode of: I), which in turn implies that(orof
the sequent, respectively) by lemma 5.5. Hence we have obtained
(or
.
and
is
Since we added an omniscient world for every $a\in M$ as a new daughter,$\mathfrak{M}’,$$\mathfrak{M}’$$a$$\mathfrak{M},$$\mathfrak{M}’\# A$$\mathrm{N}_{\neg}\mathrm{O}$$\mathfrak{M}’$$\vec{x}\in p^{I^{+}(a)}$

$a$

$($

$\mathrm{N}_{\neg}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1.$$\mathfrak{M},$$p^{I^{-}(a)})_{-^{\mathrm{b}\mathrm{h}\mathrm{e}\mathrm{n}}}$$\mathrm{g}\Delta$$\mathcal{T}.$$\Gamma_{\neg}\Rightarrow$$\mathrm{L}\mathrm{K},$$p(\vec{x})(\mathrm{o}\mathrm{r}\sim p(\vec{x}))$$\Gamma$$\mathfrak{U}$$\mathfrak{U}\models\neg p(\vec{\underline{x}})$$\mathfrak{U}\models p(\vec{\underline{x}})$$a’\models^{-}p(\vec{\underline{x}})$$a’\models^{+}p(\vec{\underline{x}})$$p^{I^{+}(a)}\subseteq p^{I^{+}(a’)}$$p^{I^{-}(a)}\subseteq p^{I^{-}(a’)}$

$a’$

an

$\mathrm{N}_{\neg}\mathrm{O}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1$.

Now it suffices to show$\mathfrak{M}’\# A,$

which is reduced to the following:

For every node $a:\Gamma\xi\Delta$ of, respectively) in(or$\overline{\mathcal{T}},$$a\#^{+}B[\vec{\underline{x}}/\vec{x}]$$\mathfrak{M}’$$B\in\Gamma$$\mathfrak{M}’$(or $B\in\Delta$ ) implies.

$a\models^{+}B[\vec{\underline{x}}/\vec{x}]$115, not of
Please note that in the above statement is considered as apossible world of,, by the definition of we have
. This is verified as follows. If.
hence the addition of does not affect the fact that
$B\in\Delta$. It is an important fact here that the cases where $a\#^{+}B$ is
Assumeare limited to those where the logicalaffected by the addition of anew daughter
holds or not
is involved; i.e. where in order to verify whether
connective
in such
it,
to
show
.
of
top
of
And
on
we must see the descendants
cases what we must verify is “there is one world where ”. Since was already the.
, it also holds inmodel where
for aclosed formula $B$ . Then there is a
For example, assume $a\#^{+}\neg B$ in. Hence we have $a\#^{+}\neg B$
where $b\models^{+}B$ , and is also indescendant of inI, too.
in$\mathfrak{M}’$

$a$

$a’$

$B\in\Gamma$$\mathfrak{M}$$a’$$a’\models^{+}B[\vec{\underline{x}}/\vec{x}]$$a\models^{+}B[\vec{\underline{x}}/\vec{x}]$$a’$$\neg,$$arrow \mathrm{o}\mathrm{r}$$\models^{+}$$\forall$$a\#^{+}B[\vec{\underline{x}}/\vec{x}]$$a$$\mathfrak{M}$$\ldots$$\mathfrak{M}’$$a\#^{+}B[\vec{\underline{x}}/\vec{x}]$$\mathfrak{M}$

$b$

$a$

$\mathfrak{M}’$$b$$\mathfrak{M}$$\mathfrak{M}’$Another Proof-For

5.2$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$and$\mathrm{G}\mathrm{N}_{\neg}\mathrm{D}\mathrm{O}$. As weIn this subsection we present another proof of Kripke completeness of
DO; that issaw above, we cannot apply the method in the previous subsection to
constructingabecause we construct omniscient possible worlds after we have finished-model. In this way we cannot take affesh variable which is necessary tocountermake an omniscient world, without increasing variables.
The method presented here overcomes this kind of difficulty; it constructs both a-model and omniscient worlds simultaneously.
counter. Roughly
In the proof we use atree-sequent with guardians, often abbreviated aseach of whose nodes has an extra sequent of
is atree-sequent of
speaking,
The
and afinite set of variables; each node has two sequentsis said to be aguardian sequent, or simply aguardian, of that
second sequentnode.
. To construct an omniscient world for each
Now we explain the idea of
possible world of acounter-model after extending an unprovable tree-sequent of, it is necessary to have arecord which formula must be verified or refuted at, and this information is written in the guardian sequent of . In other words, theguardian sequent of is the seed of the omniscient world for .
We present the precise definition:$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$\Gamma\Rightarrow\Delta\uparrow\Sigma\Rightarrow\Pi\beta.$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\Sigma\Rightarrow\Pi\beta$$a’$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$a$$\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\mathrm{O}$

$a’$

$a$

$a$

$a$

DEFINITION 5.14
Atree-sequent with guardians (TSg)with its own two sequents of(we will denote this fact by (condition:

is afinite tree each of whose node is associatedandand two finite sets of variables,)), which satisfies the following
: [3
$a$

$\mathcal{G}$$\Gamma \mathrm{g}\Delta$$\Sigma\Rightarrow\Pi\beta$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$a$$\Delta\uparrow\Sigma\Rightarrow\beta\Pi$to
Let be atree obtained by adding anew daughter, and then omitting all the guardians (Fig.
each nodesatisfies the conditions as; that is,3). Thenis atree-sequent ofto the availability of variables.
$(a_{g} :$\mathcal{G}^{t}$\Sigma\Rightarrow\Pi\beta\uparrow \Rightarrow )$$(a:\Gamma\xi\Delta\uparrow\Sigma\Rightarrow\Pi)\beta$$\mathrm{T}\mathrm{N}_{\neg}$$\mathcal{G}^{t}$$\mathcal{G}^{t}$.
for
aguardianis said to be aleft-sequent, or simply sequent of , andis atranslation into tree-sequent
sequent, or simply guardian of . The tree-sequent

For example,$\alpha\cap\beta=\emptyset$$(a:\Gamma\Rightarrow\Delta\uparrow\Sigma\Rightarrow\Pi)\beta$$\Sigma\Rightarrow\Pi\beta$$\mathrm{r}\Rightarrow\Delta$

$a$

$a$

$\mathcal{G}^{t}$116$\overline{\fbox \mathcal{G}^{t}}$$\mathcal{G}$.

$\Sigma\Rightarrow\Pi\beta$.

$\mathrm{r}.\grave{3}$$.\Delta\uparrow\Sigma\Rightarrow\Pi\backslash \ldots\beta$$.\backslash \cdot/\Gamma\Rightarrow\Delta\alpha\backslash \ldots$

Fig. 3:$\mathcal{G}$and$\mathcal{G}^{t}$of . Avariable is available at the node in if it is available at in the translationinwhere is a node of
if is available at the daughter
is available atof in .
$x$$\mathcal{G}$$a$$\mathcal{G}^{t}\cdot x$$a_{g}$$x$$\mathcal{G},$$\mathcal{G}^{t}$$a$$a_{g}$$a$$\mathcal{G}$$a$$\mathcal{G},$Now we introduce the-system$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$for the logic$\mathrm{N}_{\neg}\mathrm{O}$:(axiom 1)$\ldots$[A(axiom 2)$\xi A\uparrow\Sigma\Rightarrow\Pi|\beta\ldots$$\ldots[A,$(axiom$\mathrm{g}1$)$\sim A\Rightarrow$$\uparrow\Sigma\Rightarrow\Pi|\beta\ldots$$\overline{\ldots[\Gamma 3\Delta\uparrow A,\sim A3|\cdots}$$\overline{\ldots[\Gamma\Rightarrow\Delta\uparrow A4A|\cdots}$(axiom$\mathrm{g}2$)(axiom gO). . . [I$\Rightarrow\Delta\uparrow\Rightarrow A\vee\sim A|\beta\ldots$

Inference rules(weakening), (drop ),$\mathrm{L}$$(\sim\Lambda \mathrm{L}),$and$(\sim\Lambda \mathrm{R}),$$(\sim\forall \mathrm{R})$$(\Lambda \mathrm{L}),$$(\simarrow \mathrm{L}),$$(\Lambda \mathrm{R}),$$(\simarrow \mathrm{R}),$$(arrow \mathrm{L}),$$(\sim\neg \mathrm{L}),$$(arrow \mathrm{R})_{\mathrm{t}},$$(\sim\neg \mathrm{R}),$$\mathrm{T}\mathrm{N}_{\neg}$$(\sim\sim \mathrm{L}),$$(\sim\sim \mathrm{R}),$$(\forall \mathrm{R})_{\mathrm{t}}$,$(\sim\forall \mathrm{L})_{\mathrm{V}\mathrm{C}}$(enlightenment L)

involve only guardians but no left-sequents. For them we will indicate

only guardians.

...
...

$\uparrow \mathrm{I}\Rightarrow\Delta|\beta\ldots$(g-weakening)$\uparrow\Sigma,$$\Pi|\beta\ldots$$\Gamma\Rightarrow\Delta,$(g-cut)$\ldots\frac{\uparrow\Sigma\Rightarrow\Pi,A|\cdots\cdots\uparrow A,\Phi\Rightarrow\Psi|\beta\beta}{\beta}\ldots$...

$\uparrow\Sigma,$$\underline{\ldots\uparrow A,B,\Sigma\Rightarrow\Pi|\beta\ldots}(\mathrm{g}\Lambda \mathrm{L})$$\ldots\uparrow A\Lambda B,$$(\forall \mathrm{L}),$except (cut), are adopted and applied to left-sequents,$. \cdot...\cdot\frac{[\Gamma\epsilon\Delta\uparrow A,\Sigma\Rightarrow\Pi|\beta}{[A,\Gamma\Rightarrow\Delta\uparrow\Sigma\Rightarrow\Pi|\alpha\beta}.\cdot...\cdot$$(\mathrm{g}\cdots)$$(\neg \mathrm{R})_{\mathrm{t}},$,i.e. all the inference rules of
not to guardians.

The rules$(\neg \mathrm{L}),$$\Sigma\Rightarrow\Pi\beta|\cdots$$\Phi\Rightarrow\Pi,$$\Psi|\cdots$.. .

$\uparrow\Sigma\Rightarrow\Pi,$$B|\beta\ldots(\mathrm{g}\Lambda \mathrm{R})$$\ldots\ldots\frac{\uparrow\Sigma\Rightarrow\Pi,A|\beta}{\beta}$...

$\uparrow\Sigma\Rightarrow\Pi,$$\ldots\ldots\frac{\uparrow\Sigma\Rightarrow\Pi,A|\cdots\cdots\uparrow B,\Phi\Rightarrow\Psi|\beta\beta}{\uparrow Aarrow B,\Sigma,\Phi\Rightarrow\Pi,\Psi|\beta}\ldots\cdots(\mathrm{g}arrow \mathrm{L})$A$\Lambda B|\cdots$$. \cdot\cdot\cdot\cdot\frac{\uparrow A,\Sigma\Rightarrow\Pi,B|\beta}{\uparrow\Sigma\Rightarrow\Pi,Aarrow B|\beta}...\cdot\cdot\cdot(\mathrm{g}arrow \mathrm{R})$.

117$\underline{\ldots\uparrow A,\Sigma\Rightarrow\Pi|\beta\ldots}(\mathrm{g}\neg \mathrm{R})$$. \cdot\cdot\cdot\cdot\cdot\frac{\uparrow\Sigma\Rightarrow\Pi,A|\beta}{\uparrow\neg A,\Sigma\Rightarrow\Pi|\beta}..\cdot\cdot\cdot\cdot(\mathrm{g}\neg \mathrm{L})$... 1$\ldots\frac{\uparrow A[y/x],\Sigma\Rightarrow\Pi|\beta}{\beta}\ldots(\mathrm{g}\forall \mathrm{L})$...

$\uparrow\forall xA,$$\neg A|\beta\ldots$$\Sigma\Rightarrow\Pi,$$\ldots\frac{\uparrow\Sigma\xi^{z\}}\beta\cup\square ,A[z/x]|}{\beta}\ldots(\mathrm{g}\forall \mathrm{R})_{\mathrm{V}\mathrm{C}}$...

$\Sigma\Rightarrow\Pi|\cdots$$\uparrow\Sigma\Rightarrow\Pi,\forall xA|\cdots$$\ldots\ldots\frac{\uparrow\sim A,\Sigma\Rightarrow\Pi|\cdots\cdots\uparrow\sim B,\Sigma\Rightarrow\Pi|\beta\beta}{\uparrow\sim(A\Lambda B),\Sigma\Rightarrow\square |\beta}\ldots\cdots(\mathrm{g}\sim\Lambda \mathrm{L})\ldots\frac{\uparrow\Sigma\Rightarrow\Pi,\sim A,\sim B|\beta}{\beta}\ldots(\mathrm{g}\sim\Lambda \mathrm{R})$

...
...
...

$\uparrow A,$$\sim B,$$\uparrow\Sigma\Rightarrow\Pi,$.. .

$\Sigma\Rightarrow\Pi|\beta\ldots$$\uparrow\sim(Aarrow B),$$\sim(A\wedge B)|\cdots$$\uparrow\Sigma\Rightarrow\Pi,$$\sim B|\beta\ldots(\mathrm{g}\simarrow \mathrm{R})$$( \mathrm{g}\simarrow \mathrm{L})\ldots\frac{\uparrow\Sigma\Rightarrow\Pi,A|\beta}{\beta}\ldots$...

$\Sigma\Rightarrow\Pi|\beta\ldots$$\underline{\ldots\uparrow A,\Sigma\Rightarrow\Pi|\beta\ldots}(\mathrm{g}\sim\neg \mathrm{L})$$\uparrow\Sigma\Rightarrow\Pi,$...

$\sim(Aarrow B)|\cdots$$A|\beta\ldots$$\uparrow\Sigma\Rightarrow\Pi,$$(\mathrm{g}\sim\neg \mathrm{R})$.. .

$\uparrow\sim\neg A,$...

$\uparrow A,$...

$\Sigma\Rightarrow\Pi|\beta\ldots$$\sim\neg A|\beta\ldots$$\uparrow\Sigma\Rightarrow\Pi,$...

$\Sigma\Rightarrow\Pi|\beta\ldots$$A|\beta\ldots$$\uparrow\Sigma\Rightarrow\Pi,$$(\mathrm{g}\sim\sim \mathrm{L})$.

$..\uparrow\sim\sim A,$$\underline{\ldots\uparrow\sim A[z/x],\Sigma\beta\cup\xi^{z\}}\Pi|\cdots}(\mathrm{g}\sim\forall \mathrm{L})_{\mathrm{V}\mathrm{C}}$...

$\uparrow\sim\forall xA,$$(\mathrm{g}\sim\sim \mathrm{R})$...

$\Sigma\Rightarrow\square |\beta\ldots$$\sim\sim A|\beta\ldots$$\uparrow\Sigma\Rightarrow\Pi,$$\ldots\frac{\uparrow\Sigma\Rightarrow\Pi,\sim A[y/x]|\beta}{\beta}\ldots(\mathrm{g}\sim\forall \mathrm{R})$...

$\Sigma\Rightarrow\Pi|\beta\ldots$$\uparrow\Sigma\Rightarrow\square ,$$\sim\forall xA|\cdots$

In view of the function of aguardian as aseed of an omniscient possible world, thelogical rules as to guardians are to be of the form of those in, as above.
(;, in an inductive way similar
Now we define the translation irvto a formula ofto that of tree-sequent. A
except the one thatsatisfies every condition of
if is free in the sequent of (or in the guardian of ), then is available at (orat(;, denoted byrespectively). A translation into a formula of a
, isdefined inductively on the height of :$\mathrm{L}\mathrm{K}$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$pre- \mathrm{T}\mathrm{S}_{\mathrm{g}}$$x$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$

$a$

$x$

$a$

$a$

$\mathcal{G}^{f}$$a_{g},$$\mathrm{p}\mathrm{r}\mathrm{e}-\mathrm{T}\mathrm{S}_{\mathrm{g}}$$\mathcal{G}$$\backslash [\Gamma\xi\Delta\uparrow\Sigma\Rightarrow\Pi|\mathcal{G}_{1}\ldots \mathcal{G}_{m}]^{f}\beta$$:\equiv\forall\partial((\Lambda^{\Gamma})arrow(\vee\Delta)\vee\forall\vec{\beta}\neg\neg((\wedge\Sigma)arrow(\vee\Pi))\vee \mathcal{G}_{1}^{f}\vee\cdots\vee \mathcal{G}_{m}^{f})$As is the case for systems of tree-sequent, we can prove the following lemma, which
may be regarded as the soundness of:$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$LEMMA 5.15

If
Proof.

$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}\vdash(;$, then$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash Cif$.

Since the counterparts of lemma 2.11 and 2.12 are easily verified, we canassume that the node to which an inference rule is applied (or the node which is in theform indicated in an axiom) is nothing but the root. Now we prove the lemma by the
induction on the derivation of in.
The cases for (axiom 1), (2), (g1) or (g2) are easy.
.
For the (axiom gO), by omniscience axiom,L) or
For the rules which are common in
(drop
such
as
and
the proof is carried out just as we did in the proof of lemma 2.10.
$\mathcal{G}$$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\neg\neg(A\vee\sim A)$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$$(\sim\forall \mathrm{R})$118
For remaining rules involving guardians, some proofs are obvious, others are complicated. Here we present the latter cases.
Before considering each cases, we prepare the following fact:$\mathrm{G}\mathrm{N}_{\neg}$($\mathrm{L}\mathrm{J}$or$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$(S)) $\vdash\neg\neg(A\vee\neg A)$$\frac{A\Rightarrow A}{\underline A\Rightarrow A\vee\neg A}(\vee \mathrm{R})(\neg \mathrm{L})$$\underline{A,\neg(A\vee\neg A)\Rightarrow}(\neg \mathrm{R})$$\underline{\neg(A\vee\neg A)\Rightarrow\neg A}(\vee \mathrm{R})$$\neg(A\vee\neg A)\Rightarrow A\vee\neg A$$\overline{\neg(A\vee\neg A),\neg(A\vee\neg A)\Rightarrow}(\neg \mathrm{L})$$\overline{\Rightarrow\neg\neg(A\vee\neg A)}(\neg \mathrm{R})$For$(\mathrm{g}\neg \mathrm{R})$, it suffices to show that.

$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\neg\neg(C\Lambda Aarrow D)\Rightarrow\neg\neg(Carrow D\vee\neg A)$.

$C\Lambda Aarrow.\cdot.\cdot D\Rightarrow D\vee\neg A$$C\Lambda Aarrow..\cdot$$D\Rightarrow D\vee\neg A$$C,$ $A,$$C,$ $\neg A,$$\frac{\Rightarrow\neg\neg(A\vee\neg A)\overline{\neg\neg(A\vee\neg A),\neg\neg(C\Lambda Aarrow D)\Rightarrow\neg\neg(Carrow D\vee\neg A)}(l)\frac{\overline C,A\vee\neg A,C\Lambda Aarrow D\Rightarrow D\vee\neg A}{\overline A\vee\neg A,C\Lambda Aarrow D\Rightarrow Carrow D\vee\neg A}(arrow \mathrm{R})}{\neg\neg(C\Lambda Aarrow D)\Rightarrow\neg\neg(Carrow D\vee\neg A)}(\mathrm{c}\mathrm{u}\mathrm{t})(\neg \mathrm{L},\mathrm{R})(\vee \mathrm{L})$, the proof is similar to above, using, it suffices to show that$D\vee\forall xA)$ , whereis not free in $C$ nor $D$ .

For
For

$(\mathrm{g}arrow \mathrm{R})$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\neg\neg(A\vee\neg A)$.

$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash\forall z\neg\neg(Carrow D\vee A[z/x])\Rightarrow\neg\neg(Carrow$$(\mathrm{g}\forall \mathrm{R})$$z$$\overline{D,\sim D\Rightarrow}$$C\Rightarrow C$(axiom 2)$\overline{A[z/x],\sim A[z/x]\Rightarrow}(\mathrm{a}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}2)$$\overline{D\vee A[z/x],\sim D,\sim A[z/x]\Rightarrow}(\vee \mathrm{L})$$\overline{\forall z\neg\neg(Carrow D\vee A[z/x]),C,\sim D,\sim A[z/x]\Rightarrow\underline{\underline{Carrow D\vee A[z/x],C,\sim D,\sim A[z/x]\Rightarrow}}}(\neg \mathrm{R},\neg \mathrm{L},\forall \mathrm{L})(arrow \mathrm{L})$$\overline{\overline{\forall z\neg\neg(Carrow D\vee A[z/x]),\sim(Carrow D\vee\forall xA)\Rightarrow}}\overline{\forall z\neg\neg(Carrow D\vee A[z/x]),C,\sim D,\sim\forall xA\Rightarrow}(\sim\forall \mathrm{L})_{\mathrm{V}\mathrm{C}}(\sim\vee \mathrm{L},\simarrow \mathrm{L})$$\overline{\forall z\neg\neg(Carrow D\vee A[z/x]),\neg(Carrow D\vee\forall xA)\Rightarrow}(l2)$$\overline{\forall z\neg\neg(Carrow D\vee A[z/x])\Rightarrow\neg\neg(Carrow D\vee\forall xA)}(\neg \mathrm{R})$1
into saturation and derive a counter model
We are to extend an unprovablefrom it; hence the definition of saturatedness is as follows:$\mathrm{T}\mathrm{S}_{\mathrm{g}}$DEFINITION 5.16
isAn infinite$(\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}- \mathrm{S}\mathrm{A}\mathrm{T}\mathrm{U}\mathrm{R}\mathrm{A}\mathrm{T}\mathrm{E}\mathrm{D}\mathrm{N}\mathrm{E}\mathrm{S}\mathrm{S})$$\mathrm{T}\mathrm{S}_{\mathrm{g}}\mathcal{G}$$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$-saturated if it satisfies the following conditions:

1. The translation into a tree-sequent,
2. For every node
thenavailable at$\mathcal{G}^{t},$$(a:\Gamma\xi\Delta\uparrow\Sigma\Rightarrow\Pi)\beta$$a_{g}$

is$\mathrm{T}\mathrm{N}_{\neg}- \mathrm{s}\mathrm{a}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d}$;and every atomic formula$p(\vec{x})\in\Sigma \mathrm{o}\mathrm{r}\sim p(\vec{x})\in\Sigma$.

$p(\vec{x}),$if$\vec{x}$is119(; and at least one variable is available at its root.
Let be asuch that T,
will extend step by step to obtain asequence of unprovable
is the same
. The step fromas we did in
involves $A_{i}(A_{1},$toquence of formula as subsection 2.4), and is stated in detail as follows:$\mathcal{G}$$\mathrm{g}\mathrm{N}_{\neg}\mathrm{O}\forall$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$\mathrm{T}\mathrm{S}_{\mathrm{g}}\mathrm{s}\mathcal{G}\mathrm{o}(\equiv \mathcal{G}),$$\mathcal{G}$$\mathrm{e}$$\mathcal{G}_{i-1}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{s}\mathrm{t}$$A_{2},$$\mathcal{G}_{i}$$\mathcal{G}_{1},$$\ldots$$\ldots$

1. APPly the same operations (inheritance and reduction) to the left-sequents of .
, then add
to the antecedent) andFor example, if ( :Iof the left-sequent of each decsendant of , not involving guardians;$\mathcal{G}$$\beta$$\Rightarrow\Delta\uparrow\Sigma\Rightarrow\Pi$$a$$A_{i}\in\Gamma$$A_{i}$$a$, ifthen add
to X. This
2. (report) For each nodeoperation is called areport and unprovability is preserved because of the rule$(a : \Gamma\Rightarrow\Delta\alpha\uparrow \mathrm{I}\Rightarrow\square )\beta$(enlightenment$\mathrm{L}$$A_{i}\in\Gamma$$A_{i}$);

3. ( -reduction)According to the shape of
executed for each node$\mathrm{g}$$A_{i}$, one of the following operations is$(a:\Gamma\Rightarrow\Delta\uparrow \mathrm{I}\Rightarrow\Pi):\beta$(a), then add
or
to , sois available atthat unprovability is preserved. This is possible; if not, we can derive acontradiction as follows:$A_{i}\equiv p(\vec{x})$. If$p(\vec{x})$$\vec{x}$$a_{g}$$\sim p(\vec{x})$$\Sigma$(axiom gO)$\ldots\ldots\frac{\uparrow\Rightarrow p(\vec{x})\vee\sim p(\vec{x})1\beta\frac{\uparrow p(\vec{x}),\Sigma\Rightarrow\Pi|\cdots\cdots\uparrow\sim p(\vec{x}),\Sigma\Rightarrow\Pi|\beta\beta}{\uparrow\Sigma\Rightarrow\Pi|\beta\uparrow p(\vec{x})\vee\sim p(\vec{x}),\Sigma\Rightarrow\Pi|\beta(\mathrm{g}- \mathrm{c}\mathrm{u}\mathrm{t})}}{}\ldots\cdots\ldots\ldots\cdots.\cdots(\mathrm{g}\vee \mathrm{L})$, then add both $B$ and $C$ to I. Unprovability is(b) $A_{i}\equiv B\Lambda C$ . If
so thatpreserved by the rule
. If $A_{i}\in\Pi$ , then add $B$ or $C$ to;unprovability is preserved. This is possible by, then add $B$ to or $C$ to , so that unprovability(c) $A_{i}\equiv Barrow C$ . If
$A_{i}\in\Pi$, then add $B$ to I and $C$ to ;is preserved. If(or , respectively) ;(d). If(or ), then add $B$ to$A_{i}\in\Sigma$$\Pi,$$(\mathrm{g}\Lambda \mathrm{L})$$(\mathrm{g}\Lambda \mathrm{R})$$\Pi$$A_{i}\in\Sigma$$\Sigma$$\Pi$$A_{i}\equiv\neg B$

. If

$\Pi$

$\Pi$

$A_{i}\in \mathrm{I}$$\Sigma$, then add $B[y/x]$ to , for every which is availableat. If $A_{i}\in\Pi$ , then take afresh variable , add
and is in$A[x_{m}/x]$ toand also add
to ;to , so that unprovability is(f) $A_{i}\equiv\sim(B\Lambda C)$ . If
preserved. If
to ;
, add
to I. If $A_{i}\in\Pi$ , add(g) $A_{i}\equiv\sim(Barrow C)$ . If
to so that unprovability is preserved;(or ), add $B$ to I(or , respectively) ;
. If
(h)
or
to ,
, then take afresh variable(i). If
for every which isand also add
to . If $A_{i}\in\Pi$ , add $\sim B[y/x]$ to.
available atand in(e)$A_{i}\equiv\forall xB$$A_{i}\in\Sigma$$\Sigma$$y$$\{x_{1}, \ldots, x_{i}\}$$a_{g}$$\Pi$$x_{m}$$\beta$$x_{m}$$A_{i}\in\Sigma,$$A_{i}\in\square ,$$\mathrm{a}\mathrm{d}\mathrm{d}\sim B\mathrm{o}\mathrm{r}\sim C$$\Pi$$\mathrm{a}\mathrm{d}\mathrm{d}\sim B\mathrm{a}\mathrm{n}\mathrm{d}\sim C$$A_{i}\in\Sigma$$\Sigma$$B\mathrm{o}\mathrm{r}\sim C$$B\mathrm{a}\mathrm{n}\mathrm{d}\sim C$$\Pi$$A_{i}\equiv\sim\neg B$$A_{i}\equiv\sim\sim B$$A_{i}\equiv\sim\forall xB$$A_{i}\in\Sigma$$x_{m}$$A_{i}\in\Sigma$$\Pi$$\square$$x_{m},$$\Pi$$\beta$Let be the infinite
which is the union ofis
Gurated. Indeed, it satisfies the condition thatdeofsatisfies the condition$\tilde{\mathcal{G}}$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$\overline{\mathcal{G}}^{t}$\Sigma\Rightarrow\Pi)\beta$$a_{g}$$y$$\mathcal{G}0,$$\mathcal{G}_{1},$$\mathrm{T}\mathrm{N}_{\neg}$$\ldots$. Then$\tilde{\mathcal{G}}$is$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}-$-saturated;for example, a$\tilde{\mathcal{G}}^{t}$, then there exists adescendant-saturated:If
and avariable such that $A[y/x]\in\Psi$$\forall xA\in\Sigma$$(\forall \mathrm{R})_{\mathrm{t}}$$y$$\Sigma$$\{x_{1}, \ldots, x_{i}\}$$a_{g}$$(a_{g} :$\mathrm{a}\mathrm{d}\mathrm{d}\sim B[x_{m}/x]$$b:\Phi\Rightarrow\beta\Psi$

of

120
satisfies the second condition of
itself as
by taking-saturatedness by
the operation ( -reduction)as to atomic formulas.
isit induces an
Since an infinite tree-sequentin theway stated in subsection 2.4. Moreover, the second condition of-saturatedness
where the omniscient world for each worldis actually anyields thatof .
induced byverified by the induction on the construction of aformula
The following isisfor every node :using the fact thatofis(or $a\in\Delta$ ) implies
which is unprovable),(or
an original, respectively). Hence we have proved the following theorem:$b.\overline{\mathcal{G}}$$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$$a_{g}$$\mathrm{g}$$\overline{\mathcal{G}}^{t}$$\mathrm{N}_{\neg}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1\mathfrak{M}$$\mathrm{T}\mathrm{N}_{\neg}- \mathrm{s}\mathrm{a}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d},$$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$$\mathfrak{M}$$a’$$\mathrm{N}_{\neg}\mathrm{O}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1,$$\overline{\mathcal{G}}^{t}$$a$$a_{g}$$\mathrm{e}\mathrm{a}\mathrm{s}\underline{\mathrm{i}\mathrm{l}}\mathrm{y}$$A$$\mathcal{G}^{t}$$\Gamma \mathrm{g}\Delta$$a$$\mathrm{T}\mathrm{N}_{\neg}- \mathrm{s}\mathrm{a}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d}:$$a\in\Gamma$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$\mathcal{G}^{t}(\mathcal{G}$$a\models^{+}A[\vec{\underline{x}}/\vec{x}]$$a\#^{+}A[\vec{\underline{x}}/\vec{x}]$)THEOREM 5. 17 (KRIPKE COMPLETENESS OF
at whose root at least one varriable is available, andLet be aof
Then there exists a counter
for ;that is,in the sense stated in theorem 2.14.
a counter model for the tree-sequent$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$$\mathcal{G}$$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}\forall$$\mathrm{N}_{\neg}\mathrm{O}- model\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$$\mathcal{G}.$$\mathcal{G}$$\mathfrak{M}$is$\mathcal{G}^{t}$

COROLLARY 5.18 (KRIPKE cOMPLETENESS OF
implies
For every formula of$A$$\mathrm{N}_{\neg}\mathrm{O},$$\mathrm{N}_{\neg}\mathrm{O}\models A$$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$)$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}\vdash A$.

. By the contraposition of
be
where
Let a
hence the theorem yields that there exists a counter
lemma 5.15 we have-modelfor , which makes not valid.
I

Proof.

$[\Rightarrow\alpha A\uparrow\Rightarrow\emptyset]$$\alpha\neq\emptyset$$\mathrm{T}\mathrm{S}_{\mathrm{g}}\mathcal{G}$$\mathrm{T}_{\mathrm{g}}\mathrm{N}_{\neg}\mathrm{O}\forall \mathcal{G},$$\mathfrak{M}$$\mathrm{N}_{\neg}\mathrm{O}$$A$$\mathcal{G}$DO. The Gentzen-style sequent system
Now we consider the logic
plus constant domain axiom
isthe logic$\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{O}$DO for$\mathrm{G}\mathrm{N}_{\neg}\mathrm{O}$$\overline{\Rightarrow\forall x(A(x)\vee B)arrow\forall xA(x)\vee B}$. An$\mathrm{G}\mathrm{N}_{\neg}$(axiom D)

is an
DO-model if $U$ is aconstant map.
, thetoAfter making the same kind of alterations as we did from
DO, and we obtainmethod forstated above can be also applied to the logic
the following theorem:$\mathrm{N}_{\neg}\mathrm{O}- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1\mathfrak{M}=(M, \leq, U, I^{+}, I^{-})$$\mathrm{N}_{\neg}$$\mathrm{T}\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\mathrm{O}$$\mathrm{T}\mathrm{N}_{\neg}\mathrm{D}$$\mathrm{T}\mathrm{S}_{\mathrm{g}}$$\mathrm{N}_{\neg}$

THEOREM 5. 19 (MAIN THEOREM 2, KRIPKE COMPLETENESS OF
DO
For every formula of DO,
if and only if$A$$\mathrm{N}_{\neg}$$\mathrm{N}_{\neg}\mathrm{D}\mathrm{O}\models A$$\mathrm{G}\mathrm{N}_{\neg}$$\mathrm{G}\mathrm{N}_{\neg}$$\vdash A$.

DO)

References[AN84] Ahmad Almukdad and David Nelson. Constructible falsity and inexact predicates. The Joumal of Symbolic Logic, 49(1):231-233, 1984.
[Ish70]

Arata Ishimoto. A Sch\"utte-type formulation of the intuitionistic functional
calculus with strong negation. Bulletin of the Tokyo Institute of Technology,
100:161-189, 1970.

[Kas99] Ryo Kashima. Sequent calculi of non-classical logics-Proofs of completenesstheorems by sequent calculi (in Japanese). In Proceedings of MathematicalSociety of Japan Annual Colloquium of Foundations of Mathematics, pages
49-67, 1999.

[Mar50] A. A. Markov. Konstruktivnaja logika. Uspehi $Matemati\check{c}eskih$ Nauk, 5:187188, 1950.

121[Ne149] D. Nelson. Constructible falsity. The Journal of Symbolic Logic, 14:16-26,

1949.

[PR84]

Graham Priest and Richard Routley. Introduction: Paraconsistent logics.
Studia Logica, 43:3-16, 1984.

[Tan80] Kazuyuki Tanaka. Astudy of intuitionistic logic with strong negation (inJapanese). Master’s thesis, Tokyo Institute of Technology, 1980.