The curse of constructive mathematics -Can the gadget computer go beyond the NP problem?-

KYUMA, Eido

                      kyuma@dpc.aichi-gakuin.ac.jp

General Education, Aichi-gakuin University

1 Introduction

Most computer scientists believe that normal computers work in constructive mathematics. In constructive mathematics, “there exists something” means “we can construct something” or “we know the position of something”, and usual algorithms of most computers work in this way.

Now, I think about the “P = NP ” problem. The P problems and the NP problems are decision problems.

When we solve a decision problem, we have only to get either a ‘yes’ answer or a ‘no’ answer. However, before we know a ‘yes’-‘no’ answer, we get more information from constructive mathematics.

My main question is if there exists an algorithm which gets a ‘yes’-‘no’ answer before we get more information. I think that most computers have the curse of constructive mathematics, and I doubt whether such a thing is possible using algorithms of normal computers.

In this paper, we try to compute an NP problem by using concrete objects, which is called “gadgets”. In the gadget world, it seems that “there exists something” dose not necessarily mean “we can con-

struct something” or “we know the position of something.”

For example, let’s think about the existence of a hole in a sheet. In constructive mathematics, “there exists the hole” means “we know the position of the hole correctly.” However, in the gadget world, if we want to know the existence of the hole, it is sufficient to illuminate this sheet. We do not have to know the position of the hole beforehand.

In this case, it seems that we can know the existence of the hole before we measure the position. This paper discusses the time complexity between these algorithms.

2 Basic Notation

In this paper, we think about the satisfiability of the conjunctive normal form, which is called SAT.

Definition 1. Let n be a natural number. Let U_{n} = {x_{1}, x_{2}, …, x_{n}} be a set of n boolean variables.

Definition 2. Let k be a natural number, and each l_{i} (i = 1, 2, …, k) be either a boolean variable or a negated boolean variable in U_{n}. Then,

l_{1} ∨ l_{2} ∨ ⋯ ∨ l_{k}

is said to be the clause.

Definition 3. Let m be a natural number, and each C_{j} (j = 1, 2, …, m) be a clause. Then,

C_{1} ∧ C_{2} ∧ ⋯ ∧ C_{m}

is said to be the conjunctive normal form.

Definition 4. Let D be the conjunctive normal form w.r.t. U_{n} . If there exists the assignment f : U_{n} → {True, False} such that the value of D is True by substituting the assignment f into variables, then D is satisfied.

Example 5. We use U_{4} = {x_{1}, x_{2}, x_{3}, x_{4}}.

D = \begin{aligned}& ( & x_{1} & ∨ & ¬x_{2} & & & & & ) \\ ∧ & ( & & & x_{2} & ∨ & ¬x_{3} & & & ) \\ ∧ & ( & x_{1} & ∨ & x_{2} & ∨ & x_{3} & & & ) \\ ∧ & & & & ¬x_{2} \\ ∧ & ( & ¬x_{1} & ∨ & x_{2} & ∨ & x_{3} & ∨ & x_{4} & ) \end{aligned}

is the conjunctive normal form. And, there exists the assignment

