A modified subformula property for the modal logic K5

Motio Takano

takano@ed.niigata-u.ac.jp

Department of Mathematics, Niigata University

This paper is not included in this on-line proceedings.

2

A Natural Deduction for Classical Logic, in which there exists a proof with the Subformula Property

Yuichi KOMORI

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

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

In this note, we will pose a new system, named μ–calculus. λ–calculus can be simulated in μ–calculus. While the type assignment system T A_{λ} gives a natural deduction for implicational intuitionistic logic, the type assignment system T A_{μ} gives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem α there exists a proof of α in T A_{μ} enjoying the subformula property.

Ryo Kashima has posed a Natural deduction system for the classical implicational logic. His system has three rules, the elimination of the implication, the introduction of the implication and the case rule. The author has noticed that the introduction of the implication is derivable from the case rule and the weakening. So we have gotten the system T A_{μ} from Kashima’s system by replacing the introduction of implication by the weakening.

1 The type-free μ-calculus and its type assignment

DEFINITION 1.1 (μ-terms) An infinite sequence of term-variables is assmed to be given. Then linguistic expression called μ-terms are defined thus:

1. each term-variable is a μ-terms, called an atom or atomic term;

2. if M and N are μ-terms then (MN) is a μ-term called an application;

3. if M is a μ-term then KM is a μ-term called a weakening;

4. if x is a term-variable and M and N are μ-terms then (μx.M ∗ N) is a μ-term called an abstract or a μ-abstract.

DEFINITION 1.2 (β-reduction) Any μ-term of form KMN, (μx.M∗N)R, μx.[xMN/z]P ∗Q (where z ∈ F V (P) and x ∉ F V (MP)) or μx.xM ∗ N (where x ∉ F V (M)) is called a β-redex. β-contracting an occurrence of a redex in a term U means replacing one occurence of

KMN  by M ,
(μx.M ∗ N)R by μx.MR ∗ NR (we α-convert (μx.M ∗ N) if necessary),
μx.[xMN/z]P ∗ Q by μx.[xM/z]P ∗ Q (where z ∈ F V (P) and x ∉ F V (MP)),
μx.xM ∗ N  by [M/x]N  (where x ∉ F V (M)).

If this changes U to V, we say U β-contracts to V, or

U ⊳_{1β} V.

We say U β-reduces to V, or

U ⊳_{β} V,

iff V is obtained from U by a finite (perhaps empty) series of β-contractions and changes of bound variables.

CONJECTURE 1.3 (or FACT (Church-Rosser Theorem for β)) If M ⊳_{β} P and N ⊳_{β} Q then there exist T such that

P ⊳_{β} T, Q ⊳_{β} T.

We can consider different types of reductions that have logical reasons, for example,

R(μx.M ∗ N) ⊳_{1} μx.RM ∗ RN.

But the reduction obtained from β-reduction adding the above reduction does not enjoy the Church-Rosser property.

ABBREVIATION 1.4 (λx.M) ≡ (μx.x ∗ KM).

FACT 1.5 (μ-calculus simulates λ-calculus)

(λx.M)N ⊳_{β} [M/x]N.

DEFINITION 1.6 (η-reduction) Any μ-term of form μx.x∗K(Nx) or μx.M ∗N (where x ∉ F V (N)) is called a η-redex. η-Contracting an occurrence of a η-redex in a term U means replacing one occurence of

μx.x ∗ K(Nx) by μx.x ∗ N ,
μx.M ∗ N  by N  (where x ∉ F V (N)) .

If this changes U to V, we say U η-contracts to V, or

U ⊳_{1η} V.

We say U η-reduces to V, or

U ⊳_{η} V,

iff V is obtained from U by a finite (perhaps empty) series of η-contractions and changes of bound variables.

CONJECTURE 1.7 (or FACT (Church-Rosser Theorem for βη)) If M ⊳_{βη}P and N ⊳_{βη}Q then there exist T such that

P ⊳_{βη} T, Q ⊳_{βη} T.

Types are defined as usual.

DEFINITION 1.8 (The type-assignment system T A_{μ}) T A_{μ} is a Natural Deduction system. Its formulas are arbitrary expressions M : α, where M is a μ-term and α is a type.

\begin{matrix}{Π_{1} \atop M : α → β} & {Π_{2} \atop N : α} \\ MN : β \end{matrix} (→ E),  {Π \atop M : β} ; KM : α → β (W eakening),

\begin{matrix}{k \atop x : α → β} ; Π_{1} ; M : γ & {k \atop x : α} ; Π_{2} ; N : γ \\ μx.M ∗ N : γ \end{matrix} k(Case).

FACT 1.9 (T A_{μ} is a proof of classical implicational logic) α is a classical implicational theorem if and only if there exists a closed μ-term M such that ⊢_{μ} M : α.

2 The type-free λA-calculus and its type assignment

We will next introduce an auxiliary type type-assignment system T A_{λA} to prove the subformula property of the system T A_{μ}.

DEFINITION 2.1 (λA-terms) An infinite sequence of term-variables is assmed to be given. Then linguistic expression called λA-terms are defined thus:

1. each term-variable is a λA-terms, called an atom or atomic term;

2. if M and N are λA-terms then (MN) is a λA-term called an application;

3. if M is a λA-term then AM is a λA-term called a r-weakening;

4. if x is a term-variable and M is a λA-terms then (λx.M) is a λA-term called an abstract or a λ-abstract.

DEFINITION 2.2 (Aβ-reduction) Any λA-term of form AMN and (λx.M)N is called a redex. Contracting an occurrence of a redex in a term U means replacing one occurence of

\begin{matrix}AMN & by & AM, \\ (λx.M)N & by & [N/x]M. \end{matrix}

If this changes U to V, we say U Aβ-contracts to V, or

U ⊳_{1Aβ} V.

We say U Aβ-reduces to V, or

U ⊳_{Aβ} V,

iff V is obtained from U by a finite (perhaps empty) series of Aβ-contractions and changes of bound variables.

FACT 2.3 (Church-Rosser Theorem for Aβ) If M ⊳_{Aβ} P and N ⊳_{Aβ} Q then there exist T such that

P ⊳_{Aβ} T, Q ⊳_{Aβ} T.

A ⊥-type is a type constructed from variables and a type constant ’⊥’.

DEFINITION 2.4 (The type-assignment system T A_{λA}) T A_{λA} is a Natural Deduction system. Its formulas are arbitrary expressions M : α, where M is a λA-term and α is a ⊥-type.

\begin{matrix}{Π_{1} \atop M : α → β} & {Π_{2} \atop N : α} \\ MN : β \end{matrix} (→ E),  {k \atop x : α} ; Π ; M : β ; λx.M : α → β k(→ I),

{Π \atop M : ⊥} ; AM : α (R − W eakening).

FACT 2.5 (T A_{λA} is a proof of intutionistic logic) α is a theorem of intutionistic {→, ⊥}-fragment logic if and only if there exists a closed λA-term M such that ⊢_{λA} M : α.

FACT 2.6 (Normalization Theorem for T A_{λA}) Every T A_{λA}-typable term has a Aβ-normal form.

FACT 2.7 (Subformula Property for T A_{λA}) Let λA-term M be a Aβ-normal form and Δ a T A_{λA}- deduction of M : α. Then every type in Δ has an occurence in α or in a predicate of undischarged assumptions.

3 Transelation of λA-terms to μ-terms

In this section we will define a translation 𝒯 of λA-terms to μ-terms. At first, we define a simple translation 𝒯 ^{∗} of λA-terms without occurences of A to μ-terms. DEFINITION 3.1 (Translation 𝒯 ^{∗}) We define recursively the translation 𝒯 ^{∗} of λA-terms, in which no A occurs, to μ-terms, as follows:

1. 𝒯 ^{∗}(x) ≡ x,

2. 𝒯 ^{∗}(MN) ≡ (𝒯 ^{∗}(M)𝒯 ^{∗}(N)),

3. 𝒯 ^{∗}(λx.M) ≡ (μx.x ∗ K𝒯 ^{∗}(M)). DEFINITION 3.2 (Translation 𝒯 ) We define recursively the translation 𝒯 of λA-terms of the form AM to μ-terms, as follows:

1. 𝒯 (AM) ≡ 𝒯 ^{∗}(M) if no A occurs in N,

2. 𝒯 (AM) ≡ 𝒯 (AN) if M is of the form (⋯ AN ⋯) where this A is the leftmost occurence and no free variable in N is bounded in M,

3. 𝒯 (AM) ≡ μx.𝒯 (AN) ∗ 𝒯 (AR) if M is of the form (⋯ (λx. · · · AQ ⋯) ⋯) where this A is the leftmost occurence and this ’λx’ is the leftmost occurence which bounds a free variable in Q and N is obtained from M by replacing (λx. · · · AQ ⋯) by x (we α-convert M if necessary) and R ≡ (⋯ (λz. · · · AQ ⋯) ⋯) and the variable z is new.

4 Proof of Subformula Property

LEMMA 4.1 Let M be a Aβ-normal term without occurences A, Γ ⊢_{λA} M : α and g be a new type variable. Then

1. [g/⊥]Γ ⊢_{μ} 𝒯 ^{∗}(M) : [g/⊥]α,

2. every type in T A_{μ}-deduction of 𝒯 ^{∗}(M) : [g/⊥]α has an occurence in [g/⊥]α or in a type in [g/⊥]Γ. LEMMA 4.2 Let AM be a Aβ-normal term, Γ ⊢_{λA} M : ⊥ and g be a new type variable. Then

1. [g/⊥]Γ ⊢_{μ} 𝒯 (AM) : g,

2. every type in T A_{μ}-deduction of 𝒯 (AM) : g is g or has an occurence in a type in [g/⊥]Γ. LEMMA 4.3 Let α be a implicational formula and g be the rightmost variable in α. Then α is a classical teorem if and only if [⊥/g]α is an intuitionistic theorem. THEOREM 4.4 (Subformula Property of T A_{μ}) If a type α is a classical implicational theorem, then there exists a closed μ-term M such that

1. ⊢_{μ} M : α,

2. for any T A_{μ}-deduction Δ of M : α, every type in Δ has an occurence in α. Acknowledgement. The author would like to thank Ryo Kashima for informing him of Kashima’s Natural deduction system.

References

[1] J. Roger Hindley. Basic Simple Type Theory, Vol. 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997.

[2] J. Roger Hindley and Jonathan P. Seldin. Introduction to combinators and λ–calculus, Vol. 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986.

Labelled Sequent Calculi and Completeness Theorems for Implicational Relevant Logics

Ryo Kashima

Department of Mathematical and Computing Sciences Tokyo Institute of Technology Ookayama, Meguro, Tokyo 152-8552, Japan.

                             e-mail: kashima@is.titech.ac.jp

This is the first section of the research report “Labelled Sequent Calculi and Completeness Theorems for Implicational Relevant Logics” (No. C-140, Department of Mathematical and Computing Sciences, Tokyo Institute of Technology).

1 Introduction

A natural semantic treatment of relevant logics was given by Urquhart [10]. (See [1], [2] and [4] for information on relevant logics.) Let E be the implicational fragment of the relevant logic E. (In this paper, we treat only “→” (implication) as a logical symbol; therefore, E/R/S4⋯ will denote the implicational fragments of themselves.) An Urquhart’s model for E (we call it an E-model) consists of two structures ⟨I, ·, e⟩ and ⟨W, R⟩ where the former is an idempotent commutative monoid (i.e., semilattice with identity e) and the latter is a quasi-ordered set (i.e., R is a reflexive and transitive relation on W). 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 structure ⟨W, R⟩ is, like a Kripke’s model for modal logics, considered to be a “structure of possible worlds”—W is a set of worlds, and R is an accessibility relation. The notion “α, x ⊧ A” (a formula A holds according to a piece α of information at a world x) is inductively defined by the following.

α, x ⊧ B→C ⟺ ∀β ∈ I, ∀y ∈ W [(xRy) & (β, y ⊧ B) ⇒ (α·β, y ⊧ C)].

We say that a formula A is valid in the model if e, x ⊧ A for any x ∈ W. The completeness theorem, which was shown in [10] (a proof appeared in [2]), claims that a formula A is provable in E if and only if A is valid in any E-model.

The relevant logic R and the logic S4 of “strict implication” are obtained from E by adding, respectively, the axiom schemes

C: (A→(B→C))→(B→(A→C)), and
K^{01}: \overrightarrow{A}→(B→\overrightarrow{A})

where \overrightarrow{A} is an abbreviation for A_{1}→A_{2}; and the intuitionistic logic Int is obtained from E by adding both the schemes C and K^{01} (or, equivalently, Int is obtained from R by adding the scheme K: A→(B→A)). (See, e.g., [1] and [9] for axiomatizations of these logics. The name K^{01} comes from [9], where the superscripts represent certain restrictions by “over-arrows”.) The completeness theorems for these logics were shown as follows. We define two conditions on E-models:

(Single World Condition) The set of possible worlds is a singleton.

(Hereditary Condition) If α, x ⊧ A, then α·β, x ⊧ A.

Then, the logic (R / S4 / Int) is complete with respect to the class of E-models satisfying the condition (Single World / Hereditary / both Single World and Hereditary, respectively). That is, for example, a formula A is provable in Int if and only if A is valid in any E-model that satisfies both the Single World and Hereditary Conditions.

Moreover, such completeness results were shown for other two relevant logics—called E5 and RM0 (the names come from [5] and [1]).

The logic E5 is obtained from E by adding the axiom scheme

C^{001}: (A→(B→\overrightarrow{C}))→(B→(A→\overrightarrow{C})).

(In [5] and [10], the axiom scheme B→((B→\overrightarrow{C})→\overrightarrow{C}) was adopted where this scheme and C^{001} are mutually inferable over E.) The scheme C^{001} is an instance of the scheme C, and therefore E5 is an intermediate logic between E and R. It was shown that the logic E5 is complete with respect to the class of E-models satisfying the following condition.

(Single Cluster Condition) The accessibility relation is universal, that is, xRy for any x, y ∈ W.

Note that this condition is weaker than the Single World Condition.

The logic RM0 is obtained from R by adding the axiom scheme

M: A→(A→A).

This scheme is an instance of the scheme K, and therefore RM0 is an intermediate logic between R and Int. It was shown that the logic RM0 is complete with respect to the class of E-models satisfying both the Single World Condition and the following condition.

(Mingle Condition) If α, x ⊧ A and β, x ⊧ A, then α·β, x ⊧ A.

Note that the Mingle Condition is weaker than the Hereditary Condition.

