Modal companion
   HOME

TheInfoList



OR:

In
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
, a modal companion of a superintuitionistic (intermediate) logic ''L'' is a
normal Normal(s) or The Normal(s) may refer to: Film and television * ''Normal'' (2003 film), starring Jessica Lange and Tom Wilkinson * ''Normal'' (2007 film), starring Carrie-Anne Moss, Kevin Zegers, Callum Keith Rennie, and Andrew Airlie * ''Norma ...
modal logic Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
that interprets ''L'' by a certain canonical translation, described below. Modal companions share various properties of the original
intermediate logic In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic; thus, consistent superintuitionistic logics are called intermediate l ...
, which enables to study intermediate logics using tools developed for modal logic.


Gödel–McKinsey–Tarski translation

Let ''A'' be a
propositional In logic and linguistics, a proposition is the meaning of a declarative sentence. In philosophy, " meaning" is understood to be a non-linguistic entity which is shared by all sentences with the same meaning. Equivalently, a proposition is the no ...
intuitionistic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fu ...
formula. A modal formula ''T''(''A'') is defined by induction on the complexity of ''A'': :T(p)=\Box p, for any
propositional variable In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is an input variable (that can either be true or false) of a truth function. Propositional variables are the basic building-blocks of propositi ...
p, :T(\bot)=\bot, :T(A\land B)=T(A)\land T(B), :T(A\lor B)=T(A)\lor T(B), :T(A\to B)=\Box(T(A)\to T(B)). As negation is in intuitionistic logic defined by A\to\bot, we also have :T(\neg A)=\Box\neg T(A). ''T'' is called the Gödel translation or Gödel
McKinsey McKinsey & Company is a global management consulting firm founded in 1926 by University of Chicago professor James O. McKinsey, that offers professional services to corporations, governments, and other organizations. McKinsey is the oldest and ...
Tarski translation. The translation is sometimes presented in slightly different ways: for example, one may insert \Box before every subformula. All such variants are provably equivalent in S4.


Modal companions

For any normal modal logic ''M'' that extends S4, we define its si-fragment ''ρM'' as :\rho M=\. The si-fragment of any normal extension of S4 is a superintuitionistic logic. A modal logic ''M'' is a modal companion of a superintuitionistic logic ''L'' if L=\rho M. Every superintuitionistic logic has modal companions. The smallest modal companion of ''L'' is :\tau L=\mathbf\oplus\, where \oplus denotes normal closure. It can be shown that every superintuitionistic logic also has a largest modal companion, which is denoted by ''σL''. A modal logic ''M'' is a companion of ''L'' if and only if \tau L\subseteq M\subseteq\sigma L. For example, S4 itself is the smallest modal companion of intuitionistic logic (IPC). The largest modal companion of IPC is the Grzegorczyk logic Grz, axiomatized by the axiom :\Box(\Box(A\to\Box A)\to A)\to A over K. The smallest modal companion of classical logic (CPC) is
Lewis Lewis may refer to: Names * Lewis (given name), including a list of people with the given name * Lewis (surname), including a list of people with the surname Music * Lewis (musician), Canadian singer * "Lewis (Mistreated)", a song by Radiohead ...
' S5, whereas its largest modal companion is the logic :\mathbf=\mathbf K\oplus(A\leftrightarrow\Box A). More examples:


Blok–Esakia isomorphism