f(x) = \{ \begin{matrix}True & if x = x_{1}, x_{4} \\ False & if x = x_{2}, x_{3} \end{matrix}

such that the value of D is True by the substitution f. Therefore, D is satisfied.

We fix the number n of variables. And N is the set of all natural numbers. Definition 6. \overline{U_{n}} is defined as the set \{i ∈ N | 1 ≤ i ≤ 2^{n} \}. Definition 7. Let x_{i} be the element of U_{n}. Then, x̃_{i} is defined as

\{ j ∈ \overline{U_{n}} | ∃u, v, w ∈ N ( \begin{matrix}(j = u + v × w) ∧ (1 ≤ u ≤ 2^{n−i}) \\ ∧ (1 ≤ v ≤ 2^{i−1}) ∧ (w = 2^{n−i+1}) \end{matrix} ) \} .

And, ˜¬x_{i} is defined as the set \overline{U_{n}} − x̃_{i} . Example 8. Let n be 4 . Then,

\overline{U_{4}} = \{ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16 \} ,
x̃_{1} = { 1, 2, 3, 4, 5, 6, 7, 8  } ,
˜¬x_{1} = {  9, 10, 11, 12, 13, 14, 15, 16 } ,
x̃_{2} = { 1, 2, 3, 4,  9, 10, 11, 12  } ,
˜¬x_{2} = {  5, 6, 7, 8,  13, 14, 15, 16 } ,
x̃_{3} = { 1, 2,  5, 6,  9, 10,  13, 14  } ,
˜¬x_{3} = {  3, 4,  7, 8,  11, 12,  15, 16 } .

Exercise 9. Let n be 4 . Then, what are x̃_{4} and ˜¬x_{4}? Definition 10. Let C be the clause (l_{1} ∨ l_{2} ∨ ⋯ ∨ l_{k}) . Then, \overline{C} is defined as

\overline{U_{n}} − l̃_{1} − l̃_{2} − ⋯ − l̃_{k} .

Example 11. Let n be 4, and C be the clause (¬x_{1} ∨ x_{2} ∨ x_{3}) . Then,

\begin{aligned}\overline{C} & = & \overline{U_{4}} − ˜¬x_{1} − x̃_{2} − x̃_{3} \\ & = & \{7, 8\} . \end{aligned}

Definition 12. Let D be the conjunctive normal form (C_{1} ∧ C_{2} ∧ … ∧ C_{m}) . Then, \overline{D} is defined as

\overline{C_{1}} ∪ \overline{C_{2}} ∪ ⋯ ∪ \overline{C_{m}} .

Theorem 13. Let D be the conjunctive normal form. Then, \overline{D} ⫋ \overline{U_{n}} if and only if D is satisfied. Proof. We use the function

g(x) = \{ \begin{matrix}0 & if x = True, \\ 1 & if x = False. \end{matrix}

For each assignment f : \overline{U_{n}} → \{True, False\},

∑_{i=1}^{n} g ( f (x_{i}) ) × 2^{n−i} ∈ \overline{U_{n}} − \overline{D} ↔ D is True by substituting f.

3 The Gadget Computer

First, we fix the conjunctive normal form D = (C_{1} ∧ C_{2} ∧ … ∧ C_{m}) w.r.t. U_{n} .

In this section, we calculate the satisfiability of the conjunctive normal form in the gadget computer. We use m pieces of sheets, whose figures are rectangles 2 height and 2^{n} wide, as gadgets.

Each clause C_{j} correspond to the j-th sheet. And each sheet is in a coordinate plane, such that

{(x, y) ∈ R × R | 0 ≤ x ≤ 2^{n}, 0 ≤ y ≤ 2 } .

Lemma 14. We can make these sheets, and the number of steps in this process is O(m × n) .

Proof. We can measure the length 2^{n} by the n-th folded sheet.

Definition 15. Let l be either a boolean variable or a negated boolean variable in U_{n}. Then, l̂ is defined as

{(x, y) ∈ R × R | ∃ i ∈ l̃ (i − 1 < x < i) , 0 ≤ y < 1 } .

Definition 16. Let C_{j} be the clause l_{1} ∨ l_{2} ∨ ⋯ ∨ l_{k} . Then, Ĉ_{j} is defined as the remainder, such that we cut off parts l_{1}, l_{2}, …, l_{k} from the j-th sheet.

Lemma 17. The number of steps in this cutting process is O(k × n) .

Proof. If we fold this sheet O(n)-times and cut twice well, then we can cut off the part l̂from the sheet. Of course, if n is sufficiently large, then it is physically impossible. However, now we think about the ideal gadget.

Theorem 18. Now, we lay m pieces of cut sheets Ĉ_{1}, Ĉ_{2}, …, Ĉ_{m} one on top of another. Then, we can find the hole in the area {(x, y) ∈ R × R | 0 ≤ x ≤ 2^{n}, 0 ≤ y ≤ 2} , if and only if D is satisfied.

Proof. It is obvious by Theorem 13.

Theorem 19. Using the gadget computer, we can compute the satisfiability of the conjunctive normal form, and the number of steps in this process is the polynomial function of n .

Proof. It is obvious by above Lemmata and Theorem.

4 Conclusion

Using the above algorithm of the gadget computer, it seems that we can know a ‘yes’-‘no’ answer before we get more information. However, I can not prove that it is true at present.

Now, we think about the relation of the time complexity between these algorithms.

Theorem 20. We assume that, for any conjunctive normal form D w.r.t. U_{n} , we compute the satisfiability problem of D O (p (n))-times . If this problem of D has a ‘yes’ answer, then we can get the satisfied assignment f O (n × p (n))-times.

Proof. If D is the conjunctive normal form w.r.t. U_{n} , then the substitute D[x_{i} := True] and D[x_{i} := False] are conjunctive normal forms w.r.t. U_{n} also.

We use the next algorithm.

E := D

for i := 1 to n

if E[x_{i} := True] is satisfied then f(x_{i}) := True and E := E[x_{i} := True]

else f(x_{i}) := False and E := E[x_{i} := False]

next i

If the satisfiability problem of D has a ‘yes’ answer, then we can get the satisfied assignment f using this algorithm.

This result is not good for my project. Because, even if there exists an algorithm which gets a ‘yes’- ‘no’ answer before we get more information, we can get more information almost at the same time by using the algorithm of the same process.

By this thing, I doubts whether it is essential that the NP problem must be a decision problem in the P = NP problem.

Models for Normal Modal Logics over KR

Takahiro Seki

                            tseki@jaist.ac.jp

School of Information Science, Japan Advanced Institute of Science and Technology

KR is the system of the logic excluding only ‘paradox of relevance’, which is one of paradoxes of material implication, in classical logic. In KR we can identify relevant negation with classical negation, so it is thought that KR is too closer system to classical logic. This paper examines this fact from a viewpoint introducing modal operator. In semantical study of relevant logic, Routley-Meyer semantics are often used and there are two kinds of models, the one is an unreduced model and the other is a reduced model. In general, there is a limit to apply a reduced model. So we consider when a reduced model can be used.

1 Unreduced Model

In this section, based on [4], we deal with the system of normal modal logics over KR (in below, we call them simply normal logics). And we will prove the completeness for them by using unreduced models.

First of all, we determine the language. The language is as follows: (i) propositional variables p, q, r, ⋯; (ii) logical connectives → (relevant implication), ∧ (and), ∨ (or) and ¬ (negation); (iii) modal operator □; and (iv) auxiliary symbols.

The formulas are defined by the usual way, and they are denoted by the capital letters A, B, C, ⋯ (possibly with subscripts). In below Wff, Prop denote the set of all formulas and that of all propositional variables, respectively, and capital Greeks Σ, Γ, Δ, ⋯ (possibly with prime) denote the non-empty sets of formulas.

First, we define the system KRN of the least normal logic. KRN is defined as follows:

(a) Abbreviation

◇A =^{ab} ¬□¬A

(b) Axioms (A1) A → A (A2) A → ((A → B) → B) (A3) (A → B) → ((B → C) → (A → C)) (A4) (A → (A → B)) → (A → B) (A5) A ∧ B → A (A6) A ∧ B → B (A7) (A → B) ∧ (A → C) → (A → B ∧ C) (A8) A → A ∨ B

(A9) B → A ∨ B
(A10) (A → C) ∧ (B → C) → (A ∨ B → C)
(A11) A ∧ (B ∨ C) → (A ∧ B) ∨ C
(A12) (A → ¬B) → (B → ¬A)
(A13) ¬¬A → A
(A14) A ∧ ¬A → B
(A15) □A ∧ □B → □(A ∧ B)
(A16) □(A → B) → (□A → □B)

(c) Rules of inference

\frac{A → B A}{B}(Modus Ponens)  \frac{A B}{A ∧ B} (Adjunction)  \frac{A}{□A}(Necessitation)

Now we define the typical systems of normal logics. Consider the systems obtained by adding the following formulas as axioms to KRN:

(A17) □A → ◇A ; (A18) □A → A ; (A19) □A → □□A  {(A20) A → □◇A \atop (A21) ◇A → □◇A}

We call the systems KRN.D, KRN.T, KRN.4, KRN.B and KRN.5 are obtained by adding (A17),(A18),(A19),(A20) and (A21) to KRN, respectively. We can combine more than two systems. For example, KRN.T4 is obtained by adding (A18) and (A19) to KRN, or by adding (A19) to KRN.T.

In below L denote any systems of normal logics. We write L ⊢ A if A is a theorem of L. Next we give the semantics of the systems of normal logics in terms of unreduced models, and prove

the soundness for them.

An (unreduced) KRN-frame is a quadruple ⟨O, W, R, S⟩ where (a) W is the set of all worlds, (b) O is the non-empty subset of W, (c) R is a ternary relation on W, and (d) S is a binary relarion on W.

A KRN-frame F = ⟨O, W, R, S⟩ satisfies the following postulates, for all a, b, c, d ∈ W:

(p1) ∃x(x ∈ O & Rxab) ⟺ a = b ; (p2) Raaa ; (p3) Rabc ⟹ Rbac & Racb  (p4) Rabe & Recd ⟹ ∃x(Racx & Rxbd) ; (p5) Rabd & Sdc ⟹ ∃x∃y(Sax & Sby & Rxyc) ; (p6) ∃x(x ∈ O & Sxa) ⟹ a ∈ O

(Unreduced) L-frames are KRN-frame ⟨O, W, R, S⟩ which satisfies adding postulates. Adding postulates are as follows, for all a, b, c ∈ W:

(p7) ∃x(Sax) ; (p8) Saa ; (p9) Sab & Sbc ⟹ Sac  {(p10) Sab ⟹ Sba \atop (p11) Sab & Sac ⟹ Sbc}

We call F a KRN.D-frame, KRN.T-frame, KRN.4-frame, KRN.B-frame and KRN.5-frame, if F is a KRN-frame satisfying the postulate (p7), (p8), (p9), (p10) and (p11), respectively. As in systems, we can combine some of distinct L-frames. For example, if a L-frame F holds postulates (p1) - (p6), (p8) and (p9), then F is called a KRN.T4-frame.

We call a quintuple ⟨O, W, R, S, v⟩ L-model on a frame ⟨O, W, R, S⟩ (in below, simply L-model), where ⟨O, W, R, S⟩ is a L-frame and v : Prop×W → {t, f} is called a valuation. For a given model ⟨O, W, R, S, v⟩, the relation a ⊧ A for a ∈ W and A ∈ Wff is defined inductively as follows:

i. for any p ∈ Prop, a ⊧ p iff v(p, a) = t

ii. a ⊧ A ∧ B iff a ⊧ A and a ⊧ B

iii. a ⊧ A ∨ B iff a ⊧ A or a ⊧ B

iv. a ⊧ A → B iff ∀x∀y(Raxy & x ⊧ A ⇒ y ⊧ B)
v. a ⊧ ¬A iff a |̸= A
vi. a ⊧ □A iff ∀x(Sax ⇒ x ⊧ A).

By the abbreviation and an interpretation defined above, a ⊧ ◇A iff ∃x(Sax & x ⊧ A). We say that A is L-valid, if x ⊧ A for every x ∈ O in any L-model ⟨O, W, R, S, v⟩.

Theorem 1 (Soundness of L) For any L, if A is a theorem of L, then A is L-valid.

Finally, we prove the completeness for the systems of normal logics. Basically we follows the method in section 4.6 of [8]. To prove the completeness, the following notions play a key role:

• Let Σ ≠ Wff and Δ ≠ Wff. Then (i) L ⊢ Σ → Δ iff there exist A_{1}, ⋯, A_{m} ∈ Σ(m > 0) and B_{1}, ⋯, B_{n} ∈ Δ(n > 0) such that L ⊢ A_{1} ∧ ⋯ ∧ A_{m} → B_{1} ∨ ⋯ ∨ B_{n}, and (ii) (Σ, Δ) is a L-pair iff (a) L ⊬ Σ → Δ and (b) Σ ∪ Δ = Wff.

• Σ is a L-theory iff (a) if A, B ∈ Σ then A ∧ B ∈ Σ and (b) if L ⊢ A → B and A ∈ Σ, then B ∈ Σ.

• Let Σ be a L-theory. Then (i) Σ is regular iff Σ contains all theorems of L, and (ii) Σ is maximal iff either A ∈ Σ or ¬A ∈ Σ and both do not hold for all A ∈ Wff

• Let Σ, Γ, Δ be L-theories. Then (i) RΣΓΔ iff if A → B ∈ Σ and A ∈ Γ then B ∈ Δ, and (ii) SΣΓ iff if □A ∈ Σ then A ∈ Γ.

Note that SΣΓ iff if A ∈ Γ then ◇A ∈ Σ.

To show the completeness, we see the unreduced case in [8], though there are slight differences in some terminologies and we must replace the part of ‘prime’ by ‘maximal’. Here we pick up the following lemma which does not appear in [8].

Lemma 2 If Σ is a maximal L-theory such that □C ∉ Σ, then there exist maximal L-theory Γ′ such that SΣΓ′ and C ∉ Γ′.

Then it is established that there exists a regular maximal L-theory Π such that A ∉ Π whenever L ⊬ A. Then we construct a canonical L-model ⟨O′, W′, R′, S′, v′⟩ as follows: (1) W′ is the set of all maximal L-theories; (2) O′ is the set of all regular maximal L-theories; (3) R′ is a ternary relation R restricted on W′; (4) S′ is a binary relation S restricted on W′; (5) v′ is defined by v′(p, Σ) = t iff p ∈ Σ, for all p ∈ Prop and Σ ∈ W′.

Theorem 3 (Completeness of L) If A is L-valid, then A is a theorem of L.

2 Reduced Model

In this section, we consider a reduced model. First we define the system KR4 in order to use a reduced model. The system KR4 is the corresponding system of modal logic over KR to NR in [7] or R4 in [5], which are the systems of modal logics over R. Though NR and R4 are different systems, adding A ∧ ¬A → B as an axiom to them, the result systems are equivalent.

KR4 is obtained from KRN.T4 by adding an axiom

(A□) if A is an axiom, then so is □A

instead of eleminating (Necessitation).

If A is a theorem of KR4, we write KR4 ⊢ A.

Next we consider a reduced model and give the semantics of KR4 and prove the soundness for it. A KR4-frame is a quadruple ⟨0, W_{r}, R_{r}, S_{r}⟩ where (a_{r}) W_{r} is the set of all worlds, (b_{r}) 0 ∈ W_{r} is

called a base world, (c_{r}) R_{r} is a ternary relation on W_{r}, and (d_{r}) S_{r} is a binary relation on W_{r}, and satisfies the following postulates, for all a, b, c, d ∈ W_{r}:

(pr1) ∃x(S_{r}0x & R_{r}xab) ⟺ a = b (pr2) R_{r}aaa (pr3) R_{r}abc ⟹ R_{r}acb (pr4) R_{r}abe & R_{r}ecd ⟹ ∃x(R_{r}acx & R_{r}xbd)

(pr5) R_{r}abd & S_{r}dc ⟹ ∃x∃y(S_{r}ax & S_{r}by & R_{r}xyc)
(pr6) S_{r}aa
(pr7) S_{r}ab & S_{r}bc ⟹ S_{r}ac

We call a quintuple ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ KR4-model on a frame ⟨0, W_{r}, R_{r}, S_{r}⟩ (in below, simply KR4model), where ⟨0, W_{r}, R_{r}, S_{r}⟩ is a KR4-frame and v_{r} : Prop × W_{r} → {t, f} is called a valuation. For a given KR4-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩, the relation a ⊧ A for a ∈ W_{r} and A ∈ Wff is defined by the same way in section 1.

We say that A is KR4-valid, if 0 ⊧ A for all KR4-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩.

Theorem 4 (Soundness) If A is a theorem of KR4, then A is KR4-valid.

Finally we prove the completeness theorem for KR4. We prove it by using the style of [8] based on the argument in [7] or [5].

First we give several notions in order to prove the completeness theorem. Note that there are slight differences between in section 1 and in this section. The key notions are as follows.

• Let Σ ≠ Wff and Δ ≠ Wff. Then (i) KR4 ⊢ Σ → Δ iff there exist A_{1}, ⋯, A_{m} ∈ Σ(m > 0) and B_{1}, ⋯, B_{n} ∈ Δ(n > 0) such that KR4 ⊢ □(A_{1} ∧ ⋯ ∧ A_{m} → B_{1} ∨ ⋯ ∨ B_{n}), and (ii) (Σ, Δ) is a KR4-pair iff (a) KR4 ⊬ Σ → Δ and (b) Σ ∪ Δ = Wff.

• Σ is a KR4-theory iff (a) if A, B ∈ Σ then A ∧ B ∈ Σ and (b) if KR4 ⊢ □(A → B) and A ∈ Σ, then B ∈ Σ.

• Let Σ be a KR4-theory. Then (i) Σ is regular, iff Σ contains all theorems of KR4, and (ii) Σ is maximal, iff either A ∈ Σ or ¬A ∈ Σ and both do not hold for all A ∈ Wff.

Let Π be a regular maximal KR4-theory.

• Let Σ ≠ Wff and Δ ≠ Wff. Then (i) Π ⊢ Σ → Δ iff there exist A_{1}, ⋯, A_{m} ∈ Σ(m > 0) and B_{1}, ⋯, B_{n} ∈ Δ(n > 0) such that □(A_{1} ∧ ⋯ ∧ A_{m} → B_{1} ∨ ⋯ ∨ B_{n}) ∈ Π, and (ii) (Σ, Δ) is a Π-pair iff (a) Π ⊬ Σ → Δ and (b) Σ ∪ Δ = Wff.

• Σ is a Π-theory iff (a) if A, B ∈ Σ then A ∧ B ∈ Σ and (b) if □(A → B) ∈ Π and A ∈ Σ, then B ∈ Σ.

• A Π-theory Σ is maximal, iff either A ∈ Σ or ¬A ∈ Σ and both do not hold for all A ∈ Wff.

• Let Σ, Γ, Δ be Π-theories. Then (i) RΣΓΔ iff if A → B ∈ Σ and A ∈ Γ then B ∈ Δ, and (ii) SΣΓ iff if □A ∈ Σ then A ∈ Γ.

To show the completeness, we see the reduced case in [8], though there are slight differences in some terminologies and we must replace the part of ‘prime’ by ‘maximal’. Here we pick up the following lemma which does not appear in [8].

Lemma 5 If Σ is a maximal Π-theory such that □C ∉ Σ, then there exist maximal Π-theory Γ′ such that SΣΓ′ and C ∉ Γ′.

Then it is established that there exists a regular maximal KR4-theory Π such that A ∉ Π whenever KR4 ⊬ A. Using this Π, we construct a canonical model ⟨0′, W′_{r}, R′_{r}, S′_{r}, v′_{r}⟩ as follows: (1’) 0′ = Π; (2’) W′_{r} is the set of all maximal Π-theories; (3’) R′_{r} is a ternary relation R restricted on W′_{r}; (4’) S′_{r} is a binary relation S restricted on W′_{r}; (5’) v′_{r} is defined by v′_{r}(p, Σ) = t iff p ∈ Σ, for all p ∈ Prop and Σ ∈ W′_{r},

Theorem 6 (Completeness) If A is KR4-valid, then A is a theorem of KR4.

3 Unreduced Models and Reduced Models

In this section we consider the relationship between unreduced models, dealt with sections 1, and reduced models, dealt with section 2. Generally, unreduced models can be applied wider than reduced models. We shall see that unreduced models can be translated into reduced models in special case.

The following fact holds:

Lemma 7 For any A ∈ Wff, KRN.T4 ⊢ A iff KR4 ⊢ A.

Hence KR4 can be regarded the same system as KRN.T4, so KR4 is a normal logic. So a KR4frame can be said a (reduced) KRN.T4-frame.

As in [5], there is a way to construct an unreduced frame from a reduced frame in the argument of the soundness of R4. However, this method cannot be applied to the argument of the completeness. So we consider the generalized method to obtain an unreduced model from a reduced model.

In this paper, there is a reduced model only for KR4. We shall consider constructing an unreduced KR4-model from a reduced KR4-model. Note that an unreduced KR4-model can be identified an unreduced KRN.T4-model by Lemma 7.

There is most difference between the postulates (p1) and (p5) in an unreduced KRN.T4-frame and the postulates (p’1) in a reduced KR4-frame. Though (p3) and (p’3) are different, they can be identified because the postulate Rabc ⟹ Rbac can be derived in a KR4-frame. To construct an unreduced KRN.T4-model ⟨O, W, R, S, v⟩ from a reduced KR4-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩, we define a translation σ from a reduced KR4-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ into an unreduced KRN.T4-model ⟨O, W, R, S, v⟩ as follows, for a, b, c ∈ W_{r}:

• W = {σ(x) | x ∈ W_{r}} • O = {σ(x) | S_{r}0x} • Rσ(a)σ(b)σ(c) iff R_{r}abc

• Sσ(a)σ(b) iff S_{r}ab

• v(p, σ(a)) = v_{r}(p, a), for all p ∈ Prop.

Lemma 8 ⟨O, W, R, S, v⟩ defined above is an unreduced KRN.T4-frame.

For the converse, there are some restrictions to make a reduced model. We can use a reduced model only if the system of the normal logic can be derived the following formula:

(A18) □A → A  and  (A19) □A → □□A.

L_{T4} denotes the system of normal logics in which (A18) and (A19) can be derived. For example, we can take KRN.T4 and KRN.T5 as L_{T4}.

Using L_{T4}, we can say as follows: for any L_{T4}, there is a reduced model for L_{T4}.

In order to construct a reduced L_{T4}-model from an unreduced L_{T4}-model, we introduce the translation τ from an unreduced L_{T4}-model ⟨O, W, R, S, v⟩ into a reduced L_{T4}-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ as follows, for a, b, c ∈ W:

• W_{r} = {τ(x) | x ∈ W } • for all x ∈ O, τ(x) = 0 • R_{r}τ(a)τ(b)τ(c) iff Rabc

• S_{r}τ(a)τ(b) iff Sab
• v_{r}(p, τ(a)) = v(p, a), for all p ∈ Prop.

Lemma 9 ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ defined above is L_{T4}-model.

Note that L_{T4} has (Necessitation) as the rule of inference. From Lemma 7 and Lemma 9, we show the method constructing a reduced L_{T4}-model from an unreduced L_{T4}-model as follows:

1. Eliminate (Necessitation) from L_{T4} and add the following axiom to axioms of L_{T4}:

if A is an axiom, then so is □A.

2. Construct a reduced L_{T4}-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ from an unreduced L_{T4}-model ⟨O, W, R, S, v⟩ by using the translation τ defined above.

When we enjoy the completeness by using a reduced L_{T4}-model, we should argue the same way as in section 2.

The argument in this section can be applied to normal logics over R. Therefore this fact give us the information about the relationship between an unreduced model, investigated in [4], and a reduced model, investigated in [7].

References

[1] A.R.Anderson and N.D.Belnap Jr., Entailment: The Logic of Relevance and Necessity, Vol.I, Princeton University Press, 1975.

[2] A.R.Anderson, N.D.Belnap Jr. and J.M.Dunn, Entailment: The Logic of Relevance and Necessity, Vol.II, Princeton University Press, 1992.

[3] B.F.Chellas, Modal Logic: an Introduction, Cambridge University Press, 1980.

[4] A.Fuhrmann, ‘Models for relevant modal logics’, Studia Logica 49, 1990, pp.501-514.

[5] E.D.Mares and R.K.Meyer, ‘The semantics of R4’, Journal of Philosophical Logic 22, 1993, pp.95-110.

[6] R.K.Meyer and R.Routley, ‘Classical relevant logics I’, Studia Logica 32, 1973, pp.51-68.

[7] R.Routley and R.K.Meyer, ‘The semantics of entailment II’, Journal of Philosophical Logic 1, 1972, pp.53-73.

[8] R.Routley, V.Plumwood, R.K.Meyer and R.T.Brady, Relevant Logics and Their Rivals I, Ridgeview Publishing Company, Atascadero, 1982.

Subframe formulas for S4-type intuitionistic modal logic

Kazuyo Inoi

                    inoi@maphy.jcn.nihon-u.ac.jp

Junior College, Nihon University

The subframe formulas Y for S4-type intuitionistic modal logic L_{0} is introduced. It is shown that the logic L_{0} + Y + bw_{n} has the finite model property.

1 Intuitionistic modal logics

In this section, we repeat some definitions and notations in [3].

Formulas are constructed using by propositional variables, p_{0}, p_{1}, ⋯, logical symbols, ∧, ∨, ⊃, ¬, □, ⊤ and ⊥ (not included ◇).

The logic L_{0} is the logics obtained from H by adding the following axioms,

• □p ⊃ p,

• □p ⊃ □□p,

• □(p ⊃ q) ⊃ (□p ⊃ □q),

and closed under the rules of substitution, necessitation and modus ponens.

The intuitionistic modal logics are extension of L_{0} and closed the above rules. A triple (N, ≤, R) is called an I-frame if the following conditions are satisfied.

• N is a non-empty set.

• ≤ is a partial order on N.

• R is a reflexive and transitive relation on N such that x ≤ y implies xRy for each x, y ∈ N.

Let M be an I-frame (M, ≤, R). M is said to be rooted if it has a least element with respect to R, that is, there is an element 0 ∈ M such that 0Ra and a ≰ 0 for any other element a ∈ M. This element 0 is said to be a root. If M is an I-frame, then we let

IS_{≤}(a) = {b : a ≤ b}
IS_{R}(a) = {b : aRb}

aR^{∼}b denotes aRb and bRa. w is said to be maximal with respect to A if

A ≡ B ⊃ C, w |̸= A ⇒ ∀v(w ≤ v and v ⊧ A),  (1)
A ≡ ¬B, w |̸= A ⇒ ∀v(w ≤ v and v ⊧ A),  (2)
A ≡ □B, w |̸= A ⇒ ∀v(w\overrightarrow{R}v and v ⊧ A).  (3)

A pair (M, ⊧) is said to be an I-model if, for all a ∈ M, any propositional variable p and any formulas A, B,

1. a ⊧ p and a ≤ b ⇒ b ⊧ p,

2. a ⊧ A ∧ B ⇔ a ⊧ A and a ⊧ B, 3. a ⊧ A ∨ B ⇔ a ⊧ A or a ⊧ B,

4. a ⊧ A ⊃ B ⇔ ∀b(a ≤ b)b |̸= A or b ⊧ B,

5. a ⊧ ¬A ⇔ ∀b(a ≤ b implies b |̸= A),

6. a ⊧ □A ⇔ ∀b(aRb implies b ⊧ A).

2 Preliminaries

In this section, we show some property of I-models. We can easily verify the next propositions. Proposition 2.1 L_{0} ⊢ □¬(□p ∨ □¬□p) ⊃ ⊥

L_{0} ⊢ ¬(¬p ∨ p) ⊃ ⊥

Let L ⊇ L_{0}, ML be a canonical model for L and u ∈ ML. Proposition 2.2 u is an element in maximal cluster iff □A ∨ □¬□A ∈ u for every wff A. Proposition 2.3 u is maximal with respect to ≤ iff ¬A ∨ A for every wff A. Proposition 2.4 For all u ∈ ML , there exists a maximal element with respect to ≤. Proposition 2.5 For all u ∈ ML, there exists a maximal element with respect to R.

Let bw_{n} be the following formula:

bw_{n} = ⋁_{i=0}^{n} □(□p_{i} → ⋁_{i≠j} □p_{j})(n ≥ 1).

Lemma 2.6 M validates bw_{n} iff each point in M has at most n R-incomparable successors.

For a formula A, we define the relation ∼_{F (A)} to get results on model equivalence with respect to A between two models. Let M and N are I-frames. We define ∼_{F (p)}, ≤_{F (p)}, ≡_{F (A)} and ∼_{F (A)} as follows:

(M, a) ∼_{F (p)} (N, v) ⇔ ∀p(a ⊧ p ⇔ w ⊧′ p)
(M, a) ≤_{F (A⊃B)} (N, v) ⇔ ∀b ∈ M, ∃v ∈ N(a ≤ b → u ≤′ v) and
(M, b) ∼_{F (A)} (N, v) and
(M, b) ∼_{F (B)} (N, v))
(M, a) ≤_{F (¬A)} (N, v) ⇔ ∀b ∈ M, ∃v ∈ N(a ≤ b → u ≤′ v) and
(M, b) ∼_{F (A)} (N, v)
(M, a) ≤_{F (□A)} (N, v) ⇔ ∀b ∈ M, ∃v ∈ N(aRb → uR′v), and
(M, b) ∼_{F (A)} (N, v)
(M, a) ≡_{F (A)} (N, v) ⇔ (M, a) ≤_{F (A)} (N, v) and
(N, v) ≤_{F (A)} (M, a)
(M, a) ∼_{F (A)} (N, v) ⇔ (M, a) ∼_{F (p)} (N, v) and
(M, a) ≡_{F (A)} (N, v)

For (M, w) ∼_{F (A)} (M, v), we write w ∼_{F (A)} v if M is understood. |w|_{F (A)} denotes the set {v ∈ M : w ∼_{F (A)} v}. Lemma 2.7 Let M and N be I-frames. For any formula A and a ∈ M, v ∈ N,

(M, a) ∼_{F (A)} (N, v) ⇒ (v ⊧ A → a ⊧ A)

Proof. By the induction on the construction of A

Lemma 2.8 Suppose A ⊃ B ∉ w (respectively, ¬A ∉ w) for w ∈ M_{L}, w is not maximal element with respect to A ⊃ B (respectively, ¬A). Then there exists v(v ∈ M_{L}, w ≤ v) which v is maximal with respect to A ⊃ B (respectively, ¬A).

Lemma 2.9 Suppose □A ∈ w, for w ∈ M_{L}, w is not maximal element with respect to □A. Then there exists v(v ∈ M_{L}, wRv) which v is maximal with respect to □A.

Definition 2.10 (p-morphism,subreduction) Let M and N be I-frames. A map f from N = (N, ≤_{N} , R_{N}) to M = (M, ≤_{M}, R_{M}) is called a p-morphism if the following conditions are satisfied, for any u, v ∈ N and a ∈ M,

(p-1) f is onto,

(p-2) If u ≤_{N} v then f(u) ≤_{M} f(v),

(p-3) If uR_{N}v then f(u)R_{M}f(v),

(p-4) If f(u) ≤_{M} a then there exists v such that u ≤_{N} v and f(v) = a,

(p-5) If f(u)R_{M}a then there exists v such that uR_{N}v and f(v) = a.

A map f from N to M is called a subreduction if f is a p-morphism from a subframe of N to M. And then, N is subreducible to M.

3 subframe formulas

In this section, we introduce subframe formulas for L_{0} by the method as Shimura defined for the intuitionistic logic in [4]. Fine showed the completeness of subframe logics Y (M, 0) for K4 [2]. It was shown by selecting finite points from canonical models. We show the completeness some logics containing L_{0} by the same method as Fine.

For a rooted and finite I-frame, we define the subframe formulas by the induction on the cardinality of a ↑_{≤}, a ↑_{R} as follows:

X_{≤}(M, a) = ⋁_{b≰a} p_{b} ∨ ⋁_{aR̸^{∼}d^{d∈IS_{≤}(a)}} Y (M, d) ∨ ⋁_{aR^{∼}e^{a∈IS_{≤}(e)}} X(M, e),

X_{R}(M, a) = ⋁_{cR̸a} □q_{c} ∨ ⋁_{e∈IS_{R}(a)} □Y (M, e),
X(M, a) = p_{a} ∧ □q_{a} ⊃ p ∨ X_{≤}(M, a) ∨ X_{R}(M, a),
Y_{R}(M, a) = ⋀_{a′∈Cl(a)}( ⋀_{a′′R^{∼}a′} □(□X(M, a′′) ⊃ X(M, a′))),
Y (M, a) = Y_{R}(M, a) ⊃ X(M, a).

Proposition 3.1 Let M be a finite and rooted I-frame and a, b ∈ M. Then,

1. if b ≤ a does not hold, L_{0} ⊢ p_{b} ⊃ Y (M, a),

2. if bRa does not hold, L_{0} ⊢ □q_{b} ⊃ Y (M, a),

3. if a ≤ b hold, Y (M, b) ⊃ Y (M, a),

4. if a ≤ b hold, Y (M, b) ⊃ Y (M, a),

5. if aRb hold, □Y (M, b) ⊃ Y (M, a).

Lemma 3.2 Let (N, ⊧) be an I-frame, u ∈ N and M be a finite and rooted I-frame. If u |̸= Y (M, a) then there exists v ∈ N such that

u ≤ v, v ⊧ p_{a} ∧ □q_{a} and v |̸= Y (M, a).

Lemma 3.3 Suppose there is a subreduction f from N to M, formula E and formulas sets {F_{a}; a ∈ M} and {□G_{a}; a ∈ M} such that

∃v(a ≰ f(v), u ≤ v) → u |̸= F_{a}
∃v(a R̸f(v), uRv) → u |̸= □G_{a}
∃v(uRv, v ∈ dom(f)) → u |̸= E

Then the formula obtained from Y (M) by substituting F_{a} (respectively, G_{a}) for p_{a} (respectively, q_{a}) for every a ∈ M and E for p is refuted on N.

Theorem 3.4 Let M be a finite and rooted I-frame. Then the following are equivalent, for any I-frame N,

• N |̸= Y (M),

• there is a subreduction f from N to M.

Proof. (⇒) Assume N |̸= Y (M). Define a partial map f from N to M

f(u) = \{ \begin{matrix}a & (u ⊧ p_{a} ∧ □q_{a} and u |̸= Y (M, a)), \\ undefined & (otherwise). \end{matrix}

Then, f is a subreduction from N to M. (⇐) For u ∈ N, define a valuation ⊧ on N as follows:

∃v(a ≰ f(v), u ≤ v) → u |̸= p_{a}
∃v(a R̸f(v), uRv) → u |̸= □q_{a}
∃v(uRv, v ∈ dom(f)) → u |̸= p

Lemma 3.5 Let L_{0} + {Y (M_{i})}_{i∈I} + bw_{n}. There no finite subframe of NL is reducible to M_{i}.

Lemma 3.6 Suppose that w ∈ ML, w |̸= A. Then there is a finite submodel N = (N, ≤′, R′, ⊧′) of w ↑_{R} and v |̸= A for v ∈ N.

Proof. By the induction on the construction A.

(i) If A is a propositional variable, let N = {w} and w = v. (ii) Otherwise. By Proposition 2.4 Proposition 2.5, there exists a point w′ such that w′ |̸= □A and w′ is maximal with respect to R. We define N by the induction on the cardinality of \{|v|_{F (A)} : w′ ≤ v\} and \{|v|_{F (A)} : w′\overrightarrow{R}v\}. Let N′ = {w′}. Suppose U = {u : w′ ∼ u}, X = {|u|_{F (A)} : u ∈ U}. Pick representatives x_{1}, x_{2}, ⋯, x_{n} from X such that each x_{i}(i = 1 ⋯ n) is maximal with respect to ≤. Let rank_{x_{i}} = |{|u|_{F (A)} : x_{i} ≤ u and u ∈ U}|. If rank_{x_{i}} = 1 then U_{x_{i}} = {x_{i}}. Otherwise, let Y = {|x_{ij}|_{F (A)} : x_{i} ≤ x_{ij} and x_{ij} ∈ U}. Pick representatives y_{1}, y_{2}, ⋯, y_{l} from Y such that each y_{i}(i = 1 ⋯ l) is maximal with respect to ≤. Let U_{x_{i}} = U_{y_{1}} ∪ U_{y_{2}} ∪ ⋯ ∪ U_{y_{l}} and U = ⋃_{i=1}^{n} U_{x_{i}}. Next for each w_{i} ∈ U, let S = \{|s|_{F (A)} : w_{i} ≤ s and w_{i}\overrightarrow{R}s\}, and S′ = \{|s′|_{F (A)}\S : w_{i}\overrightarrow{R}s′\}. If S = {|w_{i}|_{F (A)}} or S = ∅ then let T_{w_{i}}^{≤} = ∅. Otherwise, pick representatives s_{1}, s_{2}, ⋯, s_{m} from S such that each s_{i}(i = 1 ⋯ m) is maximal with respect to ≤. And Let T_{w_{i}}^{≤} = N_{s_{1}} ∪ N_{s_{2}} ∪ ⋯ ∪ N_{s_{m}}. If S′ = {|w_{i}|_{F (A)}} or S′ = ∅ then let T_{w_{i}}^{R} = ∅. Otherwise, pick representatives s′_{1}, s′_{2}, ⋯, s′_{n} from S′ such that each s_{i}(i = 1 ⋯ n) is maximal with respect to R. And Let T_{w_{i}}^{R} = N_{s′_{1}} ∪ N_{s′_{2}} ∪ ⋯ ∪ N_{s′_{n}}. Set T_{w_{i}} = T_{w_{i}}^{≤} ∪ T_{w_{i}}^{R} and T = T_{w_{1}} ∪ T_{w_{2}} ⋯ T_{w_{p}}.

Let N = N′ ∪ U ∪ T.

Theorem 3.7 L_{0} + {Y (M_{i})}_{i∈I} + bw_{n} has finite model property. Corollary 3.8 L_{0} + {Y (M_{i})}_{i∈I} + bw_{n} is complete.

References

[1] K. FINE, Logics containing K4 part I, Journal of Symbolic Logic 39(1974), pp.31-42.

[2] K. FINE, Logics containing K4 part II, Journal of Symbolic Logic 50(1985), pp.619-651.

[3] H. ONO, On some intuitionistic modal logics, Publ. RIMS, Kyoto Univ.13(1977), pp.687-722.

[4] T. SHIMURA, Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas, Studia Logica 52(1993), pp.23-40.

[5] M. ZAKHARYASCHEV, Canonical formulas for K4 part I: basic results, Journal of Symbolic Logic 57(1992), pp.1377-1402.

Residuation Theory and Substructural Logics

Hiroakira Ono

                             ono@jaist.ac.jp

School of Information Science, JAIST

1 Introduction

For these years, the author has been working at an algebraic study of substructural logics, in particular of logics over FL_{ew} ( see e.g. [6] ). Here, by FL_{ew} we mean the logic obtained from the intuitionistic logic by deleting the contraction rule, if it is formulated as a sequent system. The corresponding algebraic structures are residuated lattices. An important aspect of algebraic study of these logics will come from the fact that algebraic methods enable us to discuss various logics and related algebraic structures within a uniform framework. For instance, by discussing algebraic structures for Łukasiewicz’s many-valued logics and also for fuzzy logics together with hoops and pocrims from universal algebra, it becomes possible to see strong interrelations behind them.

In this paper, we will show the importance of the notion of residuation in the study of substructural logics, and thus residuated structures based on residuation theory offer us algebraic structures which are suitable for substructural logics.

A part of the content of the present paper was presented also at University of Torino, September, 2000. After this, T. Kowalski informed me of the Ph.D thesis [3] by K. Blount and of a book on residuation theory [4] by T.S. Blyth and M.F. Janowitz. Then the author has realized that roles played by the residuation in substructural logics can be stated more explicitly by the help of residuation theory.

2 Residuated maps

In this section, we will give a brief survey of basic facts in residuation theory. For more information, see e.g. [4]. See also [3].

Let P and Q be posets. A map f: P → Q is residuated if there exists a map f^{∗}: Q → P such that the following holds for any p ∈ P and any q ∈ Q:

f(p) ≤ q ⟺ p ≤ f^{∗}(q).

In the above case, we say that f and f^{∗} form a residuated pair, ( or, an adjunction in category theory ) and that f^{∗} is a residual of f. We can show the following results.

Lemma 2.1 If f and f^{∗} form a residuated pair, both f and f^{∗} are monotone increasing.

Lemma 2.2 Maps f: P → Q and f^{∗}: Q → P form a residuated pair if and only if both id_{P} ≤ f^{∗} ∘ f and f ∘ f^{∗} ≤ id_{Q} hold.

Lemma 2.3 If a map f is residuated then its residual is determined uniquely by f.

Hereafter, f^{∗} denotes the residual of a map f when f is residuated. Similarly to Lemma 2.3, we can show that f is determined uniquely by f^{∗} when f and f^{∗} form a residuated pair. In fact, the following holds;

1. f^{∗}(q) = max{p ∈ P; f(p) ≤ q},

2. f(p) = min{q ∈ Q; p ≤ f^{∗}(q)}.

Proposition 2.4 Suppose that f and f^{∗} form a residuated pair between P and Q, and that X ⊆ P and Y ⊆ Q. If sup X exists then sup f(X) ( = sup{f(p); p ∈ X} ) exists and f(sup X) = sup f(X). Also if inf Y exists then inf f^{∗}(Y) exists and f^{∗}(inf Y) = inf f^{∗}(Y).

When both P and Q are lattices in the above proposition, we have the following.

Corollary 2.5 Suppose that f and f^{∗} form a residuated pair between lattices L and M. Then f(a∪b) = f(a) ∪ f(b) for all a, b ∈ L, and f^{∗}(c ∩ d) = f^{∗}(c) ∩ f^{∗}(d) for all c, d ∈ M.

If both L and M are moreover complete, we have the converse of Proposition 2.4.

Proposition 2.6 Suppose that both L and M are complete lattices and that f is a map from L to M. Then, f is residuated if and only if f preserves all ( possibly infinite ) joins. Dually, a map f^{∗} : M → L is the residual of a map f : L → M if and only if f^{∗} preserves all ( possibly infinite ) meets.

3 Residuated structures

Now we will apply results in the previous section to the case where posets are ordered groupoids. Then, we will discuss particular classes of ordered groupiods which originate from algebras for substructural logics.

A structure G = ⟨G, ·, ≤⟩ is an ordered groupoid if · is a binary operation on a poset ⟨G, ≤⟩ which satisfies the following monotonicity ( see [4] ) :

x ≤ x′ and y ≤ y′ imply x · y ≤ x′ · y′

Only for the simplicity’s sake, we assume moreover the commutativity of · in the rest of this section. For each x ∈ G, define a map f_{x} : G → G by f_{x}(y) = x · y. When f_{x} is residuated for any x ∈ G, we say that the ordered commutative groupoid G is residuated. The residual f^{∗}_{x} of f_{x} is expressed as f^{∗}_{x}(y) = x → y. ( One may call such an operation ·, a fusion, and →, an implication. ) Then, the following must hold:

f_{x}(y) ≤ z ⟺ y ≤ f^{∗}_{x}(z),
i.e. x · y ≤ z ⟺ y ≤ x → z

which is called the law of residuation.

When G has also a lattice structure, we have the following equations by Corollary 2.5: For all a, b, c ∈ G

1. (a ∪ b) · c = (a · c) ∪ (b · c),

2. a → (b ∩ c) = (a → b) ∩ (a → c).

In particular, suppose that G is a Heyting algebra. In this case, ∩ and → form a residuation pair. Thus, the above 1 becomes the distributive law. This gives the well-known fact that any Heyting algebra is distributive. Similarly, when G is a complete lattice, by using Proposition 2.6 we have the following.

1. (⋃_{i} a_{i}) · c = ⋃_{i}(a_{i} · c),

2. a → (⋂_{i} c_{i}) = ⋂_{i}(a → c_{i}).

There are many residuated structures related to logic and universal algebra. We have already mentioned Heyting algebras in the above. A pocrim is a ( partially ) ordered commutative residuated groupoid which is also an integral monoid, i.e. a monoid whose unit is the greatest element. If a pocrim has moreover a lattice structure, it is called a residuated lattice. Pocrims and residuated lattices are algebraic structures for ( the implication-fusion fragment ) of logics without contraction rule ( more precisely, logics over FL_{ew} ). See e.g. [2, 6] for the details. Note here that in the definition of “residuated lattices” in [3] neither the commutativity nor the integrality are assumed and therefore they are related to extensions of Lambek calculus.

In the folllowing, we will take two more examples of residuated structures from logic.

1. Commutative quantales A structure A = ⟨A, ∩, ∪, ·⟩ is a commutative quantale if

1. ⟨A, ∩, ∪⟩ is a complete lattice ( and hence is bounded ),

2. ⟨A, ·⟩ is a commutative semigroup,

3. (⋃_{i} x_{i}) · y = ⋃_{i}(x_{i} · y) for x_{i}, y ∈ A.

By Proposition 2.6, A is residuated. If ⟨A, ·⟩ has moreover the unit element, A becomes an intuitionistic phase structure. See [5].

2. Triangular norms in fuzzy logic A triangular norm ( or, simply, a t-norm ) T is a map from [0, 1]^{2} to [0, 1] which satisfies the following conditions:

1. T (x, T (y, z)) = T (T (x, y), z),

2. T (x, y) = T (y, x),

3. T (x, 1) = x,

4. x ≤ y implies T (x, z) ≤ T (y, z).

Define ∗ by x ∗ y = T (x, y). The above conditions mean that ⟨[0, 1], ∗, 1⟩ is a partially-ordered commutative integral monoid. It is obvious that ⟨[0, 1], min, max, 0, 1⟩ forms a complete lattice. Typical examples of t-norms are min{x, y} ( Heyting ), x × y ( product ) and max{x + y − 1, 0} ( Łukasiewicz ).

Now, a question is when the above structure becomes residuated. By Proposition 2.6, it is residuated if and only if

T (⋃_{i} x_{i}, y) = ⋃_{i} T (x_{i}, y).

This condition is equivalent to the following. For x, y

T (x, y) = lim_{z→x−0} T (z, y),

i.e. T is left-continuous. Note that any of t-norms given above is left-continuous.

Thus, we can say that every left-continuous t-norm determines a residuated lattice and therefore determines a substructural logic over FL_{ew}.

4 Concluding remark: why and how far the framework of substructural logics works well

Ten years have passed after a study of nonclassical logics under the name “substructural logics” started. The study seems to be quite promising, as so many different kinds of nonclassical logics introduced so far can be discussed within this framework. On the other hand, it seems to be not clear yet why it works so well, or more precisely why restrictions on “structural rules” play key roles in it. Here we will give an explanation of it by using the notion of residuation.

One will agree that the “implication” is the most important logical connective. At the same time, it is not so easy to analyze its functions and meanings from both mathematical and philosophical points of view. Suppose here that our implication satisfies the following relation in a sequent system of a given logic L under consideration:

⊢ Γ, A ⟹ B if and only if ⊢ Γ ⟹ A → B,

where ⊢ means the provability in the logic L. The above relation holds when we have both introduction rule and elimination rule for →. Now, we introduce a new logical connective ∗, called fusion, to represent commas ( in the left-hand side ) of sequents. Then, the above relation means that implication is the residual of fusion. From the mathematical point of view, fusion may be much more manageable than implication. In such a case, we can shift our attention from implication to fusion, since residuation theory tells us that each fusion determines uniquely an implication and vice versa.

It is easy to see that some of basic properties of fusions ( as groupoid operations ) can be expressed by structural rules. For example, the commutativity of fusions is expressed by exchange rules. This might be the main but hidden reason why the study of substructural logics has begun with restrictions on structural rules.

So our conclusion is that the essense of substructural logics comes from residuation between fusion and implication, rather than from their structural rules.

Of course, the above explanation may oversimplifies the problem. For example, it is not clear for a given implicational logic whether or not it is possible to introduce fusion as a new connective, whose residual is exactly a given implication. As an example, consider the logic BCK. In this case, an appropriate fusion can be introduced. In fact, this is proved either by using the cut elimination theorem of a sequent system of BCK with the fusion, or by showing the embedding theorem of BCK-algebras into BCK-algebras with the fusion ( see e.g. [2, 7] for the latter ). In order to apply residuation theory, we need to make sure of the existence of such a fusion. But, we cannot assume this always. For instance, in [1] authors introduce the “basic logic” B and consider its extensions without the deductive face, i.e. logics in which the law of residuation does not hold. In algebraic terms, each algebraic structure for B is a ( partially ) ordered commutative monoid but without assuming the law of residuation. It might be necessary here to consider once again what is a proper definition of substructural logics.

References

[1] Battilotti, G. and G. Sambin, Basic logic and the cube of its extensions, draft, 1995.

[2] Blok, W.J. and J.G. Raftery, On the quasivariety of BCK-algebras and its subvarieties, Algebra Univerisalis 33, (1995) pp.68-90.

[3] Blount, K., On the structure of residuated lattice, Ph. D. thesis, Vanderbilt University, 1999.

[4] Blyth, T.S. and M.F. Janowitz, Residuation Theory, Pergamon Press, 1972.

[5] Ono, H., Semantics for substructural logics, Substructural Logics, eds. by K. Došen and P. Schroeder-Heister, Studies in Logic and Computation 2, Oxford University Press 1993, pp.259-291.

[6] Ono, H., Logics without contraction rule and residuated lattices I, to appear.

[7] Ono, H. and Y. Komori, Logics without the contraction rule, Journal of Symbolic Logic 50 (1985) pp.169-201.

Alternatives to the relevant logic R

Ryo Kashima

                         kashima@is.titech.ac.jp

Department of Mathematical and Computing Sciences Tokyo Institute of Technology

We study two relevant logics^{∪}R_{+} and RNND, which are proper extensions of the well-known relevant logic R. The logic ^{∪}R_{+} (“semilattice relevant logic”) has connectives → (implication), ∧ (conjunction), and ∨ (disjunction), and is characterized by semilattice models in which ∧ and ∨ are interpreted in a natural way. The logic RNND (“Relevant Normal Natural Deduction”) has connectives →, ∧, ∨, and ¬ (negation), and is formulated by a natural deduction system which is quite simple and easy to understand as compared with the usual natural deduction system of R. We try to show some nice properties of ^{∪}R_{+} and RNND — decidability, variable sharing, etc.

1 Semilattice Relevant Logic

In this note, the formulas of the relevant logic R are constructed by {→, ∧, ∨, ¬}. If c is a list of connectives in {→, ∧, ∨, ¬}, then F_{c} will denote the set of formulas whose connectives are in c, and R_{c} will denote the c-fragment of R.

A semilattice model is a 4-tuple ⟨I, ·, e, ⊧⟩ that satisfies the following.

• ⟨I, ·, e⟩ is an idempotent commutative monoid (a semilattice with identity e). That is,

I is a non-empty set, · is a binary operator on I, e ∈ I. (α·β)·γ = α·(β·γ), α·β = β·α, α·α = α, α·e = α.

• ⊧ is a relation on I × F_{→∧∨} such that

α ⊧ A→B ⟺ ∀β ∈ I[(β ⊧ A) ⇒ (α·β ⊧ B)], α ⊧ A∧B ⟺ [(α ⊧ A) and (α ⊧ B)], α ⊧ A∨B ⟺ [(α ⊧ A) or (α ⊧ B)].

We say that a formula A is valid in this model if e ⊧ A. (The structure ⟨I, ·, e⟩ is considered to be a “structure of information”—I is a set of pieces of information, · is a binary operator which combines two pieces of information, and e is an empty piece of information; and the notion α ⊧ A is considered to be a fact “a formula A holds according to a piece α of information”.)

The “semilattice relevant logic” ^{∪}R_{+} is defined to be the set

{A ∈ F_{→∧∨} | A is valid in any semilattice model}.

Proposition 1.1 ([6]) ^{∪}R_{+} is a proper superset of the set of provable formulas in R_{→∧∨} while the →-fragment of ^{∪}R_{+} coincides with R_{→}. For example,

[(A→(B∨C))∧(B→D)]→(A→(D∨C)) ∈ ^{∪}R_{+}, ∉ R_{→∧∨}.

If α is a finite set of natural numbers and A is a formula, then the expression α:A is called a labelled formula (α is called a label). If Γ and Δ are finite multisets of labelled formulas, then the expression Γ ⇒ Δ is called a labelled sequent. A labelled sequent calculus L^{∪}R_{+} is defined as follows.

[Axioms]

Γ , α:A ⇒ α:A, Δ

[Inference rules]

\begin{matrix}Γ , α:A, α:A ⇒ Δ \\ Γ , α:A ⇒ Δ \end{matrix} (contraction left)  \begin{matrix}Γ ⇒ α:A, α:A, Δ \\ Γ ⇒ α:A, Δ \end{matrix} (contraction right)
\begin{matrix}Γ ⇒ β:A, Δ & Γ , α∪β:B ⇒ Δ \\ Γ , α:A→B ⇒ Δ \end{matrix} (→ left)
\begin{matrix}Γ , \{a\}:A ⇒ α∪\{a\}:B, Δ \\ Γ ⇒ α:A→B, Δ \end{matrix} (→ right) with a condition:

(Label Condition) The natural number a does not appear in the labels of the lower sequent.

\begin{matrix}Γ , α:A, α:B ⇒ Δ \\ Γ , α:A∧B ⇒ Δ \end{matrix} (∧ left)  \begin{matrix}Γ ⇒ α:A, Δ & Γ ⇒ α:B, Δ \\ Γ ⇒ α:A∧B, Δ \end{matrix} (∧ right)
\begin{matrix}Γ , α:A ⇒ Δ & Γ , α:B ⇒ Δ \\ Γ , α:A∨B ⇒ Δ \end{matrix} (∨ left)  \begin{matrix}Γ ⇒ α:A, α:B, Δ \\ Γ ⇒ α:A∨B, Δ \end{matrix} (∨ right)

Proposition 1.2 ([4](cf.[5])) A ∈ ^{∪}R_{+} if and only if L^{∪}R_{+} ⊢ ⇒ ∅:A.

The system L^{∪}R′_{+} is obtained from L^{∪}R_{+} by replacing “→ left” rule by

\begin{matrix}Γ ⇒ β:A & Γ , α∪β:B ⇒ Δ \\ Γ , α:A→B ⇒ Δ. \end{matrix} (→ left′)

We can (probably) prove: Theorem 1.3 L^{∪}R_{+} and L^{∪}R′_{+} are equivalent with respect to provable labelled sequents. By using this theorem, now I attack the following problems.

• Give a simple proof of the completeness of a Hilbert style axiomatization of ^{∪}R_{+}. (A Hilbert style axiomatization of ^{∪}R_{+} was given by Charlwood ([2]), but the proof is somewhat complicated, and I cannot follow the detail.)

• Decision problem of ^{∪}R_{+}. (I try to make a decision procedure for R_{→} using the →-fragment of L^{∪}R_{+}. This and the above Theorem 1.3 may offer a decision procedure for ^{∪}R_{+}.)

• Prove (or disprove) the variable sharing (and the interpolation) property for ^{∪}R_{+}. Remark

• A decision procedure for “contractionless ^{∪}R_{+}” was given by Giambrone and Kron ([3]).

• Giambrone and Urquhart ([4]) introduced a natural deduction system and “proved” that the system is equivalent to L^{∪}R_{+}. However, the proof seems to be wrong—(A∨B)_{a} ⊢ A_{a}, B_{a} is (probably) a counterexample to Fact 6 in [4].

2 Relevant Normal Natural Deduction

The natural deduction system of R_{→} is quite simple:

\begin{matrix}A→B & A \\ B \end{matrix} (→E)  [A] ; ⋮ . ; B ; A→B (→I) with a condition:

(Relevant Condition) We must cancel at least one occurrence of the assumption A.

But introducing other connectives makes the situation problematic. For example, an irrelevant formula B→(A→A) is provable by the proof

\begin{matrix}[A]^{1} & [B]^{2} \\ A∧B \end{matrix} ; A ; A→A ; 1 ; B→(A→A) 2

which satisfies the Relevant Condition. To avoid such a situation, Yoshiura and Yonezaki ([7]) introduced a natural deduction system in which only “normal proofs” are permitted. This is a nice idea, but Yoshiura and Yonezaki’s system is not elegant in the treatment of negation. Here we combine Yoshiura and Yonezaki’s idea with Andou’s “regular and normal proofs” ([1]), and we make an elegant natural deduction system of a relevant logic.

Remark

• The above proof of B→(A→A) is not normal, and the normal form of it violates the Relevant Condition.

• Usually natural deduction systems of R have a restriction on ∧I rule—two premises must have the same assumption set. This excludes the above proof of B→(A→A).

Andou’s regular NK for F_{→∧∨¬}

[A] ; ⋮ . ; B ; A→B (→I)  \begin{matrix}A→B & A \\ B \end{matrix} (→E)  \begin{matrix}A & B \\ A∧B \end{matrix} (∧I)  {A∧B \atop A} (∧E)  {A∧B \atop B} (∧E)

{A \atop A∨B} (∨I)  {B \atop A∨B} (∨I)  \begin{aligned}A∨B & [A] ; ⋮ . ; C & [B] ; ⋮ . ; C \\ & C \end{aligned} (∨E)  [A] ; ⋮ . ; ⊥ ; ¬A (¬I)  \begin{matrix}¬A & A \\ ⊥ \end{matrix} (¬E)

\begin{matrix}[¬A] & ⋮ . ; A \\ ⊥ \end{matrix} ; ⋮ . ; ⊥ ; A ; (⊥C)

The ⊥C rule means that an assumption which is cancelled by ⊥C must be the major premise of a ¬E.

Let ⟨X_{1}, ⋯, X_{n}⟩ be a path in a proof of regular NK (X_{1} is an assumption and X_{n} is the last formula), and ⟨Y_{1}, ⋯, Y_{m}⟩ be a subsequence of it (i.e., ⟨Y_{1}, ⋯, Y_{m}⟩ = ⟨X_{i_{1}}, ⋯, X_{i_{m}}⟩ where i_{1} < ⋯ < i_{m}). We say that the sequence ⟨Y_{1}, ⋯, Y_{m}⟩ is redundant if it satisfies the following conditions.

• Y_{1} is the conclusion of an “introduction rule” (→I, ∧I, ∨I, or ¬I).

• The position of Y_{k} and Y_{k+1} is one of the following.

\begin{aligned}⋮ . ; A∨B & [A] ; ⋮ . ; Y_{k} & [B] ; ⋮ . ; C \\ & Y_{k+1} \end{aligned} (∨E) ; ⋮ .  \begin{aligned}⋮ . ; A∨B & [A] ; ⋮ . ; C & [B] ; ⋮ . ; Y_{k} \\ & Y_{k+1} \end{aligned} (∨E) ; ⋮ .  \begin{matrix}[¬A] & ⋮ . ; Y_{k} \\ ⊥ \end{matrix} ; ⋮ . ; ⊥ ; Y_{k+1} ; (⊥C) ; ⋮ .

• Y_{m} is the major premise of an “elimination rule” (→E, ∧E, ∨E, or ¬E).

A proof is said to be normal if it contains no redundant sequence, and to be relevant if the Relevant Condition on cancelling assumptions holds (i.e., in the applications of the rules →I, ∨E, ¬I, and ⊥C, there must be an occurrence of each cancelled assumption indicated by [A], [B], and [¬A] in the above list of the rules).

The logic RNND (Relevant Normal Natural Deduction) is defined by relevant normal proofs; that is, a formula A is said to be a theorem of RNND if there is a regular NK proof of A which is relevant and normal.

Now I attack the problem to show the following nice properties of RNND. (For Yoshiura and Yonezaki’s system, these have been shown by [7], [8] and [9].)

• Variable sharing (and interpolation).

• Decidability.

• RNND is strictly stronger than R. (There are some “natural” formulas which are provable in RNND and not provable in R; e.g., A→(B→(A∧B)). On the other hand, I do not know whether the following holds: If R ⊢ A then RNND ⊢ A. This is a nontrivial problem because RNND is not closed under modus ponens.)

References

[1] Y. Andou, A normalization-procedure for the first order classical natural deduction with full logical symbols, Tsukuba Journal of Mathematics 19, 153-162, (1995).

[2] G. Charlwood, An axiomatic version of positive semilattice relevance logic, Journal of Symbolic Logic 46, 233-239, (1981).

[3] S. Giambrone and A. Kron, Four relevant Gentzen systems, Studia Logica 46, 54-71 (1987).

[4] S. Giambrone and A. Urquhart, Proof theories for semilattice logics, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33, 433-439 (1987).

[5] R. Kashima, Completeness of implicational relevant logics, Logic Journal of the Interest Group in Pure and Applied Logics 8, 761-785 (2000).

[6] A. Urquhart, Semantics for relevant logics, Journal of Symbolic Logic 37, 159-169, (1972).

[7] N. Yoshiura and N. Yonezaki, Relevant logic ER with extended provability (in Japanese), Journal of Japanese Society for Artificial Intelligence 13, 981-989, (1998). (吉浦紀晃, 米崎直樹: 証明力を拡張した適切さの論理 ER，人工知能学会誌)

[8] N. Yoshiura and N. Yonezaki, Decidability of relevant logic ER (in Japanese), Journal of Japanese Society for Artificial Intelligence 14, 819-827, (1999). (吉浦紀晃, 米崎直樹: 適切さの論理 ER の決定可能性，人工知能学会誌)

[9] N. Yoshiura and N. Yonezaki, Comparison of relevant logic R and ER (in Japanese), Journal of Japanese Society for Artificial Intelligence 14, 1088-1099, (1999). (吉浦紀晃, 米崎直樹: 適切さの論理 R と ER の証明力の比較，人工知能学会誌)

A Kripke Type Semantics for Substructural Logics with Strong Negation (Abstract)

Norihiro Kamide

                        kamide@wakayama-nct.ac.jp

(Wakayama National College of Technology, Noshima 77, Nada, Gobo, Wakayama 644-0023, JAPAN)

Abstract

We introduce a Kripke type semantics for propositional substructural logics with strong negation, and show completeness theorems for these logics by using extended Ishihara’s canonocal model construction method. The present paper’s framework can deal with broard range of substructural logics with strong negation including Nelson’s logic N^{−}, Wansing’s logic COSPL (and its extensions), extended Visser’s basic propositional logic with strong negation and extended positive relevant logics with strong negation.

1 Introduction

First, we will present a short servey of Kripke type semantics for substructural logics and logics with strong negation. Second, we will show the organization of this paper.

Examples of substructural logics discussed in this paper are as follows: positive relevant logics in philosophical motivation, intuitionistic linear logic in computer science and BCK-logic closely related to BCK-algebras. A historical servey of Kripke type semantics for these logics is as follows. In 1972, Routley and Meyer introduced a Kripke type semantics for positive relevant logics, which semantics was characterized with three-termed accessibility relation. (See [2]). In 1985, Ono and Komori gave us a Kripke type semantics for FL-family including BCK-logic, intuitionistic linear logic and full Lambek logic FL, which semantics was characterized with semilattice-orderd monoid. (see [10]). In 1988, Došen introduced a Kripke type semantics, named groupoid semantics, for broard range of substructural logics including the logics mentioned above (see [4][5]). Došen’s semantics is essentially the same as Ono and Komori’s one, but the semantics was independently proposed. In 2000, Ishihara introduced a canonical model construction method for the semantics of Ono and Komori (see [6]). This method can deal with broard range of substructural logics including some Došen’s logics, Corsi’s logic F and the standard substructural logics mentioned above. A class of the logics characterized by this method is called, by Ishihara, normal substructural logic.

Next we explain a servey of logics with strong negation (or constructive negation) and their Kripke type semantics. The strong negation was first proposed by Nelson (1949) and Markov (1950) independently. The negation was introduced to express ”constructive falsity” in recursive realizability (see [8]). Nelson’s logics such as N and N^{−} have been studied by many logicians (see, e.g., [1] [14]). These logics are, roughly speaking, slight extensions or modifications of the intuitionistic logic. Kripke type semantics for Nelson’s logics are different from that for the intuitionistic logic. These semantics have two kinds of valuation: ⊧^{+} (correspond to provability) and ⊧^{−} (correspond to refutability). In 1969, Thomason introduced a Kripke type semantics for a predicate logic with strong negation, which semantics was characterized with binary accessibility relation similar to the binary relation of Kripke type semantics for the predicate intuitionistic logic (see [12]). In 1993, Wansing proposed propositional substructural logics with strong negation such as COSPL-family including some Nelson’s logics (roughly speaking, COSPL-family is obtained from FLfamily by adding strong negation). Wansing gave us a Kripke type semantics and its informational interpretation for these logics (see [14]). Wansing’s semantics is a natural extention of Došen’s one.

In the present paper, we extend Ishihara’s result to substructural logics with strong negation. As a result, we can deal with broad range of logics with strong negation such as Nelson’s N^{−} and Wansing’s COSPL (and its extensions). Thus, the result is also an extension of Wansing’s one.

Next we present the orgnization of the paper.

In Section 2, we present Ishihara’s basic normal substructural logic L and its extensions, and introduce new normal substructural logics such as Visser’s basic propositional logic BPL in [13] (a Hilbert style system for BPL is proposed in [9] [11]), relevant logics RMO^{+}, EMO^{+}, Corsi’s logics FT, FR, FRT in [3] and Méndez’s logics T_{+}^{∘}, E_{+}^{∘}, R_{+}^{∘}, RMO_{+}^{∘}, EMO_{+}^{∘}, S4_{+}^{∘} in [7]. (We can prove the compleateness theorem for the new logics by using Ishihara’s canonical model construction method.) Next we introduce extended basic normal substructural logic with strong negation L^{∼} and its extensions. These extensions include Nelson’s logic N^{−} and Wansing’s logic COSPL (and its extensions). Further we define a new family of normal substructural logics with strong negation. The new logics are as follows: extended Došen’s logic DE^{∼}, extended positive relevant logics B^{∼}, T^{∼}, E^{∼}, R^{∼}, RMO^{∼}, EMO^{∼}, extended strict implication S4^{∼}, extended Corsi’s logics F^{∼}, FT^{∼}, FR^{∼} FRT^{∼}, extended Visser’s logic BPL^{∼}, and extended Méndez’s logics T_{∘}^{∼}, E_{∘}^{∼}, R_{∘}^{∼}, EMO_{∘}^{∼}, RMO_{∘}^{∼}, S4_{∘}^{∼}.

In Section 3, we introduce a Kripke type semantics for the normal substructural logics with strong negation mentioned above and show soundness theorem and a correspondence between axiom schemes and conditions on frames.

In Section 4, we prove the completeness theorems for the logics by using extended Ishihara’s canonical model construction method. In the sequel, we can show the completeness theorem for any logic obtained from L^{∼} by adding arbitrary combinations of the axiom schemes introduced in Section 2.

References

[1] Almukdad, A., and D. Nelson, Constructible falsity and inexact predicates. Journal of Symbolic Logic 49 (1984), 231 - 233.

[2] Anderson, A. R., and N.D.JR. Belnap, Entailment Vol.1, Princeton university press, 1975.

[3] Corsi, G., Weak logics with strict implication. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33 (1987) 389 - 406.

[4] Došen, K., Sequent systems and groupoid models. I. Studia Logica 47 (1988) 353 - 385.

[5] Došen, K., Sequent systems and groupoid models. II. Studia Logica 48 (1988) 41 - 65.

[6] Ishihara, H., A canonical model construction for substructural logics. Journal of Universal Computer Science 6 (2000) 155 - 168.

[7] Méndez, J M., A Routley-Meyer semantics for converse Ackermann property. Journal of Philosophical Logic 16 (1987) 65 - 76.

[8] Nelson, D., Constructible falsity. Journal of Symbolic Logic 14 (1949) 16 - 26.

[9] Ono, H., A note on Visser’s basic propositional logic. manuscript, 1997.

[10] Ono, H., and Y. Komori, Logics without the contraction rule. Journal of Symbolic Logic 50 (1985) 169 - 201.

[11] Suzuki, Y., and H. Ono, Hilbert style proof system for BPL. Research Report, Japan Advanced Institute of Science and Technology, 1997.

[12] Thomason, H., A semantical study of constructible falsity. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 15 (1969) 247 - 257.

[13] Visser, A., A propositional logic with explicit fixed points. Studia Logica 40 (1981) 155 - 174.

[14] Wansing. H., Informational interpretation of substructural propositional logics. Journal of Logic, Language and Information 2 (1993) 285 - 308.

Kripke completeness of predicate extensions of cofinal subframe logics

SHIMURA Tatsuya

               shimura@math.cst.nihon-u.ac.jp

Department of Mathematics, College of Science and Technology, Nihon University

1 The problem.

In the study of non-classical logics, it is a natural and fundamental question to ask the completeness of predicate extensions of Kripke complete propositional logics.

For the subframe logics containing S4, we have the following characterization for the completeness of the predicate extensions with constant domains.

Theorem 1 (Shimura [5], Tanaka-Ono [7], Chagrov-Zakharyashev [1]) Let L be a subframe logic containing S4. The following are equivalent:

• L is canonical.

• L has the finite embedding property.

• Q-L + BF is Kripke complete.

In particular, we have the following corollary.

Corollary 1 (Shimura [5], cf. Shimura [3]) (1). Let {M_{i}} be a set of finite and rooted Kripke frames without non-trivial clusters.

Then, QS4 + {α(M_{i})} + BF is Kripke complete.

(2). Let M be a finite and rooted Kripke frame with a non-trivial cluster.

Then, QS4 + α(M) + BF is Kripke incomplete.

If we consider a similar characterization problem for cofinal subframe logics, it is natural to settle the following question. (The necessity of axioms like T (K) is discussed in the talk [5]).

Question 1 Find a necessary and sufficient condition for the Kripke completeness of QS4 + {α(M_{i}, ⊥)} + T (K) + BF.

Note that the canonicity of L is not sufficient for the completeness by the result of Skvortsov [6]. So, the answer of the above question seems much difficult than the subframe case.

Although we do not have the answer, we give a partial answer corresponding to Corollary 1.

Theorem 2 We consider the following conditions for finite and rooted (S4-) Kripke frame.

(C1) There is no non-trivial inner clusters.

(C2) The set of the inner points has a common upper bound c such that {c} is a trivial cluster.

Then, we have the following.

(1). Let {M_{i}} be a set of finite and rooted Kripke frames satisfying above conditions. Then, QS4 + {α(M_{i}, ⊥)} + T (K) + BF is Kripke complete.

(2). Let M be a finite and rooted Kripke frame. If lM does not satisfy one of the above conditions, QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

2 The sketch of the proof of Theorem 2 (1).

To axiomatize the cofinal subframe logics, we use a variant ¬C_{M_{i}} of Fine’s subframe formula ¬B_{M_{i}} and frame formula ¬F_{M_{i}}, where B_{M_{i}}, F_{M_{i}} and C_{M_{i}} are the following:

B_{M_{i}} = p_{r} ( r is the root of M_{i}) ∧ ⋀_{a≠b} □¬(p_{a} ∧ p_{b})

∧ ⋀_{aRb} □(p_{a} ⊃ ◇p_{b}) ∧ ⋀_{aR̸b} □(p_{a} ⊃ ¬◇p_{b})

F_{M_{i}} = □( ⋁_{a∈M_{i}} p_{a}) ∧ B_{M_{i}},

C_{M_{i}} = □◇( ⋁_{a∈M_{i}} p_{a}) ∧ B_{M_{i}}.

The main tool of the completeness proof is the same as in [3], that is, the method of canonical models. Let N be the canonical frame for QS4 + {α(M_{i}, ⊥)} + T (K) + BF. We show a contradiction from the assumption that there is a cofinal subreduction from N to some M_{i}. Let C′ = {c} be a maximal cluster of M_{i} such that c is a common upper bound of the inner points.

We show that there is a ’definable’ cofinal subreduction from N to M_{i}. A function h from a Kripke model to a Kripke frame M_{i} is said to be difinable if there are formulas F_{a} (a ∈ M_{i}) such that

u ∈ h^{−1}(a) ⇔ u ⊧ F_{a}.

The difficulty arises from the fact that the family {u|u ⊧ F_{a}} (a is maximal) must forms a partition of the maximal points of N. To avoid this difficulty, we construct the map in two steps. Firstly, we construct a disjoint family {u|u ⊧ F_{a}} (a is maximal, a ≠ c). Secondly, we define the map so that the rest maximal points are mapped to c. By virtue of the condition (C2), the map constructed turns to be a cofinal subreduction.

Lemma 1 There is a finite subframe N′ of N with the following conditions.

• There is a p-morphism g from N′ to M_{i}.

• Each maximal cluster of N′ is contained by some maximal cluster of N.

Proof) This is because of the conditions that T (K) is valid N and M_{i} contains no non-trivial inner clusters. ■

Lemma 2 (1). For each a ∈ N′, there exists a formula F_{a} satisfying the following:

a ⊧ F_{a}, a |̸= F_{b} (b ≠ a).

(2). For each maximal cluster C of N′, there exists a formula G_{C} satisfying the following:

a ⊧ □G_{C} (a ∈ C), a |̸= ◇G_{C} (a is maximal, a ∉ C).

(3). For each inner point a ∈ N′, there exists a formula H_{a} satisfying the following:

a |̸= □◇□H_{a} ⊃ H_{a}.

Definition 1

H = ⋀ □(□◇□H_{a} ⊃ H_{a})

P_{a} = \{ \begin{matrix}H ∧ □G_{C} ∧ ⋀_{b∈C} □◇F_{b} ∧ F_{a} & (a is maximal , a ≠ c, a ∈ C) \\ H ∧ ⋀_{b≠c,b is maximal} □¬P_{b} & (a = c) \\ \begin{aligned}¬(□◇□H_{a} & ⊃ H_{a}) ∧ F_{a} \\ & ∧ ⋀_{aR̸b} □¬F_{b} ∧ ⋀_{b≠a} ¬F_{b} ∧ ⋀_{aRb} ◇P_{b} \end{aligned} & (a is an inner point.) \end{matrix}

Lemma 3 (1). N_{0} = {u ∈ N|u ⊧ P_{a} for some a} is a cofinal subframe of N.

(2). For each u ∈ N_{0}, there exists exactly one a ∈ N′ with u ⊧ P_{a}. The map f defined by f(u) = g(a) is a cofinal subreduction from N to M_{i}.

(3). u ⊧ P_{0} implies u ⊧ C for some instance C of C_{M_{i}}.

3 The outline of the proof of Theorem 2 (2).

We treat the case dviding into three cases.

Lemma 4 If M does not satisfy the condition (C1), QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

Proof) The incompleteness proof for QS4 + α(M) + BF works in this case. ■

Lemma 5 If the set of the inner points of M does not have a common upper bound, QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

Lemma 6 If the inner points of M has a common upper bound but no trivial clusters are u QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

Since the proofs of Lemma 5, 6 are quite complicated, we show the outline usinge typical examples.

The example for Lemma 6 is treated by Skvortsov [6] for intermediate predicate logics. But, his proof seems difficult to generalize since he uses Kripke bundle semantics.

We give a proof using a Kripke model. For each formula, the model behaves as a finite model, but it behaves as an infinite model for the whole formulas. The idea is described in Hughes-Cresswell [2].

Example 1 Let M and N be the following frames. There exist a formula A and a model ⟨N, ω, ⊧⟩ with the following conditions.

(1). A is not separable from L = QS4+α(M, ⊥)+T (K)+BF by Kripke frame semantics.

(2). Every instance of L is true in ⟨N, ⊧⟩.

(3). A is refuted in ⟨N, ⊧⟩.

[figure: a_{1}; a_{2}; a_{3}; b_{1}; b_{2}; b_{3}; ⋯]

For each language with finitely many constants, some a_{n} and b_{n} has completely same behaver under the valuation ⊧.

Example 2 Let M and N be the following frames. There exist a formula A and a model ⟨N, ω, ⊧⟩ with the following conditions.

(1). A is not separable from L = QS4+α(M, ⊥)+T (K)+BF by Kripke frame semantics.

(2). Every instance of L is true in ⟨N, ⊧⟩.

(3). A is refuted in ⟨N, ⊧⟩.

[figure] [figure: · · · · · ·]

For each language with finitely many constant symboles, some cluster behaves as a trivial cluster under ⊧.

References

[1] A. Chagrov, and M. Zakharyaschev, Modal logic, Clarendon Press, Oxford (1997)

[2] Hughes, G.E. and Cresswell, M.J., A new introduction to modal logic, Routledge, London (1986).

[3] Shimura, T., Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas, Studia Logica 52 (1993), 23–40.

[4] Shimura, T., On some modal predicate logics with Glivenko type characterization. MLG meeting (2000-1-11).

[5] Shimura, T., Kripke incompleteness of predicate extensions of the modal logics axiomatized by a canonical formula for a frame with a nontrivial cluster, Studia Logica 65 (2000), 237–247.

[6] D. Skvortsov, On some Kripke complete and Kripke incomplete intermediate predicate logics, Studia Logica 61 (1998), 281–292.

[7] Y. Tanaka, and H. Ono, Rasiowa-Sikorski lemma and Kripke completeness of predicate and infinitary modal logics, Advances in Modal Logic ’98, (1998).

On Komori Algebras

Yuichi KOMORI

                       komori@math.s.chiba-u.ac.jp

Department of Mathematics, Faculty of Science, Chiba University Inage-ku Chiba 263-8522 JAPAN

Humberstone([2]) has defined the notion of Komori algebras and proved a generalization of Lemma 2 of [3]. In this note, we will define Komori Algebras as a broader class of algebras than Komori algebras by Humberstone. And we will make the result of Humberstone more general.

We begin with the definition of Komori algebras. A Komori algebra is an algebra ⟨A, →, 1⟩ of type ⟨2, 0⟩ in which a quasi-identity (Ko) are satisfied:

(Ko) if x → y = y → x = 1, then x = y.

Henceforth Komori algebras defined by Humberstone are called Humberstone algebras. A Humberstone algebras is a Komori algebras which is satisfying the following three identities (M),(I) and (K):

\begin{aligned}(M) & 1 → x & = & x \\ (I) & x → x & = & 1 \\ (K) & x → 1 & = & 1. \end{aligned}

A BIK^{+}-algebra is a Humberstone algebra which is satisfying the following identity (B):

(B) (y → z) → (x → y) → x → z = 1.

A BIK^{+}-algebra had been called a BCC-algebra in [3]. In that paper, we proved that the quasivariety of all BIK^{+}-algebras is not a variety. A BCK-algebra ia a BIK^{+}-algebra which is satisfying the following identity (C):

(C) x → (y → z) = y → (x → z).

Wronski([5]) proved that the quasivarieties of all BCK-algebras is not a variety.

Now we define two finite algebras NK and K4. The algebra NK is closely related to the partition of the set of terms constructed out of the variables x, y (and the constant 1) defined in [3]. The algebras NK and K4 are defined by Hasse diagrams Figure 1 and Figure 2 with the definition of a binary operation →, respectively. The algebra NK is not a Komori algebra. The algebra K4 is a BIK^{+}-algebra, but not a BCK-algebra because c → (a → b) = 1 ≠ a → (c → b) = c. Let f be a function from K4 onto NK such that f(1) = f(c) = 1, f(a) = a and f(b) = b. Then f is a homomorphism from K4 onto NK. So we have the following.

Theorem 1 If a class K of Komori algebras contains K4, then K is not a variety.

Corollary 2 The class of all BIK^{+}-algebras is not a variety.

[figure: a; 1; b] \{ \begin{matrix}1 → x = x, \\ x → y = 1 if x ≤ y, \\ a → b = b → a = 1. \end{matrix}

Figure 1: NK

[figure: a; c; 1; b] \{ \begin{matrix}1 → x = x, \\ x → y = 1 if x ≤ y, \\ a → b = b → a = c, \\ c → a = a, c → b = b. \end{matrix}

Figure 2: K4

Let WR be the algebra defined by Wronski to prove that the class of all BCK-algebras is not a variety.

Theorem 3 If a class K of Komori algebras contains WR, then K is not a variety.

Corollary 4 The class of all BCK-algebras is not a variety.

The above corollaries have been proved in [3] and [5], respectively. Corollary 2 follows from Corollary 4 becase a class K of Komori algebras is not a variety if Id(K) ⊆ Σ and {A|Σ ⊆ Id(A) and A is a Komori algebra} is not a variety, in general. Here Id(K) is the set of identities holding in all algebras in K and Id(A) = Id({A}). Theorem 1 and Theorem 3 are mutually independent becasue x → (x → y) = x → (x → (x → y)) ∈ Id(K4) and the identity ∉ Id(WR). We call such algebras in the above theorems criterions.

Definition 5 A Komori algebra A is a criterion if any class of Komori algebras containing A is not variety.

For any Komori algebras A and B, if Id(A) ⊆ Id(B) and B is a criterion, then A is a criterion. For any criterion A, by Zorn’s lemma, there exists a criterion B such that Id(A) ⊆ Id(B) and C is not a criterion if Id(B) ⊊ Id(C). We call such criterion B maximal.

Conjecture 6 The Komori algebras K4 and WR are both maximal, that is, any Komori algebra A is not a criterion if Id(K4) ⊊ Id(A) or Id(WR) ⊊ Id(A).

Now we describe a partition in [3] of the set of terms constructed out of the variables x, y (and the constant 1), whose blocks are called X, Y, and 1. The partition in question is defined by induction on the construction of these x, y-terms:

1. x ∈ X, y ∈ Y, and 1 ∈ 1,

2. if s ∈ X or s ∈ Y, then s → t ∈ 1,

3. if s ∈ 1, then s → t belongs to the block which t belongs to.

Let XY be the set of identities {s = t|s ∈ X and t ∈ Y}.

Lemma 7 Let K be a class of Komori algebras. If x, y-terms s_{1} and s_{2} lie in the different block of the partition {X, Y, 1} and s_{1} = s_{2} ∈ Id(K), then

Id(K) ∩ XY ≠ ∅ .

Let K be a class of Komori algebras and F_{K}(2) be the K-free algebra on two generators(x and y). Suppose that Id(K) ∩ XY = ∅. Let f be a function from F_{K}(2) onto NK defined below:

f([t]) = \{ \begin{matrix}1 & if t ∈ 1, \\ a & if t ∈ X, \\ b & if t ∈ Y. \end{matrix}

By Lemma 7, the function f is well-defined. Remark that Lemma 7 and Id(K)∩XY = ∅ are used only for establishing the well-definedness of the function f. The function f is a homomorphism from F_{K}(2) onto NK. So the algebra F_{K}(2) is a criterion.

Theorem 8 Let K be a class of Komori algebras. If Id(K) ∩ XY = ∅, then the class K is not a variety.

The above theorem is a generalization of Lemma 2 of [3] and Proposition 3 of [2]. Remark that a identity in the set XY is not always a Komori identity (in the sence of [1]) for the quasi-variety of all Komori algebras though the set XY is a complete set of Komori identies for the quasi-variety of all Humberstone algebras.

References

[1] W. J. Blok and Silvia B. La Falce. Komori identities in algebraic logic. to appear in Reports on Mathematical Logic, 2000.

[2] Lloyd Humberstone. Note on a lemma of komori. submitted to Mathematica Japonica, 2000.

[3] Yuichi Komori. The class of BCC–algebras is not a variety. Mathematica Japonica, 29:391– 394, 1984.

[4] Misao Nagayama. On a property of BCK-identities. Studia Logica, 53:227–234, 1994.

[5] Andrzej Wroński. BCK-algebras do not form a variety. Mathematica Japonica, 28:211–213, 1983.

An Extension of Martin-Löf’s Type Theory with an Evolution Relation

Tadao Ishii

                            ishii@jaist.ac.jp

School of Information Science, Japan Advanced Institute of Science and Technology

In this note, we will extend Martin-Löf’s type theory by introducing an evolution relation between types and also expressions (similar discussions are found in [1]). The purpose is to formalize the software evolution problem proposed by T. Katayama in [2] under the constructive type theory [3,4].

1 Introduction

As a method of maintaining and/or producing a large scale of software rapidly, the software evolution problem was proposed by T. Katayama in [2]. Here software evolution means to the mechanism that software can change its structure and functions to adapt changes of its requirements and environment.

Let 𝕊 = ⟨S, ⊑⟩ and ℙ = ⟨P, ⊑⟩ be the structures of specification and program, respectively. Then in general, software evolution problem is defined as finding a new program P′ of a new specification S′, in symbols, P′ ⊢ S′ under the assumption that the program P of S is given, P ⊢ S and the specification S changes to S′, in symbols S ⊑ S′. Here, if the change S ⊑ S′ is arbitrary, then we should make P′ newly and software evolution problem does not arise. In [2], there are explanations of two typical evolutional patterns:

(1) P ⊢ S and S ⊑ S′ : if we calculate the difference of specifications S′ and S, in symbols, ΔS = Diff(S′, S) and derive the program ΔP corresponding to this difference ΔS, ΔP ⊢ ΔS then the desired program P′ is obtained by merging two programs P and ΔP, in symbols, P′ = Sup(P, ΔP).

(2) P ⊢ S, T ⊑ S and T ⊑ S′ : if ΔS = Diff(S′, T), ΔP ⊢ ΔS and derive the program Q of T by degenerating the original program P with ΔP, in symbols, Q = Diff(P, ΔP) then the desired program P′ is obtained by applying pattern (1).

2 Martin-Löf’s Type Theory

In this section we will introduce Martin-Löf’s type theory (MTT in short) [3,4]. Since MTT is one of the predicative type theory, in general MTT has a universe type U_{n} (n = 0, 1, 2, …). But in this investigation we will omit to include universes type U_{n} (and also well orderings type W) for the sake of simplicity. MTT has its two major syntactical categories, that is MTT-type and MTT-expression. Here the MTT-types are words over the alphabet and Greek letters such that (1) constants : finite set type N_{n} (n = 0, 1, …) and natural number set type N (here we abbreviate empty set type as ⊥ (= ∅ = N_{0}) and singleton set type as T (= N_{1})), (2) symbols : type constructors Π, Σ, +, I, types A, B, C, …, objects a, b, c, …, object variables x, y, z, …, parentheses (,) and membership relation ∈.

Definition 2.1 The set of MTT-types T is defined inductively as follows:

(i) all constants N_{n} (n = 0, 1, …), N, ⊥ and T are MTT-types (called atomic types),

(ii) if A and B are any MTT-types and x ∈ A is any object variable, then (Πx ∈ A)B(x) is a MTTtype (called dependent product type), (iii) if A and B are any MTT-types and x ∈ A is any object variable, then (Σx ∈ A)B(x) is a MTT-type

(called dependent sum type),

(iv) if A and B are any MTT-types, then A + B is a MTT-type (called direct sum type),

(v) if A is any MTT-type and a, b ∈ A are any objects, then I(A, a, b) is a MTT-type (called propositional equality type).

On the other hand, the MTT-expressions are words over the alphabet and Greek letters such that (1) constant : elements of finite set m_{n} (n = 0, 1, …; m = 0, 1, …, n − 1), natural number 0, here ϵ and t (= 0_{1}) are abbreviation of empty element and singleton element, respectively, (2) variables : x, y, z, …,

(3) symbols : form constructors Ap, E, D, J, R_{n} (n = 0, 1, …), R, functional abstraction λ, indices of set i, j, successor function succ, objects a, b, c, …, parentheses or ordered pair (,).

Definition 2.2 The set of MTT-expressions E is defined inductively as follows (notice that [,] denotes the assumptions) :

(i) all variables x, y, z, … and constants m_{n} (n = 0, 1, …; m = 0, 1, …, n − 1), 0, ϵ and t are MTTexpresssions (called atomic expressions),

(ii) if a ∈ A, b(x) ∈ B(x) [x ∈ A] and c ∈ (Πx ∈ A)B(x) are any MTT-expressions, then (λx)b(x) ∈ (Πx ∈ A)B(x) and Ap(c, a) ∈ B(a) are MTT-expressions (called canonical and noncanonical expressions of the type (Πx ∈ A)B(x), respectively),

(iii) if a ∈ A, b ∈ B(a), c ∈ (Σx ∈ A)B(x) and d(x, y) ∈ C((x, y)) [x ∈ A, y ∈ B(x)] are any MTTexpressions, then (a, b) ∈ (Σx ∈ A)B(x) and E(c, d(x, y)) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type (Σx ∈ A)B(x), respectively),

(iv) if a ∈ A, b ∈ B, c ∈ A + B, d(x) ∈ C(i(x)) [x ∈ A] and e(y) ∈ C(j(y)) [y ∈ B] are any MTTexpressions, then i(a), j(b) ∈ A + B and D(c, d(x), e(y)) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type A + B, respectively),

(v) if a, b ∈ A, c ∈ I(A, a, b) and d ∈ C(r) are any MTT-expressions, then r ∈ I(A, a, b) and J(c, d) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type I(A, a, b), respectively),

(vi) if c, m_{n} ∈ N_{n} (n = 0, 1, …; m = 0, 1, …, n − 1) and c_{m} ∈ C(m_{n}) are any MTT- expressions, then m_{n} ∈ N_{n} and R_{n}(c, c_{0}, c_{1}, …, c_{n−1}) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type N_{n} (n = 0, 1, …)), respectively,