[figure: Figure 1; E; EM^{#}; S4; E5; E5M^{#}; S5I; R; RM0; Int; +M^{#}; +K^{01} (K^{01}); +C^{001}; +C; Mingle Condition; Hereditary Condition; E-models /; Linear Order E-models; Single Cluster E-models; Single World E-models]

To sum up, it has been shown that the six logics E, E5, R, RM0, Int, and S4, which are located on the edges of the diagram in Figure 1, are complete with respect to the class of E-models with the additional conditions. (See [2], [5] and [10] for the proofs.) Then, bringing the diagram to completion is a natural requirement. In other words, there are two questions: (Q1) Is there an axiom scheme A that satisfies the following?

• The logic E+A is complete with respect to the class of E-models satisfying the Mingle Condition.

• The logic E5+A is complete with respect to the class of E-models satisfying both the Single Cluster Condition and the Mingle Condition.

• The logic R+A is equivalent to RM0.

(Q2) Is the logic S5I = S4+C^{001} complete with respect to the class of E-models satisfying both the Single Cluster Condition and Hereditary Condition? (We will account for the name S5I later.)

This paper gives positive answers to these questions. (It is somewhat surprising that such a natural question has been open.) For Q1, the required scheme A is

M^{#}: (\overrightarrow{A}→B)→(\overrightarrow{A}→(B→B)),

and the logics E+M^{#} and E5+M^{#} are denoted by EM^{#} and E5M^{#}, respectively. (Note that M^{#} is an instance of the scheme

K^{01}: (\overrightarrow{A}→B)→(\overrightarrow{A}→(C→B))

while this scheme and K^{01} are mutually inferable over E; see Section 2.) Moreover we show a strong version of the completeness of E/EM^{#}/S4, which claims that these logics are complete with respect to the linear order E-models. That is, for example, a formula A is provable in S4 if and only if A is valid in any E-model in which the accessibility relation is a linear order and the Hereditary Condition holds. These complete the diagram in Figure 1, which shows a nice correspondence between simple axiom schemes and natural conditions on models.

An outline of the proof of the completeness is as follows. For each logic X = E, EM^{#}, …, we introduce two systems GX and LX. The system GX is an ordinary “sequent calculus”, and it is easy to show that a “sequent” A_{1}, …, A_{n} ↦ B is provable in GX if and only if the formula A_{1}→(⋯ →(A_{n}→B) ⋯) is provable in X. The system LX is a “labelled sequent calculus”, that is, a system to treat “labelled sequents”—sequents consisting of labelled formulas where a label reflects the structure of E-models. By a standard way, we show that LX is complete with respect to the class of E-models satisfying the additional conditions for X. In particular, if a formula A is valid in any E-model of X, then the labelled sequent “⇒ (∅, 0):A”, which consists of A and the “empty label” (∅, 0), is provable in LX. Then, the following claim completes the proof of the completeness.

If the labelled sequent ⇒ (∅, 0):A is provable in LX, then the unlabelled sequent ↦ A is provable in GX.

This is proved by showing a stronger claim:

If a labelled sequent S is provable in LX, then an unlabelled sequent T is provable in GX where T is “extracted” from S in a certain way.

Since unlabelled sequents have less expressive power than labelled sequents, this “extraction” is somewhat complicated; and proving this claim is the hardest (and the most interesting) part of the proof of the completeness theorem. There have been a lot of studies on labelled sequent calculi (e.g. see [7] and [8]). Among them, the author thinks, this paper is a good example of an application of labelled sequent calculi to solve important problems on the logics, which are independent from the labelled systems.

The completion of the diagram in Figure 1 induces further questions, for which the author does not have any nontrivial answers now: (1) There are a lot of possible conditions on E-models. Is there a corresponding axiom scheme for each condition? For example, if the models lack the condition α·α = α (idempotence), the corresponding logics might be axiomatized by deleting the scheme W: (A→(A→B))→ (A→B). Is this true for each logic in the diagram? (2) Introducing other connectives (∧, ∨, ¬, …) is an important problem. It was shown ([3], [6]) that the logic R_{→∧∨} with an extra inference rule is complete with respect to the class of models of R in which ∧ and ∨ are interpreted in a natural way. What happens for the other logics in the diagram?

If we get acceptable answers for these questions, Urquhart’s semantics will be a major paradigm of “possible worlds semantics”, while Routley-Meyer’s “ternary relation semantics” (see, e.g., [2] or [4]) is major now. The diagram in Figure 1 is a starting point.

We make remarks about the scheme M^{#} and the logic S5I. In literature (see, e.g., [1] or [4]), the axiom scheme M′: \overrightarrow{A}→(\overrightarrow{A}→\overrightarrow{A}) was suggested as a “Mingle for E”. But the author thinks the scheme M^{#} is the very axiom of “Mingle for E” because of its completeness with respect to the class of E-models satisfying the Mingle Condition. (M′ is inferable from M^{#} (by B:= \overrightarrow{A}), but the author does not know whether the converse holds.) The name S5I comes from [8]. In [8], a sequent style system for S5I was introduced, whereas the Hilbert style axiomatization S4+C^{001} did not appear. The name S5I reflects the fact that the models of this logic are considered to be the intuitionistic variants of the models for “S5 strict implication”. We will discuss this fact in Section 3.

The plan of this paper is as follows. Let X = {E, EM^{#}, S4, E5, E5M^{#}, S5I} (the six logics in the bottom and the middle rows in Figure 1). In Section 2, we introduce implicational relevant logics by Hilbert-style axiomatizations; and then we introduce six Gentzen-style sequent calculi named GX for X ∈ X. In Section 3, we define the E-models and prove that the Hilbert-style systems are sound with respect to the class of E-models with the additional conditions. In Section 4, we introduce labelled sequent calculi named LX for X ∈ X, and prove their completeness with respect to the class of E-models with the additional conditions. In Section 5, we show the “extraction” from the labelled sequent calculi LX into the unlabelled sequent calculi GX. Finally, in Section 6, we state the main results of this paper—completeness of the six logics in X.

References

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

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

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

[4] J. M. Dunn, Relevance Logic and Entailment, in Handbook of Philosophical Logic, Vol. III (edited by D. Gabbay and F. Guenthner) (D. Reidel 1986).

[5] K. Fine, Completeness for S5 analogue of E_{I} (abstract), Journal of Symbolic Logic 41, 559-560 (1976).

[6] K. Fine, Completeness for the semilattice semantics with disjunction and conjunction (abstract), Journal of Symbolic Logic 41, 560 (1976).

[7] D. M. Gabbay, Labelled Deductive Systems, Vol.1, (Oxford 1996).

[8] D. M. Gabbay and N. Olivetti, Algorithmic proof methods and cut elimination for implicational logics, part I, Studia Logica 61, 237-280 (1998).

[9] R. Kashima and N. Kamide, Substructural implicational logics including the relevant logic E, Studia Logica 63, 181-212, (1999).

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

Semantics and Cut-free Provability of Modal Substructural Logics

Takafumi SAKURAI

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

Department of Mathematics and Informatics Chiba University

In this paper, we study the model of modal propositional Lambek logics. We give the model similar to the phase space and demonstrate its usefulness by showing the cut-free provability theorem and giving the Kripke semantics.

1 Preliminaries

For the definitions of Lambek logic FL_{σ}, FL_{σ}-algebra, so_{σ}-monoid, modal Lambek logic FL_{σ}^{m}, and modal FL_{σ}-algebra, we refer Ono [3].

2 Construction by Filter

We can construct so_{σ}-monoid from FL_{σ}-algebra and vice versa by Ono and Komori [4]’s method.

Definition 2.1 Let A be an FL-algebra. SOM(A) is a structure ⟨𝔽^{−}(A), ∩, ·, ϵ, ω⟩ where ∩ is the set

intersection, x · y =^{def} F{a ⋆ b | a ∈ x, b ∈ y}, ϵ =^{def} 1↑, ω =^{def} A, 𝔽^{−}(A) =^{def} {x | x ∈ 𝔽(A), x · ϵ = ϵ · x = x}.

Theorem 2.2 If A is an FL_{σ}-algebra, SOM(A) is an so_{σ}-monoid.

Definition 2.3 Let D be an so-monoid. FLA(D) is a structure ⟨𝔽(D), →, ∪, ∩, ⋆, 1, 0, ⊤, ⊥⟩ where a → b =^{def} {y ∈ D | for all x ∈ a, y · x ∈ b}, ∩ is the set intersection, a ∪ b =^{def} F(a ∪ b) where ∪ in the

righthand is the set union, a ⋆ b =^{def} F{x · y | x ∈ a, y ∈ b}, ⊤ =^{def} D, ⊥ =^{def} {ω}, 1 =^{def} ϵ↑, 0 =^{def} ⊥ (if w ∈ σ)

or any filter (otherwise).

Theorem 2.4 If D is an so_{σ}-monoid, FLA(D) is an FL_{σ}-algebra.

Definition 2.5 Let A ≡ ⟨A, →, ∪, ∩, ⋆, 1, 0, ⊤, ⊥⟩ be an FL-algebra. A^{s} is a structure ⟨A, ∪, ⋆, 1, ⊥⟩.

Theorem 2.6 If A is an FL_{σ}-algebra, A^{s} is an so_{σ}-monoid. (The order induced in A^{s} is the opposite order of the order of A.)

3 Modality

Definition 3.1 Let D be an so_{σ}-monoid ⟨D, ∩, ·, ϵ, ω⟩. Cent(D) denotes the set {x ∈ D | ϵ ≤ x, x · x ≤ x, for all y ∈ D, x · y = y · x}. ⟨FLA(D), I, ¿, 0⟩ is a modal so_{σ} phase structure iff I is a submonoid of Cent(D), 0 ∈ FLA(D), and ¿ is an operation on D that satisfies

1. ¿x ≤ x, ¿x ≤ ¿¿x for x ∈ D

2. ¿(x · y) ≤ x · ¿y for x ∈ I and y ∈ D

3. if x ∈ 0, then ¿x ∈ 0 A modal so_{σ} phase structure has operations ! and ? on 𝔽(D) which are defined as follows.

!a =^{def} F(I ∩ a) ?a =^{def} F(0 ∪ ¿a) where ¿a =^{def} {¿x | x ∈ a}

Theorem 3.2 A modal so_{σ} phase structure is a modal FL_{σ}-algebra.

Proposition 3.3 Let A be a modal FL_{σ}-algebra and put D = SOM(A), I =^{def} {(!u)↑ | u ∈ A}, ¿x =^{def} F{?u | u ∈ x}, and 0 =^{def} (0_{A}↑)↑ (0_{A} is 0 in A). Then, ⟨FLA(D), I, ¿, 0⟩ is a modal so_{σ} phase structure.

Proposition 3.4 Let A be a modal FL_{σ}-algebra and put I =^{def} {!a | a ∈ A} and 0 =^{def} 0_{A^{s}}↑ (0_{A^{s}}↑ is a filter generated using the order of A^{s}, therefore, 0 = {a | a ≤_{A} 0_{A}} where ≤_{A} is the order in A.) Then, ⟨FLA(A^{s}), I,?, 0⟩ is a modal so_{σ} phase structure.

Theorem 3.5 Let A be a modal FL_{σ}-algebra.

1. Let B be ⟨FLA(D), I, ¿, 0⟩ given in Prop. 3.3. Then, a map from A to B defined by a ↦ (a↑)↑ is an embedding of modal FL_{σ}-algebra.

2. Let B be ⟨FLA(A^{s}), I,?, 0⟩ given in Prop. 3.4. Then, a map from A to B defined by a ↦ a↑ is an embedding of modal FL_{σ}-algebra.

Theorem 3.6 FL_{σ}^{m} is complete with respect to the class of all modal so_{σ} phase structures.

Remark: FL_{ewc}^{m} is equivalent to the constructive modal logic CS4 which consists of intuitionistic propositional logic, necessitation rule, and following axioms.

□K: □(A → B) → (□A → □B)  ◇K: □(A → B) → (◇A → ◇B)
□T: □A → A  ◇T: A → ◇A
□4: □A → □□A  ◇4: ◇◇A → ◇A
◇⊥E: ◇⊥ → A

(□ and ◇ are to be replaced by ! and ? respectively.) Therefore, ! and ? in so_{ewc}-modal phase structure can be used to interpret □ and ◇ in CS4.

Remark: (Girard’s modal op for classical phase space [1]) Let (P, ·) be a commutative monoid, O ⊆ P, and C(a) =^{def} (a → O) → O for a ⊆ P. Operations ! and ? are defined on {a | C(a) = a}.

!a =^{def} ((I ∩ a) → O) → O ?a =^{def} (I ∩ (a → O)) → O

4 Cut-Free Provability

In this section, we show the cut-free provability theorem for some FL_{σ} by using modal so_{σ} phase structure.

Lemma 4.1 In FL_{σ}^{m}, if Γ_{1}, α ∨ β, Γ_{2} ⊢ θ is cut-free provable, then Γ_{1}, α, Γ_{2} ⊢ θ and Γ_{1}, β, Γ_{2} ⊢ θ are cut-free provable.

Lemma 4.2 In FL_{σ}^{m} (c ∉ σ or e ∈ σ), if Γ_{1}, α ⋆ β, Γ_{2} ⊢ θ is cut-free provable, then Γ_{1}, α, β, Γ_{2} ⊢ θ is cut-free provable.

We define the preorder ≤ on formulas of FL_{σ}^{m} as follows:

α ≤ β iff, for every Γ_{1}, Γ_{2}, θ, if Γ_{1}, α, Γ_{2} ⊢ θ is cut-free provable, then Γ_{1}, β, Γ_{2} ⊢ θ is cut-free provable.

Let ∼ be the equivalence relation defined by α ∼ β iff α ≤ β and β ≤ α, [α] be the equivalence class to which a formula α belongs, and L_{σ} be the quotient set. Then, a partial order ≤ on L_{σ} is induced. We define the operations ∩ and · on L_{σ} as follows: [α] ∩ [β] =^{def} [α ∨ β], [α] · [β] =^{def} [α ⋆ β]. The definition of ∩ does not depend on the choice of the representative by Lemma 4.1 and, in the case of FL_{σ}^{m} (c ∉ σ or e ∈ σ), the definition of · does not depend on the choice of the representative by Lemma 4.2. Therefore, if c ∉ σ or e ∈ σ, operations ∩ and · are well-defined and we can check that L_{σ} =^{def} ⟨L_{σ}, ∩, ·, [1], [⊥]⟩ is an so_{σ}-monoid. Note that the order induced from ∩ coincides with ≤, that is, [α] ∩ [β] = [α] iff [α] ≤ [β].

Put I =^{def} {[!α_{1} ⋆ ⋯ ⋆ !α_{n}]} and ¿[α] =^{def} [?α]. Let ||α|| =^{def} {[γ] | γ ⊢ α is cut free provable} and put 0 =^{def} ||0_{σ}|| (0_{σ} is a formula 0 in FL_{σ}^{m}). Then, P_{σ} =^{def} ⟨FLA(L_{σ}), I, ¿, 0⟩ is a modal so_{σ} phase structure.

Let [[α]] be the valuation of α on P_{σ} where we put [[p]] = ||p|| for propositional variable p.

Theorem 4.3 In P_{σ} (c ∉ σ or e ∈ σ), [α] ∈ [[α]] ⊆ ||α||.

Corollary 4.4 In FL_{σ}^{m} (c ∉ σ or e ∈ σ), if Γ ⊢ θ is provable with cuts, then Γ ⊢ θ is provable without cuts. Proof. If Γ ≡ α_{1}, …, α_{n}, we write Γ^{⋆} for α_{1} ⋆ … ⋆ α_{n}. (Γ^{⋆} ≡ 1 if n = 0.) If Γ ⊢ θ is provable, then Γ^{⋆} ⊢ θ is provable. By Th. 4.3, [Γ^{⋆}] ∈ [[Γ^{⋆}]] ≤ [[θ]] ⊆ ||θ||. Therefore, Γ^{⋆} ⊢ θ is cut-free provable. By Lemma 4.2, Γ ⊢ θ is cut-free provable. □

Fortunately(?), the cut-elimination theorem does not hold either in FL_{c} or FL_{cw}.

Remark: The idea of using ||α|| and proving the theorem of the form Th. 4.3 comes from [2]. In [2], the cut-free provability and the cut-elimination theorems for intuitionistic and classical linear logics with modality are proved. In [5], the cut-elimination theorems for the predicate logic FLs (but not for the modal FLs) are proved.

5 Kripke Semantics

5.1 Kripke Semantics by Filter

In [3, 4], Kripke semantics of FL_{σ} is defined as follows.

Definition 5.1 (Kripke model) ⟨D, 0, g⟩ is a Kripke model of FL_{σ} iff D is a so_{σ}-monoid, 0 ∈ 𝔽(D) where 0 = {ω} if w ∈ σ, and g is a map from propositional variables to 𝔽(D). The valuation relation x ⊧ α for x ∈ D and a formula α is defined by the following clauses.

1. x ⊧ p iff x ∈ g(p), if p is a propositional variable

2. x ⊧ 1 iff ϵ ≤ x,

3. x ⊧ 0 iff x ∈ 0,

4. x ⊧ ⊤, for every x,

5. x ⊧ ⊥ iff x = ω,

6. x ⊧ α → β iff, for every y and z, y ⊧ α and x · y ≤ z implies z ⊧ β,

7. x ⊧ α ∨ β iff, there exist y and z such that y ∩ z ≤ x, y ⊧ α and z ⊧ β,

8. x ⊧ α ∧ β iff x ⊧ α and x ⊧ β,

9. x ⊧ α ⋆ β iff, there exist y and z such that y · z ≤ x, y ⊧ α and z ⊧ β.

This Kripke semantics is shown to be sound by Th. 2.4, that is, by reading x ⊧ α as x ∈ [[α]]. We will give the Kripke semantics for FL_{σ}^{m} by paraphrasing the filter generation in the definition of modal operations of Th. 3.2.

Definition 5.2 A binary relation R is a filter relation if it satisfies the following.

1. if x ≤ y and x R z, then there exists z′ such that y R z′ and z ≤ z′

2. if x_{1} R y_{1} and x_{2} R y_{2}, then x_{1} ∩ x_{2} R y_{1} ∩ y_{2}

Definition 5.3 ⟨D, R, S, 0, g⟩ is a Kripke model of FL_{σ}^{m} iff ⟨D, 0, g⟩ is a Kripke model of FL_{σ}, R is a transitive relation on D, S is a reflexive and transitive relation on D, and the following conditions are satisfied.

1. R and S are filter relations

2. if x R y, then x ≥ y, y R y, and y ∈ Cent(D)

3. if x_{1} R y_{1} and x_{2} R y_{2}, then x_{1} · x_{2} R y_{1} · y_{2}

4. if x_{1} R y_{1} and x_{2} S y_{2}, then x_{1} · x_{2} S y_{1} · y_{2}

5. if z ∈ 0 and x S z, then x ∈ 0 The valuation relation x ⊧ α is defined by the clauses 1 – 9 in Def. 5.1 and the following clauses.

10. x ⊧ !α iff, there exists y such that x R y and y ⊧ α,

11. x ⊧ ?α iff, there exists y such that x S y and y ⊧ α.

Theorem 5.4 Let ⟨D, R, S, 0, g⟩ be a Kripke model of FL_{σ}^{m} and ! and ? be the following operations on 𝔽(D).

!a =^{def} {x | ∃y(x R y ∧ y ∈ a)} ?a =^{def} {x | ∃y(x S y ∧ y ∈ a)}

Then, FLA(D) with ! and ? is a modal FL_{σ}-algebra.

Proposition 5.5 Let ⟨FLA(D), I, ¿, 0⟩ be a modal so_{σ} phase structure that satisfies (¿ω)↑ ≥ 0. Put

Î =^{def} {x_{1} ∩ ⋯ ∩ x_{n} | x_{i} ∈ I, n ≥ 1} and define the relations R and S on D by x R y =^{def} x ≥ y ∧ y ∈ Î

and x S y =^{def} x ≥ ¿y. Then, ⟨D, R, S, 0, g⟩ is a Kripke model of FL_{σ}^{m} and it holds that x ∈ [[α]] in ⟨FLA(D), I, ¿, 0⟩ (where [[p]] = g(p) for a propositional variable p) iff x ⊧ α in ⟨D, R, S, 0, g⟩.

Theorem 5.6 FL_{σ}^{m} is complete with respect to the class of all Kripke models.

5.2 Traditional Kripke Semantics

Usually, □ of the intuitionistic modal logic is interpreted using universal quantifier, that is, in the simplest case, □ is interpreted like this: (□) x ⊧ □α iff, for every z, x R_{□} z implies z ⊧ α. Here, we consider the following clause. (dom(R) =^{def} {x | ∃y(x R y)}.)

(!) x ⊧ !α iff, there exists y ≤ x such that y ∈ dom(R_{!}) and for every y R_{!} z, z ⊧ α. We do not list the conditions R_{!} should satisfy (R_{!} is transitive, and so on), but just remark that the clause 10 in Def. 5.3 and the clause (!) have the common instance that is obtained by putting x R y =^{def} x ≥ y ∧ y ∈ R_{0} in 10 and y R_{!} z =^{def} y ∈ R_{0} ∧ y ≤ z in (!). If we can take y independently of α in (!), we write the y as r_{x} and have the clause of the form (□) by putting x R_{□} z =^{def} r_{x} R_{!} z. In the case of σ = ewc, we have an example.

Proposition 5.7 Let A be a modal FL_{ewc}-algebra and put D = SOM(A), r_{x} =^{def} F{u | !u ∈ x},

¿x =^{def} F{?u | u ∈ x}, and 0 =^{def} (0_{A}↑)↑ (0_{A} is 0 in A). Then, ⟨FLA(D), 0, g⟩ with x R z =^{def} r_{x} ≤ z and

x S z =^{def} x ≥ ¿z is a model of FL_{ewc}^{m} defined by the clauses 1 – 9 in Def. 5.1, the clause 11 in Def. 5.3, and 10’. x ⊧ !α iff, for every z, x R z implies z ⊧ α.

References

[1] J.-Y. Girard. Linear logc: its syntax and semantics. In Girard, Lafont, and Regnier, editors, Advances in Linear Logic. Cambridge Univ. Press, 1995.

[2] M. Okada. Phase semantics for higher order completeness, cut-elimination and normalization proofs (extended abstract). Electronic Notes in Theoretical Computer Science, 3, 1996.

   http://www.elsevier.nl/locate/entcs/volume3.html.

[3] H. Ono. Semantics for substructural logics. In K. Došen and P. Schroeder-Heister, editors, Substructural Logics, pages 259–291. Oxford Univ. Press, 1993.

[4] H. Ono and Y. Komori. Logics without the contraction rule. Journal of Symbolic Logic, 50:169–201, 1985.

[5] B. Surarso and H. Ono. Cut elimination in noncommutative substructural logics. Reports on Mathematical Logic, 30:13–29, 1996.

Similarity on a tableau method between modal propositional logic S5 and classical propositional logic Cl

Yasuhito SUZUKI

                      x-suzuki@cce.numazu-ct.ac.jp

Department of Control and Computer Engineering, Numazu College of Technology

Abstract

A.Chagrov and M.Zakharyashcev show that there exist embeddings between propositional modal logic S5 and classical propositional logic Cl in terms of frame semantics ([CZ97]). So, it is natural to consider that there is also something similar on tableau method between S5 and Cl. Combining a few propositions in [CZ97], we can quite easily find a new tableau method for S5, which resembles for Cl.

1 Notation

Through this report, except treating classical tableau, we will use propositional modal formulas, only. They are introduced in usual way; Let P be the set of propositional variables. Letters p, q, r, …, p_{0}, p_{1}, … will denote propositional variables. The set of propositional modal formulas is constructed from P, ∧, ∨, ⊃, □, ◇ and ⊥ in usual way. Greek letters φ, ψ, χ, … will denote formulas. We consider ⊤ and the negation ¬φ of formula φ as abbreviations of ⊥ ⊃ ⊥ and φ ⊃ ⊥, respectively. We call a formula which outermost connective is □ box formula. In box formulas, we separate formulas which second outermost connective are disjunction, and call such a formula box disjunctive formula.

As for model, we suppose frame semantics. The truth relation and validity are introduced similar to [CZ97], as follows; Let W and R be a denumerable set of possible worlds and equationl relation on W, respectively. A frame F is a pair ⟨W, R⟩, a valuation V is a function from P to 2^{W}, and a model M is a pair ⟨F, V⟩. Suppose x and y are arbitrary possible worlds, and C is a class of frames, then;

(M, x) |̸= ⊥,
(M, x) ⊧ p iff x ∈ V(p),
(M, x) ⊧ φ ∧ ψ iff (M, x) ⊧ φ and (M, x) ⊧ ψ,
(M, x) ⊧ φ ∨ ψ iff (M, x) ⊧ φ or (M, x) ⊧ ψ,
(M, x) ⊧ φ ⊃ ψ iff (M, x) |̸= φ or (M, x) ⊧ ψ,
(M, x) ⊧ □φ iff for all y(xRy ⇒ (M, y) ⊧ φ),
(M, x) ⊧ ◇φ iff for some y(xRy and (M, y) ⊧ φ),
M ⊧ φ iff for all x((M, x) ⊧ φ),
F ⊧ φ iff for all V(M ⊧ φ),
(F, x) ⊧ φ iff for all V((M, x) ⊧ φ),
C ⊧ φ iff for all F(F ∈ C ⇒ F ⊧ φ).

φ is true at x in M if (M, x) ⊧ φ. φ is false at x in M if φ is not true. φ is true in M if M ⊧ φ. φ is valid in F if F ⊧ φ. A set Γ of formulas is characterized by a class C of frames if C ⊧ φ for any φ(∈ Γ), and is denoted by C ⊧ Γ. A generated subframe of a given frame ⟨W, R⟩ is a pair ⟨V, S⟩ such that V and S is a closure of R for some subset of W and a restriction of R by V, respectively. A generated submodel of a given model ⟨F, V⟩ is a pair ⟨G, U⟩ where G is a generated subframe of F and U is a restriction of V by the base set of G.

2 Frame which is constructed from one cluster

In our report, a cluster has a main role. For any possible world x, a cluster C(x) is defined as follows;

C(x) = {y : xRy and yRx}.

Under an equivalence relation R, C(x) means an equivalence class of W/R. A.Chagrov and M.Zakharyascev introduced the following proposition for a frame with a transitive relation.

Proposition 2.1 (3.7 of [CZ97]) Suppose x is a possible worlds in a model M built on a transitive frames and φ an arbitrary fromula. Then for every y ∈ C(x),

(M, x) ⊧ □φ iff (M, y) ⊧ □φ,
(M, x) ⊧ ◇φ iff (M, y) ⊧ ◇φ.

This proposition 2.1 asserts that any box formula has same truth value in each clusters. Next,

Proposition 2.2 (3.11 of [CZ97]) If N is a generated submodel of M then, for every point x in N and every modal formula φ,

(N , x) ⊧ φ iff (M, x) ⊧ φ.

Proposition 2.3 (3.13 of [CZ97]) Let K be the set of theorems of propositional modal logic K. Then,

K = {φ : F ⊧ φ for all rooted frames F}.

The set of theorems of S5 is the set of formulas which are valid in all frames with equivalence relation. As for the case of S5, a rooted frame means that one cluster frames. By proposition 2.2 and 2.3, we can easily show that S5 is characterized by the class of frames which is constructed from one cluster. That is,

Proposition 2.4 Let S5 be the set of theorems of S5. Then,

S5 = {φ : F ⊧ φ for any frame which is constructed from one cluster F}.

By proposition 2.4, it is sufficient to know cardinal of W when expressing frame for S5. Combining propositions 2.1and 2.4, it is natural to dispose box formulas from another types of formulas if we consider tableau proof for S5.

3 Tableau proof of S5

We will introduce a tableau proof method of S5. The essence of this method was introduced first in [Suz97], but the method in [Suz97] is difficult to read because it is intended to implement in a computer system. To simplify it, a similar point between our method and tableau proof of Cl becomes clear.

Basically, tableau method makes a tree structure which is called tableau tree. Beth tableau is a pair (Γ, Δ) of two sets Γ, Δ of formulas. Roughly speaking, Γ of Beth tableau indicates a set of formulas which truth value are true, and Δ indicates a set of formulas which truth value are false. For normal tableau system, each node of a tableau tree is Beth tableau, and each Beth tableau corresponds to a possible world of a frame. In our system, each node of tableau tree corresponds to a model (that is, a set of Beth tableaus).

In this report, S5 tableau is a set of Beth tableau. To dispose box formulas and box disjunctive formulas, we prepare special Beth tableaus in S5 tableau. Each S5 tableau has two special Beth tableaus.

One is called □-tableau (denoted by (Γ_{□} , Δ_{□} )), and another □-∨-tableau (denoted by (Γ_{□∨} , Δ_{□∨} )), respectively. Thus, S5 tableau itself is denoted by [(Γ_{□} , Δ_{□} ) : (Γ_{□∨} , Δ_{□∨} ) : (Γ_{1}, Δ_{1}), …, (Γ_{n}, Δ_{n})]. S5 tabelau tree is a tree structure which is constructed from S5 tableaus.

In our tableau method, two types of tableau extension rules are introduced. Each rule is applied to a formula of Beth tableau on leaf S5 tableaus. Formula which is applied rule is marked with check mark. Checked formulas do not become target of applying rules. Checked formula (\overline{φ}) and non-checked formula (φ) are treated the identical element (checked-formula) in any set if both \overline{φ} and φ are elements of the set. Tableau extension rule is applied to non-checked formulas of all Beth tableaus except □-∨-tableau, and tableau box disjunctive extension rule is applied to non-checked formulas of □-∨-tableau.

Tableau extension rule is defined as follows;

• ⊥ ∈ Γ(Γ_{□} ): Stop applying extension rule to this S5 tableau.

• ¬φ ∈ Γ(Γ_{□} ): Check ¬φ, and add φ into Δ (Δ_{□} ).

• φ ∧ ψ ∈ Γ(Γ_{□} ): Check φ ∧ ψ, and add φ, ψ into Γ (Γ_{□} ).

• φ ∨ ψ ∈ Γ: Make two copies of S5 tableau, and add them as children of this node. Then, check φ ∨ ψ in Γ in each child, and add φ into Γ of one child and ψ into Γ of another child.

• φ ⊃ ψ ∈ Γ: Make two copies of S5 tableau, and add them as children of this node. Then, check φ ⊃ ψ from Γ in each child, and add φ into Δ of one child and ψ into Γ of another child.

• φ ∨ ψ ∈ Γ_{□} : Check φ ∨ ψ in Γ_{□} , and add φ ∨ ψ to Γ_{□∨} .

• φ ⊃ ψ ∈ Γ_{□} : Check φ ⊃ ψ in Γ_{□} , and add ¬φ ∨ ψ to Γ_{□∨} .

• □φ ∈ Γ(Γ_{□} ): Check □φ, and add φ into Γ_{□} (Γ_{□} ).

• ◇φ ∈ Γ(Γ_{□} ): Suppose {φ_{1}, …, φ_{h}} and {φ_{h+1}, …, φ_{k}} are the set of checked formulas of Γ_{□∨} and the set of checked formulas of Δ_{□∨} , respectively. For each i, φ_{i} is denoted by α_{i}^{0} ∨α_{i}^{1} when 1 ≤ i ≤ h and by α_{i}^{0} ∧ α_{i}^{1} when h + 1 ≤ i ≤ k. Make 2^{k} copies of S5 tableau and indexes each copies like T_{1}, …, T_{2^{k}}, and add them as children of this S5 tableau. For each S5 tableau children T_{s}, add a Beth tableau ({φ, α_{1}^{j_{1}}, …, α_{h}^{j_{h}}}, {α_{h+1}^{j_{h+1}}, …, α_{k}^{j_{k}}}) such that s = j_{1}2^{0} + j_{2}2^{1} + ⋯ + j_{k}2^{k−1}. Check ◇φ of all Γ-nodes of Beth tableaus including □-tableau at last.

• ⊥ ∈ Δ(Δ_{□} ): Check ⊥.

• φ ∧ ψ ∈ Δ: Make two copies of S5 tableau, and add them as children of this node. Then, check φ ∧ ψ from Δ in each child, and add φ into Δ of one child and ψ into Δ of another child.

• φ ∧ ψ ∈ Δ_{□} : Check φ ∧ ψ, and add φ ∧ ψ to Δ_{□∨} .

• φ ∨ ψ ∈ Δ(Δ_{□} ): Check φ ∨ ψ, and add φ, ψ into Δ (Δ_{□} ).

• φ ⊃ ψ ∈ Δ(Δ_{□} ): Check φ ⊃ ψ, and add φ into Γ (Γ_{□} ) and ψ into Δ (Δ_{□} ).

• □φ ∈ Δ(Δ_{□} ): Suppose {φ_{1}, …, φ_{h}} and {φ_{h+1}, …, φ_{k}} are the set of checked formulas of Γ_{□∨} and the set of checked formulas of Δ_{□∨} , respectively. For each i, φ_{i} is denoted by α_{i}^{0} ∨ α_{i}^{1} when 1 ≤ i ≤ h and by α_{i}^{0} ∧α_{i}^{1} when h+1 ≤ i ≤ k. Make 2^{k} copies of S5 tableau and indexes each copies like T_{1}, …, T_{2^{k}}, and add them as children of this S5 tableau. For each S5 tableau children T_{s}, add a Beth tableau ({α_{1}^{j_{1}}, …, α_{h}^{j_{h}}}, {φ, α_{h+1}^{j_{h+1}}, …, α_{k}^{j_{k}}}) such that s = j_{1}2^{0} + j_{2}2^{1} + ⋯ + j_{k}2^{k−1}. Check □φ of all Δ-nodes of Beth tableaus including □-tableau at last.

• ◇φ ∈ Δ(Δ_{□} ): Check ◇φ, and add φ into Δ_{□} (Δ_{□} ).

Tableau box disjunctive extension rule is defined as follows;

• φ ∨ ψ ∈ Γ_{□∨} : Check φ ∨ ψ. Denote φ and ψ by α^{0} and α^{1}, respectively. Suppose n is the number of Beth Tableaus of S5 tableau [(Γ_{□} , Δ_{□} ) : (Γ_{□∨} , Δ_{□∨} ) : (Γ_{1}, Δ_{1}), …, (Γ_{n}, Δ_{n})]. Make 2^{n} copies of S5 tableau and indexes each copies like T_{1}, …, T_{2^{n}}, and add them as children of this S5 tableau. For each Beth tableau (Γ_{i}, Δ_{i}) of T_{j}, add α^{j_{i}} to Γ_{i} such that j = j_{1}2^{0} + j_{2}2^{1} + ⋯ + j_{n}2^{n−1}.

• φ ∧ ψ ∈ Δ_{□∨} : Check φ ∧ ψ. Denote φ and ψ by α^{0} and α^{1}, respectively. Suppose n is the number of Beth Tableaus of S5 tableau [(Γ_{□} , Δ_{□} ) : (Γ_{□∨} , Δ_{□∨} ) : (Γ_{1}, Δ_{1}), …, (Γ_{n}, Δ_{n})]. Make 2^{n} copies of S5 tableau and indexes each copies like T_{1}, …, T_{2^{n}}, and add them as children of this S5 tableau. For each Beth tableau (Γ_{i}, Δ_{i}) of T_{j}, add α^{j_{i}} to Δ_{i} such that j = j_{1}2^{0} + j_{2}2^{1} + ⋯ + j_{n}2^{n−1}.

We will show two examples of applying to S5 tableau.

Example 3.1 Let S5 tableau [(∅, ∅) : (∅, ∅) : (∅, {◇p ⊃ □◇p})] be given. Then,

[(∅, ∅) : (∅, ∅) : (∅, \{◇p ⊃ □◇p\})] ⇒ [(∅, ∅) : (∅, ∅) : (\{◇p\}, \{□◇p, \overline{◇p ⊃ □◇p}\})]
⇒ [(∅, ∅) : (∅, ∅) : (\{\overline{◇p}\}, \{□◇p, \overline{◇p ⊃ □◇p}\}), (\{p\}, ∅)]
⇒ [(∅, ∅) : (∅, ∅) : (\{\overline{◇p}\}, \{\overline{□◇p}, \overline{◇p ⊃ □◇p}\}), (\{p\}, ∅), (∅, \{◇p\})]
⇒ [(∅, \{p\}) : (∅, ∅) : (\{\overline{◇p}\}, \{\overline{□◇p}, \overline{◇p ⊃ □◇p}\}), (\{p\}, ∅), (∅, \{\overline{◇p}\})]

Example 3.2 Let S5 tableau [(∅, ∅) : (∅, ∅) : ({□(p ∨ ◇q)}, ∅)] be given. Then,

[(∅, ∅) : (∅, ∅) : (\{□(p ∨ ◇q)\}, ∅)] ⇒ [(\{p ∨ ◇q\}, ∅) : (∅, ∅) : (\{\overline{□(p ∨ ◇q)}\}, ∅)]
⇒ [(\{\overline{p ∨ ◇q}\}, ∅) : (\{p ∨ ◇q\}, ∅) : (\{\overline{□(p ∨ ◇q)}\}, ∅)]
⇒ \{ \begin{matrix}[(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{p, \overline{□(p ∨ ◇q)}\}, ∅)] \\ [(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{◇q, \overline{□(p ∨ ◇q)}\}, ∅)] \end{matrix}

⇒ \{ ; \begin{matrix}[(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{p, \overline{□(p ∨ ◇q)}\}, ∅)] \\ \{ & \begin{matrix}[(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{◇q}, \overline{□(p ∨ ◇q)}\}, ∅), (\{p, q\}, ∅)] \\ [(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{◇q}, \overline{□(p ∨ ◇q)}\}, ∅), (\{\overline{◇q}, q\}, ∅)] \end{matrix} \end{matrix}

It is natural condsidered from the above examples, closeness on S5 tableau is defined as follows.

Definition 3.3 S5 tableau [(Γ_{□} , Δ_{□} ) : (Γ_{□∨} , Δ_{□∨} ) : (Γ_{1}, Δ_{1}), …, (Γ_{n}, Δ_{n})] is closed if (Γ_{□} ∪ Γ_{i}) ∩ (Δ_{□} ∪ Δ_{i}) ≠ ∅ holds for some i.

Closeness of S5 tabelau tree and ⊢ are defined in usual way. Then, the following completeness result holds.

Proposition 3.4 For any formula φ, ⊢ φ holds, if and only if, ⊧ φ.

4 Conclusion

Modal logic S5 is characterized by the class of one cluster frames. Meanwhile propositional classical logic Cl is characterized by the singleton of the one point frame. Combining with proposition 2.1 and 2.4, we could devide modal formulas into three layers in our tableau method. We tried to simplify extension rules. If box disjunctive formula in Γ (and its dual in Δ) does not appear in our tableau tree, our method quite resembles to Cl tableau. Box disjunctive formulas are the reason why increasing nodes of S5 tableau. We conjecture that box disjunctive formula becomes the cause of deviding S5 from Cl.

References

[CZ97] Alexander Chagrov and Michael Zakharyaschev. Modal Logic. Oxford, 1997.

[Suz97] Yasuhito Suzuki. The realization of the hybrid multi-modal logic theorem prover in the term rewriting system cafeobj. Sequent calculs � Kripke semantics �������������, �� �������� 1021, pp. 96–111, 1997.

Products of Modal Logics by General Frames

Yasusi Hasimoto

                          yasusi-h@jaist.ac.jp

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

1 Products of Modal Logics by Kripke Frames

Let F = (W, R) and G = (V, S) be Kripke frames. As Shehtman introduced in [3], we define the products of Kripke frames as F ×_{s} G := (W × V, R^{∨}, S^{∨}), where R^{∨} = {((x, y), (z, y)) | xRz}, S^{∨} = {((x, y), (x, z)) | ySz}. Moreover we will define as follows.

For any modal logic L, F (L) := {F | F ⊧ L}.

For any class C of Kripke frames, L(C) := {φ | F ⊧ φ for any F ∈ C}.

For any classes C_{1}, C_{2} of Kripke frames, C_{1} ×_{s} C_{2} := {F ×_{s} G | F ∈ C_{1}, G ∈ C_{2}}.

For modal logics L_{1}, L_{2}, we define the products of logics as L_{1} ×_{s} L_{2} := L(F (L_{1}) ×_{s} F (L_{2})).

The properties of L_{1} ×_{s} L_{2} is, for example, investigated as follows (see [1]).

• The logic L_{1} ×_{s} L_{2} is Kripke complete. (Trivial.)

• L_{1} ×_{s} L_{2} ⊇ [L_{1}, L_{2}], where [L_{1}, L_{2}] := L_{1} ∗ L_{2} ⊕ □_{1}□_{2}p ↔ □_{2}□_{1}p ⊕ ◇_{1}□_{2}p → □_{2}◇_{1}p.

• If L_{1}, L_{2} are PTC-logics (i.e. the logics axiomatized by a set of pseudotransitive formulas ◇^{m}□p → □^{n}p and/or closed formulas), then L_{1} ×_{s} L_{2} is product-matching (i.e. L_{1} ×_{s} L_{2} = [L_{1}, L_{2}]).

• If L is axiomatized by a set of □p → □^{n}p, ◇□p → p and/or closed formulas, then L ×_{s} S5 has f.m.p..

But the products (×_{s}) of logics have a bad property. We do NOT always have

L(C_{1}) ×_{s} L(C_{2}) = L(C_{1} ×_{s} C_{2}), (1)

for any classes C_{1}, C_{2} of Kripke frames. The logic LIN ×_{s} S5 give us a counterexample [2].

In the following (Sections 4), we will define another products (×) of logics on which the property (1) holds.

2 Products of Modal Logics by General Frames

Let F = (W, R, P) and G = (V, S, Q) be general frames. That is, P is a modal algebra of sets on Kripke frame F, which contains ∅ and is closed under ∩, ∪, −, □, where □X = {x ∈ W | xRy ⇒ y ∈ X}. Also we set κF as (W, R, 2^{W}). We define the products of general frames as follows. F × ×G := (W × V, R × S, P × ×Q), where

R × S := {((x, y), (t, u)) | xRt, ySu},
P × ×Q := ma({X × Y | X ∈ P, Y ∈ Q}),

i.e. the smallest modal algebra containing {X × Y | X ∈ P, Y ∈ Q}.

Note that (W, R) ×_{s} (V, S) = (W × V, R × Δ, Δ × S), where Δ denotes a diagonal relation.

Theorem 2.1  P × ×Q = {⋃_{i∈I} X_{i} × Y_{i} | X_{i} ∈ P, Y_{i} ∈ Q, I : finite}.

Proof. It is implied by following (2)–(7).

•  ∅ = ∅ × ∅(= ∅ × V = W × ∅).  (2)
•  ⋃_{i∈I} X_{i} × Y_{i} ∩ ⋃_{j∈J} T_{j} × U_{j} = ⋃_{(i,j)∈I×J}(X_{i} ∩ T_{j}) × (Y_{i} ∩ U_{j}).  (3)

•  ⋃_{i∈I} X_{i} × Y_{i} ∪ ⋃_{j∈J} T_{j} × U_{j} = ⋃_{k∈I⊔J} A_{k} × B_{k},  (4)

where I ⊔ J = {(i, 0) | i ∈ I} ∪ {(j, 1) | j ∈ J}, A_{(i,0)} = X_{i}, A_{(j,1)} = T_{j}, B_{(i,0)} = Y_{j}, B_{(j,1)} = U_{j}.

•  − ⋃_{i∈I} X_{i} × Y_{i} = ⋃_{J∈2^{I}}(− ⋃_{i∈J} X_{i}) × (− ⋃_{i∈−J} Y_{i}).  (5)

•  ◇ ⋃_{i∈I} X_{i} × Y_{i} = ⋃_{i∈I} ◇X_{i} × ◇Y_{i}.  (6)

•  □ ⋃_{i∈I} X_{i} × Y_{i} = ⋃_{A⊆2^{I}}(□ ⋂_{J∈A} ⋃_{i∈J} X_{i}) × (□ ⋃_{J∈A} ⋂_{i∈J} Y_{i}).  (7)

Moreover, the following holds.

• ⋃_{i∈I} X_{i} × Y_{i} = ⋃_{j∈J} T_{j} × U_{j}

⟺ ∀i ∈ I, ∃A ⊆ 2^{J} such that X_{i} ⊆ ⋂_{J′∈A} ⋃_{j∈J′} T_{j}, Y_{i} ⊆ ⋃_{J′∈A} ⋂_{j∈J′} U_{j},  (8)
and ∀j ∈ J, ∃A ⊆ 2^{I} such that T_{j} ⊆ ⋂_{I′∈A} ⋃_{i∈I′} X_{i}, U_{j} ⊆ ⋃_{I′∈A} ⋂_{i∈I′} Y_{i}.

Proposition 2.2 κF × ×κG = κ(F × ×G) ⟺ either F or G is finite.

Proposition 2.3 Let α be ◇^{m_{1}}□^{n_{1}}p_{1} ∧ ⋯ ∧ ◇^{m_{k}}□^{n_{k}}p_{k} → φ(p_{1}, …, p_{k}), where φ is constructed by ∧, →, □, ◇ from p_{1}, …, p_{k}. Then F ⊧ α, G ⊧ α ⇒ F × ×G ⊧ α, and κF ⊧ α, κG ⊧ α ⇒ κ(F × ×G) ⊧ α.

3 The Dual Algebras

For any general frame F = (W, R, P), we denote the dual algebra of F by F^{+} = (P, ∩, ∪, −, ∅, □).

For any (normal) modal algebra A = (A, ∧, ∨, ¬, 0, □), we denote the dual frame of A by A_{+} = (P F (A), RA, PA), where

1. P F (A) is the set of all prime filters of A

2. xRA y ⟺^{def} ∀a ∈ A(□a ∈ x ⇒ a ∈ y),

3. PA = {{x ∈ P F (A) | a ∈ x} | a ∈ A}.

We define the products of modal algebras as follows. For modal algebras A, B, A × ×B := (A_{+} × ×B_{+})^{+}

By (2)–(8), we can easily get the following proposition.

Proposition 3.1 F_{1}^{+} ≃ F_{2}^{+}, G_{1}^{+} ≃ G_{2}^{+} ⇒ (F_{1} × ×G_{1})^{+} ≃ (F_{2} × ×G_{2})^{+}. Especially, A ≃ F^{+}, B ≃ G^{+} ⇒ A × ×B ≃ (F × ×G)^{+}.

Hence for general frames F, G, we have

(F × ×G)^{+} ≃ F^{+} × ×G^{+}. (9) Recall that

a general frame F = (W, R, P) is descriptive (i.e. ∃A: modal algebra, F ≃ A_{+} ) ⟺

• differentiated ∀x, y ∈ W (x ≠ y ⇒ ∃X ∈ P such that x ∈ X, y ∉ X),

• tight ∀x, y ∈ W (x R̸y ⇒ ∃X ∈ P such that x ∈ X, y ∉ X),

• compact ∀A ⊆ P((⋂ A_{0} ≠ ∅ for finite A_{0} ⊆ A) ⇒ ⋂ A ≠ ∅). Proposition 3.2 If general frames F, G are descriptive, then the product F × ×G is also descriptive. Hence for modal algebras A, B, we have

(A × ×B)_{+} ≃ A_{+} × ×B_{+}. (10)

4 Products of Modal Logics by General Frames

For any modal logic L, we denote by F (L) the set of all general frames which validate L, and by V (L) the set of all modal algebras which validate L. For modal logics L_{1}, L_{2}, we define

L_{1} × ×L_{2} := L(F (L_{1}) × ×F (L_{2})). By (9) and (10), we have

L_{1} × ×L_{2} = L(V (L_{1}) × ×V (L_{2})). Let K be a class of modal algebras.

V (K) denotes the smallest variety containing K. H(K) denotes the smallest class containing K closed under homomorphic images. S(K) denotes the smallest class containing K closed under subalgebras. P (K) denotes the smallest class containing K closed under direct product.

For any modal algebra A, we denote by fA a isomorphism from A to (A_{+})^{+}. Theorem 4.1

1. If h : A_{1} → A_{2} and g : B_{1} → B_{2} are homomorphic onto maps, then h × ×g : A_{1} × ×B_{1} → A_{2} × ×B_{2}

defined by

h × ×g(⋃_{i∈I} X_{i} × Y_{i}) = ⋃_{i∈I} f_{A_{2}} ∘ h ∘ fA_{1}^{−1}(X_{i}) × f_{B_{2}} ∘ g ∘ fB_{1}^{−1}(Y_{i})

is also homomorphic onto map.

2. If A_{1} is a subalgebra of A_{2} and B_{1} is a subalgebra of B_{2}, then A_{1} × ×B_{1} is also a subalgebra of A_{2} × ×B_{2}.

3. ∏_{λ∈Λ} A_{λ} × × ∏_{μ∈M} B_{μ} is a subalgebra of ∏_{(λ,μ)∈Λ×M} A_{λ} × ×B_{μ}.

Hence for classes K_{1}, K_{2} of modal algebras,

1. H(K_{1}) × ×H(K_{2}) ⊆ H(K_{1} × ×K_{2}),

2. S(K_{1}) × ×S(K_{2}) ⊆ S(K_{1} × ×K_{2}),

3. P (K_{1}) × ×P (K_{2}) ⊆ SP (K_{1} × ×K_{2}).

Therefore we have the following theorem. Theorem 4.2 Let K_{1} and K_{2} be classes of modal algebras, and let C_{1} and C_{2} be classes of general frames. Then

1. V (V (K_{1}) × ×V (K_{2})) = V (K_{1} × ×K_{2}),

2. L(K_{1}) × ×L(K_{2}) = L(K_{1} × ×K_{2}),

3. L(C_{1}) × ×L(C_{2}) = L(C_{1} × ×C_{2}).

Now we define another products (×) of logics instead of products (×_{s}) of logics.

Let A = (A, ∧, ∨, ¬, 0, □A) and B = (B, ∧, ∨, ¬, 0, □B) be modal algebras, and let F = (W, R, P) and G = (V, S, Q) be general frames. Then we define as follows. A^{∘} := (A, ∧, ∨, ¬, 0, □A, □B) with □Bb = b, ∘B := (B, ∧, ∨, ¬, 0, □A, □B) with □Aa = a. F^{∘} := (W, R, Δ, P), ∘G := (V, Δ, S, Q). F × G := F^{∘} × ×^{∘}G. For modal logics L_{1}, L_{2}, L_{1} × L_{2} := L(F (L_{1}) × F (L_{2})).

Since (A_{+})^{∘} = (A^{∘})_{+} and (F^{+})^{∘} = (F^{∘})^{+} hold, we have the following theorem. Theorem 4.3 Let K_{1}, K_{2} be classes of modal algebras, and let C_{1}, C_{2} be classes of general frames. Then

1. V (K^{∘}) = V (K)^{∘}, V (^{∘}K) = ^{∘}V (K),

2. L(K_{1}) × L(K_{2}) = L(K_{1}^{∘} × ×^{∘}K_{2}),

3. L(C_{1}) × L(C_{2}) = L(C_{1} × C_{2}).

Note that L_{1} × L_{2} = (L_{1} ∗ (K ⊕ □p ↔ p)) × ×((K ⊕ □p ↔ p) ∗ L_{2}).

The following proposition about properties of L_{1} × L_{2} holds. Proposition 4.4 Let L_{1}, L_{2} be modal logics. Then

1. If L_{1} and L_{2} are consistent mono-modal logics, then L_{1} × L_{2} is a conservative extension of L_{1} and L_{2}.

2. L_{1} × L_{2} ⊇ [L_{1}, L_{2}],

3. If L_{1} andL_{2} have f.m.p., then L_{1} × L_{2} has product f.m.p.(i.e. L_{1} × L_{2} = L(F_{f}(L_{1}) × F_{f}(L_{2}))), hence L_{1} × L_{2} also has f.m.p.. (F_{f}(L) denotes the set of all general frames which validate L.)

4. If one of L_{1} and L_{2} has f.m.p. and the other is Kripke complete, then L_{1} × L_{2} is also Kripke complete.

References

[1] D. Gabbay and V. Shehtman, Products of modal logics, Part I . L. J. of IGPL, 6(1), pp. 73 – 146, 1998.

[2] M. Reynolds, A decidable temporal logic of parallelism. (Forthcoming)

[3] V. Shehtman, Two-dimensional modal logics. Math. Zametki, 5, pp. 759 – 772, 1978. (In Russian)

On some modal predicate logics with Glivenko type characterization.

SHIMURA Tatsuya

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

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

2000.1.11 (at MLG meeting)

1 Problem

Ghilardi [3] showed that QS4.1, the least predicate extension of S4.1 = S4 + □◇p ⊃ ◇□p, is not Kripke complete. Hughes-Cresswell [4] showed that QS4.1 + BF is Kripke incomplete, where BF is the Barcan formula ∀x□A(x) ⊃ □∀x A(x).

So, we consider the following problem.

Problem 1

(1). Find the Kripke completion of QS4.1.

That is, find the logic characterized by the modal predicate Kripke frames in which □◇p ⊃ ◇□p is valid.

(2). Find the Kripke completion of QS4.1 + BF.

That is, find the logic characterized by the modal predicate Kripke frames of constantdomains in which □◇p ⊃ ◇□p is valid.

Note that □◇p ⊃ ◇□p is valid in a Kripke frame (M, U) if and only if M has the following property:

For every u ∈ M, there is a maximal trivial cluster above w, that is, there is an element v such that uRv and vRw implies w = v for all w.

In this talk, I show a syntactical characterization of the Kripke completion of QS4.1 can be obtained by the method described in Shimura [6], and that of QS4.1+BF by modifying the method in Shimura [7].

2 Glivenko type characterization

It is well-known that the cut-free system GS4 for the modal propositional logic S4 gives a useful machinery to prove some syntactical properties and the completeness of S4. Shimura [6] gave some kinds of cut-free sequent style systems and showed that a similar machinery works for the logics defined by them.

The propositional logic S4.1 is one of the logics defined by the sequent style systems. That is, we can define it as the logic defined by the the sequent style system obtained from GS4 by adding the sequents of the form □Γ → provable in GTriv, where Triv = S4 + p ⊃ □p.

In other words, S4.1 can be characterized as the least logic with the following propety:

Triv ⊢ A ⇔ L ⊢ ◇□A.

The completeness proof of S4.1 by means of this sequent style system tells us that the characterization of the frames validating S4.1 is nothing but the following:

For every world w, there exits a world w′ above w in which Triv is valid. By transferring the above fact to predicate case, we can obtain the answer to Problem 1 (1).

Theorem 1 The Kripke completion is the logic defined by the sequent style system obtained from GQS4 by adding all the sequents of the form □Γ → provable in GQTriv.

3 Axiomatization.

We should find a formula C with the folloing property to give an axiomatizatiion of the Kripke completion of QS4.1.

QTriv ⊢ A ⇒ QS4.1 + C ⊢ ◇□A. If we try to prove the above assertion by induction on the complexity of the proof in GQTriv, the

crucial case is that the last inference is (→ ∀) or (∃ → ). So, we should take C as □∀x◇□A(x) ⊃ ◇□∀x A(x), which is the formula given by Corsi-Ghilardi [1].

Note that this formula is equivalent to the McKinsey-Tarski translation T (K) of Kroda axiom K = ∀x¬¬A(x) ⊃ ¬¬∀x A(x).

The logic axiomatized by T (K) over QS4 has the following characterization. Theorem 2 QS4 + T (K) is characteized as the least logic Lwith the folloing Glivenko type property.

QS5 ⊢ A ⇔ L ⊢ ◇□A. We can summarize the above facts as follows:

Fact 1 • QS4.1 + T (K) is Glivenko type characterization by QTriv

• QS4.1 + T (K) is the Kripke completion of QS4.1,

• QS4.1 + T (K) has modal disjunction property,

• QS4.1 + T (K) has modal existence property,

• QS4.1 + T (K) has interpolation property. Fact 2

• QS4 + T (K) has the Glivenko type characterization by QS5

• QS4 + T (K) has modal disjunction property,

• QS4 + T (K) has modal existence property, Note that QS4 + T (K) does not have the interpolation property since QS5 does not have it. We have few examples of modal predicate logics with the interpolation property. Moreover, we have

no general method to determine whether a given logic has the interpolation property or not. So the following question may be interesting. Question 1 (1). Does QS4.1 have interpolation property? (2). Does QS4.1 + T (K) + BF have interpolation property?

4 Completeness for the logics with the Barcan axiom.

First note that T (K) must be valid in the Kripke frames in which □◇p ⊃ ◇□p is valid. This implies the Kripke completion of QS4.1 + BF must contains T (K).

So we have to investigate the structure of the Kripke models with constant domains in which all the instances of T (K) are true.

Lemma 3 (cf. Shimura [7, Lemma 3.8]) Let (M, D, ⊧) be a canonical model with constant domains and (Γ, Δ) ∈ M the root of M. Then, if all the instances of T (K) belong to Γ, there exits a final cluster above any element of M.

Lemma 4 Let (M, D) be a Kripke frame with constant domains in which there exits a final cluster above any element of M. Then, □◇p ⊃ ◇□p is not valid in (M, D) if and only if there is a non-trivial final cluster in M.

Since QS4 + BF is strongly Kripke complete with respect to Kripke frames with constant domains, we can apply the method of canonical models by the aid of the above lemmas.

Theorem 5

(1). QS4 + T (K) + BF is Kripke complete.

(2). QS4.1 + T (K) + BF is Kripke complete.

This implies the following:

Fact 3 QS4 + T (K) + BF and QS4.1 + T (K) + BF have the following properties:

• modal disjunction property,

• modal existence property.

We can generalize the above completeness result as follows:

Theorem 6 (cf. Shimura [7]) Let M be the frame in the following figure and {M_{i}} a set of finite Kripke frames. If there is no cofinal subreduction from M_{i} to M for every M_{i}, QS4 + {α(M_{i}, ⊥)} + T (K) + BF is Kripke complete.

[figure: Figure 1:]

It is natural to ask whether L + T (K) + BF is complete or not for every cofinal subframe logic L. The answer was implicitely given in Isoda and Shimura [5]. In fact, the incompleteness proof of QS4.1.4+BF actually proves that of QS4.1.4 + T (K) + BF.

Theorem 7 (Isoda-Shimura [5]) Then, QS4.1.4 + T (K) + BF = QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

Added in proof: The author noticed after the talk that Theorem 6 is wrong. It seems that we can correct the statement by adding two more conditions on non-exsistence of cofinal subreductions to the frames M_{i}, but the author does not check whether this correction works yet.

References

[1] Corsi, G., and Ghilardi, S., Directed frames, Archive for Mathematical Logic 29 (1989), 53–67.

[2] Gabbay, D. M., Application of trees to intermediate logics,Journal of symbolic logic 37 (1972), 135–138.

[3] Ghilardi, S., presheaf semantics and independence results for some non-classical first-order logics, Archive for Mathematical Logic 29 (1989), 125–136.

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

[5] Isoda, E., and Shimura, T., Kripke incompleteness of some predicate extensions of modal subframe logics without finite embedding property, Bulletin of Section of Logic 27 (1998), pp. 182–189.

[6] Shimura, T., Cut-free systems for modal logics containing S4, Reports on Mathematical Logic 26 (1992), 39–65.

[7] 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.

[8] Umezawa, T., On some properties of intermediate logics, Proceedings of Japan Academy 35 (1959), 575–577.

Quantum Set Theory

Satoko Titani

                           titani@chubu.ac.jp

Chubu University

1 Introduction

Quantum physics is interpreted in a Hilbert space model : Physical states are represented as vectors in a Hilbert space, and observables are represented as self-adjoint operators on the Hilbert space. Let H be a Hilbert space realizing a physical system and let Q(H) be the complete orthomodular lattice consisting of closed linear subspaces of H, where

⋁_{α} p_{α} = \overline{⋃_{α} p_{α}},
⋀_{α} p_{α} = ⋂_{α} p_{α},
p^{⊥} = the orthocomplement of p.

Q(H) is the algebraic expression of quantum logic on the physical system.

We deal with a theory on Q(H)-valued sets, in classical set theory. Let V be the universe of classical set theory as our standpoint, and Q = Q(H). Q-valued sets and Q-valued universe V^{Q} consisting of all Q-valued sets are constructed in V. We call V the external universe for V^{Q}. Set theory on the Q-valued universe V^{Q} is called quantum set theory.

In [1] and [2], G.Takeuti developed the quantum set theory and showed that each real number in V^{Q}, which is defined as a Dedekind cut of rational numbers, represents a self-adjoint operator in the external universe V. We call these reals in V^{Q} q-reals. Thus, observables are represented by q-reals. G.Takeuti defined addition + and multiplication · for commutative q-reals and showed that they represent the corresponding operations on the set of self-adjoint operators. Even if self-adjoint operators u, v are not commutative, u + v and u · v are defined as linear operators.

We develop Takeuti’s quantum set theory by adding a strong implication to the logic, and extend the concept of q-reals and q-complexes.

2 Quantum Logic

Let C be a property of the states of a physical system S. C is considered as an observable as follows: Each measurement which distinguished between the presence or absence of C is considered as a measurement of this observable, such that its value is 1 if C is verified, and zero in the opposite case. The observable that is identified with property C is represented by a projection [[C]] on H. Namely, [[C]] is the projection on the closed subspace consisting of all states φ which possess the property C with certainty. The closed subspace which is the range of [[C]] will also denoted by [[C]] without any confusion. [[C]] is an element of Q, and is also a q-real in V^{Q} as a projection.

Now we consider the property C as a proposition with the truth value [[C]], and logical operators ∧, ∨ are interpreted as lattice operators ∧, ∨ on Q. Complete orthomodular lattice Q = Q(H) consisting of closed subspaces of a complex Hilbert space H is called quantum logic. Q is irreducible, that is, the center Z(Q) of Q consists of two elements 0 and 1. We define implication → on Q by

(p → q) {def \atop =} ⋁\{x∈Z(Q) | p ∧ x ≤ q\} = \{ \begin{matrix}1 & if p ≤ q \\ 0 & otherwise. \end{matrix}

This implication represents the lattice order ≤ on Q, and is called the basic implication.

Generally, lattice valued universe V^{L} is constructed for any complete lattice L. In [3], we showed that a lattice valued set theory on the lattice valued universe V^{L} can be developed by introducing the basic implication →.

Our quantum logic has, as primitive logical symbols, ∧, ∨, ∀, ∃, orthogonal complementation ^{⊥}, and basic implication →.

3 Quantum set theory

Quantum valued universe V^{Q}, consisting of all Q-valued sets, is constructed in the same way as Boolean valued universe V^{B} in the external universe V of classical set theory. G.Takeuti developed a quantum set theory in [1] and [2] using the notation p → q by which he denotes p^{⊥} ∨ (p ∧ q). We call p^{⊥} ∨ (p ∧ q) quantum implication, and denote it by →_{Q} in order to distinguish from the basic implication →. That is,

p →_{Q} q \underleftrightarrow{def} p^{⊥} ∨ (p ∧ q).

→_{Q} is weaker than → in the sense that (p → q) ≤ (p →_{Q} q). Equality and membership relation =_{Q} and ∈_{Q} corresponding to the quantum implication are interpreted on the universe V^{Q} in [1] and [2] as follows :

[[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)

For the quantum equality =_{Q}, the axiom of equality is not valid, because of non-distributivity of Q. Distributive law

p ∧ (q ∨ r) = (p ∧ q) ∨ (p ∧ r)

holds only in the case that p commutative with both of q and r, where “p commutative with q” means that

p = (p ∧ q) ∨ (p ∧ q^{⊥}).

Thus, the axiom of equality for =_{Q} is restricted. This means that the quantum equality =_{Q} is not strong enough to be qualified for an equality.

So, as primitive predicate symbles, we introduce = and ∈ corresponding to the basic implication →. They are interpreted on V^{Q} as

[[u=v]] = ⋀_{x∈Du}(u(x) → [[x∈v]]) ∧ ⋀_{x∈Dv}(v(x) → [[x∈u]])
[[u∈v]] = ⋁_{x∈Dv}[[u=x]] ∧ v(x).

These = and ∈ are called the basic equality and the basic membership relation. The quantum equality =_{Q} and the quantum membership relation ∈_{Q} will be defined in our quantum set theory.

We use the following abbreviations.

φ →_{Q} ψ \underleftrightarrow{def} φ^{⊥} ∨ (ψ ∧ φ)
φ\begin{matrix}| \\ ∘ \end{matrix}ψ \underleftrightarrow{def} φ → (φ ∧ ψ) ∨ (φ ∧ ψ^{⊥})
\begin{matrix}| \\ ∘ \end{matrix}(Γ) \underleftrightarrow{def} ⋀_{φ,ψ∈Γ} φ\begin{matrix}| \\ ∘ \end{matrix}ψ

φ \underleftrightarrow{def} (φ → φ) → φ

Then the following nonlogical axioms GA1–GA11 of lattice valued set theory LZFZ in [3] are valid on V^{Q}.

GA1. Equality ∀u∀v (u = v ∧ φ(u) → φ(v)) .

GA2. Extensionality ∀u, v (∀x(x∈u ↔ x∈v) → u = v).

GA3. Pairing ∀u, v∃z (∀x(x∈z ↔ (x = u ∨ x = v))).

The set z satisfying ∀x(x∈z ↔ (x = u ∨ x = v)) is denoted by {u, v}.

GA4. Union ∀u∃z (∀x(x∈z ↔ ∃y ∈u(x∈y))) .

The set z satisfying ∀x(x∈z ↔ ∃y ∈u(x∈y)) is denoted by ⋃ u.

GA5. Power set ∀u∃z (∀x(x∈z ↔ x ⊂ u)), where

x⊂u \underleftrightarrow{def} ∀y(y ∈x → y ∈u).

The set z satisfying ∀x(x∈z ↔ x⊂u) is denoted by P(u).

GA6. Infinity ∃u (∃x(x∈u) ∧ ∀x(x∈u → ∃y ∈u(x∈y))) .

GA7. Separation ∀u∃v (∀x(x∈v ↔ x∈u ∧ φ(x))).

The set v satisfying ∀x(x∈v ↔ x∈u ∧ φ(x)) is denoted by {x∈u | φ(x)}.

GA8. Collection

∀u∃v (∀x(x∈u → ∃yφ(x, y)) → ∀x(x∈u → ∃y ∈vφ(x, y))).

GA9. ∈-induction ∀x (∀y(y ∈ x → φ(y)) → φ(x)) → ∀xφ(x).

GA10. Zorn Gl(u) ∧ ∀v (Chain(v, u) → ⋃ v ∈ u) → ∃zMax(z, u), where

Gl(u) \underleftrightarrow{def} ∀x(x ∈ u → x ∈ u),
Chain(v, u) \underleftrightarrow{def} v ⊂u ∧ ∀x, y(x, y ∈v → x⊂y ∨ y ⊂x),
Max(z, u) \underleftrightarrow{def} z ∈ u ∧ ∀x(x∈u ∧ z ⊂x → z = x).

GA11. Axiom of ♢ ∀u∃z∀t(t∈z ↔ ♢(t∈u)).

The set z satisfying ∀t(t∈z ↔ ♢(t∈u)) is denoted by ♢u.

We take GA1–GA11 as nonlogical axioms of quantum set theory. Then the induction principle is provable in the quantum set theory, and enables us to define the quantum equality =_{Q} and quantum membership relation ∈_{Q}, inductively.

4 Quantum numbers

The external universe V, in which V^{Q} is constructed, can be embedded in V^{Q} :

u ↦ ǔ ∈ V^{Q} for u∈V

The set of rational numbers in V^{Q} is Q̌ corresponding to the set of rational numbers Q in V by the embedding. Real numbers are defined as Dedekind cuts of Q̌. (cf.[1]). Since V^{Q} has more members than V̌, Dedekind cuts of Q̌ in V^{Q} are more rich than those in V. The set of q-reals is denoted by R^{Q}. Q-reals represent self-adjoint operators on the Hilbert space H, hence q-reals represent observables in the physical system. If u, v are commutative q-reals, then u + v and u · v are defined in R^{Q}, as shown in [1]. Q-complexes are defined as u + iv where u, v are commutative q-reals. Each q-complex represents normal operator on H. The set of all q-complexes is denoted by C^{Q}, and the set of all bounded q-complexes is denoted by C_{b}^{Q}.

Let L(H) be the set of closed and densely defined linear operators on H. Self-adjoint operators and normal operators are in L(H), that is, R^{Q} and C^{Q} are subsets of L(H). We extend the concept of numbers such as q-reals and q-complexes to closed and densely defined linear operators. For that, we represent H as a Hilbert space H in V^{Q}.

For a q-real A, that is, a self-adjoint operator A on H, there exists a unique resolution E of the identity such that A = ∫ λdE(λ). Let E be the set of all resolutions of the identity. We can show that for each resolution of the identity, E ∈E, there exists an isomorphism of H into C^{Q} :

σ_{E}:H→C^{Q}

σ_{E}(H) is a Hilbert space over Č. It follows that each vector x in H is considered as a mapping of E into C^{Q} :

x̂:E →C^{Q} by x̂(E) = σ_{E}(x)

For each E ∈E, let

H(E) = {x̂(E) | x∈H}
H_{b}(E) = H(E) ∩ C_{b}^{Q}

H(E) is isomorphic to H as Hilbert space. H_{b}(E) is dense in H(E) and forms an abelian von Neumann algebra. Each u∈H(E) defines a multiplication operator û on H_{b}(E) :

û : x̂(E) ↦ (ux)ˆ (E) = u · x̂(E)

We represent H as the set of x̂∈Π_{E∈E}H(E)∈V^{Q}, and denote it by H.

H = {x̂:E →C^{Q} | x∈H}⊂Π_{E∈E}H(E)∈V^{Q}.

Thus, q-real (or q-complex) ∫ λdE(λ) is in H(E), and represents a self-adjoint operator (or normal operator) on H.

H can be defined in the language of quantum set theory, and q-reals (or q-complexes) are considered as closed and densely defined linear operators on H. Let L(H) be the set of all closed and densely defined linear operators on H. Members of L(H) we call q-numbers.

References

[1] G.Takeuti, Two Applications of Logic to Mathematics, Iwanami and Princeton University Press, Tokyo and Princeton (1978).

[2] G.Takeuti, Quantum Set Theory, Current Issues in Quantum Logic, eds. E.Beltrametti and B.C.van Frassen, Plenum,New York (1981) p.303

[3] S.Titani, Lattice Valued Set Theory, Arch. Math. Logic vol 38-6(1999).

A real vector space which has a base but which has no well-orderable one

Nobutaka Tsukada

Institute of Mathematics, Tsukuba University

This paper is not included in this on-line proceedings.

Epistemic Models of Shallow Depths and Decision Making in Games

Mamoru Kaneko

kaneko@shako.sk.tsukuba.ac.jp

Institute of Policy and Planning Science, Tsukuba University

Nobu-Yuki Suzuki

smnsuzu@ipc.shuzuoka.ac.jp

Department of Mathematics, Shizuoka University

This paper is not included in this on-line proceedings.

37

A new system of common knowledge predicate logic

Takashi Nagashima^{∗}

Private address: 351-76 Kohan 2-chōme, Higashiyamato-shi, 207-0002 Japan

                      nagasima-t@mta.biglobe.ne.jp
                   http://www2s.biglobe.ne.jp/~hotori/

Yoshihito Tanaka^{∗} Kyushu Sangyo University, 2-3-1 Matsukadai, Higashi-ku, Fukuoka 813-8503, Japan

                        ytanaka@ip.kyusan-u.ac.jp

January 12, 2000, at MLG meeting in Yuzawa

Abstract

We propose a Kripke complete sequent calculus for common knowledge predicate logic^{1}. Though the system is infinitary, it is finitary except for one inference rule.

Kaneko and Nagashima [KN96, KN97] proposed a system GL_{ω} for predicate common knowledge logic. The system GL_{ω} is infinitary in the following sense: (1) GL_{ω} allows conjunctions and disjunctions of countably many formulae. Common knowledge is defined as an infinite conjunction. (2) GL_{ω} has inference rules with countably many premises.

Halpern and Moses [HM92] proposed a finitary system for propositional common knowledge logic. In contrast to GL_{ω}, Halpern and Moses’ system has a symbol for common knowledge. The system has a set of an axiom and an inference rule which defines common knowledge as a fixed point.

A seemingly natural system for predicate common knowledge logic would be obtained by adding quantification rules to Halpern and Moses’ system. However, this cannot be Kripke complete. Indeed, any Kripke complete system for predicate common knowledge logic cannot be finitary because of the following: Fact. (Wolter [W99]) Any Kripke complete system for predicate common knowledge logic is not recursively enumerable.

Here we propose a Kripke complete sequent calculus CK for common knowledge predicate logic. Though the system CK is infinitary, it is finitary except for one inference rule. The system CK has a symbol for common knowledge, and the meaning of this symbol is determined with two inference rules.

The language L of CK consists of the following symbols. A positive integer n is fixed throughout this article. Free variables a_{0}, a_{1}, … (countably many). Bound variables x_{0}, x_{1}, … (countably many). Individual constants (at most finite). Predicate letters. Logical symbols ¬, ⊃, ∧, ∨, ∀, ∃. Epistemic symbols K_{1}, …, K_{n}, C.

∗Supported partially by Grant-in-Aid for Scientific Research, Ministry of Education, Science and Culture.The authors would like thank to Mamoru Kaneko and Nobu-Yuki Suzuki for their valuable comments.

1We consider common knowledge logics based upon KD4, but similar arguments may be carried out for some other modal logics such as K, S4 and so on.

N = {1, …, n} is the set of agents or players. K_{i} means that agent i knows (or believes) a proposition. C means that it is common knowledge among the agents in N.

Formulae are constructed as in the classical predicate logic with the additional rules: If A is a formula then K_{i}A is a formula (i = 1, …, n); If A is a formula then CA is a formula.

A sequent is an expression of the form Γ ⟶ Θ where Γ and Θ are finite sets of formulae.

Let N^{∗} be the set of all words i_{1} … i_{m} (i_{1} ∈ N, …, i_{m} ∈ N, m ≥ 0) on the alphabet N = {1, …, n}. The concatenation of words u ∈ N^{∗} and v ∈ N^{∗} is denoted as uv. The length of a word w ∈ N^{∗} is denoted as |w|. Let N^{⟨ω⟩} = {i_{1} … i_{m} | m ≥ 0, i_{1} ≠ i_{2} ≠ … ≠ i_{m}} ⊂ N^{∗}. For a word e = i_{1} … i_{m} ∈ N^{⟨ω⟩}, K_{i_{1}} ⋯ K_{i_{m}} is abbreviated as K_{e}. For e = i_{1}i_{2} … i_{m} ∈ N^{⟨ω⟩} and e′ = j_{1}j_{2} … j_{l} ∈ N^{⟨ω⟩}, e ∗ e′ is defined as

e ∗ e′ = \{ \begin{matrix}i_{1}i_{2} … i_{m}j_{2} … j_{l} & if e ≠ ε, e′ ≠ ε and i_{m} = j_{1}, \\ i_{1}i_{2} … i_{m}j_{1}j_{2} … j_{l} = ee′ & otherwise. \end{matrix}

N^{⟨ω⟩} is closed under this operation. Now we introduce a notation K[u; Δ; A] where A is a formula, u ∈ N^{∗}, and Δ is a sequence of formulae such that |u| = |Δ|. K[i_{1}i_{2} … i_{k}; D_{1}, D_{2}, …, D_{k}; A] means

K_{i_{1}}(D_{1} ⊃ K_{i_{2}}(D_{2} ⊃ … ⊃ K_{i_{k}}(D_{k} ⊃ A) …)).

The notation K[u; Δ; A] is meaningful only when |u| = |Δ|.

The system CK has the following schemas for initial sequents and inference rules. The only infinitary rule is (→ C), which has countably many premises.

Initial Sequent: A ⟶ A Inference rules:

{Γ ⟶ Θ \atop Γ, Δ ⟶ Θ, Λ} (set)
\begin{matrix}Γ ⟶ Θ, A & A, Δ ⟶ Λ \\ Γ, Δ ⟶ Θ, Λ \end{matrix} (cut)
{Γ ⟶ Θ, A \atop ¬A, Γ ⟶ Θ} (¬ →)  {A, Γ ⟶ Θ \atop Γ ⟶ Θ, ¬A} (→ ¬)
\begin{matrix}Γ ⟶ Θ, A & B, Δ ⟶ Λ \\ A ⊃ B, Γ, Δ ⟶ Θ, Λ \end{matrix} (⊃ →)  {A, Γ ⟶ Θ, B \atop Γ ⟶ Θ, A ⊃ B} (→ ⊃)

\begin{matrix}{B, Γ ⟶ Θ \atop A ∧ B, Γ ⟶ Θ} & (∧ →) \\ {A, Γ ⟶ Θ \atop A ∧ B, Γ ⟶ Θ} & (∧ →) \end{matrix}  \begin{matrix}Γ ⟶ Θ, A & Γ ⟶ Θ, B \\ Γ ⟶ Θ, A ∧ B \end{matrix} (→ ∧)

\begin{matrix}A, Γ ⟶ Θ & B, Γ ⟶ Θ \\ A ∨ B, Γ ⟶ Θ \end{matrix} (∨ →)  \begin{matrix}{Γ ⟶ Θ, A \atop Γ ⟶ Θ, A ∨ B} & (→ ∨) \\ {Γ ⟶ Θ, B \atop Γ ⟶ Θ, A ∨ B} & (→ ∨) \end{matrix}

{F (t), Γ ⟶ Θ \atop ∀x F (x), Γ ⟶ Θ} (∀ →)  {Γ ⟶ Θ, K[u; Δ; F (a)] \atop Γ ⟶ Θ, K[u; Δ; ∀x F (x)]} (→ ∀) (u ∈ N^{∗})
{F (a), Γ ⟶ Θ \atop ∃x F (x), Γ ⟶ Θ} (∃ →)  {Γ ⟶ Θ, F (t) \atop Γ ⟶ Θ, ∃x F (x)} (→ ∃)
{Γ, K_{i}Δ ⟶ Θ \atop K_{i}Γ, K_{i}Δ ⟶ K_{i}Θ} (K_{i}) (i ∈ N , |Θ| ≤ 1)

{K_{e}A, Γ ⟶ Θ \atop CA, Γ ⟶ Θ} (C →) (e ∈ N^{⟨ω⟩})  \{Γ ⟶ Θ, K[u; Δ; K_{e}A] | e ∈ N^{⟨ω⟩}\} ; Γ ⟶ Θ, K[u; Δ; CA] (→ C) (u ∈ N^{∗})

Condition on variables: In the rules (→ ∀) and (∃ →), the free variable a should not occur in the lower sequent.

We define the fixed-point systems HM^{2}, QHM and QHM + BF as follows. The language L′ of HM is the propositional fragment of L. The system HM is Hilbert style calculus for propositional multimodal KD4_{n} with an additional axiom

2Slightly different from the original systems in [HM92] but the difference is not essential.

CA ⊃ A ∧ K_{1}CA ∧ … ∧ K_{n}CA

and an additional inference rule

{B ⊃ A ∧ K_{1}B ∧ … ∧ K_{n}B \atop B ⊃ CA} .

The quantificational extension QHM is a system over L, and it has additional quantification rules same as in classical predicate logic. The system QHM + BF is QHM with additional Barcan axiom BF:

∀x K_{i}F (x) ⊃ K_{i}∀x F (x).

Theorem 1. CK is Kripke complete.

Proof will be reported at proof 2000 meeting^{3}.

Lemma 2. ⊢_{CK} K_{u}A ⟶ K[u; Δ; A] and ⊢_{CK} K[u; ⊤, …, ⊤; A] ⟶ K_{u}A, where ⊤ is A_{0} ⊃ A_{0} and A_{0} is any closed atomic formula.

Theorem 3. [Barcan rule] ⊢_{CK} ∀x K_{i}F (x) ⟶ K_{i}∀x F (x). Proof. By Lemma 2,

\begin{matrix}\begin{matrix}{K_{i}F (a) ⟶ K_{i}(⊤ ⊃ F (a)) \atop ∀x K_{i}F (x) ⟶ K_{i}(⊤ ⊃ F (a))} & (∀ →) \\ ∀x K_{i}F (x) ⟶ K_{i}(⊤ ⊃ ∀x F (x)) \end{matrix} ; (→ ∀) & K_{i}(⊤ ⊃ ∀x F (x)) ⟶ K_{i}∀x F (x) \\ ∀x K_{i}F (x) ⟶ K_{i}∀x F (x) \end{matrix} (cut)

Lemma 4. If ⊢_{CK} K_{e_{1}}A_{1}, …, K_{e_{m}}A_{m} ⟶ Θ and if |Θ| ≤ 1 then ⊢_{CK} K_{e∗e_{1}}A_{1}, …, K_{e∗e_{m}}A_{m} ⟶ K_{e}Θ.

Lemma 5. [Barcan rule for K_{e}] ⊢_{CK} ∀x K_{e}F (x) ⟶ K_{e}∀x F (x).

Theorem 6. [Barcan rule for C] ⊢_{CK} ∀x CF (x) ⟶ C∀x F (x).

Theorem 7. [Conservativeness] If A contains none of K_{1}, …, K_{n}, C then ⊢_{CK} A ⟺ ⊢_{LK} A. Proof. Similarly as in proof of Proposition 4.1 of [KN96], the result of eliminating all occurrences of K_{1}, …, K_{n}, C from a CK-proof can be easily transformed into an LK-proof.

Theorem 8. [Conservativeness] If A contains no C then ⊢_{CK} A if and only if A is provable in QKD4_{n} + BF, where QKD4_{n} is the quantificational extension of multimodal KD4_{n}.

Conjecture. If no C occurs positively in a CK-provable formula A then there exists a CK-proof of A without (→ C).

Lemma 9. (1) ⊢_{CK} CA ⟶ A.  (2) ⊢_{CK} CA ⟶ K_{i}CA.  (3) ⊢_{CK} CA ⟶ CCA.

(4) If ⊢_{CK} Γ ⟶ A then ⊢_{CK} CΓ ⟶ CA.

Theorem 10. A CK-provable formula containing none of K_{1}, …, K_{n} is provable in S4 if we regard C as the box symbol . Conversely, a S4-provable formula is provable in CK if we regard as C. Proof. First we replace all occurrences of K_{1}, …, K_{n}, C by in a given CK-proof. The result of this replacement can be easily converted into an S4-proof. The converse follows from Lemma 9.

Theorem 11. [Conservativeness] If a quantifier-free sequent Γ ⟶ Θ is provable in CK then there exists a CK-proof of Γ ⟶ Θ without quantifier rules. Corollary 12. If a quantifier-free formula is provable in CK, then it is provable in HM.^{4}

Theorem 13. [Fixed point] ⊢_{CK} CA ⟶ A ∧ K_{1}CA ∧ … ∧ K_{n}CA and ⊢_{CK} A, K_{1}CA, …, K_{n}CA ⟶ CA.

3“Shōmeiron kenkyūshūkai”, January 18–20, Tokyo University, Komaba, Tokyo

4Cf. Kaneko’s Theorem 3.4 in [K99]

Theorem 14. If ⊢_{CK} B ⟶ A ∧ K_{1}B ∧ … K_{n}B then ⊢_{CK} B ⟶ CA.

Definition. [K99] A formula in GL_{ω} is a cc-formula if it satisfies the following conditions.

(1) It contains no infinitary disjunction.

(2) If it contains an infinitary conjunction then the conjunction has the form ∧{K_{e}B | e ∈ N^{⟨ω⟩}} for some B.

Definition. [K99] We define a mapping ψ which transforms a L-formula into a cc-formula. Definition is by induction on the structure of formula.

(1) If no C occurs in A, then ψ(A) is A.

(2) ψ(A ⊃ B) is ψ(A) ⊃ ψ(B) and similarly for the other logical symbols.

(3) ψ(K_{i}A) is K_{i}(ψ(A)).

(4) ψ(CA) is ∧{K_{e}(ψ(A)) | e ∈ N^{⟨ω⟩}}.

Kaneko [K99] proved that ψ is a bijection from the set of L-formulae to the set of cc-formulae. Theorem 15. If a formula A is provable in CK, then ψ(A) is provable in GL_{ω}.

Theorem 16. If a cc-formula A is provable in GL_{ω}, then ψ^{−1}(A) is provable in CK.

For a certain propositional fragment of GL_{ω}, a corresponding theorem is proved by Kaneko [K99]. Proof. If a cc-formula A is provable in GL_{ω}, then ψ^{−1}(A) is valid in every Kripke model of CK, hence provable.

Any formula provable in QHM + BF is provable in CK, but not conversely. Open problems. (1) Find a formula that is CK-provable but not provable in QHM + BF. (2) [Hiroakira Ono] What X makes QHM + BF + X equivalent to CK?

References

[HM92] Halpern, Joseph Y. and Moses, Yoram:

A guide to completeness and complexity for modal logics of knowledge and belief .

Artificial Intelligence, 54 (1992), pp. 319–379.

[K99] Kaneko, Mamoru: Common knowledge logic and game logic.

J. Symbolic Logic, 64, No. 2 (1999), pp.685–700.

[KN96] Kaneko, Mamoru and Nagashima, Takashi: Game logic and its applications I . Studia Logica, Vol.57 (1996), pp.325–354.

[KN97] Kaneko, Mamoru and Nagashima, Takashi: Game logic and its applications II . Studia Logica, Vol.58 (1997), pp.273–303.

[W98] Wolter, Frank: Fragments of common knowledge logics.

Invited talk at LOFT3, to appear in Studia Logica.

     Manuscript available at http://www.informatik.uni-leipzig.de/~wolter/.

Ultraproduct of Kripke sheaves and Halldén-completeness in super-intuitionistic predicate logics

Nobu-Yuki SUZUKI

                       smnsuzu@ipc.shizuoka.ac.jp

Department of Mathematics, Shizuoka University

Abstract The Kripke sheaf semantics is an extended Kripke-type semantics, and was introduced in Shehtman-Skvortsov[1]. We can introduce ultraproduct of Kripke sheaves and present an application to variants of Halldén-completeness in super-intuitionistic predicate logics.

1 Kripke sheaves and their ultraproducts

We fix a pure first-order language L. Note that L contains neither individual constants nor function symbols. For each non-empty set U, we denote by L[U] the language obtained from L by adding the name \overline{u} of each u ∈ U. In what follows, we will sometimes use the same letter u for the name of u.

Definition 1.1 A partially ordered set M = ⟨M, ≤⟩ with the least element 0_{M} is said to be a Kripke base (for super-intuitionistic logics). We can regard a Kripke base M as a category in the usual way. Let S denote the category of all non-empty sets. A covariant functor D from a Kripke base M to S is called a domain-sheaf over M. That is,

DS1) D(a) is a non-empty set for every a ∈ M, DS2) for every a, b ∈ M with a ≤ b, there exists a mapping D_{ab} : D(a) → D(b), DS3) D_{aa} is the identity mapping id_{D(a)} of D(a) for every a ∈ M, DS4) D_{ac} = D_{bc} ∘ D_{ab} for every a, b, c ∈ M with a ≤ b ≤ c.

A pair K = ⟨M, D⟩ of a Kripke base M and a domain-sheaf D over M is called a Kripke sheaf (for super-intuitionistic predicate logics).

If every D_{ab} (a ≤ b) is the set-theoretic inclusion, ⟨M, D⟩ is said to be a Kripke frame (for superintuitionistic predicate logics). Intuitively, each D(a) is the individual domain of the world a ∈ M. For each d ∈ D(a) and each b ∈ M with a ≤ b, D_{ab}(d) is said to be the inheritor of d at b. For each formula A of L[D(a)] and each b ∈ M with a ≤ b, the inheritor A_{a,b} of A at b is a formula of L[D(b)] obtained from A by replacing occurrences of \overline{u} (u ∈ D(a)) by the name \overline{v} of the inheritor v of u at b. That is, A_{ab} is A^{D_{ab}}.

A binary relation ⊧ between each a ∈ M and each atomic sentence of L[D(a)] is said to be a valuation on ⟨M, D⟩ if for every a, b ∈ M and every atomic sentence A of L[D(a)], a ⊧ A and a ≤ b imply b ⊧ A_{a,b}. We extend ⊧ to a relation between each a ∈ M and each sentence of L[D(a)] inductively as follows:

• a ⊧ A ∧ B if and only if a ⊧ A and a ⊧ B,

• a ⊧ A ∨ B if and only if a ⊧ A or a ⊧ B,

• a ⊧ A ⊃ B if and only if for every b ∈ M with a ≤ b, either b |̸= A_{a,b} or b ⊧ B_{a,b},

• a ⊧ ¬A if and only if for every b ∈ M with a ≤ b, b |̸= A_{a,b},

• a ⊧ ∀xA(x) if and only if for every b ∈ M with a ≤ b and every u ∈ D(b), b ⊧ A_{a,b}(\overline{u}),

• a ⊧ ∃xA(x) if and only if there exists u ∈ D(a) such that a ⊧ A(\overline{u}).

A pair (K, ⊧) of a Kripke sheaf K and a valuation ⊧ on it is said to be a Kripke-sheaf model. A formula A of L is said to be true in a Kripke-sheaf model (K, ⊧) if 0_{M} ⊧ \overline{A}, where \overline{A} is the universal closure of A. A formula A of L is said to be valid in a Kripke sheaf K if for every valuation ⊧ on K, A is true in (K, ⊧). The set of formulas of L valid in K = ⟨M, D⟩ is denoted by L(K) or L⟨M, D⟩. The following propositions are fundamental properties of Kripke-sheaf semantics.

Proposition 1.2 For every Kripke-sheaf model (⟨M, D⟩, ⊧), every a, b ∈ M, and every sentence A ∈ L[D(a)], if a ⊧ A and a ≤ b, then b ⊧ A_{a,b}.

Proposition 1.3 For each Kripke-sheaf K, the set L(K) contains all formulas provable in H_{∗}, and is closed under the modus ponens, the rule of generalization and the rule of substitution. Namely, L(K) is a super-intuitionistic predicate logic.

By virtue of this Proposition, we can apply the Kripke sheaf semantics to the study of superintuitionistic predicate logics. Now we introduce ultraproduct of Kripke sheaves. First, we state a first-order representation of Kripke sheaves.

Definition 1.4 A triple ⟨W, R, ρ⟩ of a non-empty set W, a quasi-order R on W and a partial order ρ on W is said to be a double-ordered structure, if

WS0) W has an R-minimum element 0_{R}. WS1) for every a, b ∈ W, aρb implies aRb. WS2) for every a, b ∈ W, aRb implies that there exists exactly one c such that aρc and c ∼_{R} b.

where ∼_{R} is the equivalence relation induced by R. The c determined by a and b is denoted by [a]_{b}

Double-ordered structures are first-order representation of Kripke sheaves. Let ⟨W, R, ρ⟩ be a doubleordered structure. We denote by W^{∗} the partially ordered set induced by the quasi-ordered set (W, R). Define D^{∗}(a/∼_{R}) = a/∼_{R} for each a/∼_{R}∈ W^{∗}, and for every a/∼_{R}, b/∼_{R}∈ W^{∗} with aRb,

D_{a/∼_{R} b/∼_{R}}^{∗}(d) = [d]_{b}

for each d ∈ a/∼_{R}. Then ⟨W^{∗}, D^{∗}⟩ is a Kripke sheaf with the least element 0_{R}/∼_{R} of W^{∗}.

Theorem 1.5 For every Kripke sheaf ⟨M, D⟩, there exits a double-ordered structure ⟨W, R, ρ⟩ such that ⟨W^{∗}, D^{∗}⟩ is isomorphic to ⟨M, D⟩.

Conversely, we can show that every double-ordered structure is obtained from a Kripke sheaf. Since double-ordered structures are first-order structures, we can introduce ultraproducts of them very easily as first-order structures. Let {⟨M_{i}, D_{i}, ⊧_{i}⟩; i ∈ I} be a family of Kripke sheaf models and U an ultrafilter over I. We denote the untraproduct by ⟨Π_{U}M_{i}, Π_{U}D_{i}, Π_{U} ⊧_{i}⟩. Note that the Kripke base of the ultraproduct product ⟨Π_{U}M_{i}, Π_{U}D_{i}, Π_{U} ⊧_{i}⟩ is (isomorphic to the partially ordered set) obtained from {M_{i}; i ∈ I} by taking ultraproduct. Therefore we write it by Π_{U}M_{i}.

Theorem 1.6 (à la Łoś) Let A(x_{1}, …, x_{n}) be a formula of L having no free variables other than x_{1}, …, x_{n}. Then for every a/U ∈ Π_{U}M_{i} and every d_{1}/U, …, d_{n}/U ∈ Π_{U}D_{i}(a/U),

a/UΠ_{U}⊧_{i} A(d_{1}/U, …, d_{n}/U) if and only if {i ∈ I; d_{1}(i) ∈ D_{i}(a(i)), …, d_{n}(i) ∈ D_{i}(a(i)) and a(i) ⊧_{i} A(d_{1}(i), …, d_{n}(i))} ∈ U.

2 Halldén-completeness

Definition 2.1 (Cf. [2] and [4]) A super-intuitionistic predicate logic L is said to be Halldéncomplete (H-complete), if for every formulas A and B containing no predicate variable in common, A ∨ B ∈ L implies either A ∈ L or B ∈ L. A super-intuitionistic predicate logic L is said to be sentential Halldén-complete (SH-complete), if for every sentences S and T containing no predicate variable in common, S ∨ T ∈ L implies either S ∈ L or T ∈ L.

For super-intuitionistic propositional logics, H-completeness and SH-completeness are the same concept by the definition. We have the following facts for super-intuitionistic propositional logics.

Fact 2.2 Let L be a super-intuitionistic propositional logic.

(1) L is H-complete if and only if L is meet-irreducible.

(2) (Wroński [4]) L is H-complete if and only if L is characterized by a single subdirectly irreducible Heyting algebra.

Since every logic is a (possibly infinite) meet of meet-irreducible elements, every super-intuitionistic propositional logic turns out to be a (possibly infinite) meet of H-complete logics.

We will try to deal with these concepts in super-intuitionistic predicate logics. For super-intuitionistic predicate logics, Semantical tools do not work well as they do in the study of propositional logics. We try to use Kripke sheaves here. The following can be shown quite easily.

Proposition 2.3 Let L be a super-intuitionistic predicate logic characterized by a single Kripke sheaf. Then L is SH-complete.

We can show a partial converse of Proposition 2.3 by making use of the ultraproduct construction.

Theorem 2.4 Let L be a super-intuitionistic predicate logic characterized by a class C of Kripke sheaves such that C is closed under ultraproducts. Then the following conditions are equivalent.

(1) L is SH-complete.

(2) L is characterized by a single Kripke sheaf.

Clearly, H-completeness implies SH-completeness. But the converse does not hold. To show this, we introduce the following condition on a class C of Kripke sheaves called the joint p-morphism property :

(JPP) for every K_{1} and K_{2} in C, there exist a member K = ⟨M, D⟩ in C, elements a_{1}, a_{2} ∈ M, and p-morphisms f_{1} of K^{a_{1}} to K_{1} and f_{2} of K^{a_{2}} to K_{2}.

where K^{a_{1}} and K^{a_{2}} are generated subsheaves determined by a_{1} and a_{2}, respectively.

Lemma 2.5 Suppose that a class C of Kripke sheaves satisfies (JPP). Then a super-intuitionistic predicate logic characterized by C is SH-complete.

Consider the following condition (#) on a Kripke sheaf ⟨M, D⟩:

(#) ∀x ∈ M : D(x) has exactly two elements.

i.e. ∃d_{1} ∃d_{2} ∈ D(x) d_{1} ≠ d_{2} and ∀e ∈ D(x)(e = d_{1} or e = d_{2}).

Let D be the class of Kripke sheaves satisfying (#). Clearly, D satisfies the condition (JPP). Let L_{0} be a super-intuitionistic predicate logic characterized by D. Then,

(1) D is closed under ultraproducts,

(2) L_{0} is SH-complete,

(3) Hence, L_{0} is characterized by a single Kripke sheaf.

However L_{0} is not H-complete. Let A and B be p(x) ≡ p(y) and (q(y) ≡ q(z))∨(q(z) ≡ q(x)), respectively, where p and q are distinct unary predicate variables and x, y, z are mutually distinct individual variables. Then A and B contain no predicate variable in common. We have A ∨ B ∈ L_{0}, A ∉ L_{0}, and B ∉ L_{0}. Therefore,

Theorem 2.6 SH-completeness does not imply H-completeness.

3 One more variant of Halldén-completeness

We can introduce another variant of Halldén-completeness as follows.

Definition 3.1 A super-intuitionistic predicate logic L is said to be weakly Halldén-complete (WHcomplete), if for every formulas A and B containing no predicate variable nor free individual variable in common, A ∨ B ∈ L implies either A ∈ L or B ∈ L.

It is obvious that WH-completeness implies SH-completeness. Under a condition, WH-completeness is equivalent to SH-completeness.

Proposition 3.2 Let Dis be the sentence ∀x(p(x) ∨ r) ⊃ (∀xp(x) ∨ r), where p and r are a unary predicate variable and a propositional variable, respectively. Suppose that a super-intuitionistic predicate logic L contains Dis. Then, L is SH-complete if and only if L is WH-complete.

Note that the example L_{0} introduced in the previous section contains Dis. Therefore, even if we assume L ∋ Dis, SH-completeness and WH-completeness do not imply H-completeness. Now we show

Theorem 3.3 SH-completeness does not imply WH-completeness.

Proof. Let 2 be {0, 1} with the canonical order, U a mapping of 2 defined by: U(0) = {0} and U(1) = ω = {i : i < ω}. Then ⟨2, U⟩ is a Kripke sheaf. Let L_{1} be a super-intuitionistic predicate logic characterized by ⟨2, U⟩. Clearly L_{1} is SH-complete. Let C and D be formulas p(x) ≡ p(y) and r ∨ ¬r, respectively, where p and r are a unary predicate variable and a propositional variable, respectively. Then C and D contain no predicate variable nor free individual variable in common. Verify that

(0) C ∨ D is valid in ⟨2, U⟩,

(1) neither C nor D is valid in ⟨2, U⟩.

Namely, C ∨ D ∈ L_{1}, C ∉ L_{1}, and D ∉ L_{1}. Therefore, L_{1} is not WH-complete. q.e.d.

References

[1] V. B. Shehtman and D. P. Skvortsov, Semantics of non-classical first-order predicate logics, in Mathematical Logic, edited by P. P. Petkov, Plenum Press, New York, 1990, 105–116.

[2] N.–Y. Suzuki, Some syntactical properties of intermediate predicate logics, Notre Dame Journal of Formal Logic 31(1990), 548–559.

[3] N.–Y. Suzuki, An application of the Kripke sheaf semantics in intermediate predicate logics, Kyoto Daigaku Surikaiseki Kenkyujo Kokyuroku No. 1010(1997), 131–141.

[4] A. Wroński, Remarks on Halldén completeness of modal and intermediate logics, Reports on Mathematical Logic 2(1974), 55–62.

Nobu-Yuki SUZUKI

Department of Mathematics Faculty of Science Shizuoka University Ohya, Shizuoka 422–8529 Japan

Propositional Dynamic Logic has interpolation

Tomasz Kowalski JAIST-Hokuriku, 1–1 Asahidai, Tatsunokuchi, 923-1292 Ishikawa,

                       email: kowalski@jaist.ac.jp

9 January 2000

1 Prelude

Propositional Dynamic Logic (PDL) is the logic corresponding in a natural way to the variety D of dynamic algebras. Consult e.g., [5] for details on dynamic algebras. Precisely speaking, the correspondence holds between D and the so-called test-free PDL, but since it is proved in [2] that test-free PDL has interpolation iff full PDL does, we will systematically disregard the distinction between them. It is also conjectured in [2] that PDL indeed has interpolation.

2 Dynamic algebras

A dynamic algebra is an algebra A = ⟨A; ∨, ∧, ¬, 0, 1, π(π ∈ Π)⟩, such that:

1. ⟨A; ∨, ∧, ¬, 0, 1⟩ is a boolean algebra;

2. Π is the universe of the absolutely free algebra Π = ⟨Π; ∘, ∪, ∗⟩, of the type ⟨2, 2, 1⟩, countably generated by the set Ξ = {ξ_{n} : n ∈ ω}.

3. A satisfies:

(i) π0 = 0, (ii) π(x ∨ y) = πx ∨ πy, (iii) (π ∪ σ)x = πx ∨ σx, (iv) (πσ)x = π(σx),

(v) x ∨ ππ^{∗}x ≤ π^{∗}x ≤ x ∨ π^{∗}(¬x ∧ πx). An algebra A, of the type of dynamic algebras, is called ∗-continuous iff π^{∗}x = ⋁{π^{n} : n ∈ ω}, for all

π ∈ Π, with π^{n}x defined inductively by: π^{0}x = x, π^{n+1}x = ππ^{n}x. All ∗-continuous algebras are dynamic algebras. A class K of dynamic algebras is ∗-continuous iff if all its members are. Fact 1 All finite dynamic algebras are ∗-continuous. If a class K is ∗-continuous, then so is SP (K).

Recall, that an algebra is called residually finite iff it is a subdirect product of finite algebras. Fact 2 ([5] Theorem 5.4.) Free dynamic algebras are residually finite. Lemma 1 Free dynamic algebras are ∗-continuous.

3 Amalgamation and interpolation

A triple ⟨A_{0}, A_{1}, A_{2}⟩ of similar algebras, is called a V-formation iff there are embeddings i_{1} : A_{0} ⟶ A_{1} and i_{2} : A_{0} ⟶ A_{2}. In other words, in a V-formation, A_{1} and A_{2} share an isomorphic copy of A_{0} as a subalgebra. Thus, dealing with V-formations we will always tacitly assume i_{1} and i_{2} to be identity maps.

A V-formation ⟨A_{0}, A_{1}, A_{2}⟩, with A_{i} ∈ K, for i = 0, 1, 2 and K a class of similar algebras, can be amalgamated in K iff there is an algebra B ∈ K and embeddings e_{1} : A_{1} ⟶ B, e_{2} : A_{2} ⟶ B, such that e_{1} ∘ i_{1} = e_{2} ∘ i_{2} (or, by our convention, e_{1}|_{A_{0}} = e_{2}|_{A_{0}}).

A class K of similar algebras has the amalgamation property (AP) iff every V-formation from K can be amalgamated in K.

Assume that the universes of algebras in K are partially ordered. Then K is said to have the superamalgamation property (SupAP) iff for any V-formation ⟨A_{0}, A_{1}, A_{2}⟩, there is a B that amalgamates it, with the embeddings f_{1} : A_{1} ⟶ B and f_{2} : A_{2} ⟶ B, such that we have: for any x ∈ A_{k} and y ∈ A_{j}, if f_{k}(x) ≤ f_{j}(y), then there is a z ∈ A_{0} with x ≤ i_{k}(z), i_{j}(z) ≤ y, where {k, j} = {1, 2} (or, again, by our convention, simply x ≤ z, z ≤ y).

Clearly, SupAP is stronger than AP; thus, by obvious extensions of the definitions above we will speak of V-formations that superamalgamate, or of superamalgams of certain V-formations.

A (propositional) logic Λ, with a certain reasonable implication →, possesses Craig interpolation property iff for any formulas ϕ, ψ in the appropriate language, the following holds:

(†) if ⊢_{Λ} ϕ → ψ, then there is a formula χ, whose variables are a subset of those that ϕ and ψ have in common, and such that ⊢_{Λ} ϕ → χ and ⊢_{Λ} χ → ψ.

The next, crucial, proposition follows easily from Madarász’s generalisation of Maximova’s celebrated theorem (see [3] and [4]), and the folklore about dynamic algebras recalled above. Let F_{K}(Z) stand for the K-free algebra generated by Z. We say that free algebras from K superamalgamate iff every V-formation ⟨F_{K}(X ∩ Y), F_{K}(X), F_{K}(Y)⟩ (which implicitly assumes the existence of all the algebras involved) can be superamalgamated in the variety V(K). If the above holds for finite X and Y, we say that free finitely generated algebras from K superamalgamate.

Proposition 1 For the variety D of dynamic algebras the following are equivalent:

(i) D has SupAP,

(ii) free finitely generated algebras from D superamalgamate,

(iii) Λ(D) has Craig interpolation.

4 Boolean interlude

We will need two constructions well-known in the theory of boolean algebras (BAs). For lack of space we will not recall any definitions, instead, we refer the reader to [1]. The first construction is that of minimal completion.

Fact 3 For any BA A there is a unique complete BA C, such that A ⊆ C and C preserves all joins that exist in A.

The unique complete algebra C above is called the minimal completion of A. Let A ⊆ B be BAs, and C, D their respective minimal completions. We have:

Lemma 2 If B preserves all joins that exist in A, then the embedding i : A ⟶ B extends in a natural way to a complete embedding e : C ⟶ D.

Let F(X), F(Y) be BAs freely generated by X and Y, with Y ⊆ X and |Y | ≤ |X| = ω.

Lemma 3 The identity embedding i : F(Y) ⟶ F(X) preserves all joins that exist in F(Y).

Let ⟨B_{0}, B_{1}, B_{2}⟩ be a V-formation of BAs. The amalgamated free product B of B_{1}, B_{2} over B_{0} satisfies the following characterisation lemma (dual of [2] Corollary 11.22).

Fact 4 B is the amalgamated free product of B_{1}, B_{2} over B_{0}, with the embeddings e_{1}, e_{2} iff e_{1}(B_{1}) ∪ e_{2}(B_{2}) generates B and for any two elements b_{1} ∈ B_{1}, b_{2} ∈ B_{2} with e_{1}(b_{1}) ∨ e_{2}(b_{2}) = 1, there is a c ∈ B_{0} such that b_{1} ≥ ¬c and b_{2} ≥ c.

Under certain completeness assumptions amalgamated free products behave extremely well (cf.[1] Lemma 12.16).

Fact 5 If the algebras B_{0}, B_{1}, B_{2}, and the identity embeddings are all complete, then the amalgamated free product B of ⟨B_{0}, B_{1}, B_{2}⟩ preserves all joins from B_{i} (i = 1, 2).

5 Finale

First we extend the notion of minimal completion to dynamic algebras. Recall that, by Lemma 1, free dynamic algebras are ∗-continuous.

Lemma 4 Fact 3 and Lemma 2 remain valid for ∗-continuous algebras. Lemma 3 holds also for free dynamic algebras.

Then, take the V-formation ⟨F(X ∩ Y), F(X), F(Y)⟩. As D has constants, the free algebras involved always exist. Clearly, the boolean reducts of the algebras above also constitute a V-formation.

Since F(X ∩ Y), F(X), and F(Y) are all ∗-continuous, it follows by the lemma above that there are unique complete ∗-continuous algebras G_{X∩Y}, G_{X}, and G_{Y} with F(Z) ⊆ G_{Z}, for Z ∈ {X, Y, X ∩ Y } such that G_{Z} preserves all joins existing in F(Z). It also follows that for Z ∈ {X, Y }, G_{Z} preserves all joins existing in F(X ∩ Y). Consider the V-formation ⟨G_{X∩Y} , G_{X}, G_{Y} ⟩.

Fact 6 The identity embeddings in ⟨G_{X∩Y} , G_{X}, G_{Y} ⟩ are complete.

Let G be the amalgamated free product of the boolean reducts of G_{X} and G_{Y} over G_{X∩Y}. Let C be the minimal completion of G (as a BA).

Fact 7 C can be expanded to a ∗-continuous algebra D, with D = C. Moreover, D is a superamalgam of ⟨F(X ∩ Y), F(X), F(Y)⟩.

Corollary 1 Free finitely generated algebras from D superamalgamate.

By Proposition 1, we obtain:

Theorem 1 The variety D of dynamic algebras has SupAP. Full propositional dynamic logic has Craig interpolation property.

References

[1] S. Koppelberg, Handbook of Boolean Algebras. Volume 1 (edited by J.D. Monk with R. Bonnet), North Holland, 1989.

[2] M. Kracht, Tools and Techniques in Modal Logic, Elsevier Studies in Logic No. 142, 1999.

[3] J.X. Madarász, Interpolation and Amalgamation; Pushing the Limits. Part I, Studia Logica 61 (1998), 311–345. Part II, Studia Logica 62 (1999), 1–19.

[4] L.L. Maksimova, Interpolation theorems in modal logics and amalgamable varieties of topological boolean algebras, Algebra and Logic 18 (1979), 348–370

[5] V. Pratt, Dynamic Algebras: Examples, Constructions, Applications, Studia Logica 50 (1991), 571–601.

On interpretability logics

Katsumi Sasaki

                        sasaki@iq.nanzan-u.ac.jp

Department of Information Systems and Quantitative Sciences, Nanzan University

The idea of interpretability logics arose in Visser [Vis90]. He introduced the logics as extensions of the provability logic GL with a binary modality ▷. The arithmetic realization of A ▷ B in a theory T will be that T plus the realization of B is interpretable in T plus the realization of A. (T + A interprets T + B). More precisely, there exists a function f (the relative interpretation) on the formulas of the language of T such that T + B ⊢ C implies T + A ⊢ f(C).

The basic interpretability logic IL is the smallest set of formulas containing GL and axioms (J1) : □(p ⊃ q) ⊃ (p ▷ q), (J2) : (p ▷ q) ∧ (q ▷ r) ⊃ (p ▷ r), (J3) : (p ▷ r) ∧ (q ▷ r) ⊃ (p ∨ q ▷ r), (J4) : (p ▷ q) ⊃ (◇p ⊃ ◇q), (J5) : ◇p ▷ p,

and closed under modus ponens, substitution and necessitation. The principles of IL are arithmetically sound for a wide class of theories and for various interpretations of its main connective ▷. The theory is not arithmetically complete for any known interpretation. The motivation for studying this specific set of formulas comes form its modal simplicity and elegance.

The modality ▷ has more than one interpretation. Another most salient interpretation is Π_{1}-conservativity. More precisely, the arithmetic realization of A ▷ B in a theory T, containing IΣ_{1}, will be that T plus the realization of B is Π_{1}-conservative over T plus the interpretation of A. In Berarducci [Ber90] and Shavrukov [Sha88], it was proved that the interpretability logic (ILM) obtained by adding Montagna’s axiom

M : (p ▷ q) ⊃ (p ∧ □r) ▷ (q ∧ □r)

to IL is complete for this arithmetic interpretation. The definition of the arithmetic interpretation ∗ given for the proof of Solovay’s theorem was extended to the language of interpretability logics by stipulating that

(A ▷ B)^{∗} = Conserv(⟨A^{∗}⟩, ⟨B^{∗}⟩), where Conserv(⟨A^{∗}⟩, ⟨B^{∗}⟩) is an intensional formalization of “T + B^{∗} is Π_{1}-conservative over T + A^{∗}”, and it was proved

A ∈ ILM if and only if T ⊢ A^{∗} for any ∗.

The interpretability logic ILP, an extension of IL by adding the axiom

P : (p ▷ q) ⊃ □(p ▷ q),

is also complete for another arithmetic interpretation. P is valid for interpretations in finitely axiomatized arithmetical theories extending, say, IΔ_{0} + Ω_{1}, and an arithmetic completeness for this interpretation was proved in [Vis90].

The completeness with respect to Kripke semantics due to Veltman was, for IL, ILM and ILP, proved in de Jongh and Veltman [JV90]. The fixed point theorem of GL can be extended to IL and hence ILM and ILP(de Jongh and Visser [JV91]). The unary pendant “T interprets T + A” is much less expressive and was studied in de Rijke [Rij92]. For an overview of interpretability logic, see Visser [Vis97], and Japaridze and de Jongh [JJ98].

Here we give a cut-free sequent system for the basic interpretability logic IL. First, we give a cut-free system for a sublogic IK4, whose ▷-free fragment is the modal logic K4. In other words, IK4 is the logic obtained from K4 by adding the axioms (J1), (J2), (J3), (J4) and (J5). Using the system and a property of Löb’s axiom presented in [Sas99c] we obtain a cut-free system for IL.

Let us define a sequent system for IK4. We use Greek letters, possibly with suffixes, for finite sets of formulas, in particular, we use Σ, possibly with suffices, for finite set of ▷-formulas^{1}. The expression Γ_{A} denotes Γ − {A}. For each prefix ◯ ∈ {□, ¬}, the expression ◯Γ denotes the set {◯X|X ∈ Γ}. By a sequent, we mean the expression

Γ → Δ.

For brevity’s sake, we write

A_{1}, ⋯, A_{n}, Γ_{1}, ⋯, Γ_{m} → B_{1}, ⋯, B_{ℓ}, Δ_{1}, ⋯, Δ_{k}

instead of

{A_{1}, ⋯, A_{n}} ∪ Γ_{1} ∪ ⋯ ∪ Γ_{m} → {B_{1}, ⋯, B_{ℓ}} ∪ Δ_{1} ∪ ⋯ ∪ Δ_{k}.

Let S_{1}, ⋯, S_{n} be a sequence of sequents. The depth d_{S_{1},···,S_{n}}(o_{i}) of the occurrence o_{i} of S_{i} denotes n + 1 − i. If there is no confusion, we omit the subscript of d.

Let Σ be a finite set of ▷-formulas. A sequent is said to be a sequent on a sequent Σ, □Γ → A ▷ B if it is of the form

C, □¬(B^{∗}, Δ), Γ, □Γ → B^{∗}, Δ,

where C ∈ {A} ∪ {Y |X ▷ Y ∈ Σ}, Δ ⊆ {X|X ▷ Y ∈ Σ} and

B^{∗} = \{ \begin{matrix}∅ & if B = ⊥ \\ B & otherwise. \end{matrix}

We put

cl(C, □¬(B^{∗}, Δ), Γ, □Γ → B^{∗}, Δ) = C,
cr(C, □¬(B^{∗}, Δ), Γ, □Γ → B^{∗}, Δ) = Δ.

Immediately, a sequent S on Σ, □Γ → A ▷ B is of the form

cl(S), □¬(B^{∗}, cr(S)), Γ, □Γ → B^{∗}, cr(S).

For an occurrence o of a sequent S in SEQ, we also use the expressions cl(o) and cr(o) for cl(S) and cr(S), respectively. We say that a sequence SEQ of sequents is on a sequent Σ, □Γ → A ▷ B if it is finite sequence of sequents on Σ, □Γ → A ▷ B and cl(o) = A for some occurrence o of a sequent in SEQ.

Let Σ′ be a subset of Σ. A mapping

f : {(o, X)|o is an occurrence of a sequent in SEQ, X ∈ cr(o)}

→ {o|o is an occurrence of a sequent in SEQ, cl(o) ≠ A}

is called a mapping on SEQ/Σ′ if X ▷ cl(f(o, X)) ∈ Σ′ and d(o) > d(f(o, X)) for any occurrence o and an formula X ∈ cr(o).

We say that a sequence SEQ of sequents is essential on a sequent Σ, □Γ → A ▷ B if it is on Σ, □Γ → A ▷ B and the following two conditions hold:

(I) there exists an onto mapping on SEQ/Σ,

(II) cl(o_{1}) ≠ cl(o_{2}) for any different occurrences o_{1} and o_{2} of sequents in SEQ.

Let SEQ be an essential sequence on Σ, □Γ → A ▷ B and let f be an onto mapping on SEQ/Σ. Since SEQ is finite, we can see a sequent

C, □¬(B^{∗}, Δ), Γ, □Γ → B^{∗}, Δ

1formulas of the form A ▷ B

at the end occurrence o of SEQ. If X ∈ Δ, then 0 = d(o) > d(f(o, X)). This is a contradiction. So, we have Δ = ∅, i.e., we can see a sequent

Y, □¬B^{∗}, Γ, □Γ → B^{∗}

at the end of the sequence SEQ.

Here we show some examples of essential sequences. A sequence of a sequent

p, □¬q, r, □r → q

is only one essential sequence on

□r → p ▷ q.

Two sequences of sequents

p, □¬q, □¬p_{1} → q, p_{1} q_{1}, □¬q → q

and

p, □¬q → q

are essential on

p_{1} ▷ q_{1} → p ▷ q.

Also two sequences

p, □¬q, □¬p_{1} → q, p_{1} q_{1}, □¬q, □¬p_{2}, → q, p_{2} q_{2}, □¬q → q

and

p, □¬q, □¬p_{1}, □¬p_{2} → q, p_{1}, p_{2} q_{1}, □¬q → q q_{2}, □¬q → q

are essential on

p_{1} ▷ q_{1}, p_{2} ▷ q_{2} → p ▷ q.

Our system GIK4 is defined from the following axioms and inference rules in the usual way.

Axioms of GIK4

A → A
⊥ →

Inference rules of GIK4

\frac{Γ → Δ}{A, Γ → Δ}(T →) \frac{Γ → Δ}{Γ → Δ, A}(→ T)

\frac{Γ → Δ, A A, Π → Λ}{Γ, Π_{A} → Δ_{A}, Λ}(cut)

\frac{A_{i}, Γ → Δ}{A_{1} ∧ A_{2}, Γ → Δ}(∧ →_{i}) \frac{Γ → Δ, A Γ → Δ, B}{Γ → Δ, A ∧ B} (→ ∧)

\frac{A, Γ → Δ B, Γ → Δ}{A ∨ B, Γ → Δ}(∨ →) \frac{Γ → Δ, A_{i}}{Γ → Δ, A_{1} ∨ A_{2}} (→ ∨_{i})

\frac{Γ → Δ, A B, Γ → Δ}{A ⊃ B, Γ → Δ}(⊃→) \frac{A, Γ → Δ, B}{Γ → Δ, A ⊃ B} (→⊃)

\frac{SEQ}{X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → A ▷ B} (▷_{IK4})

where SEQ is essential on the lower sequent,

\frac{SEQ}{X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → □A}(□_{IK4})

where SEQ is essential on

X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → ¬A ▷ ⊥

A proof figure for a sequent Γ → Δ is defined as usual. We say that Γ → Δ is provable in GIK4, and write Γ → Δ ∈ GIK4, if there exists a proof figure for Γ → Δ.

Then we have the following two theorems.

Theorem 1. A ∈ IK4 if and only if → A ∈ GIK4.

Theorem 2. If Γ → Δ ∈ GIK4, then there exists a cut-free proof figure for Γ → Δ in GIK4.

Next, we define a sequent system GIL for IL. The system GIL is obtained from GIK4 by replacing (□_{IK4}) and (▷_{IK4}) by the following two inference rules, respectively:

\frac{SEQ}{X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → A ▷ B} (▷_{IL})

where SEQ is essential on the sequent X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → (A ∧ □¬A) ▷ B,

\frac{SEQ}{X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → □A}(□_{IL})

where SEQ is essential on the sequent X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → (¬A ∧ □A) ▷ ⊥.

Theorem 3. A ∈ IL if and only if → A ∈ GIL.

For cut-elimination theorem, we use the method in [Sas99c]. By sketching his proof, we obtain

Theorem 4. If Γ → Δ ∈ GIL, then there exists a cut-free proof figure for Γ → Δ.

References

[Ber90] A. Berarducci, The interpretability logic of Peano arithmetic, The Journal of Symbolic Logic, 55, 1990, pp. 1059–1089.

[JJ98] G. Japaridze and D. H. J. de Jongh, The Logic of Provability, in Handbook of proof theory, edited by S. R. Buss, University of California, 1998, pp. 475–546.

[JV90] D. H. J. de Jongh and F. Veltman, Provability logics for relative interpretability, in Mathematical logic, Proceedings of the Heyting 1988 Summer School, edited by P. Petkov, Plenum Press, 1990, pp. 31–42.

[JV91] D. H. J. de Jongh and A. Visser, Explicit fixed points in interpretability logic, Studia Logica, 50, 1991, pp. 39–50.

[Rij92] M. de Rijke, Unary interpretability logic, Notre Dame Journal of Formal Logic, 33, 1992 pp. 249–272.

[Sas99c] K. Sasaki, On a property of Löb’s axiom in propositional logics, submitted.

[Sha88] V. Yu. Shavrukov, The logic of relative interpretability over Peano arithmetic (Russian), Technical Report No. 5, Stekhlov Mathematical Institute, Moscow, 1988.

[Vis90] A. Visser, Interpretability logic, in Mathematical logic, Proceedings of the Heyting 1988 Summer School, edited by P. Petkov, Plenum Press, 1990, pp. 175–209.

[Vis97] A. Visser, An overview of interpretability logic, in Advances in Modal Logic ’96, edited by M. Kraft, M. de Rijke, and H. Wansing, CSLI Publications, 1997.

Cut-free Sequent Calculi for Visser’s Propositional Logics

Kentaro KIKUCHI

                           kentaro@jaist.ac.jp

School of Information Science, JAIST

1 Introduction

Visser [5] introduced Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL) in the form of natural deduction systems which are complete with respect to transitive models and finite irreflexive transitive models, respectively. A sequent style formulation of BPL can be found in [1], but it is not satisfactory because it does not enjoy the subformula property. Here we introduce another sequent calculus for BPL as well as one for FPL, and show the admissibility of the cut rule through semantical completeness. These are extensions of systems in [2].

2 A sequent calculus for BPL

Definition 2.1 Formulas are constructed from {→, ∧, ∨, ⊥} and the set V of propositional variables. A sequent is an expression of the form Γ ⇒ Δ where Γ and Δ are finite sets of formulas. As far as sequents are concerned, we write A_{1}, ..., A_{n} for {A_{1}, ..., A_{n}}, and A, Γ for {A} ∪ Γ, etc.

Definition 2.2 A (transitive) model is a triple ⟨W, R, V ⟩ where W is a non-empty set, R is a transitive relation on W, and V is a mapping from V to 2^{W} such that x ∈ V (p) and xRy imply y ∈ V (p). If W is a finite set, we say that a model ⟨W, R, V ⟩ is finite. Given a model M = ⟨W, R, V ⟩, the truth-relation ⊧ is defined as follows:

(M, x) ⊧ p  iff x ∈ V (p) for each propositional variable p,
(M, x) |̸= ⊥,
(M, x) ⊧ A ∧ B iff (M, x) ⊧ A and (M, x) ⊧ B,
(M, x) ⊧ A ∨ B iff (M, x) ⊧ A or (M, x) ⊧ B,
(M, x) ⊧ A→B iff ∀y ∈ W [xRy and (M, y) ⊧ A imply (M, y) ⊧ B].

We say that a formula A is true in M if (M, x) ⊧ A for every x ∈ W. The truth-relation for sequents is defined by

(M, x) ⊧ Γ ⇒ Δ iff ∀A ∈ Γ[(M, x) ⊧ A] implies ∃A ∈ Δ[(M, x) ⊧ A].

We say that a sequent Γ ⇒ Δ is true in M if (M, x) ⊧ Γ ⇒ Δ for every x ∈ W.

Definition 2.3 The system LBP consists of the following initial sequents

\begin{matrix}A ⇒ A, \\ ⊥ ⇒ \end{matrix}

and the following rules of inference:

{Γ ⇒ Δ \atop A, Γ ⇒ Δ} (weakening left)  {Γ ⇒ Δ \atop Γ ⇒ Δ, A} (weakening right)

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

\begin{matrix}A, Γ ⇒ Δ & B, Γ ⇒ Δ \\ A ∨ B, Γ ⇒ Δ \end{matrix} (∨left)  {Γ ⇒ Δ, A, B \atop Γ ⇒ Δ, A ∨ B} (∨right)
Δ_{1}, Σ, A ⇒ B, Γ_{1} Δ_{2}, Σ, A ⇒ B, Γ_{2} ⋯ Δ_{2^{n}}, Σ, A ⇒ B, Γ_{2^{n}}

Σ, C_{1}→D_{1}, ..., C_{n}→D_{n} ⇒ A→B (→)

where n ≥ 0, Γ_{i} = {C_{j} | j ∈ γ(i)}, Δ_{i} = {D_{j} | j ∈ δ(i)}, and the sets γ(i) and δ(i) of natural numbers are defined as follows. Enumerate all the “partitions” of {1, ..., n}:

\begin{matrix}⟨\{\}, \{1, ..., n\}⟩, ⟨\{1\}, \{2, ..., n\}⟩, ⟨\{2\}, \{1, 3, ..., n\}⟩, ..., \\ ⟨\{1, 2\}, \{3, ..., n\}⟩, ⟨\{2, 3\}, \{1, 4, ..., n\}⟩, ..., ⟨\{1, ..., n\}, \{\}⟩. \end{matrix}

The number of the partitions is 2^{n}, and ⟨δ(i), γ(i)⟩ is defined to be the i-th partition. For example, when n = 0, 1, 2, the rule (→) is of the forms

{Σ, A ⇒ B \atop Σ ⇒ A→B} (→), \begin{matrix}Σ, A ⇒ B, C_{1} & D_{1}, Σ, A ⇒ B \\ Σ, C_{1}→D_{1} ⇒ A→B \end{matrix} (→),

\begin{aligned}Σ, A ⇒ B, C_{1}, C_{2} & D_{1}, Σ, A ⇒ B, C_{2} & D_{2}, Σ, A ⇒ B, C_{1} & D_{1}, D_{2}, Σ, A ⇒ B \\ & Σ, C_{1}→D_{1}, C_{2}→D_{2} ⇒ A→B \end{aligned} (→).

Theorem 2.4 (Soundness) If Γ ⇒ Δ is provable in LBP, then Γ ⇒ Δ is true in any model.

To prove the completeness theorem, we need the following notion.

Definition 2.5 A sequent Γ ⇒ Δ is said to be saturated if, for all formulas A, B,

A ∧ B ∈ Γ implies A ∈ Γ and B ∈ Γ,
A ∧ B ∈ Δ implies A ∈ Δ or B ∈ Δ,
A ∨ B ∈ Γ implies A ∈ Γ or B ∈ Γ,
A ∨ B ∈ Δ implies A ∈ Δ and B ∈ Δ.

Given a finite set Λ of formulas, S(Λ) is defined to be the set of all sequents Γ ⇒ Δ satisfying the following conditions:

• Γ ⇒ Δ is saturated,

• Γ ⇒ Δ is not provable in LBP,

• Γ ∪ Δ ⊆ Sub(Λ), where Sub(Λ) is the set of all the subformulas in Λ.

Lemma 2.6 If a sequent Γ ⇒ Δ is not provable in LBP, then there is a sequent Γ′ ⇒ Δ′ in S(Γ ∪ Δ) such that Γ ⊆ Γ′ and Δ ⊆ Δ′.

Theorem 2.7 (Completeness) Γ ⇒ Δ is provable in LBP if and only if Γ ⇒ Δ is true in any model.

(Sketch of proof) Suppose that Γ ⇒ Δ is not provable in LBP. Then by Lemma 2.6, there is a sequent Γ′ ⇒ Δ′ in S(Γ ∪ Δ) such that Γ ⊆ Γ′ and Δ ⊆ Δ′. Now define a model M = ⟨W, R, V ⟩ as follows:

• W = S(Γ ∪ Δ),

• (Σ ⇒ Θ)R(Φ ⇒ Ψ) iff Σ ⊆ Φ and ∀(A→B) ∈ Σ[A ∈ Ψ or B ∈ Φ],

• V (p) = {Σ ⇒ Θ ∈ W | p ∈ Σ}.

We can verify that R is transitive and that Σ ⇒ Θ ∈ V (p) and (Σ ⇒ Θ)R(Φ ⇒ Ψ) imply Φ ⇒ Ψ ∈ V (p). To see that Γ ⇒ Δ is not true in M because of (M, Γ′ ⇒ Δ′) |̸= Γ ⇒ Δ, it suffices to show that, for any sequent Σ ⇒ Θ ∈ W, ∀A ∈ Σ[(M, Σ ⇒ Θ) ⊧ A] and ∀A ∈ Θ[(M, Σ ⇒ Θ) |̸= A]. □

The above proof provides the model M based on the finite set W = S(Γ ∪ Δ). So we have Theorem 2.8 (Finite model property) If Γ ⇒ Δ is not provable in LBP, then there is a finite model in which Γ ⇒ Δ is not true.

As a consequence of the completeness theorem, we derive

Corollary 2.9 The rule

\begin{matrix}Γ ⇒ Δ, A & A, Γ ⇒ Δ \\ Γ ⇒ Δ \end{matrix} (cut)

is admissible in LBP.

3 A sequent calculus for FPL

Definition 3.1 An irreflexive model is a model ⟨W, R, V ⟩ in which R is irreflexive, i.e., there is no x ∈ W such that xRx.

Definition 3.2 The system LFP is obtained from LBP by providing the left hand side of each upper sequent in the rule (→) with the formula A→B. Then, the rule (→) of LFP is of the form

Δ_{1}, Σ, A→B, A ⇒ B, Γ_{1} Δ_{2}, Σ, A→B, A ⇒ B, Γ_{2} ⋯ Δ_{2^{n}}, Σ, A→B, A ⇒ B, Γ_{2^{n}}

Σ, C_{1}→D_{1}, ..., C_{n}→D_{n} ⇒ A→B (→)

where n ≥ 0, and Γ_{i} and Δ_{i} are as in the rule (→) of LBP.

Theorem 3.3 (Soundness) If Γ ⇒ Δ is provable in LFP, then Γ ⇒ Δ is true in any finite irreflexive model.

Theorem 3.4 (Completeness) Γ ⇒ Δ is provable in LFP if and only if Γ ⇒ Δ is true in any finite irreflexive model.

(Sketch of proof) We construct a model M = ⟨W, R, V ⟩ similar to that in the proof of Theorem 2.7 except that R is defined by

• (Σ ⇒ Θ)R(Φ ⇒ Ψ) iff Σ ⊊ Φ and ∀(A→B) ∈ Σ[A ∈ Ψ or B ∈ Φ].

We can verify that M defines a finite irreflexive model. The rest of the proof is similar to that of Theorem 2.7. □

Corollary 3.5 The rule

\begin{matrix}Γ ⇒ Δ, A & A, Γ ⇒ Δ \\ Γ ⇒ Δ \end{matrix} (cut)

is admissible in LFP.

4 Relationships with other systems

Definition 4.1 We define ⋀ Γ (⋁ Γ) as the conjunction (the disjunction) of all formulas in Γ if Γ is non-empty, as ⊥ → ⊥ (⊥, respectively) if Γ empty.

Definition 4.2 The Hilbert-style system HB [4] consists of the following axiom schemes and inference rule:

\begin{matrix}A → A & (A → B) ∧ (B → C) → (A → C) \\ A ∧ B → A & A ∧ B → B \\ (A → B) ∧ (A → C) → (A → B ∧ C) & A → A ∨ B \\ B → A ∨ B & (A → C) ∧ (B → C) → (A ∨ B → C) \\ A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) & ⊥ → A \\ A → (B → A) & A → (B → A ∧ B) \end{matrix}

\begin{aligned}A & A → B \\ & B \end{aligned} (modus ponens).

Lemma 4.3 If A is provable in HB, then ⇒ A is provable in LBP.

Lemma 4.4 If Γ ⇒ Δ is provable in LBP, then ⋀ Γ → ⋁ Δ is provable in HB.

Combining Lemmas 4.3 and 4.4 with Theorem 2.7, we derive

Theorem 4.5 (Completeness of HB) A is provable in HB if and only if A is true in any model.

Definition 4.6 Sequents of the system GVPL^{+} [3] consist of finite sequences of formulas which are possibly of the form (A → B)^{+} where A and B are ordinary ones. The system GVPL^{+} consists of the following initial sequents

\begin{matrix}A ⇒ A, \\ ⊥ ⇒ \end{matrix}

and the following rules of inference:

\begin{matrix}Γ ⇒ A & Γ ⇒ B \\ Γ ⇒ A ∧ B \end{matrix} (⇒ ∧)  {A, Γ ⇒ Δ \atop A ∧ B, Γ ⇒ Δ} (∧ ⇒_{1})  {B, Γ ⇒ Δ \atop A ∧ B, Γ ⇒ Δ} (∧ ⇒_{2})
{Γ ⇒ A \atop Γ ⇒ A ∨ B} (⇒ ∨_{1})  {Γ ⇒ B \atop Γ ⇒ A ∨ B} (⇒ ∨_{2})  \begin{matrix}A, Γ ⇒ Δ & B, Γ ⇒ Δ \\ A ∨ B, Γ ⇒ Δ \end{matrix} (∨ ⇒)
{A, Γ^{+} ⇒ B \atop Γ ⇒ A → B} (⇒→)  {A, Γ ⇒ B \atop Γ ⇒ (A → B)^{+}} (⇒→^{+})  \begin{matrix}Γ ⇒ A & B, Π ⇒ Δ \\ (A → B)^{+}, Γ, Π ⇒ Δ \end{matrix} (→^{+}⇒)
{Γ ⇒ \atop Γ ⇒ D} (⇒ T)  {Γ ⇒ Δ \atop D, Γ ⇒ Δ} (T ⇒)  {D, D, Γ ⇒ Δ \atop D, Γ ⇒ Δ} (C ⇒)
{Γ, C, D, Π ⇒ Δ \atop Γ, D, C, Π ⇒ Δ} (I ⇒)  \begin{matrix}Γ ⇒ D & D, Π ⇒ Δ \\ Γ, Π ⇒ Δ \end{matrix} (cut)

where Δ is the empty sequence or a formula, and Γ^{+} is obtained from Γ by replacing every C → D with (C → D)^{+}.

In the following, we let Γ denote both a finite set of ordinary formulas and a finite sequence of them, and let A denote an ordinary formula.

Lemma 4.7 If Γ ⇒ Δ is provable in LBP, then Γ ⇒ ⋁ Δ is provable in GVPL^{+}.

Lemma 4.8 If Γ, Σ ⇒ A is provable in GVPL^{+}, then Σ^{−} ⇒ ⋀ Γ → A is provable in LBP, where Σ^{−} is obtained from Σ by replacing every (C → D)^{+} with C → D.

Theorem 4.9 Γ ⇒ A is provable in LBP if and only if Γ ⇒ A is provable in GVPL^{+}.

Definition 4.10 The system GFPL^{+} [3] is obtained from GVPL^{+} by replacing (⇒→) with

{A, A → B, Γ^{+} ⇒ B \atop Γ ⇒ A → B} (⇒→_{f}).

Lemmas 4.7, 4.8, and Theorem 4.9 hold also between LFP and GFPL^{+}.

References

[1] M. Ardeshir. Aspects of Basic Logic. PhD thesis, Marquette University, Milwaukee, 1995.

[2] R. Kashima. Sequent calculi for strict implications. manuscript, 1997.

[3] K. Sasaki. Cut-elimination theorem for Visser’s propositional logic and formal propositional logic. submitted, 1998.

[4] Y. Suzuki and H. Ono. Hilbert style proof system for BPL. Research Report IS-RR-97-0040F, JAIST, 1997.

[5] A. Visser. A propositional logic with explicit fixed points. Studia Logica, 40:155–175, 1981.

Logics of finite width for Some Intuitionistic Modal Logic

Kazuyo Inoi Junior college, Nihon University

             E-mail: inoi@info.jcn.nihon-u.ac.jp

Abstract

Fine [1] showed the completeness of logics of finite width for K4. We treat the logic containing the S4-type intuitionistic modal logic L_{0}.

For the logic L_{0}, we show the completeness of the logics of finite width with respect to one relation.

1 Preliminaries.

In [2], Ono introduced the intuitionistic modal logic L_{0} and it is shown the logic is complete for the I-frame.

We repeat the axioms of the intuitionistic modal logic L_{0} and I-frame. L_{0} is the logic obtained from the intuitionistic logic 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. A triple F = (M, ≤, R) is called an I-frame if the following conditions are satisfied.

• M is a non empty set.

• ≤ is a partial order on M.

• R is a pre-order on M, that is, x ≤ y implies xRy for each x, y ∈ M.

A relation ⊧ between M and the set of propositional variables is said to be a valuation on F if

a ⊧ p and a ≤ b ⇒ b ⊧ p

holds for every a, b ∈ M and every variable p. We can extend a valuation on M and the set of formulas in the following way.

1. a ⊧ A ∧ B ⇔ a ⊧ A and a ⊧ B,

2. a ⊧ A ∨ B ⇔ a ⊧ A or a ⊧ B,

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

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

The pair (F, ⊧) of I-frame F and a valuation ⊧ on F is said to be an I-model.

A formula A is said to be true in (F, ⊧) if a ⊧ A holds for any a ∈ M. A formula A is said to be valid in F if a is true in any model (F, ⊧), and any a ∈ M.

We write FL instead of the canonical frame for a logic L and ML instead of the canonical model for a logic L. If a logic L′ is the restriction of L to finite subset of propositional valiables then L′ is said to be weak.

Lemma 1.1 Suppose M = (M, ≤, R, ⊧) is an I-model, A′ is a formula substituted B_{i} for p_{i} in A and M′ = (M, ≤, R, ⊧′) is an I-model such that

∀x ∈ M(M′, x) ⊧′ p_{i} ⇔ (M, x) ⊧ B_{i}, i = 0, 1, ⋯, n.

Then

(M′, x) ⊧′ A ⇔ (M, x) ⊧ A′.

Lemma 1.2 Suppose Δ is closed under substitution and true in M = (M, ≤, R, ⊧_{M}). Then Δ is true in each definable variant N = (M, ≤, R, ⊧_{N}).

Lemma 1.3 Suppose L′ is the weak restriction of a logic L. Then L is true in ML′.

2 The logics of finite ≤-width.

In this section, we define the formula of ≤-width n.

For n ≥ 1, let BW_{n} be the formula

⋁_{i=0}^{n} □(p_{i} ⊃ ⋁_{j≠i} p_{j}).

w and v are said to be ≤-incomparable if the elements are incomparable with respect to the relation ≤. An I-frame (M, ≤, R) is of ≤-width n if it does not contain (n + 1) mutually ≤-incomparable elements. A frame F is of finite ≤-width if it is of ≤-width n for some n. A logic L is of finite ≤-width if L ⊇ L_{0} + BW_{n} for some n > 0.

Theorem 2.1 Suppose L is a logic of finite ≤-width and a frame F = (M, ≤, R) is generated from FL by w. Then F is of finite ≤-width.

Lemma 2.2 Suppose an I-frame (M, ≤, R) is of finite ≤-width. If there is a infinite sequence w_{0}, w_{1}, ⋯ in M such that w_{j} R̸^{←}w_{i}forj > i. Then the sequence w_{0}, w_{1}, ⋯ consists of infinite subsequence v_{0}, v_{1}, ⋯ such that v_{i} ≤ v_{i+1} and v_{i} ≠ v_{i+1} for i = 0, 1, · · ·.

Let (M, ≤, R) be an I-model. w is ≤-deep if there is a elements w_{0}, w_{1}, ⋯ such that w_{i} ∈ M, w_{0} = w, w_{i} ≤ w_{i+1} and w_{i} ≠ w_{i+1} for i = 0, 1, · · ·. Let U_{w}^{≤} = {u ∈ M : w ≤ u and u is not ≤ -deep} and U_{w}^{R} = {u ∈ M : wRu and u is not ≤ -deep}. A ≤-deep w is called ≤-static if U_{w}^{≤} = U_{v}^{≤} for any ≤-deep v ∈ M(w ≤ v). A ≤-deep w is called R-static if U_{w}^{R} = U_{v}^{R} for any ≤-deep v ∈ M(w ≤ v).

For u ∈ M, let u_{p} = {p : u ⊧ p(p is a propositional variable)} and let |u|_{p} = {v_{p} : v ∈ M, u ≤ v and v is ≤ -deep}. A ≤-deep w is called ≤-stationary if |w|_{p} = |v|_{p} for any ≤-deep v ∈ M(w ≤ v).

Lemma 2.3 Let (M, ≤, R, ⊧) be an weak I-frame of finite ≤-width. For any ≤-deep w ∈ M, there is v(v ∈ M, w ≤ v) such that ≤-deep and ≤-static.

Lemma 2.4 Let (M, ≤, R, ⊧) be an weak I-frame of finite ≤-width. For any ≤-deep w ∈ M, there is v(v ∈ M, w ≤ v) such that ≤-deep and R-static.

Lemma 2.5 Let (M, ≤, R, ⊧) be an weak I-frame of finite ≤-width. For any ≤-deep w ∈ M, there is v(v ∈ M, w ≤ v) such that ≤-deep and ≤-stationary.

By Lemma 2.3, Lemma 2.4 and Lemma 2.5 For any ≤-deep w ∈ M, there is v(v ∈ M, w ≤ v) such that ≤-deep, ≤-static, R-static and ≤-stationary. So, we can get the next theorem.

Theorem 2.6 Suppose L is a logic of finite ≤-width. Then ML contains no infinite ≤-ascending chain.

Theorem 2.7 Suppose L is a logic of finite ≤-width. Then ML contains no infinite R-ascending chain.

Let F = (M, ≤, R) is an I-frame. A set V is said to be a ≤-cover for U ⊂ M if V ⊆ U and (∀u ∈ U)(∃v ∈ V)(u = v or u < v). F has finite ≤-cover property if each U ⊂ M has a finite ≤-cover.

Theorem 2.8 Let L′ be a weak logic of finite ≤-width and F = (M, ≤, R) be generated from FL by w. Then f has finite ≤-cover property.

3 Completeness results.

Let M = (M, ≤_{M}, R_{M}, ⊧_{M}) and N = (N, ≤_{N}, R_{N}, ⊧_{N}) be I-models and w ∈ M, v ∈ N. We defind the relations (M, w) ≤_{A} (N, v), (M, w) ≡_{A} (N, v) and (M, w) ∼_{A} (N, v) by induction on the construction of a formula A:

(M, w) ∼_{0} (N, v) ⇔ (w ⊧_{M} p ↔ v ⊧_{N} p) for any propositional variable p;
(M, w) ≤_{B⊃C} (N, v) ⇔ ∀u ∈ M∃t ∈ N[w ≠_{M} u and w ≤_{M} u ⇒
v ≤_{N} t, (M, u) ∼_{B} (N, t) and (M, u) ∼_{C} (N, t)];
(M, w) ≤_{¬B} (N, v) ⇔ ∀u ∈ M∃t ∈ N[w ≠_{M} u and w ≤_{M} u ⇒

v ≤_{N} t and (M, u) ∼_{B} (N, t)];
(M, w) ≤_{□B} (N, v) ⇔ ∀u ∈ M∃t ∈ N[w ≠_{M} u and wR_{M}u ⇒
vR_{N}t and (M, u) ∼_{B} (N, t)];
(M, w) ≡_{A} (N, v) ⇔ (M, w) ≤_{A} (N, v) and (N, v) ≤_{A} (M, w);
(M, w) ∼_{A} (N, v) ⇔ (M, w) ∼_{0} (N, v) and (M, w) ≡_{A} (N, v).

Let |w|_{A} = {v ∈ M : w ∼_{A} v}.

A model M is A-simple if there is finite V ⊂ M such that

• V covers |w|_{A} for each w ∈ M, and

• for all u, t ∈ M − V, ({v ∈ V : u ≤ v} = {v ∈ V : t ≤ v} and {v ∈ V : uRv} = {v ∈ V : tRv}) ⇒ u ∼_{0} t.

Lemma 3.1 Suppose (M, ≤, R) is an I-model of finite ≤-width. If a formula A is true in all weak A-simple models (M, ≤, R, ⊧) then A is valid in (M, ≤, R).

Proposition 3.2 Suppose M = (M, ≤, R, ⊧) is a natural model of finite ≤-width. Then there exist formula D_{w} such that w ⊧ D_{w}, w ∈ M and v |̸= D_{w}, v ∈ M(w ≰ v).

Lemma 3.3 Suppose M = (M, ≤, R, ⊧_{M}) is a natural model of finite ≤-width and N = (M, ≤, R, ⊧_{N}) is a simple weak model. Then there exist formulas A_{1}, A_{2}, ⋯, A_{n} such that w ⊧_{N} p_{i} ⇔ w ⊧_{M} A_{i}, for i = 0, 1 , ⋯ n.

Lemma 3.4 Let L be a logic of finite ≤-width and L′ be the weak restriction of L. Then FL′ is a frame for L.

Theorem 3.5 Each logic of finite ≤-width is complete.

References

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

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