The set of extensions of a superintuitionistic logic ''L'' ordered by inclusion forms a
complete lattice In mathematics, a complete lattice is a partially ordered set in which ''all'' subsets have both a supremum (join) and an infimum (meet). A lattice which satisfies at least one of these properties is known as a ''conditionally complete lattice.'' ...
, denoted Ext''L''. Similarly, the set of normal extensions of a modal logic ''M'' is a complete lattice NExt''M''. The companion operators ''ρM'', ''τL'', and ''σL'' can be considered as mappings between the lattices ExtIPC and NExtS4: :\rho\colon\mathrm\,\mathbf\to\mathrm\,\mathbf, :\tau,\sigma\colon\mathrm\,\mathbf\to\mathrm\,\mathbf. It is easy to see that all three are
monotone Monotone refers to a sound, for example music or speech, that has a single unvaried tone. See: monophony. Monotone or monotonicity may also refer to: In economics *Monotone preferences, a property of a consumer's preference ordering. *Monotonic ...
, and \rho\circ\tau=\rho\circ\sigma is the identity function on ExtIPC. L. Maksimova and V. Rybakov have shown that ''ρ'', ''τ'', and ''σ'' are actually
complete Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...
, join-complete and meet-complete lattice homomorphisms respectively. The cornerstone of the theory of modal companions is the Blok–Esakia theorem, proved independently by Wim Blok and Leo Esakia. It states :''The mappings ''ρ'' and ''σ'' are mutually inverse lattice
isomorphism In mathematics, an isomorphism is a structure-preserving mapping between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between them. The word is ...
s of'' ExtIPC ''and'' NExtGrz. Accordingly, ''σ'' and the
restriction Restriction, restrict or restrictor may refer to: Science and technology * restrict, a keyword in the C programming language used in pointer declarations * Restriction enzyme, a type of enzyme that cleaves genetic material Mathematics and logi ...
of ''ρ'' to NExtGrz are called the Blok–Esakia isomorphism. An important corollary to the Blok–Esakia theorem is a simple syntactic description of largest modal companions: for every superintuitionistic logic ''L'', :\sigma L=\tau L\oplus\mathbf.


Semantic description

The Gödel translation has a frame-theoretic counterpart. Let \mathbf F=\langle F,R,V\rangle be a transitive and reflexive modal
general frame In logic, general frames (or simply frames) are Kripke frames with an additional structure, which are used to model modal and intermediate logics. The general frame semantics combines the main virtues of Kripke semantics and algebraic semantics: ...
. The
preorder In mathematics, especially in order theory, a preorder or quasiorder is a binary relation that is reflexive and transitive. Preorders are more general than equivalence relations and (non-strict) partial orders, both of which are special c ...
''R'' induces the
equivalence relation In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive. The equipollence relation between line segments in geometry is a common example of an equivalence relation. Each equivalence relation ...
:x\sim y \iff x\,R\,y \land y\,R\,x on ''F'', which identifies points belonging to the same cluster. Let \langle\rho F,\le\rangle=\langle F,R\rangle/ be the induced
quotient In arithmetic, a quotient (from lat, quotiens 'how many times', pronounced ) is a quantity produced by the division of two numbers. The quotient has widespread use throughout mathematics, and is commonly referred to as the integer part of a ...
partial order In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary ...
(i.e., ''ρF'' is the set of
equivalence class In mathematics, when the elements of some set S have a notion of equivalence (formalized as an equivalence relation), then one may naturally split the set S into equivalence classes. These equivalence classes are constructed so that elements a ...
es of \sim), and put :\rho V=\. Then \rho\mathbf F=\langle\rho F,\le,\rho V\rangle is an intuitionistic general frame, called the skeleton of F. The point of the skeleton construction is that it preserves validity modulo Gödel translation: for any intuitionistic formula ''A'', :''A'' is valid in ''ρ''F if and only if ''T''(''A'') is valid in F. Therefore, the si-fragment of a modal logic ''M'' can be defined semantically: if ''M'' is complete with respect to a class ''C'' of transitive reflexive general frames, then ''ρM'' is complete with respect to the class \. The largest modal companions also have a semantic description. For any intuitionistic general frame \mathbf F=\langle F,\le,V\rangle, let ''σV'' be the closure of ''V'' under Boolean operations (binary
intersection In mathematics, the intersection of two or more objects is another object consisting of everything that is contained in all of the objects simultaneously. For example, in Euclidean geometry, when two lines in a plane are not parallel, their i ...
and
complement A complement is something that completes something else. Complement may refer specifically to: The arts * Complement (music), an interval that, when added to another, spans an octave ** Aggregate complementation, the separation of pitch-class ...
). It can be shown that ''σV'' is closed under \Box, thus \sigma\mathbf F=\langle F,\le,\sigma V\rangle is a general modal frame. The skeleton of ''σ''F is isomorphic to F. If ''L'' is a superintuitionistic logic complete with respect to a class ''C'' of general frames, then its largest modal companion ''σL'' is complete with respect to \. The skeleton of a
Kripke frame Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Jo ...
is itself a Kripke frame. On the other hand, ''σ''F is never a Kripke frame if F is a Kripke frame of infinite depth.