(vii) if 0, a, c ∈ N, d ∈ C(0) and e(x, y) ∈ C(succ(x)) [x ∈ N, y ∈ C(x)] are any MTT-expressions, then 0, succ(a) ∈ N and R(c, d, e(x, y)) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type N, respectively).

The theory of type MTT can evaluate each MTT-expression like a reduction of term in λ-calculus. One reduction (i.e., evaluation) of MTT-expression is performed by simultaneously substitutions. After evaluating MTT-expressions, if a MTT-expression in some MTT-type has itself as a value of substitution, then we will call this expression to canonical form, and otherwise to noncanonical form of this type. For any expressions a ∈ A and b ∈ B, an expression a is equal to b, in symbols, a = b ∈ A if two expressions a, b have the same canonical form. Moreover, for any types A and B, a type A is equal to B, in symbols, A = B if for two canonical forms c_{A} ∈ A and c_{B} ∈ B, it holds that c_{A} = c_{B} ∈ A.

Under the following judgments, the theory of type MTT is axiomatized as Gentzen’s natural deduction style. We will omit to show each individual inference rule now (see [3,4]).

(1) A type : A is a type.

(2) a ∈ A : a is an object of type A.

(3) a = b ∈ A : a and b are equal objects of type A.

(4) A = B : A and B are equal types.

