The McKinsey axiom is not compact

1992 ◽  
Vol 57 (4) ◽  
pp. 1230-1238 ◽  
Author(s):  
Xiaoping Wang
Keyword(s):  
Modal Logic ◽  
Modus Ponens ◽  
Intensional Logic ◽  
Normal System ◽  
Propositional Modal Logic ◽  
Modal Operators ◽  
Transformation Rules ◽  
Image Position ◽  
In The Beginning ◽  
Infinite Set

The canonicity and compactness of the KM system are problems historically important in the development of our understanding of intensional logic (as explained in Goldblatt's paper, The McKinsey axiom is not canonical). The problems, however, were unsolved for years in modal logic. In the beginning of 1990, Goldblatt showed that KM is not canonical in The McKinsey axiom is not canonical. The remaining task is to solve the problem of the compactness of KM. In this paper we present a proof showing that the KM system is not compact.The symbols of the language of propositional modal logic are as follows:1. A denumerably infinite set of sentence letters, for example, {p0, P1, p2, …};2. The Boolean connectives &, ⋁, ¬, →, ↔ and parentheses;3. The modal operators L and M where M is defined as ¬L¬.The formation rules of well-formed propositional modal formulae are the formation rules of formulae in classic propositional logic plus the following rule:If A is a well-formed formula, so is LA.A normal modal system is a set of formulae that contains all tautologies and the formulaand is closed under the following transformation rules:Uniform substitution. If A is a theorem, so is every substitution-instance of A.Modus ponens. If A and A → B are theorems, so is B.Necessitation. If A is a theorem, so is LA.Let L be a normal system. Then a set S of formulae is L-consistent if and only if for any formula B, which is the conjunction of some formulae in S, B is not included in L. A set S of formulae is maximal if and only if for every formula A, S either contains A or contains ¬A. A set S of formulae is maximal L-consistent if and only if it is both maximal and L-consistent.

Extremely undecidable sentences

1982 ◽  
Vol 47 (1) ◽  
pp. 191-196 ◽  
Author(s):  
George Boolos
Keyword(s):  
Modal Logic ◽  
The Other ◽  
Propositional Modal Logic ◽  
Image Position

Let ‘ϕ’, ‘χ’, and ‘ψ’ be variables ranging over functions from the sentence letters P0, P1, … Pn, … of (propositional) modal logic to sentences of P(eano) Arithmetic), and for each sentence A of modal logic, inductively define Aϕ by[and similarly for other nonmodal propositional connectives]; andwhere Bew(x) is the standard provability predicate for PA and ⌈F⌉ is the PA numeral for the Gödel number of the formula F of PA. Then for any ϕ, (−□⊥)ϕ = −Bew(⌈⊥⌉), which is the consistency assertion for PA; a sentence S is undecidable in PA iff both and , where ϕ(p0) = S. If ψ(p0) is the undecidable sentence constructed by Gödel, then ⊬PA (−□⊥→ −□p0 & − □ − p0)ψ and ⊢PA(P0 ↔ −□⊥)ψ. However, if ψ(p0) is the undecidable sentence constructed by Rosser, then the situation is the other way around: ⊬PA(P0 ↔ −□⊥)ψ and ⊢PA (−□⊥→ −□−p0 & −□−p0)ψ. We call a sentence S of PA extremely undecidable if for all modal sentences A containing no sentence letter other than p0, if for some ψ, ⊬PAAψ, then ⊬PAAϕ, where ϕ(p0) = S. (So, roughly speaking, a sentence is extremely undecidable if it can be proved to have only those modal-logically characterizable properties that every sentence can be proved to have.) Thus extremely undecidable sentences are undecidable, but neither the Godel nor the Rosser sentence is extremely undecidable. It will follow at once from the main theorem of this paper that there are infinitely many inequivalent extremely undecidable sentences.

Post completeness in modal logic

1972 ◽  
Vol 37 (4) ◽  
pp. 711-715 ◽  
Author(s):  
Krister Segerberg
Keyword(s):  
Modal Logic ◽  
Upper Bound ◽  
Modus Ponens ◽  
Proper Subset ◽  
Proper Extension ◽  
Image Position

