In logic

Logic

In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...

, a modal companion of a superintuitionistic

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 logics .-Definition:A superintuitionistic logic is a...

 (intermediate) logic L is a normal

Normal modal logic

In logic, a normal modal logic is a set L of modal formulas such that L contains:* All propositional tautologies;* All instances of the Kripke schema: \Box\toand it is closed under:...

 modal logic

Modal logic

Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...

 which interprets L by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables to study intermediate logics using tools developed for modal logic.

Gödel–McKinsey–Tarski translation

Let A be a propositional intuitionistic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

 formula. A modal formula T(A) is defined by induction on the complexity of A: for any propositional variable

Propositional variable

In mathematical logic, a propositional variable is a variable which can either be true or false...

 ,
As negation is in intuitionistic logic defined by , we also have
is called the Gödel translation or Gödel

Kurt Gödel

Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...

–McKinsey–Tarski

Alfred Tarski

Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...

 translation. The translation is sometimes presented in slightly different ways: for example, one may insert before every subformula. All such variants are provably equivalent in S4.

Modal companions

For any normal modal logic M which extends S4, we define its si-fragment ρM as
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 .

Every superintuitionistic logic has modal companions. The smallest modal companion of L is
where denotes normal closure. It can be shown that every superintuitionistic logic also has the largest modal companion, which is denoted by σL. A modal logic M is a companion of L if and only if .

For example, S4 itself is the smallest modal companion of the intuitionistic logic (IPC). The largest modal companion of IPC is the Grzegorczyk

Andrzej Grzegorczyk

Andrzej Grzegorczyk is a Polish mathematician. He is known for his work in computability, logic, and the foundations of mathematics...

 logic Grz, axiomatized by the axiom
over K. The smallest modal companion of the classical logic (CPC) is Lewis' S5, whereas its largest modal companion is the logic
More examples:

L	τL	σL	other companions of L
IPC	S4	Grz	S4.1, Dum, ...
KC	S4.2	Grz.2	S4.1.2, ...
LC	S4.3	Grz.3	S4.1.3, S4.3Dum, ...
CPC	S5	Triv	see below

Blok–Esakia isomorphism

The set of extensions of a superintuitionistic logic L ordered by inclusion forms a complete lattice

Complete lattice

In mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum and an infimum . Complete lattices appear in many applications in mathematics and computer science...

, denoted ExtL. Similarly, the set of normal extensions of a modal logic M is a complete lattice NExtM. The companion operators ρM, τL, and σL can be considered as mappings between the lattices ExtIPC and NExtS4:
It is easy to see that all three are monotone

Monotonic function

In mathematics, a monotonic function is a function that preserves the given order. This concept first arose in calculus, and was later generalized to the more abstract setting of order theory....

, and is the identity function on ExtIPC. L. Maksimova and V. Rybakov have shown that ρ, τ, and σ are actually complete lattice homomorphisms. 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

Inverse function

In mathematics, an inverse function is a function that undoes another function: If an input x into the function ƒ produces an output y, then putting y into the inverse function g produces the output x, and vice versa. i.e., ƒ=y, and g=x...

 lattice isomorphism

Isomorphism

In abstract algebra, an isomorphism is a mapping between objects that shows a relationship between two properties or operations.  If there exists an isomorphism between two structures, the two structures are said to be isomorphic.  In a certain sense, isomorphic structures are...

s of ExtIPC and NExtGrz.

Accordingly, σ and the restriction 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,

Semantic description

The Gödel translation has a frame-theoretic counterpart. Let be a transitive and reflexive

Reflexive

Reflexive may refer to:In fiction:*MetafictionIn grammar:*Reflexive pronoun, a pronoun with a reflexive relationship with its self-identical antecedent*Reflexive verb, where a semantic agent and patient are the same...

 modal general frame

General frame

In logic, general frames are Kripke frames with an additional structure, which are used to model modal and intermediate logics...

. The preorder

Preorder

In mathematics, especially in order theory, preorders are binary relations that are reflexive and transitive.For example, all partial orders and equivalence relations are preorders...

 R induces the equivalence relation

Equivalence relation

In mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...

on F, which identifies points belonging to the same cluster. Let be the induced quotient partial order (i.e., ρF is the set of equivalence classes of ), and put
Then 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 , let σV be the closure of V under Boolean operations (binary intersection

Intersection (set theory)

In mathematics, the intersection of two sets A and B is the set that contains all elements of A that also belong to B , but no other elements....

 and complement

Complement (set theory)

In set theory, a complement of a set A refers to things not in , A. The relative complement of A with respect to a set B, is the set of elements in B but not in A...

). It can be shown that σV is closed under , thus 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 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
  Decidability (logic)
  In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...
  
   is preserved by ρ, τ, and σ,
• finite model property is preserved by ρ, τ, and σ,
• tabularity is preserved by ρ and σ,
• Kripke completeness is preserved by ρ and τ,
• first-order
  First-order logic
  First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
  
   definability on Kripke frames is preserved by ρ and τ.

Other properties

Every intermediate logic L has an infinite number of modal companions, and moreover, the set of modal companions of L contains an infinite descending chain

Infinite descending chain

Given a set S with a partial order ≤, an infinite descending chain is a chain V that is a subset of S upon which ≤ defines a total order such that V has no least element, that is, an element m such that for all elements n in V it holds that m ≤ n.As an example, in the set of integers, the chain...

. For example, consists of S5, and the logics for every positive integer n, where is the n-element cluster. The set of modal companions of any L is either countable

Countable set

In mathematics, a countable set is a set with the same cardinality as some subset of the set of natural numbers. A set that is not countable is called uncountable. The term was originated by Georg Cantor...

, or it has the cardinality of the continuum

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 |\mathbb R| or \mathfrak c ....

. Rybakov has shown that the lattice ExtL can be embedded

Embedding

In mathematics, an embedding is one instance of some mathematical structure contained within another instance, such as a group that is a subgroup....

 in ; 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 of inference

In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...

s as well as formulas: the translation of a rule
is the rule
A rule R is admissible

Admissible rule

In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense,...

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.