Preservation theorems

The value of modal companions and the Blok–Esakia theorem as a tool for investigation of intermediate logics comes from the fact that many interesting properties of logics are preserved by some or all of the mappings ''ρ'', ''σ'', and ''τ''. For example, * decidability is preserved by ''ρ'', ''τ'', and ''σ'', *
finite model property In mathematical logic, a logic L has the finite model property (fmp for short) if any non-theorem of L is falsified by some ''finite'' model of L. Another way of putting this is to say that L has the fmp if for every formula ''A'' of L, ''A'' is an ...
is preserved by ''ρ'', ''τ'', and ''σ'', * tabularity is preserved by ''ρ'' and ''σ'', * Kripke completeness is preserved by ''ρ'' and ''τ'', *
first-order In mathematics and other formal sciences, first-order or first order most often means either: * "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of high ...
definability on Kripke frames is preserved by ''ρ'' and ''τ''.


Other properties

Every intermediate logic ''L'' has an
infinite Infinite may refer to: Mathematics *Infinite set, a set that is not a finite set *Infinity, an abstract concept describing something without any limit Music * Infinite (group), a South Korean boy band *''Infinite'' (EP), debut EP of American m ...
number of modal companions, and moreover, the set \rho^(L) of modal companions of ''L'' contains an
infinite descending chain In mathematics, a total or linear order is a partial order in which any two elements are comparable. That is, a total order is a binary relation \leq on some Set (mathematics), set X, which satisfies the following for all a, b and c in X: # a ...
. For example, \rho^(\mathbf) consists of S5, and the logics L(C_n) for every positive integer ''n'', where C_n is the ''n''-element cluster. The set of modal companions of any ''L'' is either
countable In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers; ...
, or it has the
cardinality of the continuum In set theory, the cardinality of the continuum is the cardinality or "size" of the set of real numbers \mathbb R, sometimes called the continuum. It is an infinite cardinal number and is denoted by \mathfrak c (lowercase fraktur "c") or , \mathb ...
. Rybakov has shown that the lattice Ext''L'' can be embedded in \rho^(L); in particular, a logic has a continuum of modal companions if it has a continuum of extensions (this holds, for instance, for all intermediate logics below KC). It is unknown whether the converse is also true. The Gödel translation can be applied to
rule Rule or ruling may refer to: Education * Royal University of Law and Economics (RULE), a university in Cambodia Human activity * The exercise of political or personal control by someone with authority or power * Business rule, a rule perta ...
s as well as formulas: the translation of a rule :R=\frac is the rule :T(R)=\frac{T(B)}. A rule ''R'' is admissible in a logic ''L'' if the set of theorems of ''L'' is closed under ''R''. It is easy to see that ''R'' is admissible in a superintuitionistic logic ''L'' whenever ''T''(''R'') is admissible in a modal companion of ''L''. The converse is not true in general, but it holds for the largest modal companion of ''L''.


References

*Alexander Chagrov and Michael Zakharyaschev, ''Modal Logic'', vol. 35 of Oxford Logic Guides, Oxford University Press, 1997. *Vladimir V. Rybakov, ''Admissibility of Logical Inference Rules'', vol. 136 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1997. Modal logic