Let ⊥, →, and □ be primitive, and let us have a countable supply of propositional letters. By a (modal) logic we understand a proper subset of the set of all formulas containing every tautology and being closed under modus ponens and substitution. A logic is regular if it contains every instance of □A ∧ □B ↔ □(A ∧ B) and is closed under the ruleA regular logic is normal if it contains □⊤. The smallest regular logic we denote by C (the same as Lemmon's C2), the smallest normal one by K. If L and L' are logics and L ⊆ L′, then L is a sublogic of L', and L' is an extension of L; properly so if L ≠ L'. A logic is quasi-regular (respectively, quasi-normal) if it is an extension of C (respectively, K).A logic is Post complete if it has no proper extension. The Post number, denoted by p(L), is the number of Post complete extensions of L. Thanks to Lindenbaum, we know thatThere is an obvious upper bound, too:Furthermore,.

The extensions of the modal logic K5

1985 ◽  
Vol 50 (1) ◽  
pp. 102-109 ◽  
Author(s):  
Michael C. Nagle ◽  
S. K. Thomason
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Abstract Characterization ◽  
Propositional Modal Logic ◽  
Normal Logic ◽  
Countably Infinite ◽  
Infinite Set

Our purpose is to delineate the extensions (normal and otherwise) of the propositional modal logic K5. We associate with each logic extending K5 a finitary index, in such a way that properties of the logics (for example, inclusion, normality, and tabularity) become effectively decidable properties of the indices. In addition we obtain explicit finite axiomatizations of all the extensions of K5 and an abstract characterization of the lattice of such extensions.This paper refines and extends the Ph.D. thesis [2] of the first-named author, who wishes to acknowledge his debt to Brian F. Chellas for his considerable efforts in directing the research culminating in [2] and [3]. We also thank W. J. Blok and Gregory Cherlin for observations which greatly simplified the proofs of Theorem 3 and Corollary 10.By a logic we mean a set of formulas in the countably infinite set Var of propositional variables and the connectives ⊥, →, and □ (other connectives being used abbreviatively) which contains all the classical tautologies and is closed under detachment and substitution. A logic is classical if it is also closed under RE (from A↔B infer □A ↔□B) and normal if it is classical and contains □ ⊤ and □ (P → q) → (□p → □q). A logic is quasi-classical if it contains a classical logic and quasi-normal if it contains a normal logic. Thus a quasi-normal logic is normal if and only if it is classical, and if and only if it is closed under RN (from A infer □A).

Reduction of tense logic to modal logic. I

1974 ◽  
Vol 39 (3) ◽  
pp. 549-551 ◽  
Author(s):  
S. K. Thomason
Keyword(s):  
Modal Logic ◽  
Logical Consequence ◽  
Tense Logic ◽  
Kripke Semantics ◽  
Relational Semantics ◽  
Propositional Modal Logic ◽  
Formal Systems ◽  
Unary Operator ◽  
Countable Infinity ◽  
Image Position

It will be shown that propositional tense logic (with the Kripke relational semantics) may be regarded as a fragment of propositional modal logic (again with the Kripke semantics). This paper deals only with model theory. The interpretation of formal systems of tense logic as formal systems of modal logic will be discussed in [6].The languages M and T, of modal and tense logic respectively, each have a countable infinity of propositional variables and the Boolean connectives; in addition, M has the unary operator ⋄ and T has the unary operators F and P. A structure is a pair <W, ≺<, where W is a nonempty set and ≺ is a binary relation on W. An assignment V assigns to each propositional variable p a subset V(p) of W. Then V(α)£ W is defined for all formulas α of M or T by induction:We say that α is valid in <W, ≺>, or <W, ≺>, ⊨ α, if ⊩ (α) = W for every assignment V for <W, ≺>. If Γ is a set of formulas of M [T] and α is a formula of M [T], then α is a logical consequence of Γ, or Γ ⊩ α,if α is valid in every model of Γ i.e., in every structure in which all γ ∈ Γ are valid.

Modal operators and functional completeness, II

1977 ◽  
Vol 42 (3) ◽  
pp. 391-399 ◽  
Author(s):  
S. K. Thomason
Keyword(s):  
Modal Logic ◽  
Possible Worlds ◽  
Kripke Semantics ◽  
Functional Completeness ◽  
Possible World ◽  
States Of Affairs ◽  
Propositional Modal Logic ◽  
Modal Operators ◽  
Fixed Frame ◽  
State Of Affairs

In the Kripke semantics for propositional modal logic, a frame W = (W, ≺) represents a set of “possible worlds” and a relation of “accessibility” between possible worlds. With respect to a fixed frame W, a proposition is represented by a subset of W (regarded as the set of worlds in which the proposition is true), and an n-ary connective (i.e. a way of forming a new proposition from an ordered n-tuple of given propositions) is represented by a function fw: (P(W))n → P(W). Finally a state of affairs (i.e. a consistent specification whether or not each proposition obtains) is represented by an ultrafilter over W. {To avoid possible confusion, the reader should forget that some people prefer the term “states of affairs” for our “possible worlds”.}In a broader sense, an n-ary connective is represented by an n-ary operatorf = {fw∣ W ∈ Fr}, where Fr is the class of all frames and each fw: (P(W))n → P(W). A connective is modal if it corresponds to a formula of propositional modal logic. A connective C is coherent if whether C(P1,…, Pn) is true in a possible world depends only upon which modal combinations of P1,…,Pn are true in that world. (A modal combination of P1,…,Pn is the result of applying a modal connective to P1,…, Pn.) A connective C is strongly coherent if whether C(P1, …, Pn) obtains in a state of affairs depends only upon which modal combinations of P1,…, Pn obtain in that state of affairs.

scholarly journals Formula size games for modal logic and μ-calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander
Keyword(s):  
Modal Logic ◽  
Optimal Strategy ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
First Order ◽  
Modal Operators ◽  
Crucial Difference ◽  
Definition Of ◽  
Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

QUANTIFIED MODAL LOGIC ON THE RATIONAL LINE

2014 ◽  
Vol 7 (3) ◽  
pp. 439-454 ◽  
Author(s):  
PHILIP KREMER
Keyword(s):  
Modal Logic ◽  
Real Line ◽  
Topological Spaces ◽  
Topological Semantics ◽  
Cantor Space ◽  
Quantified Modal Logic ◽  
Propositional Modal Logic ◽  
The Family ◽  
Modal Logic S4 ◽  
Rational Line

AbstractIn the topological semantics for propositional modal logic, S4 is known to be complete for the class of all topological spaces, for the rational line, for Cantor space, and for the real line. In the topological semantics for quantified modal logic, QS4 is known to be complete for the class of all topological spaces, and for the family of subspaces of the irrational line. The main result of the current paper is that QS4 is complete, indeed strongly complete, for the rational line.

On finite and infinite modal systems

1938 ◽  
Vol 3 (2) ◽  
pp. 77-82 ◽  
Author(s):  
C. West Churchman
Keyword(s):  
Modal Logic ◽  
Symbolic Logic ◽  
Modal Operator ◽  
Image Position ◽  
Modal Systems ◽  
Complex Modal

In Oskar Becker's Zur Logik der Modalitäten four systems of modal logic are considered. Two of these are mentioned in Appendix II of Lewis and Langford's Symbolic logic. The first system is based on A1–8 plus the postulate,From A7: ∼◊p⊰∼p we can prove the converse of C11 by writing ∼◊p for p, and hence deriveThe addition of this postulate to A1–8, as Becker points out, allows us to “reduce” all complex modal functions to six, and these six are precisely those which Lewis mentions in his postulates and theorems: p, ∼p, ◊p, ∼◊p, ∼◊∼p, and ◊∼p This reduction is accomplished by showingwhere ◊n means that the modal operator ◊ is repeated n times; e.g., ◊3p = ◊◊◊p. Then it is shown thatBy means of (1), (2), and (3) any complex modal function whatsoever may be reduced to one of the six “simple” modals mentioned above.It might be asked whether this reduction could be carried out still further, i.e., whether two of the six “irreducible” modals could not be equated. But such a reduction would have to be based on the fact that ◊p = p which is inconsistent with the set B1–9 of Lewis and Langford's Symbolic logic and independent of the set A1–8. Hence for neither set would such a reduction be possible.

scholarly journals REVERSE MATHEMATICS, YOUNG DIAGRAMS, AND THE ASCENDING CHAIN CONDITION

2017 ◽  
Vol 82 (2) ◽  
pp. 576-589 ◽  
Author(s):  
KOSTAS HATZIKIRIAKOU ◽  
STEPHEN G. SIMPSON
Keyword(s):  
Theorem Proving ◽  
Chain Condition ◽  
Reverse Mathematics ◽  
Partial Ordering ◽  
Young Diagrams ◽  
Equivalence Proof ◽  
Image Position ◽  
Countably Infinite ◽  
Infinite Set ◽  
Ascending Chain Condition

AbstractLetSbe the group of finitely supported permutations of a countably infinite set. Let$K[S]$be the group algebra ofSover a fieldKof characteristic 0. According to a theorem of Formanek and Lawrence,$K[S]$satisfies the ascending chain condition for two-sided ideals. We study the reverse mathematics of this theorem, proving its equivalence over$RC{A_0}$(or even over$RCA_0^{\rm{*}}$) to the statement that${\omega ^\omega }$is well ordered. Our equivalence proof proceeds via the statement that the Young diagrams form a well partial ordering.

Sign in / Sign up

Export Citation Format

Share Document