3 Evolution relation and its related operations

In this section we will introduce the notion of evolution relation ⊑ between MTT-types and also expressions. Then we will define some basic operations, i.e., supremum, infimum and difference operations related to this order. Here our idea is that we can order every similar types (generated by the same type constructor) in MTT from the viewpoint of an evolutional relationship by replacing some atomic types in these types with the unit type T, since only N_{n} (n = 0, 1, …) and N are atomic types in MTT and the type T = (N_{1}), which denotes a singleton set, has a noncanonical form R_{1}(c, t) that is corresponding to NOP operation in the programs.

Any MTT-expression b is degenerated according to the following rule : b[t, …, t /b_{1}, …, b_{n}], where this denotes the result of simultaneously replacements of some atomic expressions b_{1}, …, b_{n} in b by the singleton element t ∈ T. For any expressions a ∈ A and b ∈ B, an expression a is evolved to b, in symbols, a ⊑ b ∈ A if for some atomic expressions b_{1}, …, b_{n} ∈ At(b), it holds that b[t, …, t /b_{1}, …, b_{n}] = a ∈ A. Moreover, for any types A and B, a type A is evolved to B, in symbols, A ⊑ B if for two canonical forms c_{A} ∈ A and c_{B} ∈ B, it holds that c_{A} ⊑ c_{B} ∈ A. According to the above definition of an evolution relation, we will define the evolution relation of MTT-types and expressions individually below under the assumption that each type and form constructors are continuous.

Definition 3.1 For any types A and B in T , the evolution relation A ⊑ B of type, is defined inductively as follows:

(i) For any interpretations C : N_{k} → T and D : N_{l} → T , if ⋃_{m=0}^{k−1} C(m_{k}) ⊆ ⋃_{m=0}^{l−1} D(m_{l}), then N_{k} ⊑ N_{l} (k, l = 0, 1, …; k ≤ l).

