Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas (Q1208113)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas
scientific article

    Statements

    Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas (English)
    0 references
    0 references
    16 May 1993
    0 references
    The paper gives the first examples of rather general completeness results in Kripke semantics for intermediate predicate logics. For an intermediate propositional logic \(J\), \(J_ *\) denotes the smallest predicate extension of \(J\). Let \(K=\neg\neg\forall x\bigl(p(x)\lor\neg p(x)\bigr)\), \(D=\forall x\bigl(p(x)\lor q\bigr)\supset_ .\forall x p(x)\lor q\). The subsequent two theorems generalize some earlier partial results of Ono and Suzuki. Theorem 3.7. If \(J\) is tabular, \(J_ *+D\) is strongly Kripke complete. Theorem 3.9. If \(J\) is a subframe logic, then \(J_ *+D\), \(J_ *+K+D\) are strongly Kripke complete. The latter result is transferred to some kinds of confinal subframe logics (this notion was introduced by \textit{M. Zakhar'yashchev} [Algebra Logika 28, No. 4, 402-429 (1989; Zbl 0708.03011)]): Theorem 3.11. If \(J\) is a confinal subframe logic determined by a class of finite frames \(\{M_ i| i\in I\}\) such that (for any \(i\)) every subset of \(M_ i\) having an upper bound contains a maximal element of \(M_ i\), then \(J_ *+D+K\) is strongly Kripke complete. (As the author observes, D. Skvortsov has recently proved that 3.11 fails for arbitrary confinal subframe logics).
    0 references
    Zakhar'yashchev's canonical formulas
    0 references
    completeness
    0 references
    Kripke semantics
    0 references
    intermediate predicate logics
    0 references
    confinal subframe logics
    0 references

    Identifiers