In our previous paper [5], we have studied Kripke.type semantics, for propositional logics without the contraction rule. In this paper, we will extend our argument to predicate logics without the structure rules. Similarly to the propositional case, we can not carry out Henkin's construction in the predicate case. Besides, there exists a difficulty that the rules of inference (~V) and (=1~) are not always vali4 in our semantics. So, we have to introduce a notion of normal models.
In this paper, we will introduce five predicate logics without the some structure rules (except ZJ), Z.BCA, .LBCB, ZBCC,, .LBC.K, and JLJ. 1%r each of them, the cut elimination theorem holds. Then, we will introduce: a Kripke-type semantics with varying domain (a semantics with constant domain has been given by It. Ono [4]). In the proofs of the completeness theorems for those logics (except .SJ), we can not construct ttenldn's theory. It is closely related with the fact that neither the sequent A ^ (B v C) -->(An B)v (AA C) nor the sequent A^ 3xB(x)--->3x(AA B(x)) can be proved in those logics without the contraction rule. So, we must prove the completeness theorems for those logics without using Henkin's construction by changing the interpretation of v and 3. We assume the familiarity" with [3] and [5].
1. Syntactical analysis
In the following, we fix a language ~ for predicate logics. The language .Sf contains __1, T (truth), ~, v, ^, &, V and 3 as logical connectives. We suppose that 5e contains neither function symbols nor individual constants. We remark here that it does not necessarily hold in L.BCA that A-->-V is provable even if -~A is provable. On the other hand, in ZBCA, T-->A is also provable if -+A is provable. In any system with the weakening rule, both sequents A-->T and m -+A are provable if -~A is provable.
:~ow we will introduce a basic logical system called ZBCA. l~oughly speaking, ZBC~A is a formal system obtained from Gentzen's system ZJ for intuitionistic predicate logic, by eliminating all the structure rules. Initial sequents of .~.BCA are either of the form F~ J_~ A->A