(ii) N ⊑ N and ⊥ ⊑ T.

(iii) If A_{1} ⊑ A_{2} and B_{1}(x_{1}) ⊑ B_{2}(x_{2}) [x_{1} ∈ A_{1}, x_{2} ∈ A_{2}], then (Πx_{1} ∈ A_{1})B_{1}(x_{1}) ⊑ (Πx_{2} ∈ A_{2})B_{2}(x_{2}).

(iv) If A_{1} ⊑ A_{2} and B_{1}(x_{1}) ⊑ B_{2}(x_{2}) [x_{1} ∈ A_{1}, x_{2} ∈ A_{2}], then (Σx_{1} ∈ A_{1})B_{1}(x_{1}) ⊑ (Σx_{2} ∈ A_{2})B_{2}(x_{2}).

(v) If A_{1} ⊑ A_{2} and B_{1} ⊑ B_{2}, then A_{1} + B_{1} ⊑ A_{2} + B_{2}.

(vi) If A_{1} ⊑ A_{2} and a_{1} ⊑ a_{2} ∈ A_{1} and b_{1} ⊑ b_{2} ∈ A_{1}, then I(A_{1}, a_{1}, b_{1}) ⊑ I(A_{2}, a_{2}, b_{2}).

Definition 3.2 For any expressions a ∈ A and b ∈ B in E, the evolution relation a ⊑ b ∈ A of expression, is defined inductively as follows:

(i) For any object variables x ∈ A and y ∈ B in E such that A ⊑ B, x ⊑ y ∈ A.

(ii) For any m_{k} ∈ N_{k} and m_{l} ∈ N_{l} (k, l = 0, 1, …; k ≤ l), if C(m_{k}) ⊆ D(m_{l}), then m_{k} ⊑ m_{l} ∈ N_{k}.

(iii) 0 ⊑ 0 ∈ N and ϵ ⊑ t ∈ ⊥.

(iv) If A_{1} ⊑ A_{2} and b_{1}(x_{1}) ⊑ b_{2}(x_{2}) [x_{1} ∈ A_{1}, x_{2} ∈ A_{2}], then (λx_{1})b_{1}(x_{1}) ⊑ (λx_{2})b_{2}(x_{2}) ∈ (Πx_{1} ∈ A_{1})B_{1}(x_{1}). Moreover, if c_{1} ⊑ c_{2} ∈ (Πx_{1} ∈ A_{1})B_{1}(x_{1}) and a_{1} ⊑ a_{2} ∈ A_{1}, then Ap(c_{1}, a_{1}) ⊑ Ap(c_{2}, a_{2}) ∈ B_{1}(a_{1}).

(v) If a_{1} ⊑ a_{2} ∈ A_{1} and b_{1}(a_{1}) ⊑ b_{2}(a_{2}) ∈ B_{1}(a_{1}) [a_{1} ∈ A_{1}, a_{2} ∈ A_{2}], then (a_{1}, b_{1}) ⊑ (a_{2}, b_{2}) ∈ (Σx_{1} ∈ A_{1})B_{1}(x_{1}). Moreover, if c_{1} ⊑ c_{2} ∈ (Σx_{1} ∈ A_{1})B_{1}(x_{1}) and d_{1}(x_{1}, y_{1}) ⊑ d_{2}(x_{2}, y_{2}) ∈ C_{1}((x_{1}, y_{1})), then E(c_{1}, d_{1}(x_{1}, y_{1})) ⊑ E(c_{2}, d_{2}(x_{2}, y_{2})) ∈ C_{1}(c_{1}).

(vi) If a_{1} ⊑ a_{2} ∈ A_{1} and b_{1} ⊑ b_{2} ∈ B_{1}, then i(a_{1}) ⊑ i(a_{2}), j(b_{1}) ⊑ j(b_{2}) ∈ A_{1} + B_{1}. Moreover, if c_{1} ⊑ c_{2} ∈ A_{1} + B_{1}, d_{1}(x_{1}) ⊑ d_{2}(x_{2}) ∈ C_{1}(i(x_{1})) [x_{1} ⊑ x_{2} ∈ A_{1}] and e_{1}(y_{1}) ⊑ e_{2}(y_{2}) ∈ C_{1}(j(y_{1})) [y_{1} ⊑ y_{2} ∈ B_{1}], then D(c_{1}, d_{1}(x_{1}), e_{1}(y_{1})) ⊑ D(c_{2}, d_{2}(x_{2}), e_{2}(y_{2})) ∈ C_{1}(c_{1}).

(vii) If a_{1} = b_{1} ∈ A_{1}, a_{2} = b_{2} ∈ A_{2}, a_{1} ⊑ a_{2} ∈ A_{1} and b_{1} ⊑ b_{2} ∈ A_{1}, then r_{1} ⊑ r_{2} ∈ I(A_{1}, a_{1}, b_{1}). Moreover, if c_{1} ⊑ c_{2} ∈ I(A_{1}, a_{1}, b_{1}) and d_{1} ⊑ d_{2} ∈ C_{1}(r_{1}), then J(c_{1}, d_{1}) ⊑ J(c_{2}, d_{2}) ∈ C_{1}(c_{1}).

(viii) If c_{1} ⊑ c_{2} ∈ N_{k} and a_{m} ⊑ b_{m′} ∈ C_{1}(m_{k}) (m = 0, 1, …, k − 1; m′ = 0, 1, …, l − 1), then R_{k}(c_{1}, a_{0}, a_{1}, …, a_{k−1}) ⊑ R_{l}(c_{2}, b_{0}, b_{1}, …, b_{l−1}) ∈ C_{1}(c_{1}).

(ix) a ⊑ a ∈ N implies succ(a) ⊑ succ(a) ∈ N. Moreover, if c_{1} ⊑ c_{2} ∈ N, d_{1} ⊑ d_{2} ∈ C_{1}(0) and e_{1}(x_{1}, y_{1}) ⊑ e_{2}(x_{2}, y_{2}) ∈ C_{1}(succ(x_{1})) [x_{1}, x_{2} ∈ N, y_{1} ∈ C_{1}(x_{1}), y_{2} ∈ C_{2}(x_{2})], then R(c_{1}, d_{1}, e_{1}(x_{1}, y_{1})) ⊑ R(c_{2}, d_{2}, e_{2}(x_{2}, y_{2})) ∈ C_{1}(c_{1}).

Proposition 3.3 For each structures 𝕋 = ⟨T , ⊑⟩ and 𝔼 = ⟨E, ⊑⟩, the evolution relation ⊑ is a partial order.

Next we will define both supremum and infimum operations between every MTT-types w.r.t. the above evolution relation under the assumption that every type constructors are continuous.

Definition 3.4 For any types A and B in T , the supremum Sup(A, B) and infimum Inf(A, B) functions between them w.r.t. the evolution relation ⊑ is defined inductively as follows:

(i) Sup(N_{k}, N_{l}) = N_{r} and Inf(N_{k}, N_{l}) = N_{s} (k, l = 0, 1, …; k ≤ l), where r = |⋃_{m=0}^{k−1} C(m_{k}) ∪ ⋃_{m=0}^{l−1} D(m_{l})| and s = |⋃_{m=0}^{k−1} C(m_{k}) ∩ ⋃_{m=0}^{l−1} D(m_{l})|.

(ii) Sup(N, N) = N, Inf(N, N) = N, Sup(⊥, T) = T and Inf(⊥, T) = ⊥.

(iii) Sup((Πx_{1} ∈ A_{1})B_{1}(x_{1}), (Πx_{2} ∈ A_{2})B_{2}(x_{2})) = (Πx ∈ Sup(A_{1}, A_{2})) Sup(B_{1}, B_{2})(x), Inf((Πx_{1} ∈ A_{1})B_{1}(x_{1}), (Πx_{2} ∈ A_{2})B_{2}(x_{2})) = (Πx ∈ Inf(A_{1}, A_{2})) Inf(B_{1}, B_{2})(x).

(iv) Sup((Σx_{1} ∈ A_{1})B_{1}(x_{1}), (Σx_{2} ∈ A_{2})B_{2}(x_{2})) = (Σx ∈ Sup(A_{1}, A_{2})) Sup(B_{1}, B_{2})(x), Inf((Σx_{1} ∈ A_{1})B_{1}(x_{1}), (Σx_{2} ∈ A_{2})B_{2}(x_{2})) = (Σx ∈ Inf(A_{1}, A_{2})) Inf(B_{1}, B_{2})(x).

(v) Sup(A_{1} + B_{1}, A_{2} + B_{2}) = Sup(A_{1}, A_{2}) + Sup(B_{1}, B_{2}), Inf(A_{1} + B_{1}, A_{2} + B_{2}) = Inf(A_{1}, A_{2}) + Inf(B_{1}, B_{2}).

(vi) Sup(I(A_{1}, a_{1}, b_{1}), I(A_{2}, a_{2}, b_{2})) = I(Sup(A_{1}, A_{2}), Sup(a_{1}, a_{2}), Sup(b_{1}, b_{2})), Inf(I(A_{1}, a_{1}, b_{1}), I(A_{2}, a_{2}, b_{2})) = I(Inf(A_{1}, A_{2}), Inf(a_{1}, a_{2}), Inf(b_{1}, b_{2})).

(vii) For any types A and B which are not matched any cases of the above (i)–(vi), Sup(A, B) = T and Inf(A, B) = ⊥.

Moreover, we can also define both supremum and infimum functions between every MTT-expressions w.r.t. the evolution relation by the similar manner.

Lemma 3.5 (i) For any types A and B in T , Sup(A, B) and Inf(A, B) are the l.u.b. and g.l.b. of A and B w.r.t. the evolution relation ⊑, respectively.

(ii) Similarly, for any expressions a and b in E, Sup(a, b) and Inf(a, b) are the l.u.b. and g.l.b. of a and b w.r.t. the evolution relation ⊑, respectively.

(iii) Both structures 𝕋 = ⟨T , ⊑⟩ and 𝔼 = ⟨E, ⊑⟩ are the complete lattices w.r.t. the evolution relation ⊑.

Theorem 3.6 (i) For any expressions a ∈ A and b ∈ B, it holds that Sup(a, b) ∈ Sup(A, B).

(ii) For any expressions a ∈ A and b ∈ B, it holds that Inf(a, b) ∈ Inf(A, B).

For any types A and B in T such that A ⊑ B, we will say that Diff(B, A) is a difference between B and A if this operation satisfies the following conditions:

(1) Sup(A, Diff(B, A)) = B,

(2) Inf(A, Diff(B, A)) = ⊥.

Definition 3.7 For any types A and B in T , the difference Diff(B, A) function between B and A w.r.t. the evolution relation ⊑ is defined inductively as follows:

(i) Diff(N_{l}, N_{k}) = N_{v} (k, l = 0, 1, …; k ≤ l), where v = |⋃_{m=0}^{l−1} D(m_{l}) \ ⋃_{m=0}^{k−1} C(m_{k})|.

(ii) Diff(N, N) = ⊥ and Diff(T, ⊥) = T.

(iii) If (Πx_{1} ∈ A_{1})B_{1}(x_{1}) ⊑ (Πx_{2} ∈ A_{2})B_{2}(x_{2}), then

Diff((Πx_{2} ∈ A_{2})B_{2}(x_{2}), (Πx_{1} ∈ A_{1})B_{1}(x_{1}))

= (Πx ∈ Diff(A_{2}, A_{1}))B_{1}(x) ∪ (Πx_{1} ∈ A_{1}) Diff(B_{2}, B_{1})(x_{1}) ∪

(Πx ∈ Diff(A_{2}, A_{1})) Diff(B_{2}, B_{1})(x).

(iv) If (Σx_{1} ∈ A_{1})B_{1}(x_{1}) ⊑ (Σx_{2} ∈ A_{2})B_{2}(x_{2}), then

Diff((Σx_{2} ∈ A_{2})B_{2}(x_{2}), (Σx_{1} ∈ A_{1})B_{1}(x_{1}))

= (Σx ∈ Diff(A_{2}, A_{1}))B_{1}(x) ∪ (Σx_{1} ∈ A_{1}) Diff(B_{2}, B_{1})(x_{1}) ∪

(Σx ∈ Diff(A_{2}, A_{1})) Diff(B_{2}, B_{1})(x).

(v) If A_{1} + B_{1} ⊑ A_{2} + B_{2}, then

Diff(A_{2} + B_{2}, A_{1} + B_{1})

= Diff(A_{2}, A_{1}) + Diff(B_{2}, B_{1}).

(vi) If I(A_{1}, a_{1}, b_{1}) ⊑ I(A_{2}, a_{2}, b_{2}), then

