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