Diff(I(A_{2}, a_{2}, b_{2}), I(A_{1}, a_{1}, b_{1})

= I(Diff(A_{2}, A_{1}), a_{1}, b_{1}) ∪ I(A_{2}, Diff(a_{2}, a_{1}), Diff(b_{2}, b_{1})) ∪

I(Diff(A_{2}, A_{1}), Diff(a_{2}, a_{1}), Diff(b_{2}, b_{1})).

(vii) For any types A and B which are not matched any cases of the above (i)–(vi),

Diff(A, B) = ⊥.

By the similar manner, we can introduce the difference between expressions Diff(b, a) for any expressions a and b in E such that a ⊑ b.

Lemma 3.8 (i) For any types A and B in T such that A ⊑ B, Diff(B, A) is a difference between B and A.

(ii) Similary, for any expressions a ∈ A and b ∈ B in E such that a ⊑ b ∈ A, Diff(b, a) is a difference between b and a.

Theorem 3.9 For any expressions a ∈ A and b ∈ B, if an expression a is evolved to b in a type A, a ⊑ b ∈ A, then it holds that Diff(b, a) ∈ Diff(B, A).

References

[1] L. Boerio, Extending Pruning Techniques to Polymorphic Second Order λ-Calculus, Proceeding of ESOP ’94, Edinburgh, April 1994, LNCS 788, D. Sannella (ed.), Springer-Verlag, pp.120–134.

[2] T. Katayama, A Theoretical Framework of Software Evolution, International Workshop on Principles of Software Evolution, In Conjunction with International Conference on Software Engineering 1998 (ICSE98), pp.1–5.

[3] P. Martin-Löf, Constructive Mathematics and Computer Programming, In Logic, Methodolgy and Philosophy of Science, VI, NorthHolland,1980.

[4] P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis,1984.

Fuzzy relations and fuzzy mappings between fuzzy subsets

Mamoru Shimoda

                      mamoru-s@shimonoseki-cu.ac.jp

Shimonoseki City University

Introduction

In fuzzy literature, fuzzy relations and fuzzy mappings are usually treated as those between crisp sets. With our natural interpretation in a Heyting valued model for intuitionistic set theory, we are to define and study fuzzy relations and fuzzy mappings between fuzzy sets, especially between fuzzy subsets of crisp sets. By using membership functions we can characterize fuzzy relations, fuzzy mappings, and equivalence and order relations.

1 The Heyting valued model

Let H be a complete Heyting algebra with operations and constants ∧, ∨, ⋀, ⋁, →, ¬, 0, 1, and ≤. We construct an H-valued model for the extended intuitionistic set theory, which is a first order intuitionistic logic with predicates ∈, = and E (called an existence predicate) together with axioms of intuitionistic set theory. Let V be the class of all crisp sets and On be the class of all ordinals.

Definition 1.1. The H-valued model V^{H} is constructed as follows. For every ordinal α, V_{α}^{H} is defined by induction:

V_{0}^{H} = ϕ, V_{α}^{H} = ⋃_{β<α} V_{β}^{H} (if α is a limit ordinal),
V_{α+1}^{H} = { u = ⟨|u|, Eu⟩; |u| : 𝒟u⟶H, 𝒟u ⊆ V_{α}^{H}, Eu ∈ H, |u|(x) ≤ Eu ∧ Ex for all x ∈ 𝒟u}.

Then V^{H} = ⋃_{α∈On} V_{α}^{H}.

For a sentence φ of V^{H}, the Heyting value ∥φ∥ ∈ H is defined as follows.

Definition 1.2. Let u, v ∈ V^{H} and φ, ψ, φ(a) be formulas of V^{H}. For atomic formulae,

∥Eu∥ = Eu, and by simultaneous induction,

∥u ∈ v∥ = ⋁_{y∈𝒟v} (v(y) ∧ ∥u = y∥), and

∥u = v∥ = ⋀_{x∈𝒟u}(u(x)→∥x ∈ v∥) ∧ ⋀_{y∈𝒟v}(v(y)→∥y ∈ u∥) ∧ Eu ∧ Ev.

For compound formulae, by induction (on the number of logical symbols),

∥φ ∧ ψ∥ = ∥φ∥ ∧ ∥ψ∥,  ∥φ ∨ ψ∥ = ∥φ∥ ∨ ∥ψ∥,
∥φ → ψ∥ = ∥φ∥ → ∥ψ∥,  ∥¬φ∥ = ¬∥φ∥,
∥∀xφ(x)∥ = ⋀_{u∈V^{H}}(Eu → ∥φ(x)∥), and ∥∃xφ(x)∥ = ⋁_{u∈V^{H}}(Eu ∧ ∥φ(x)∥).

An element of the model is called a set in V^{H}. For a sentence φ of V^{H}, φ is valid in V^{H} if ∥φ∥ = 1. We say u is a subset of v in V^{H} (u ⊑ v) if ∥u ⊆ v∥ = ⋀_{x∈𝒟u} (u(x) → ∥x ∈ v∥) = 1. If u ⊑ v and v ⊑ u, we say u and v are similar (u ∼ v). If u ∼ v and Eu = Ev, u and v are said to be equivalent (u ≈ v). Definition 1.3. For every crisp set x in V, x̌ ∈ V^{H} is defined recursively by:

𝒟(x̌) = {y̌; y ∈ x}, Ex̌ = 1, x̌ : y̌ ⟼ 1.

We call x̌ the check set of x.

The canonical embedding which assigns to each crisp set its check set plays an important role in our interpretation. For a bounded formula φ(a_{1}, ⋯, a_{n}) and crisp sets x_{1}, ⋯, x_{n}, φ(x_{1}, ⋯, x_{n}) holds iff ∥φ(x̌_{1}, ⋯, x̌_{n})∥ = 1, and ¬φ(x_{1}, ⋯, x_{n}) holds iff ∥φ(x̌_{1}, ⋯, x̌_{n})∥ = 0. Definition 1.4. Let u, v ∈ V^{H}.

(1) 𝒟{u, v}^{H} = {u, v}, E{u, v}^{H} = Eu ∧ Ev, and {u, v}^{H} : x ⟼ 1.

(2) ⟨u, v⟩^{H} = {{u, u}^{H}, {u, v}^{H}}^{H}.

(3) 𝒟(u ×^{H} v)= {⟨x, y⟩^{H} ; x ∈ 𝒟u, y ∈ 𝒟v}, E(u ×^{H} v) = Eu ∧ Ev, and u ×^{H} v : ⟨x, y⟩^{H} ⟼ u(x) ∧ v(y).

(4) 𝒟(u ∩^{H} v) = 𝒟u ∪ 𝒟v, E(u ∩^{H} v) = Eu ∧ Ev, and u ∩^{H} v : x ⟼ ∥x ∈ u∥ ∧ ∥x ∈ v∥.

(5) 𝒟(u ∪^{H} v) = 𝒟u ∪ 𝒟v, E(u ∪^{H} v) = Eu ∨ Ev, and u ∪^{H} v : x ⟼ ∥x ∈ u∥ ∨ ∥x ∈ v∥.

(6) 𝒟(u\^{H} v) = 𝒟u ∪ 𝒟v, E(u\^{H} v) = Eu ∨ Ev, and u\^{H} v : x ⟼ ∥x ∈ u∥ ∧ ¬ ∥x ∈ v∥. The superscripts and commas may be omitted. We can also define power sets, infinite sums, and so

on. Hence all axioms of (extended) intuitionistic set theory are valid in V^{H}.

A relation in V^{H} is a subset of a cartesian product in V^{H}. For R, u, v ∈ V^{H}, R is a relation from u to v in V^{H} if R is a subset of u ×^{H} v in V^{H}. We often write xRy instead of ⟨xy⟩ ∈ R.

For each set u in V^{H}, the identity relation I_{u} on u is defined by:

𝒟(I_{u}) = {⟨xx⟩; x∈ 𝒟u}, E(I_{u}) = Eu, and I_{u}:⟨xx⟩⟼ u(x).

Definition 1.5. For R, S in V^{H}, the composition S ∘ R and the inverse relation R^{−1} are defined by: 𝒟(S ∘ R) = {⟨xz⟩; x, z ∈ V_{α}^{H}}, E(S ∘ R) = ER ∧ ES, S ∘ R : ⟨xz⟩ ⟼ ∥∃y(xRy ∧ ySz)∥, and

𝒟(R^{−1}) = {⟨xy⟩; x, y ∈ V_{α}^{H}}, E(R^{−1}) = ER, R^{−1} : ⟨xy⟩ ⟼ ∥yRx∥,

where α is a suitable ordinal which satisfies 𝒟R ∪ 𝒟S ⊆ V_{α}^{H}.

The definitions are not affected by the choice of the ordinal α. If R and S are relations from u to v and from v to w respectively, then S ∘ R is a relation from u to w and R^{−1} is a relation from v to u. Definition 1.6. Let R be a relation from u to v in V^{H}.

(1) For A ∈ V^{H}, the image R(A) ∈ V^{H} is defined by:

𝒟(R(A)) = 𝒟v, E(R(A)) = ER ∧ EA, R(A) : y ⟼ ∥(∃x ∈ A)xRy∥.

(2) For B ∈ V^{H}, the inverse image R^{−1}(B) ∈ V^{H} is defined by:

𝒟(R^{−1}(B)) = 𝒟u, E(R^{−1}(B)) = ER ∧ EB, R^{−1}(B) : x ⟼ ∥(∃y ∈ B)xRy∥.

A relation R from u to v in V^{H} is called total if (∀x ∈ u)(∃y ∈ v)(xRy) is valid, and is surjective if (∀y ∈ v)(∃x ∈ u)(xRy) is valid. Similarly, R is injective if (∀x, y ∈ u)(∀z ∈ v)(xRz ∧ yRz → x = y) is valid, and is univalent if (∀x ∈ u)(∀y, z ∈ v)(xRy∧xRz → y = z) is valid. Then R is total iff I_{u} ⊑ R^{−1}∘R, R is surjective iff I_{v} ⊑ R ∘ R^{−1}, R is injective iff R^{−1} ∘ R ⊑ I_{u}, and R is univalent iff R ∘ R^{−1} ⊑ I_{v}.

A relation R on u (that is, a relation from u to u) is called reflexive if (∀x ∈ u)(xRx) is valid. Similarly R is symmetric if ∀x∀y(xRy → yRx) is valid, is transitive if ∀x∀y∀z(xRy ∧ yRz → xRz) is valid, is antisymmetric if ∀x∀y(xRy ∧ yRx → x = y) is valid, and is connected if (∀x ∈ u)(∀y ∈ u)(xRy ∨ yRx) is valid. Then R is reflexive iff I_{u} ⊑ R, is symmetric iff R^{−1} ⊑ R iff R^{−1} ≈ R, is transitive iff R ∘ R ⊑ R, is antisymmetric iff R ∩ R^{−1} ⊑ I_{u}, and is connected iff u × u = R ∪ R^{−1}.

An equivalence relation is a reflexive, symmetric, and transitive relation, an order relation is a reflexive, antisymmetric, and transitive relation, and a total order is a connected order relation. Hence a relation R on u is an equivalence relation iff I_{u} ⊑ R, R^{−1} ⊑ R, and R ∘ R ⊑ R. If R is a relation R^{−1} ∘ R is symmetric, and in addition if R is total R^{−1} ∘ R is reflexive, and if it is univalent R^{−1} ∘ R is transitive.

A mapping in V^{H} is a total and univalent relation in the model. For u, v, f ∈ V^{H}, f is called a mapping from u to v in V^{H} if f is a total and univalent relation from u to v in V^{H}. We write f : u ⟶ v in V^{H} if f is a mapping from u to v. We often write f(x) = y instead of ⟨xy⟩ ∈ f or xfy. A relation f from u to v is a mapping iff I_{u} ⊑ f^{−1} ∘ f and f ∘ f^{−1} ⊑ I_{v}.

An injection (resp. a surjection) is an injective (resp. surjective) mapping, and a bijection is an injective and surjective mapping. A composition of injections (resp. surjections or bijections) is also an injection (resp. a surjection or a bijection). For a relation f from u to v, f is an injection iff I_{u} ≈ f^{−1} ∘ f and f ∘ f^{−1} ⊑ I_{v}, is a surjection iff I_{u} ⊑ f^{−1} ∘ f and f ∘ f^{−1} ≈ I_{v}, and f is a bijection iff I_{u} ≈ f^{−1} ∘ f and f ∘ f^{−1} ≈ I_{v}. Hence for a mapping f : u ⟶ v in V^{H}, f is injective iff I_{u} ≈ f^{−1} ∘ f and is surjective iff f ∘ f^{−1} ≈ I_{v}. For a mapping f in V^{H}, f^{−1} ∘ f is an equivalence relation.

We can define images and inverse images of mappings similarly to those of relations.

2 Relations and mappings between fuzzy subsets

In the following, let X, Y, Z be crisp sets. We call every set in the model V^{H} an H-fuzzy set.

Definition 2.1. For an H-fuzzy set A, the membership function of A on X is the mapping

μ_{A} = μA^{X} : X ⟶ H; x ⟼ ∥x̌ ∈ A∥.

An H-fuzzy subset of X is a subset of X̌ in V^{H}, that is, for A ∈ V^{H},

A is an H-fuzzy subset of X iff A ⊑ X̌.

Lemma 2.1. Every mapping from X to H is the membership function of some H-fuzzy subset of X.

Hence there is a natural correspondence between H-fuzzy subsets of X and mappings from X to H.

Definition 2.2. Let μ, ν be mappings from X to H.

(1) μ ≤ ν iff μ(x) ≤ ν(x) for all x ∈ X.

(2) The mappings μ ∧ ν, μ ∨ ν, ¬ μ : X ⟶H are defined by:

μ ∧ ν : x ⟼ μ(x) ∧ ν(x), μ ∨ ν : x ⟼ μ(x) ∨ ν(x), and ¬ μ : x ⟼ ¬ μ(x) (for all x ∈ X).

The natural correspondence preserves inclusion (order) and the basic set operations.

Proposition 2.2. Let A, B be H-fuzzy sets and all the membership functions below be on X.

(1) If A and B are H-fuzzy subsets of X, then A ⊑ B iff μ_{A} ≤ μ_{B}.

(2) μ_{A∩B} = μ_{A} ∧ μ_{B}, μ_{A∪B} = μ_{A} ∨ μ_{B}, and μ_{X̌\A} = ¬ μ_{A}.

Every relation in the model is called an H-fuzzy relation.

Definition 2.3. For R, u, v ∈ V^{H}, R is an H-fuzzy relation from u to v if it is a relation from u to v in V^{H}. For every R ∈ V^{H}, the membership function of R from X to Y is the membership function of R on X × Y, hence it is the mapping

μ_{R} : X × Y ⟶ H; ⟨xy⟩ ⟼ ∥⟨xy⟩^{∨} ∈ R∥.

An H-fuzzy relation from X to Y is an H-fuzzy subset of X ×Y.

If A, B are H-fuzzy subsets of X, Y respectively, then obviously an H-fuzzy relation from A to B is an H-fuzzy relation from X to Y.

Lemma 2.3. Let A, B be H-fuzzy subsets of X, Y respectively and R be a set in V^{H}. Then

R is an H-fuzzy relation from A to B iff μ_{R}⟨xy⟩ ≤ μ_{A}(x) ∧ μ_{B}(y) for all x ∈ X, y ∈ Y,

where μ_{A}, μ_{B}, μ_{R} be the membership functions on X, Y, X × Y respectively.

Proposition 2.4. Let A, B, C be H-fuzzy subsets of X, Y, Z respectively, R be an H-fuzzy relation from A to B, S be an H-fuzzy relation from B to C, and μ_{R}, μ_{S}, μ_{S∘R}, μ_{R^{−1}} be their membership functions on X × Y, Y × Z, X × Z, Y × X respectively.

(1) The composition S ∘ R is an H-fuzzy relation from A to C, and

μ_{S∘R}⟨xz⟩ = ⋁_{y∈Y} (μ_{R}⟨xy⟩ ∧ μ_{S}⟨yz⟩) for all x ∈ X, z ∈ Z.

(2) The inverse relation R^{−1} is an H-fuzzy relation from B to A, and μ_{R^{−1}}⟨yx⟩ = μ_{R}⟨xy⟩ for all x ∈ X, y ∈ Y.

These are extensions of the defining equations of max-min composition and those of inverse for ordinary fuzzy relations.

Proposition 2.5. Let A, B be H-fuzzy subsets of X, Y respectively, R be an H-fuzzy relation from A to B, and μ_{R} be its membership function on X × Y.

(1) For every C ∈ V^{H}, the image R(C) is a subset of B in V^{H}, and

μ_{R(C)}(y) = ⋁_{x∈X}(μ_{C}(x) ∧ μ_{R}⟨xy⟩) for all y ∈ Y,

where μ_{C} and μ_{R(C)} are the membership functions on X and on Y respectively.

(2) For every D ∈ V^{H}, the inverse image R^{−1}(D) is a subset of A in V^{H}, and

μ_{R^{−1}(D)}(x) = ⋁_{y∈Y} (μ_{D}(y) ∧ μ_{R}⟨xy⟩) for all x ∈ X,

where μ_{D} and μ_{R^{−1}(D)} are the membership functions on Y and on X respectively.

Proposition 2.6. Let A, B be H-fuzzy subsets of X, Y respectively, R be an H-fuzzy relation from A to B, and μ_{A}, μ_{B}, μ_{R} be their membership functions on X, Y, X × Y respectively.

(1) R is total iff ⋁_{y∈Y} μ_{R}⟨xy⟩ = μ_{A}(x) for all x ∈ X.

(2) R is surjective iff ⋁_{x∈X} μ_{R}⟨xy⟩ = μ_{B}(y) for all y ∈ Y.

(3) R is injective iff μ_{R}⟨xz⟩ ∧ μ_{R}⟨yz⟩ > 0 implies x = y for all x, y ∈ X and all z ∈ Y.

(4) R is univalent iff μ_{R}⟨xy⟩ ∧ μ_{R}⟨xz⟩ > 0 implies y = z for all x ∈ X and all y, z ∈ Y.

Theorem 1. Let A be an H-fuzzy subset of X, R be an H-fuzzy relation on A, and μ_{A}, μ_{R} be their membership functions on X, X × X respectively. Then the followings hold.

(1) R is reflexive iff μ_{R}⟨xx⟩ = μ_{A}(x) for all x ∈ X.

(2) R is symmetric iff μ_{R}⟨xy⟩ = μ_{R}⟨yx⟩ for all x, y ∈ X.

(3) R is transitive iff μ_{R}⟨xy⟩ ∧ μ_{R}⟨yz⟩ ≤ μ_{R}⟨xz⟩ for all x, y, z ∈ X

(4) R is antisymmetric iff μ_{R}⟨xy⟩ ∧ μ_{R}⟨yx⟩ > 0 implies x = y for all x, y ∈ X.

(5) R is connected iff μ_{R}⟨xy⟩ ∨ μ_{R}⟨yx⟩ = μ_{A}(x) ∧ μ_{A}(y) for all x, y ∈ X.

Every mapping in V^{H} is called an H-fuzzy mapping.

Definition 2.4. A mapping from u to v in V^{H} is called an H-fuzzy mapping from u to v. An H-fuzzy mapping from X to Y is a mapping from X̌ to Y̌ in V^{H}.

Obviously an H-fuzzy mapping from u to v is a total and univalent H-fuzzy relation from u to v.

Theorem 2. Let A, B be H-fuzzy subsets of X, Y respectively, and μ_{A}, μ_{B} be their membership function on X, Y respectively. Suppose f ∈ V^{H} and ψ = μ_{f} is its membership function on X × Y. Then f is an H-fuzzy mapping from A to B iff ψ satisfies the following three conditions:

(R) ψ⟨xy⟩ ≤ μ_{A}(x) ∧ μ_{B}(y) for all x ∈ X, y ∈ Y,

(E) ⋁_{y∈Y} ψ⟨xy⟩ = μ_{A}(x) for all x ∈ X,

(U) ψ⟨xy⟩ ∧ ψ⟨xz⟩ > 0 implies y = z for all x ∈ X, y, z ∈ Y.

Conversely, if a crisp mapping ψ : X × Y ⟶ H satisfies the three conditions, there is an H-fuzzy mapping f from A to B whose membership function on X × Y is identical with ψ.

Proposition 2.7. Let A, B be H-fuzzy subsets of X, Y respectively, f be an H-fuzzy mapping from A to B, and μ_{f} be its membership function on X × Y.

(1) For every C ∈ V^{H}, the image f(C) is a subset of B in V^{H}, and

μ_{f(C)}(y) = ⋁_{x∈X}(μ_{C}(x) ∧ μ_{f}⟨xy⟩) for all y ∈ Y,

where μ_{C} and μ_{f(C)} are the membership functions on X and on Y respectively.

(2) For every D ∈ V^{H}, the inverse image f^{−1}(D) is a subset of A in V^{H}, and

μ_{f^{−1}(D)}(x) = ⋁_{y∈Y} (μ_{D}(y) ∧ μ_{f}⟨xy⟩) for all x ∈ X,

where μ_{D} and μ_{f^{−1}(D)} are the membership functions on Y and on X respectively.

References

[1] M. Shimoda, Categorical aspects of Heyting-valued models for intuitionistic set theory, Comment. Math. Univ. Sancti Pauli 30(1) (1981) 17–35.

[2] M. Shimoda, A natural interpretation of fuzzy sets and fuzzy relations, submitted, 1998.

[3] M. Shimoda, A natural interpretation of fuzzy sets and relations (abstract), The Bulletin of Symbolic Logic, 5(1) (1999) 132.

[4] M. Shimoda, A natural interpretation of fuzzy mappings, submitted, 2000.

[5] S. Titani, Completeness of global intuiotionistic set theory, J. Symbolic Logic 62(2) (1997) 506–528.

Theorem Provers with Counter Models from xpe

Motohiko Mouri

                   mouri@jaist.ac.jp

JAIST, Tatsunokuti, Ishikawa, 923–1292, Japan

              http://www.jaist.ac.jp/~mouri

Abstract Xpe is a grammar editor for proof figure on TEX. It makes you easier to draw

proof figure. And theorem provers called from xpe help you to research and write papers.

1 Introduction

How do you draw proof figure on TEX? Most of us must use ‘proof.sty’ macros. But we feel confusion to draw and fix one because it has a structural problem that tree structure is expressed by so many brackets. We would desire another method to draw it. To that solution, I produce xpe here.

Xpe (X window system Proof Editor) is a grammar editor for proof figure. It interprets and displays TEXcommand, for example \Gamma ⋯ Γ,\Delta ⋯ Δ,\supset ⋯ ⊃, and so on. It supports cut and paste formulae. The file format for input and output is compatible with proof.sty. And it is easy to transfer from editor to xpe, and opposite. We can get WYSIWYG(What You See Is What You Get) environment to draw proof figure.

In addition, some theorem provers are supported. They are propositional logics:

• classical logic

• intuitionistic logic

• modal logics K, KT, S4, S5

• lambda type assign system

At this time, these theorem provers and proof checker are supported:

• modal logics K, KT with counter models (called K+, KT+)

• modal logics K5, KD5

• cut elimination checker

Most of this paper refers to System K+ and KT+ that are theorem provers of K or KT with counter modes.

By the way, xpe is a free software. Everybody can download from above my homepage.

2 System K+

Modal logic K is defined by adding (□) rule to classical logic LK of sequent calculus system. On decision procedure, it is defined by adding (□) rule including weakening to Wang’s system (see [4],[1]). The rules are shown at figure 1.

{Γ → A \atop □Γ → □A} (□) {Γ → A \atop Δ, □Γ → □A, Σ} (□)

Figure 1: □ rules for LK and Wang’s system

If we generate a counter model for a unprovable sequent, we need take the System K+ (figure 2). We consider both sides of a sequent as multi–sets. It is enough to consider as sets, too. But to make it more easily to understand decision procedure in the theorem prover, both sides of sequent are treated as multi–sets.

Γ, p → p, Δ

\begin{matrix}Γ → Δ, A & Γ, B → Δ \\ Γ, A ⊃ B → Δ \end{matrix} (⊃ L)  {Γ, A → Δ, B \atop Γ → Δ, A ⊃ B} (⊃ R)

{Γ, A, B → Δ \atop Γ, A ∧ B → Δ} (∧L)  \begin{matrix}Γ → Δ, A & Γ → Δ, B \\ Γ → Δ, A ∧ B \end{matrix} (∧R)

\begin{matrix}Γ, A → Δ & Γ, B → Δ \\ Γ, A ∨ B → Δ \end{matrix} (∨L)  {Γ → Δ, A, B \atop Γ → Δ, A ∨ B} (∨R)

{Γ, A → Δ \atop Γ → Δ, ¬A} (¬R)  {Γ, A → Δ \atop Γ → Δ, ¬A} (¬R)

\begin{matrix}Γ → A_{1} & ⋯ & Γ → A_{m} \\ p_{1}, ⋯, p_{n}, □Γ → □A_{1}, ⋯, □A_{m}, q_{1}, ⋯ q_{l} \end{matrix} (□)

Figure 2: System K+

I am explaining the procedure to generate a counter model for an unprovable sequent. Here, consider □C ∨ □B ∧ D → □(¬A ∨ □C) ∨ □B. The theorem prover of K+ outputs a decision tree and a counter modes as follows:

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}{→ C \atop C, A → □C} & (□) \\ C → ¬A, □C \end{matrix} ; (¬R) ; C → ¬A ∨ □C ; (∨R) & C → B \\ □C, D → □(¬A ∨ □C), □B \end{matrix} (□) & □B, D → □(¬A ∨ □C), □B \\ □C ∨ □B, D → □(¬A ∨ □C), □B \end{matrix} & (∨L) \\ □C ∨ □B, D → □(¬A ∨ □C) ∨ □B \end{matrix} ; (∨R) ; □C ∨ □B ∧ D → □(¬A ∨ □C) ∨ □B ; (∧L) \{\} ; ⋮ . ; \{C, A\} \{C\} ; ⋮ . ; \{D\}

Figure 3: Decision tree and counter model by K+

At first, the procedure reduces logical connectives ∧, ∨, ∧ and ⊃ to easier formulae, and determines that each consequence is an initial sequents or not. If no more rule is applied, it tries to apply (□) rule. Finally each top sequent is a form like p_{1}, ⋯, p_{n}, □Γ → q_{1}, ⋯, q_{n}. The sequent corresponds to the formulae set {p_{1}, ⋯, p_{n}}.

And (□) rule corresponds a frame \begin{matrix}\{Γ, ¬A_{1}\} ⋯ \{Γ, ¬A_{m}\} \\ ↖ ↗ \\ \{p_{1}, ⋯, p_{n}\} \end{matrix} . In the system K+, it is

expressed as {Γ, ¬A_{1}} ⋯ {Γ, ¬A_{m}} ; ⋮ . ; {p_{1}, ⋯, p_{n}} by expression restriction on proof.sty.

Roughly speaking, the sequent p_{1}, ⋯, p_{n}, □Γ → □A_{1}, ⋯, □A_{m}, q_{1}, ⋯ q_{l} corresponds to the formulae set {p_{1}, ⋯, p_{n}}. On this view, each decision tree from lower to upper

corresponds to a propositional symbol set. The correspondence bitween trees and sets for that decision tree follows:

\begin{matrix}→ C & ⋯ \{\} \\ C → B & ⋯ \{C\} \\ \begin{matrix}{C, A → □C \atop C → ¬A, □C} & (¬R) \\ C → ¬A ∨ □C \end{matrix} ; (∨R) & ⋯ \{C, A\} \\ \begin{matrix}\begin{matrix}□C, D → □(¬A ∨ □C), □B & [□B, D → □(¬A ∨ □C), □B] \\ □C ∨ □B, D → □(¬A ∨ □C), □B \end{matrix} & (∨L) \\ □C ∨ □B, D → □(¬A ∨ □C) ∨ □B \end{matrix} ; (∨R) ; □C ∨ □B ∧ D → □(¬A ∨ □C) ∨ □B ; (∧L) & ⋯ \{D\} \end{matrix}

Figure 4: Relationship between tree and set

Because the sequent □B, D → □(¬A ∨ □C), □B is provable, the procedure makes {D} from □C, D → □(¬A ∨ □C), □B.

3 System KT+

Modal logic KT is defined by adding (T) rule to K. On decision procedure, it is defined by adding (T) rule including contraction to K+ system. However, we adopt a black marked (T) rule, because (T) rule including contraction has loop. If we mark to □ whenever we apply (T), it has no loop.

{A, Γ → Δ \atop □A, Γ → Δ} (T) {□A, A, Γ → Δ \atop □A, Γ → Δ} (T) {■A, A, Γ → Δ \atop □A, Γ → Δ} (T)

Figure 5: T rules for KT and KT+

Generaging a counter model for a unprovable sequent for KT+ is similar to K+. At first, the procedure reduces logical connectives ∧, ∨, ∧ and ⊃ to easier formulae, and transfers from □ formulae to ■ formulae by (T) rule. And then it determines that each consequence is an initial sequents or not. If no more rule is applied, it tries to apply following (□) rule. Finally each top sequent is a form like p_{1}, ⋯, p_{n}, ■Γ → q_{1}, ⋯, q_{n}. The sequent corresponds to the formulae set {p_{1}, ⋯, p_{n}}.

\begin{matrix}Γ → A_{1} & ⋯ & Γ → A_{m} \\ p_{1}, ⋯, p_{n}, ■Γ → □A_{1}, ⋯, □A_{m}, q_{1}, ⋯ q_{l} \end{matrix} (□)

Figure 6: □ rule for KT+

And (□) rule corresponds a frame \begin{matrix}{↷ \atop \{Γ, ¬A_{1}\}} & ⋯ & {↷ \atop \{Γ, ¬A_{m}\}} \\ ↖ ↷ ↗ \\ \{p_{1}, ⋯, p_{n}\} \end{matrix} .

Now, consider the formula □□B, C → □(¬A∨□C). The theorem prover KT+ outputs a decision tree and a counter model as follows:

\begin{matrix}\begin{matrix}{B → C \atop ■B, B, B, A → □C} & (□) \\ □B, B, A → □C \end{matrix} ; (T) ; □B, B → ¬A, □C ; (¬R) ; □B, B → ¬A ∨ □C ; (∨R) ; ■□B, ■B, B, C → □(¬A ∨ □C) & (□) \\ ■□B, □B, C → □(¬A ∨ □C) \end{matrix} ; (T) ; □□B, C → □(¬A ∨ □C) ; (T) \{B\} ; ⋮ . ; \{B, B, A\} ; ⋮ . ; \{B, C\}

Figure 7: Decision tree and counter model by KT+

Similarly to K+, we can find correspondence between decision trees and formula sets as follows:

\begin{matrix}B → C & ⋯ \{B\} \\ \begin{matrix}{■B, B, B, A → □C \atop □B, B, A → □C} & (T) \\ □B, B → ¬A, □C \end{matrix} ; (¬R) ; □B, B → ¬A ∨ □C ; (∨R) & ⋯ \{B, B, A\} \\ \begin{matrix}{■□B, ■B, B, C → □(¬A ∨ □C) \atop ■□B, □B, C → □(¬A ∨ □C)} & (T) \\ □□B, C → □(¬A ∨ □C) \end{matrix} ; (T) & ⋯ \{C, B\} \end{matrix}

Figure 8: Relationship between tree and set

4 Conclusion

Most of theorem provers in the world reply only whether a formula is valid or not. However, I want a proof if it is provable, and a counter model if it is unprovable. And it is hard to learn how to use a theorem prover. So I take TEX style as user interface. Because most of logicians know TEX, it is easy to learn how to use xpe. Especially, as they usually use xpe to draw proof figure, they will become familiar to xpe. My primary motivation to create xpe is the easy use.

References

[1] E Kiriyama, Ono H: The contraction rule and decision problems for logics without substractural rules, Studia Logica 50 (1991), 299–319.

[2] Chris D.Peterson: Athena Widget Set – C Language Interface MIT X Consortium.

[3] Lincoln A. Wallen: Automated Proof Search in Non-Classical Logics, : Efficient Matrix Proof Methods for Modal and Intuitionistic Logics MIT Press, 1990.

[4] H Wang:: A survey of mathematical logic Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1963.

Initial segments of Rudin-Frolík order

Masahiko Murakami

                        muramasa@ms.u-tokyo.ac.jp

Department of Mathematics, Hosei University

Abstract

The Rudin-Frolík order is originally defined on β (ω) [3, 7]. We defined Rudin-Frolík order on the ultrafilters of the complete Boolean algebras [5]. It is well-known that an initial segment of Rudin-Frolík order on β (ω) is totally ordered. The main theorem is Theorem 1.1. When the complete Boolean algebra satisfies countably chain condition (ccc), an initial segment of Rudin-Frolík order is totally ordered.

1 Rudin-Frolík order

Definition 1.1 (Rudin-Frolík order). Let p be an ultrafilter of a complete Boolean algebra 𝒜 and let q be an ultrafilter of a complete Boolean algebra ℬ. The Rudin-Frolík order ⊑ is the binary relation, which is given by p ⊑ q, if there are a ∈ p, b ∈ q, a complete homomorphism h: 𝒜 → ℬ↾b and a homomorphism f: ℬ → 𝒜↾a such that f ∘ h(x) = x for all x ∈ 𝒜↾a and f^{−1}“ p = q.

Precisely saying, Rudin-Frolík order is preorder, which dose not satisfy anti-symmetric law. We consider the equivalence class, the equivalence relation is defined by p ⊑ q ∧ q ⊑ p, implicitly.

Theorem 1.1. Let q be an ultrafilter of a complete Boolean algebra ℬ with countably chain condition (ccc). Let p_{1} be an ultrafilter of a complete Boolean algebra 𝒜_{1} and let p_{2} be an ultrafilter of a complete Boolean algebra 𝒜_{2}. If p_{1} ⊑ q and p_{2} ⊑ q, then p_{1} ⊑ p_{2} or p_{2} ⊑ p_{1}.

2 Nonstandard universes

Given a set X, we define the iterated power set V_{n}(X) over X recursively by V_{0}(X) = X and V_{n+1}(X) = V_{n}(X) ∪ 𝒫(V_{n}(X)). The superstructure V (X) is the union ⋃_{n<ω} V_{n}(X). The set X is said to be a base set if ∅ ∉ X and each element of X is disjoint from V (X). From now on, we reserve the letter X for infinite base set. In a substructure W of a superstructure V (X), the elements of W \ X are called sets relative to W. We denote the model ⟨V (X), ∈⟩ for the language ℒ_{∈} = {∈} of set theory by the same symbol V (X). A Δ_{0}-formula of ℒ_{∈} is a formula obtained from atomic formulae using connectives and bounded quantifiers such as ∀x ∈ y and ∃x ∈ y. Let 𝔐 = ⟨M, ϵ_{M}⟩ and 𝔑 = ⟨N, ϵ_{N}⟩ be models for ℒ_{∈}. We say that 𝔐 is a bounded elementary submodel of 𝔑 if 𝔐 is a submodel of 𝔑 and for any Δ_{0}-formula φ(x_{1}, …, x_{n}) of ℒ_{∈} and for any a_{1}, …, a_{n} ∈ M, 𝔐 ⊧ φ(a_{1}, …, a_{n}) if and only if 𝔑 ⊧ φ(a_{1}, …, a_{n}). A map e: M → N is said to be a bounded elementary embedding of 𝔐 into 𝔑 if e is an isomorphic embedding of 𝔑 onto a bounded elementary submodel of 𝔐.

A nonstandard universe is a triple ⟨V (X), V (Y), ⋆⟩ such that:

(1) X and Y are infinite base sets.

(2) (Transfer Principle) The map ⋆ is a bounded elementary embedding of V (X) into V (Y).

(3) ^{⋆}X = Y.

(4) For every infinite subset of A of X, {^{⋆}a | a ∈ A} is a proper subset of ^{⋆}A.

Ignoring the condition (4), we call the triple a pre-nonstandard universe. By the condition (3), we can denote by ⟨V (X), V (^{⋆}X), ⋆⟩ a pre-nonstandard universe.

We call an element a ∈ V (^{⋆}X) standard if there is an x ∈ V (X) such that a = ^{⋆}x. We call an element a ∈ V (^{⋆}X) internal if there is an x ∈ V (X) such that a ∈ ^{⋆}x. We denote by V (X)^{⋆} the set of all internal elements in V (^{⋆}X). The model V (X)^{⋆} is a transitive submodel of V (^{⋆}X). Then, we can simply denote by single V (X)^{⋆} pre-nonstandard universe. The norm (of standardness) nos(a) of an internal element a is a cardinal defined by

nos(a) = min {|x| | a ∈ ^{⋆}x}.

The radius of V (X)^{⋆} is a cardinal defined by

rad( V (X)^{⋆}) = min {κ | ∀y ∈ V (X)^{⋆} nos(y) < κ}.

We call an element of V (^{⋆}X) external if it is not internal. For the general theory of nonstandard universes, we refer to [1].

Definition 2.1 (Standardizable bounded elementary embedding). Let ⋆V (X) and ^{▲ ▼}V (X) be pre-nonstandard universes. A bounded elementary embedding e: ^{⋆}V (X) → ^{▲ ▼}V (X) is standardizable if e^{−1}“ y ∈ ^{⋆}V (X) for any set y relative to ^{▲ ▼}V (X). We call e^{−1}“ y the standardization of y by e if e^{−1}“ y ∈ ^{⋆}V (X).

Definition 2.2 (End extension). Let ⟨N, <⟩ be a structure inside V (X) which is isomorphic to ⟨ω, <⟩. A bounded elementary embedding e: ^{⋆}V (X) → ^{▲ ▼}V (X) is an end extension if {e(x) | x < ν} = {y | y < e(ν)} for any ν ∈ ^{⋆}N.

Lemma 2.1. A standardizable bounded elementary embedding of pre-nonstandard universe is an end extension.

Proof. Easy.

3 Boolean valued superstructures

Definition 3.1 (Bounded Boolean ultrapower). Let 𝒜 be a complete Boolean algebra. We denote

V̂(X)^{⟨𝒜⟩} = \{ u: V (X) → 𝒜 | \begin{matrix}u(x) ∧ u(y) = 0 for x ≠ y, \\ ⋁ u“ V_{n}(X) = 1 for some n < ω \end{matrix} \} .

Let p be an ultrafilter of 𝒜. The bounded Boolean ultrapower V̂(X)^{⟨𝒜⟩} /p modulo p of 𝒜 is the set of equivalence class by p with the membership relation.

We can regard a bounded Boolean ultrapower as a pre-nonstandard universe by Mostowski collapsing. The bounded elementary embedding of V (X) into V̂(X)^{⟨𝒜⟩} /p is given by x̌/p where x̌ = V (X) × {1_{𝒜} }.

Definition 3.2 (Bounded ultrasheaf). Let 𝒜 be a complete Boolean algebra. We denote

V_{0}(X)^{(𝒜)} = {u: ⋃ X → 𝒜 | ⋁_{x∈X}(⋁ u“ x ∧ ¬ ⋀ u“ (⋃ X \ x)) = 1},
V_{n+1}(X)^{(𝒜)} = { u | dom u ⊆ V_{n}(X), rng u ⊆ 𝒜 } ,
V̂(X)^{(𝒜)} = ⋃_{n<ω} V_{n}(X)^{(𝒜)} .

Then V̂(X)^{(𝒜)} is equipped with 𝒜-valued membership relation. Let p be an ultrafilter of 𝒜. The bounded Boolean ultrasheaf V̂(X)^{(𝒜)} /p modulo p of 𝒜 is the set of equivalence class by p with the membership relation.

We can regard a bounded ultrasheaf as a pre-nonstandard universe by Mostowski collapsing. Then we can regard the bounded Boolean ultrapower V̂(X)^{⟨𝒜⟩} /p is a substructure of the bounded ultrasheaf V̂(X)^{(𝒜)} /p. For the general theory of bounded ultrasheaves, we refer to [6].

Bounded Boolean ultrapower is constructed by equivalence relation “=”. As the Boolean valued universe V^{(ℬ)} of set theory, bounded ultrasheaf is constructed by membership relation “∈”. Membership relation “∈” is stronger than equivalence relation “=”.

Definition 3.3 (Standardizable bounded elementary embedding of ultrasheaves). Let V̂(X)^{(𝒜)} /p and V̂(X)^{(ℬ)} /q be ultrasheaves. A bounded elementary embedding e: V̂(X)^{(𝒜)} /p → V̂(X)^{(ℬ)} /q is standardizable if e^{−1}“ y ∈ V̂(X)^{(𝒜)} /p for any set y relative to V̂(X)^{(ℬ)} /q. We call e^{−1}“ y the standardization of y by e if e^{−1}“ y ∈ V̂(X)^{(𝒜)} /p.

Theorem 3.1 (Characterization theorem of the Rudin-Frolík order [5]). Let p be an ultrafilter of a complete Boolean algebra 𝒜 and let q be an ultrafilter of a complete Boolean algebra ℬ. Suppose 𝒜, ℬ ∈ V (X) \ X. Then, p ⊑ q if and only if there is a standardizable bounded elementary embedding e: V̂(X)^{(𝒜)} /p → V̂(X)^{(ℬ)} /q of ultrasheaves.

Proof. See [5, Theorem 5.3].

Lemma 3.2. Let e: V̂(X)^{(𝒜)} /p → V̂(X)^{(ℬ)} /q be a standardizable bounded elementary embedding. Then e↾V̂(X)^{⟨𝒜⟩} /p is an end extension.

Proof. As easy as that of Lemma 2.1.

Theorem 3.3. Let e_{0} : V̂(X)^{⟨𝒜⟩} /p → V̂(X)^{⟨ℬ⟩} /q be a bounded elementary embedding. Suppose |𝒜|, |ℬ| < |V (X)| = ℶ_{ω}(|X|), then e_{0} can be extended to a unique bounded elementary embedding e: V̂(X)^{(𝒜)} /p → V̂(X)^{(ℬ)} /q of ultrasheaves.

I am sorry to omit the proof of the theorem above, because it is not enough space to state it — it costs at least 12 pages. The theorem seems to be deep, which suggests that every pre-nonstandard universe has the generic extension a priori. If you are interested in the theorem, please email me.

4 Proof of Theorem 1.1

Lemma 4.1. Let ℬ be a complete Boolean algebra with ccc. Let p be an ultrafilter of a complete Boolean algebra 𝒜 and let q be an ultrafilter of ℬ. Suppose p ⊑ q. Then there is a ∈ p such that 𝒜↾a satisfies ccc.

Proof. Choose a ∈ p, b ∈ q, a complete homomorphism h: 𝒜 → ℬ↾b and an epimorphism f: ℬ → 𝒜↾a satisfying that f ∘ h(x) = x for all x ∈ 𝒜↾a and f^{−1}“ p = q. Let P be a partition of unity of 𝒜↾a. Since h“ P is a partition of unity of ℬ, we have |P | ≤ ℵ_{0}.

Lemma 4.2. Let 𝒜 be a complete Boolean algebra with ccc and let p be an ultrafilter of 𝒜. Then the radius of the bounded Boolean ultrapower is at most ℵ_{1}.

Proof. For u/p ∈ V̂(X)^{⟨𝒜⟩} , put I = {x ∈ V (X) | u(x) ≠ 0_{𝒜} }, then I is a set relative to V (X). Since u“ I is a partition of unity of 𝒜, |I| is at most countable. Then [[u ∈ Ǐ]] = 1_{𝒜} ∈ p. Thus u/p is an element of Ǐ/p where |I| is at most countable.

Lemma 4.3. Let ^{⋆^{1}}V (X) and ^{⋆^{2}}V (X) be pre-nonstandard universes with the radii at most ℵ_{1}. Let e_{1} : ^{⋆^{1}}V (X) → ^{▲ ▼}V (X) and e_{2} : ^{⋆^{2}}V (X) → ^{▲ ▼}V (X) be end extensions. Then either rng e_{1} ⊆ rng e_{2} or rng e_{2} ⊆ rng e_{1}. When rng e_{1} ⊆ rng e_{2}, there is a bounded elementary embedding e_{0} : ^{⋆^{1}}V (X) → ^{⋆^{2}}V (X) such that e_{1} = e_{2} ∘ e_{0}. When rng e_{2} ⊆ rng e_{1}, there is a bounded elementary embedding e_{0} : ^{⋆^{2}}V (X) → ⋆^{1}V (X) such that e_{2} = e_{1} ∘ e_{0}.

\begin{matrix}▲ \\ ▼ \end{matrix}V (X)^{⋆_{1}}V (X)_{e_{1}}  _{e_{0}} or  ^{⋆_{1}}V (X)_{e_{2}}_{e_{0}}  .

Proof. Let ⟨N, <⟩ be a structure inside V (X) which is isomorphic to ⟨ω, <⟩. Since e_{1} and e_{2} are end extensions, we have either e_{1}“^{⋆^{1}}N ⊆ e_{2}“^{⋆^{2}}N or e_{2}“^{⋆^{2}}N ⊆ e_{1}“^{⋆^{1}}N. Suppose e_{1}“^{⋆^{1}}N ⊆ e_{2}“^{⋆^{2}}N. We shall show rng e_{1} ⊆ rng e_{2}. Let a ∈ ^{⋆^{1}}V (X). Since the radius of ^{⋆^{1}}V (X) is at most ℵ_{1}, there is a countable set I relative to V (X) such that a ∈ ^{⋆^{1}}I. Let ã: N → I be a bijection. Note that ã ∈ V (X) and that ⋆^{1}ã: ^{⋆^{1}}N → ^{⋆^{1}}I is a bijection. Then there are ν_{1} ∈ ^{⋆^{1}}N and ν_{2} ∈ ^{⋆^{2}}N such that a = (^{⋆^{1}}ã)(ν_{1}) and e_{1}(ν_{1}) = e_{2}(ν_{2}). We obtain that e_{1}(a) = e_{2}((^{⋆^{2}}ã)(ν_{2})). In fact, since e_{1}(^{⋆^{1}}ã) = e_{2}(^{⋆^{2}}ã) and e_{1}(ν_{1}) = e_{2}(ν_{2}), we have

(e_{1}(^{⋆^{1}}ã))(e_{1}(ν_{1})) = (e_{2}(^{⋆^{2}}ã))(e_{2}(ν_{2})),
e_{1}(a) = e_{1}((^{⋆^{1}}ã)(ν_{1})) = e_{2}((^{⋆^{2}}ã)(ν_{2})).

Thus we have obtained that rng e_{1} ⊆ rng e_{2}. Now we can define the map e_{0} : ^{⋆^{1}}V (X) → ^{⋆^{2}}V (X) such that e_{1} = e_{2} ∘ e_{0}. Let φ(x_{1}, …, x_{n}) be a Δ_{0}-formula of ℒ_{∈}, and let a_{1}, …, a_{n} ∈ ^{⋆^{1}}V (X). Since both e_{1} and e_{2} are bounded elementary embeddings, we get

▲ ▼V (X) ⊧ φ(e_{1}(a_{1}), …, e_{1}(a_{n})) ⟺ ^{▲ ▼}V (X) ⊧ φ(e_{2}(e_{0}(a_{1})), …, e_{2}(e_{0}(a_{n}))),
⋆^{1}V (X) ⊧ φ(a_{1}, …, a_{n}) ⟺ ^{⋆^{2}}V (X) ⊧ φ(e_{0}(a_{1}), …, e_{0}(a_{n})).

Thus we e_{0} is a bounded elementary embedding. Exchanging ⋆_{1} for ⋆_{2}, we have the proof in case e_{2}“^{⋆^{2}}N ⊆ e_{1}“^{⋆^{1}}N.

Proof of Theorem 1.1. From Lemma 4.1, we can assume both 𝒜_{1} and 𝒜_{2} satisfy ccc. Choose a base set X such that 𝒜_{1}, 𝒜_{2}, ℬ ∈ V (X) \ X. By the characterization theorem of the Rudin-Frolík order, there are standardizable bounded elementary embeddings of ultrasheaves e_{1} : V̂(X)^{(𝒜_{1})} /p_{1} → V̂(X)^{(ℬ)} /q and e_{2} : V̂(X)^{(𝒜_{2})} /p_{2} → V̂(X)^{(ℬ)} /q. Then, from Lemma 3.2, both e_{1}↾V̂(X)^{⟨𝒜_{1}⟩} /p_{1} and e_{2}↾V̂(X)^{⟨𝒜_{2}⟩} /p_{2} are end extensions.

V̂(X)^{(ℬ)} /q V̂(X)^{(𝒜_{1})} /p_{1}_{e_{1}}  V̂(X)^{(𝒜_{2})} /p_{2}_{e_{2}}  ⟶^{restriction}  V̂(X)^{⟨ℬ⟩} /q V̂(X)^{⟨𝒜_{1}⟩} /p_{1}  _{e_{0}} or V̂(X)^{⟨𝒜_{2}⟩} /p_{2}_{e_{0}}  .

Since both 𝒜_{1} and 𝒜_{2} satisfy ccc, the radii of the bounded Boolean ultrapowers V̂(X)^{⟨𝒜_{1}⟩} /p_{1} and V̂(X)^{⟨𝒜_{2}⟩} /p_{2} are at most ℵ_{1} by Lemma 4.2. Then, from Lemma 4.3, there is a bounded elementary embedding e_{0} : V̂(X)^{⟨𝒜_{1}⟩} /p_{1} → V̂(X)^{⟨𝒜_{2}⟩} /p_{2} or e_{0} : V̂(X)^{⟨𝒜_{2}⟩} /p_{2} → V̂(X)^{⟨𝒜_{1}⟩} /p_{1} that makes the diagram above commute. Suppose that there is e_{0} : V̂(X)^{⟨𝒜_{1}⟩} /p_{1} → V̂(X)^{⟨𝒜_{2}⟩} /p_{2} such that e_{1} = e_{2} ∘ e_{0}. From Theorem 3.3, let e: V̂(X)^{(𝒜_{1})} /p_{1} → V̂(X)^{(𝒜_{2})} /p_{2} be a unique extension of e_{0}. Since e_{2} ∘ e is a bounded elementary embedding of ultrasheaves, e_{2} ∘ e must coincide with e_{1}.

V̂(X)^{⟨ℬ⟩} /q V̂(X)^{⟨𝒜_{1}⟩} /p_{1} _{e_{0}} V̂(X)^{⟨𝒜_{2}⟩} /p_{2} ⟶^{extension}  V̂(X)^{(ℬ)} /q V̂(X)^{(𝒜_{1})} /p_{1}_{e_{1}}  _{e}  V̂(X)^{(𝒜_{2})} /p_{2}_{e_{2}}  .

Then e is standardizable. In fact, let y be a set relative to V̂(X)^{(𝒜_{2})} /p_{2} and let s ∈ V̂(X)^{(𝒜_{1})} /p_{1} be the standardization of e_{2}(y) by e_{1}. We have that, for any x ∈ V̂(X)^{(𝒜_{1})} /p_{1},

e(x) ∈ y ⟺ e_{1}(x) = e_{2}(e(x)) ∈ e_{2}(y),
x ∈ e^{−1}“ y ⟺ x ∈ e_{1}^{−1}“ e_{2}(y) = s.

Thus s is the standardization of y by e. We have shown e is standardizable. Again by the characterization theorem of the Rudin-Frolík order, we have p_{1} ⊑ p_{2}. In case there is e_{0} : V̂(X)^{⟨𝒜_{2}⟩} /p_{2} → V̂(X)^{⟨𝒜_{1}⟩} /p_{1}, we conclude p_{2} ⊑ p_{1} similarly.

5 Conjectures

We have proved that the initial segments of Rudin-Frolík order of the ultrafilters of the complete Boolean algebras with ccc are totally ordered. Now we consider eliminating conditions completeness or ccc.

Against completeness, we have to consider the general nonstandard universes and extend the definition of Rudin-Frolík order. This means the order completion of Rudin-Frolík order. I think that eliminating the condition completeness must be possible.

Against ccc, I state a conjecture here.

Conjecture 5.1. Under the first measurable cardinal, the initial segments Rudin-Frolík order are totally ordered.

In the conjecture above, the first measurable cardinal is derived from that every σ-complete homomorphism of Boolean algebras of sets is complete.

References

[1] C. Chang and J. Keisler, Model Theory, 3rd ed, North-Holland, Amsterdam, (1990).

[2] W. W. Comfort and S. Negrepontis, The theory of ultrafilters, Springer, Berlin, (1974).

[3] Z. Frolík, Sum of ultrafilters, Bull. Amer. Math. Soc., 73 (1967) 87–91.

[4] R. Mansfield, The theory of Boolean ultrapowers, Ann. Math. Logic, 2 (1971) 297–323.

[5] M. Murakami, Standardization principle of Nonstandard universes, Journal of Symbolic Logic, 64, 4(1999), 1645–1655.

[6] M. Ozawa, Forcing in nonstandard analysis, Annals of Pure and Applied Logic, 68 (1994), 263–297.

[7] M. Rudin, Partial orders on the type in β N, Trans. Amer. Math. Soc., 155 No.2 (1971) 353–362.

Atomic incompleteness

Marcus Kracht

                        kracht@math.fu-berlin.de

II Mathematisches Institut, Freie Universität Berlin

Tomasz Kowalski

                          kowalski@jaist.ac.jp

School of Information Science, JAIST

1 Introduction

A standard counterexample in modal logic looks somewhat like this: first conctruct a fancy Kripke frame, then take (some variation on) the algebra of finite and cofinite sets on this frame. It works. Algebraically, one outstanding feature of the algebra produced that way is that it is atomic. This may suggest the following, rather informally stated, conjecture: For any property P that does not hold of all modal logics, P can be falsified on an atomic modal algebra. True to the spirit of the great diagonalisation tradition we will exhibit a property P such that (1) if it does not hold of all modal logics then, by its very nature, it cannot be falsified on an atomic modal algebra, and (2) it indeed does not hold of all modal logics.

Let Λ be a modal logic, ϕ a formula. Further, let V(Λ) stand for the variety of modal algebras corresponding to Λ. Consider the following property:

(P) if ϕ ∉ Λ, then there is an atomic algebra A in V(Λ), with A |̸= ϕ.

Clearly, if there is a modal logic Λ that does not posses (P), then any atomic modal algebra is either not in V(Λ), or else it satisfies ϕ, hence (1) above indeed holds for our (P). All that remains is to show that (P) is not true of all modal logics Λ. Notice, that (P) expressed algebraically reads: V(Λ) is generated by its atomic members. Thus, we need to show that there is a variety of modal algebras not generated by its atomic members. This we will do in two stages. First, we will explicitly construct a variety V of tense algebras not generated by its atomic members. Then, we employ Kracht and Wolter’s simulation technique to produce a variety V^{S} of modal algebras with the same property.

2 Construction

We now proceed to construct a variety V of tense algebras which is not generated by its atomic members. Our V will be generated by a single algebra that is best described in terms of the frame defined below.

For each j ∈ ω and i ∈ {0, …, 2^{j} − 1} define U_{i,j} to be {k : k ≡ i (mod 2^{j})}. Let ℤ be the usual set of integers and ∞ an object not in ℤ. Put 𝕌 = {∞} ∪ ⋃_{i,j∈ℤ} U_{i,j}. The set of points of our frame will be W = 𝕌 ∪ ℤ. Then define the accessibility relation ◁ as follows:

• k ◁ U_{i,j} iff k ∈ U_{i,j} and i ≤ (2^{j} − 1)/2,

• U_{i,j} ◁ k iff k ∈ U_{i,j} and i > (2^{j} − 1)/2,

• U_{i,j} ◁ ∞, for all U_{i,j},

• U_{i,j} ◁ U_{k,l} iff U_{i,j} ⊂ U_{k,l}.

Put 𝔣 = ⟨W, ◁, ◁^{−1}, I⟩, with the family I of internal sets defined as follows: A ∈ I iff A = B ∪C, where B is a finite or cofinite subset of 𝕌 and C is a finite union of some U_{i,j}. Note the double role that sets U_{i,j} play: they are both points of the frame (as members of 𝕌) and internal sets (as subsets of ℤ).

Let I stand for the algebra of internal sets of the frame above. By means of a general algebraic argument, applicable to many more cases, we can prove:

Theorem 1 The variety V(I) is a minimal variety of tense algebras. It is not generated by its atomic members, in fact, it has none.

3 Lifting

Now, we lift the result from the previous section to the case of modal algebras. To do so, we make use of the simulation technique, originated in [1], [2] and developed in [3]. Intuitively, the technique works by associating with each polymodal frame a unimodal frame that consists of as many copies of the original frame as there were modal operators on it. These copies (with some additional points) form the universe of the new simulation frame, and the modal operator is so defined that: (a) it links the copies in a special way that allows to distinguish between them by constant formulas, (b) it behaves on each copy in exactly the way one of the original operators behaved on the original frame.

The same construction can be performed on any polymodal algebra A yielding a simulation algebra A^{S}. Simulation algebras form a rather well-behaved class. They are equationally definable, and given a unimodal simulation algebra B, the polymodal algebra A of which B is a simulation can be read off the structure of B.

For any class K of algebras, let H(K), S(K), P_{U}(K) stand, respectively, for the classes of homomorphic images, subalgebras, and ultraproducts of algebras from K. The key to our lifting procedure is the following slight strengthening of [4] Corollary 9.6:

Lemma 1 If K is a class of simulation algebras, so is SP_{U}(K).

Let V^{S} stand for the variety generated by the class of all simulation algebras of algebras from V, in other words: V^{S} = HSP ({A^{S} : A ∈ V}). With the help of the lemma above, we prove:

Theorem 2 The variety V^{S}(I) is not generated by its atomic members.

References

[1] S.K. Thomason, Reduction of tense logic to modal logic I, Journal of Symbolic Logic 39 (1974), 549–551.

[2] S.K. Thomason, Reduction of tense logic to modal logic II, Theoria 41 (1975), 154–169.

[3] M. Kracht, F. Wolter, Normal monomodal logics can simulate all others, Journal of Symbolic Logic 64 (1999), 99–138.

[4] M. Kracht, Tools and Techniques in Modal Logic, Elsevier Studies in Logic and the Foundations of Mathematics, vol. 142 (1999).

On Quantales

Haruhiko Kozawa

                         matrix@isc.chubu.ac.jp

Graduate School of Engineering, Chubu University

Introduction

Propositional system and Hilbert space

We shall call a question every experiment leading to alternative of which the terms are “yes” and “no”. When the physical system has been prepared in such a way that physicist may affirm that in the event of an experiment the result will be “yes”, we shall say that the question is true. For certain pairs of questions β, γ, one may have following property: “If the physical system is prepared in such a way that β is ture, then one is sure that γ is ture.” We shall denote it as β < γ. By definition, two questions β and γ are equivalent if one has β < γ and γ < β. We shall name a proposition, and denote by b, the equivalent class containing the quesiton β. Then, the set of propositions L is a lattice which is complete, orthocomplemented, and weakly moduar. We call it a propositional system. In propositional system L, two propositions b and c are said to be compatible if the sublattice generated by {b, b^{⊥}, c, c^{⊥}} is distributive.

Let ℙ(H) be the set of projection of Hilbert space H. If P_{1}, P_{2} ∈ ℙ(H)and K = P_{1}(H), L = P_{2}(H), then we define

1. P_{1} < P_{2} if and only if K ⊂ L

2. P_{1} ∨ P_{2} is projection of H onto K ∨ L.

3. P_{1} ∧ P_{2} is projection of H onto K ∩ L.

Then, ℙ(H) is complete lattice, and it is easy to verify the weak modularity relation. In ℙ(H), commutativity is completely equivalent to compatibility. Thus, ℙ(H) is the lattice which is which is complete, orthocomplemented, and weakly moduar.

By generalizing these results, the propositional systems can always realized by the lattice of closed subspaces of a generalized Hilbert space.

A Quantale

A quantale is a complete lattice Q with an associative binary operation & which is distribution over arbitrary joins:

a& ⋁ S = ⋁{a&s | s ∈ S} (⋁ S)&a = ⋁{s&a | s ∈ S}

Now, we consider a quantale Q(ℙ(H)) where

Q(ℙ(H)) = {φ : ℙ(H) → ℙ(H) | (⋁_{i} P_{i})φ = ⋁_{i}(P_{i})φ, ∀{P_{i}} ⊂ ℙ(H)}

and we shall show that ℙ(H) is embedded in Q(ℙ(H)). The multiplication operater & on Q(ℙ(H)) is interpreted as “ and then ”.

We review the quantales in C.J.Mulvey and J.W.Pelletier[4] in this paper.

Quantales

Definition 1 A complete lattice Q with an associative binary operation & is called a quantale if

a&(⋁ b_{i}) = ⋁(a&b_{i})
(⋁ a_{i})&b = ⋁(a_{i}&b)
∀a, b, a_{i}, b_{i} ∈ Q.

We denote the top and the bottom elements of Q by 1 and 0 respectively,

⋁ Q = 1, ⋁ ∅ = 0.

Definition 2 A quantale Q is said to be unital if there exits a unit element e ∈ Q satisfying

e&a = a = a&e ∀a ∈ Q.

Definition 3 A quantale Q with a unary operation *, ⟨Q, ∗⟩ is said to be involutive if

a^{∗∗} = a
(a&b)^{∗} = b^{∗}&a^{∗}
(⋁ a_{i})^{∗} = ⋁ a_{i}^{∗}.

Definition 4 An element a ∈ Q of quantale Q is said to be right-sided if

∀b ∈ Q(a&b ≤ a).

Similary, a ∈ Q of quantale Q is said to be left-sided if b&a ≤ a for all b ∈ Q. We denote R(Q) and L(Q), respectively the subsets of right-sided and of left-sided elements of Q.

Definition 5 A unital and involutive quantale ⟨Q, &, ∗, e⟩ is called a Gelfand quntale if

a&a^{∗}&a = a ∀a ∈ R(Q).

The right(left)-adjoint of & is denoted by →_{r} (→_{l}):

(a →_{r} b) = ⋁{x ∈ R(Q) | a&x ⩽ b}

(a →_{l} b) = ⋁{x ∈ L(Q) | x&a ⩽ b}

Then we have

a&(a →_{r} b) ⩽ b; (a →_{l} b)&a ⩽ b.

If a ∈ R(Q), then a^{∗} →_{r} 0 is R(Q) and denoted by a^{⊥}; if a ∈ L(Q), then a^{∗} →_{l} 0 is L(Q) and denoted

by ^{⊥}a.

lemma 6 ([4]) For any Gelfand quantale Q, the R(Q) of right-sided elements is a quantale, and has the following properties:

1. a&a = a 2. a ∧ b ≤ a^{∗}&b

3. a ∧ a^{⊥} = 0 for every a, b ∈ Q. Proof quantale: For any a_{i} ∈ R(Q)∀i and any c ∈ Q, then

(⋁_{i} a_{i})&c = ⋁_{i}(a_{i}&c)
≤ ⋁_{i} a_{i}.

Then, ⋁_{i} a_{i} ∈ R(Q). Similary, ⋀_{i} a_{i} ∈ R(Q). Thus, R(Q) is a complete lattice. Since R(Q) ⊆ Q, R(Q) is clearly a quantale.

a&a=a: For any a ∈ R(Q), we have a&a ≤ a = a&a^{∗}&a ≤ a&a. a∧b≤ a^{∗}&b: Since a^{∗}&a is left-sided, a = a&a^{∗}&a ≤ 1&a^{∗}&a ≤ a^{∗}&a. Thus,

a ∧ b ≤ (a ∧ b)^{∗}&(a ∧ b) ≤ a^{∗}&b.

a∧a^{⊥} =0:

a ∧ a^{⊥} ≤ a^{∗}&a^{⊥} = a^{∗}&(a^{∗} →_{r} 0) = 0

□

Theorem 7 ([4]) For some Hilbert space H, Q(ℙ(H)) is the quantale of sup-preserving mappings from sup-lattice ℙ(H) to itself.

Q(ℙ(H)) = {φ : ℙ(H) → ℙ(H) | (⋁_{i} P_{i})φ = ⋁_{i}(P_{i})φ, ∀{P_{i}} ⊂ ℙ(H)}

forms a Gelfand quantale, where

φ ≤ ψ \underleftrightarrow{def} (M)φ ≤ (M)ψ for allM ∈ ℙ(H)
(M)(⋁_{i} φ_{i}) {def \atop =} ⋁_{i}(M)φ_{i} for all M ∈ ℙ(H)
(M)φ&ψ {def \atop =} ((M)φ)ψ for all M ∈ ℙ(H)
(M)φ^{∗} {def \atop =} (⋁\{N ∈ ℙ(H) | (N)φ ≤ M^{⊥}\})^{⊥} for all M ∈ ℙ(H)
(M)e {def \atop =} M for all M ∈ ℙ(H).

Proof We define λ_{M}, for M ∈ ℙ(H) by

(N)λ_{M} = \{ \begin{matrix}0 & if N ≤ M \\ H & otherwise. \end{matrix}

It is clear that λ_{M} is a sup-preserving mapping from ℙ(H) to ℙ(H) and that

λ_{M}&φ ≤ λ_{M}

for all φ ∈ Q(ℙ(H)). Moreover, if φ is any right-sided element of Q(ℙ(H)), we must φ&1 ≤ φ where

(N)1 = \{ \begin{matrix}0 & if N = 0 \\ H & otherwise. \end{matrix}

Then, clearly φ must be of the form λ_{M}, where

M = ⋁{N ∈ ℙ(H) | (N)φ = 0}.

Thus, sup-preserving mappings of the form λ_{M} are the right-sided elemnts of Q(ℙ(H)). Similary, suppreserving mappings of the form κ_{M} are the left-sided elemnts of Q(ℙ(H)), where

(N)κ_{M} = \{ \begin{matrix}0 & if N = 0 \\ M & otherwise. \end{matrix}

Now we shall show that Q(ℙ(H)) is Gelfand quantale, that is, that

λ_{M}&λ_{M}^{∗}&λ_{M} = λ_{M}

for all M ∈ ℙ(H), turns on the fact λ_{M}^{∗} = κ_{M^{⊥}}. For, by definition

(N)λ_{M}^{∗} = ( ⋁_{(L)λ_{M} ≤N^{⊥}} L)^{⊥}.

Since (L)λ_{M} ≤ N^{⊥} when N = 0 and L is any projection on H or when N ≠ 0 and L ≤ M, we see that for N = 0

(0)λ_{M}^{∗} = H^{⊥} = 0

and for N ≠ 0

(N)λ_{M}^{∗} = M^{⊥}

which shows that

λ_{M}^{∗} = κ_{M^{⊥}}.

This completes the proof of the thorem, since it is easy to see that λ_{M}&κ_{M^{⊥}}&λ_{M} = λ_{M}. □

From this proof, the operation ^{∗} is an isomorphism from R(Q(ℙ(H))) onto L(Q(ℙ(H))).

Theorem 8 ([4]) For any Hilbert space H, the mapping

χ : ℙ(H) → R(Q(ℙ(H)))

defined by

(M)χ = λ_{M^{⊥}}

is an isomorphism of orthocomplemented sup-lattice.

Proof First, we shall show surjective. From previous theorem’s proof, if φ ∈ R(Q(ℙ(H))), then

φ = λ_{M}
M = ⋁{N ∈ ℙ(H) | (N)φ = 0}.

Since ℙ(H) is orthocomplemented sup-lattice, we have M, M^{⊥} ∈ ℙ(H). That is,

∃M^{⊥} ∈ ℙ(H)(M^{⊥})χ = λ_{M^{⊥⊥}} = λ_{M}.

Therefore, mapping χ is surjective. It is injective, because if M ≤ N and M ≠ N, then

(M^{⊥})λ_{M^{⊥}} = 0, (M^{⊥})λ_{N^{⊥}} = 1

and if M ≰ N, then

(N^{⊥})λ_{M^{⊥}} = 1, (N^{⊥})λ_{N^{⊥}} = 0.

The mapping χ preserves order, since

M ≤ N ⇒ N^{⊥} ≤ M^{⊥} ⇒ λ_{M^{⊥}} ≤ λ_{N^{⊥}} ⇒ (M)χ ≤ (N)χ.

Finally, we note that

(M^{⊥})χ = λ_{M^{⊥⊥}} = (λ_{M^{⊥}})^{⊥} = ((M)χ)^{⊥}.
□

From this theorem, it follows that ℙ(H) is extended to Gelfand quantale Q(ℙ(H)). The quantale valued logic is the logic for propositions represented by Gelfand quantale Q(ℙ(H)).

References

[1] C.Piron, Fundations of Quantum Pysics, W.A.Benjamin, Inc. 1976

[2] David W. Cohen, An Introduction to Hilbert space and Quantum Logic, Springer-Verlag New York Inc. 1989

[3] 竹内外史線形代数と量子力学裳華房 1981

[4] Christopher J. Mulvey and Joan Wick Pelletier, A Quantisation of the Calculus of Relations, Canadian Mathematical Society Conference Proceeding Volume 13, 1992 pp.345-360

Quantale valued set theory

Satoko Titani

                           titani@chubu.ac.jp

Chubu University

Introduction

Observation of a physical system is described by using a Hilbert space. States of the physical system are represented as vectors of the Hilbert space H, and observables (physical quantities) are represented as self-adjoint operators on H. A proposition in quantum theory, which is considered as a property of states, are represented as a projection p on H such that

“The proposition is true in state x” is certain if and only if x is in the range of p

Projections on a Hilbert space H form a complete orthomodular lattice with respect to the inclusion of their ranges. We denote the complete orthomodular lattice by ℙ(H).

In [4] and [6], G.Takeuti developed the quantum set theory on the ℙ(H)-valued universe V^{ℙ(H)}.

V_{α}^{ℙ(H)} = {u | ∃β <α ∃Du⊂V_{β}^{ℙ(H)}(u : Du → ℙ(H))}
V^{ℙ(H)} = ⋃_{α∈On} V_{α}^{ℙ(H)}

In his quantum set theory, he defined implication →_{q} by

φ →_{q} ψ \underleftrightarrow{def} φ^{⊥} ∨ (φ ∧ ψ),

and defined the interpretation of equality =_{q} by

[[u =_{q} v]] = ⋀_{x∈Du}(u(x) →_{q} [[x ∈_{q} v]]) ∧ ⋀_{x∈Dv}(v(x) →_{q} [[x ∈_{q} u]])
[[u ∈_{q} v]] = ⋁_{x∈Dv}[[u =_{q} x]] ∧ v(x).

The operation →_{q} is an implication in the sense that

[[φ ∧ (φ →_{q} ψ)]] ⩽ [[ψ]].

But, unfortunately,

[[φ ∧ ψ]] ⩽ [[ξ]] does not imply [[φ]] ⩽ [[ψ →_{q} ξ]],

because of non-distributivity of ℙ(H). It follows that the transitivity of =_{q} is not valid in the quantum

set theory on V^{ℙ(H)}.

The aim of this paper is to review the concepts of implication and equality in the universe V^{ℙ(H)}. We extend the orthomodular lattice ℙ(H) to a quantale. Quantale is a complete lattice Q with associative binary operation & which is distributive over arbitrary joins (Definition 1). Then we introduce the rightadjoint →_{r} of & as an implication on Q. The equality =_{r} corresponding to & satisfies the transitivity. The quantale Q is defined as an algebra consisting of sup-preserving mappings φ : p ↦ (p)φ from ℙ(H) to itself.

Q = {φ : ℙ(H) → ℙ(H) | (⋁ P)φ = ⋁{(p)φ | p ∈ P } for arbitrary P ⊂ ℙ(H)}.

Q is a Gelfand quantale with respect to composition & of operations, and ℙ(H) is embedded in Q as the subquantale R(Q) of right-sided elements (Theorem 1),

ℙ(H) ≅ R(Q) = {φ ∈ Q | φ&1 ⩽ φ} ⊂ Q,

The operator & on Q is interpreted as “and then”.

In [7] we formulated a lattice valued logic and a lattice valued set theory, by introducing a strong implication, which represents the lattice order ⩽. The lattice valued logic is the logical counterpart of general complete lattices. The completeness of the lattice valued logic was proved by Takano [5]. For an arbitrary complete lattice L, we can construct a L-valued universe V^{L}. The lattice valued set theory on the universe V^{L} was formulated as a set theory based on the lattice valued logic.

Now we take Q as the complete lattice L, and consider the quantale valued set theory V^{Q}. Q-valued logic is obtained from a lattice valued logic by adding new logical operations such as &, ^{∗}, →_{r}, →_{l}, and new inference rules for them.

Since the orthocomplemented sup-lattice ℙ(H) can be embedded in Q, V^{ℙ(H)} is considered as a subuniverse of V^{Q}. Similarly, ℙ(H) can be embedded in Q as the subquantale L(Q) of left-sided elements,

L(Q) = {φ ∈ Q | 1&φ ⩽ φ}.

This means that there are two isomorphic subuniverses V^{R(Q)} and V^{L(Q)} of V^{Q}, which are mutually conjugate.

In section 1 we briefly review the quantales in C.J.Mulvey and J.W.Pelletier [2], and then, in section 2, discuss the quantale valued set theory on V^{Q}.

1 Quantales

Definition 1 A sup-lattice (complete lattice) Q with an associative binary operation & is called a quantale, if the operation & is distributive over arbitrary joins:

a& ⋁ S = ⋁{a&s | s∈S}, (⋁ S)&a = ⋁{s&a | s∈S} for S ⊂ Q.

We denote the top and the bottom elements of Q by 1 and 0, respectively.

⋁ Q = 1, ⋁ ∅ = 0.

Definition 2 A quantale Q is said to be unital if there exists a unit element e in Q such that

e&a = a = a&e for all a ∈ Q

Definition 3 An element a ∈ Q of a quantale Q is said to be right-sided (respectively, left-sided) if

a&1 ⩽ a (respectively, 1&a ⩽ a).

The set of right-sided elements (respectively, left-sided elements) of Q is denoted by R(Q) (respectively, L(Q)).

R(Q) {def \atop =} \{a∈Q | a&1 ⩽ a\}, L(Q) {def \atop =} \{a∈Q | 1&a ⩽ a\}

R(Q) and L(Q) are subquantale of Q. The quantale Q is said to be right-sided (respectively, left-sided), if every a ∈ Q is right-sided (respectively, left-sided).

The right(left)-adjoint of & is denoted by →_{r} (→_{l}) :

(a →_{r} b) {def \atop =} ⋁\{x ∈ R(Q) | a&x ⩽ b\} ; (a →_{l} b) {def \atop =} ⋁\{x ∈ L(Q) | x&a ⩽ b\}.

Definition 4 Unary operation ^{∗} on a quantale Q is called an involution if 1. a^{∗∗} = a

2. (a&b)^{∗} = b^{∗}&a^{∗}

3. (⋁_{α} a_{α})^{∗} = ⋁_{α} a_{α}^{∗}. A quantale with an involution ^{∗} is called involutive quantale. If a ∈ R(Q), then (a^{∗} →_{r} 0) is an element R(Q) and denoted by a^{⊥} .

Definition 5 A unital and involutive quantale Q = (Q, ⋁, &,^{∗}, e) is called Gelfand quantale, if

a&a^{∗}&a = a for all a∈R(Q)

Lemma 1.1 ([2]) For any Gelfand quantale Q, the set R(Q) of right-sided elements is a Gelfand quantale with respect to the operations of Q, and has the following properties:

a&a = a,  a ∧ b ⩽ a^{∗}&b,  a ∧ a^{⊥} = 0  for every a, b ∈ R(Q).

Let L be an orthocomplemented sup-lattice, that is, L = (L, ⋁,^{⊥}) is a sup-lattice with operation ^{⊥} such that, for all x ∈ L and {x_{α}} ⊂ L,

x^{⊥⊥} = x,  (⋁_{α} x_{α})^{⊥} = ⋀_{α} x_{α}^{⊥},  x ∨ x^{⊥} = 1, x ∧ x^{⊥} = 0.

Then the set Q(L) of sup-preserving mappings from L to itself, φ : x ↦ (x)φ,

Q(L) = {φ:L→L | (⋁_{α} x_{α})φ = ⋁_{α}(x_{α})φ for all {x_{α}} ⊂ L},

forms a Gelfand quantal with respect to ⩽, ⋁, &, ^{∗}, e defined by

φ ⩽ ψ \underleftrightarrow{def} (x)φ ⩽ (x)ψ for all x∈L
(x)(⋁_{α} φ_{α}) {def \atop =} ⋁_{α}(x)φ_{α} for all x∈L
(x)(φ&ψ) {def \atop =} ((x)φ)ψ for all x∈L
(x)φ^{∗} {def \atop =} (⋁\{t∈L | (t)φ ⩽ x^{⊥}\})^{⊥} for all x∈L
(x)e {def \atop =} x for all x∈L

Theorem 1 ([2]) An orthocomplemented sup-lattice L is embedded in the Gelfand quantale Q(L) consisting of all sup-preserving mappings from L to itself :

L ≅ R(Q(L)) ⊂ Q(L).

Now, as L in the above Theorem 1, we take the orthocomplemented sup-lattice ℙ(H) consisting of projections on a Hilbert space H. The lattice ℙ(H) is extended to Gelfand quantale Q(ℙ(H)) by the Theorem 1. We denote the Gelfand quantale Q(ℙ(H)) simply by Q, and consider a quantale valued set theory on the Q-valued universe. Truth values of propositions in quantale valued set theory are considered as elements of Gelfand quantale Q.

On Q, we have three implications, →_{r}, →_{l}, and the basic implication → of lattice valued logic ;

a → b = \begin{cases}1 & if a ⩽ b \\ 0 & otherwise \end{cases} .

For the right-implication →_{r}, and for a, b, c ∈ R(Q), we have :

(1) a&(a →_{r} b) ⩽ b and (2) a&b ⩽ c implies b ⩽ (a →_{r} c)

→_{l} has the symmetric property.

2 Quantale valued set theory

2.1 Language of quantale valued set theory

Primitive symbols are :

1. individual variables x, y, z, ⋯

2. propositional constant E

3. predicate constants =, ∈,

4. logical symbols ∧, ∨, ¬, →, ∀, ∃, &, ^{∗}, →_{r}, →_{l}.

5. parentheses (, )

Propositional constant E and expressions of the form t_{1} = t_{2} or t_{1} ∈t_{2} with individual variables t_{1}, t_{2} are atomic formulas. Formulas are constructed from atomic formulas, by using the logical symbols. To denote formulas, we use φ, ψ, ξ, ⋯, φ(x), · · ·.

2.2 Quantale valued universe V^{Q}

Let Q = (Q, ⋁, &,^{∗} , e) be a Gelfand quantale. Q-valued universe V^{Q} is constructed by induction.

V_{α}^{Q} = {u | ∃β <α ∃Du⊂V_{β}^{Q}(u : Du → Q)}
V^{Q} = ⋃_{α∈On} V_{α}^{Q}

The least ordinal α such that u∈V_{α}^{Q} is called the rank of u, and the truth value of a formula φ is denoted by [[φ]]. u = v and u∈v for u, v ∈V^{Q} are interpreted by induction on rank of u, v.

[[u=v]] = ⋀_{x∈Du}(u(x) → [[x∈v]]) ∧ ⋀_{x∈Dv}(v(x) → [[x∈u]])
[[u∈v]] = ⋁_{x∈Dv}[[u=x]] ∧ v(x)

E is interpreted as the unit e of Q, [[E]] = e. Logical operations ∧, ∨, &, →, ∀x, ∃x, involution ^{∗}, and right- and left-implications →_{r}, →_{l} are interpreted as the corresponding operators on Q.

[[φ_{1} ∧ φ_{2}]] = [[φ_{1}]] ∧ [[φ_{2}]] ; [[φ_{1} ∨ φ_{2}]] = [[φ_{1}]] ∨ [[φ_{2}]] ; [[φ_{1} → φ_{2}]] = [[φ_{1}]] → [[φ_{2}]] [[∀xφ(x)]] = ⋀_{u∈V^{Q}}[[φ(u)]] ; [[∃xφ(x)]] = ⋁_{u∈V^{Q}}[[φ(u)]] [[φ_{1}&φ_{2}]] = [[φ_{1}]]&[[φ_{2}]] ; [[φ^{∗}]] = [[φ]]^{∗}

[[φ →_{r} ψ]] = [[φ]] →_{r} [[ψ]] ; [[φ →_{l} ψ]] = [[φ]] →_{l} [[ψ]]

In the lattice valued set theory, [[u=v]] is 1 or 0, and hence, [[u=v]] ∧ ⋁_{k} b_{k} = ⋁_{k}[[u=v]] ∧ b_{k} for u, v ∈V^{Q} and {b_{k}}_{k} ⊂ Q. It follows that equality axioms holds. Since Q is a complete lattice, all axioms of lattice valued set theory are valid on V^{Q}.

For the right-implications →_{r}, the corresponding equality =_{r} and membership relation ∈_{r} are defined by:

u =_{r} v \underleftrightarrow{def} ∀x(x∈u →_{r} x ∈_{r} v) ∧ ∀x(x∈v →_{r} x ∈_{r} u)
u ∈_{r} v \underleftrightarrow{def} ∃x((x =_{r} u)&x∈v)

Lemma 2.1 If u, v ∈ V^{R(Q)}, then [[u =_{r} v]] and [[u ∈_{r} v]] are elements of R(Q).

Theorem 2 (Equality axioms) If u, v, w ∈ V^{R(Q)}, then

[[u =_{r} v]]&[[v =_{r} w]] ⩽ [[u =_{r} w]]
[[u =_{r} v]]&[[v ∈_{r} w]] ⩽ [[u ∈_{r} w]]
[[u ∈_{r} v]]&[[v =_{r} w]] ⩽ [[u ∈_{r} w]]

Definition 6 For u ∈ V^{Q}, we define the restriction u|p ∈ V^{Q} of u to p by

D(u|p) = Du, (u|p)(x) = [[x∈u]]&p

Theorem 3 If p is a right-sided element of Q, i.e. p ∈ R(Q), and u, v ∈ V^{R(Q)}, then p ⩽ [[u =_{r} v]] if and only if [[u|p = v|p]] = 1

Proof By using Theorem 2 and distributiveity of & over ⋁.

References

[1] R.V.Kadison and J.R.Ringrose, Fundamentals of Theory of Operator Algebras, AMS 1997

[2] C.J.Mulvey and J.Wick Pelletier, Quantization of the Calculus of Relations, Canadian Mathematical Society, Conference Proceeding, Vol. 13, 1992.

[3] C.Piron, Foundations of Quantum Physics, W.A. Benjamin, Inc. 1976

[4] G.Takeuti, Two Applications of Logic to Mathematics, Iwanami and Princeton University Press, Tokyo and Princeton (1978).

[5] Mitio Takano, Strong Completeness of Lattice Valued Logic

[6] G.Takeuti, Quantum Set Theory, Current Issues in Quantum Logic, eds. E.Beltrametti and B.C.van Frassen, Plenum,New York (1981) pp.303-322

[7] S.Titani, Lattice Valued Set Theory, Arch. Math. Logic 38-6(1999) pp.395-421