HOME

TheInfoList



OR:

Kripke semantics (also known as relational semantics or frame semantics, and often confused with
possible world semantics A possible world is a complete and consistent way the world is or could have been. Possible worlds are widely used as a formal device in logic, philosophy, and linguistics in order to provide a semantics for intensional and modal logic. Their m ...
) is a formal
semantics Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and compu ...
for
non-classical logic Non-classical logics (and sometimes alternative logics) are formal systems that differ in a significant way from standard logical systems such as propositional and predicate logic. There are several ways in which this is done, including by way of ...
systems created in the late 1950s and early 1960s by
Saul Kripke Saul Aaron Kripke (; November 13, 1940 – September 15, 2022) was an American philosopher and logician in the analytic tradition. He was a Distinguished Professor of Philosophy at the Graduate Center of the City University of New York and emeri ...
and
André Joyal André Joyal (; born 1943) is a professor of mathematics at the Université du Québec à Montréal who works on category theory. He was a member of the School of Mathematics at the Institute for Advanced Study in 2013, where he was invited to jo ...
. It was first conceived for
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 ...
s, and later adapted to
intuitionistic logic Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
and other non-classical systems. The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the
model theory In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the st ...
of such logics was almost non-existent before Kripke (algebraic semantics existed, but were considered 'syntax in disguise').


Semantics of modal logic

The language of propositional modal logic consists of a
countably infinite set 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 ...
of
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 proposit ...
s, a set of truth-functional
connectives In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. They can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary co ...
(in this article \to and \neg), and the modal operator \Box ("necessarily"). The modal operator \Diamond ("possibly") is (classically) the
dual Dual or Duals may refer to: Paired/two things * Dual (mathematics), a notion of paired concepts that mirror one another ** Dual (category theory), a formalization of mathematical duality *** see more cases in :Duality theories * Dual (grammatical ...
of \Box and may be defined in terms of necessity like so: \Diamond A := \neg\Box\neg A ("possibly A" is defined as equivalent to "not necessarily not A").


Basic definitions

A Kripke frame or modal frame is a pair \langle W,R\rangle, where ''W'' is a (possibly empty) set, and ''R'' is a
binary relation In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over sets and is a new set of ordered pairs consisting of elements in and i ...
on ''W''. Elements of ''W'' are called ''nodes'' or ''worlds'', and ''R'' is known as the
accessibility relation An accessibility relation is a relation which plays a key role in assigning truth values to sentences in the relational semantics for modal logic. In relational semantics, a modal formula's truth value at a ''possible world'' w can depend on ...
. A Kripke model is a triple \langle W,R,\Vdash\rangle, where \langle W,R\rangle is a Kripke frame, and \Vdash is a relation between nodes of ''W'' and modal formulas, such that for all ''w'' ∈ ''W'' and modal formulas ''A'' and ''B'': * w\Vdash\neg A if and only if w\nVdash A, * w\Vdash A\to B if and only if w\nVdash A or w\Vdash B, * w\Vdash\Box A if and only if u\Vdash A for all u such that w\; R\; u. We read w\Vdash A as “''w'' satisfies ''A''”, “''A'' is satisfied in ''w''”, or “''w'' forces ''A''”. The relation \Vdash is called the ''satisfaction relation'', ''evaluation'', or '' forcing relation''. The satisfaction relation is uniquely determined by its value on propositional variables. A formula ''A'' is valid in: * a model \langle W,R,\Vdash\rangle, if w\Vdash A for all ''w'' ∈ ''W'', * a frame \langle W,R\rangle, if it is valid in \langle W,R,\Vdash\rangle for all possible choices of \Vdash, * a class ''C'' of frames or models, if it is valid in every member of ''C''. We define Thm(''C'') to be the set of all formulas that are valid in ''C''. Conversely, if ''X'' is a set of formulas, let Mod(''X'') be the class of all frames which validate every formula from ''X''. A modal logic (i.e., a set of formulas) ''L'' is
sound In physics, sound is a vibration that propagates as an acoustic wave, through a transmission medium such as a gas, liquid or solid. In human physiology and psychology, sound is the ''reception'' of such waves and their ''perception'' by the ...
with respect to a class of frames ''C'', if ''L'' ⊆ Thm(''C''). ''L'' is
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 ...
wrt ''C'' if ''L'' ⊇ Thm(''C'').


Correspondence and completeness

Semantics is useful for investigating a logic (i.e. a derivation system) only if the
semantic consequence Logical consequence (also entailment) is a fundamental concept in logic, which describes the relationship between statements that hold true when one statement logically ''follows from'' one or more statements. A valid logical argument is one ...
relation reflects its syntactical counterpart, the '' syntactic consequence'' relation (''derivability''). It is vital to know which modal logics are sound and complete with respect to a class of Kripke frames, and to determine also which class that is. For any class ''C'' of Kripke frames, Thm(''C'') is a
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(A\to B)\to(\Box A\to\Box B) and it is closed under: * Detachment rule (''modus po ...
(in particular, theorems of the minimal normal modal logic, ''K'', are valid in every Kripke model). However, the converse does not hold in general: while most of the modal systems studied are complete of classes of frames described by simple conditions, Kripke incomplete normal modal logics do exist. A natural example of such a system is
Japaridze's polymodal logic Japaridze's polymodal logic (GLP) is a system of provability logic with infinitely many provability modalities. This system has played an important role in some applications of provability algebras in proof theory, and has been extensively studied ...
. A normal modal logic ''L'' corresponds to a class of frames ''C'', if ''C'' = Mod(''L''). In other words, ''C'' is the largest class of frames such that ''L'' is sound wrt ''C''. It follows that ''L'' is Kripke complete if and only if it is complete of its corresponding class. Consider the schema T : \Box A\to A. T is valid in any reflexive frame \langle W,R\rangle: if w\Vdash \Box A, then w\Vdash A since ''w'' ''R'' ''w''. On the other hand, a frame which validates T has to be reflexive: fix ''w'' ∈ ''W'', and define satisfaction of a propositional variable ''p'' as follows: u\Vdash p if and only if ''w'' ''R'' ''u''. Then w\Vdash \Box p, thus w\Vdash p by T, which means ''w'' ''R'' ''w'' using the definition of \Vdash. T corresponds to the class of reflexive Kripke frames. It is often much easier to characterize the corresponding class of ''L'' than to prove its completeness, thus correspondence serves as a guide to completeness proofs. Correspondence is also used to show ''incompleteness'' of modal logics: suppose ''L''1 ⊆ ''L''2 are normal modal logics that correspond to the same class of frames, but ''L''1 does not prove all theorems of ''L''2. Then ''L''1 is Kripke incomplete. For example, the schema \Box(A\leftrightarrow\Box A)\to\Box A generates an incomplete logic, as it corresponds to the same class of frames as GL (viz. transitive and converse well-founded frames), but does not prove the GL-tautology \Box A\to\Box\Box A.


Common modal axiom schemata

The following table lists common modal axioms together with their corresponding classes. The naming of the axioms often varies; Here, axiom K is named after
Saul Kripke Saul Aaron Kripke (; November 13, 1940 – September 15, 2022) was an American philosopher and logician in the analytic tradition. He was a Distinguished Professor of Philosophy at the Graduate Center of the City University of New York and emeri ...
; axiom T is named after the truth axiom in
epistemic logic Epistemic modal logic is a subfield of modal logic that is concerned with reasoning about knowledge. While epistemology has a long philosophical tradition dating back to Ancient Greece, epistemic logic is a much more recent development with applica ...
; axiom D is named after
deontic logic Deontic logic is the field of philosophical logic that is concerned with obligation, permission, and related concepts. Alternatively, a deontic logic is a formal system that attempts to capture the essential logical features of these concepts. I ...
; axiom B is named after
L. E. J. Brouwer Luitzen Egbertus Jan Brouwer (; ; 27 February 1881 – 2 December 1966), usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, who worked in topology, set theory, measure theory and c ...
; and axioms 4 and 5 are named based on
C. I. Lewis Clarence Irving Lewis (April 12, 1883 – February 3, 1964), usually cited as C. I. Lewis, was an American academic philosopher. He is considered the progenitor of modern modal logic and the founder of conceptual pragmatism. First a noted logic ...
's numbering of symbolic logic systems. Axiom K can also be rewritten as \Box A\to B)\land Ato \Box B, which logically establishes
modus ponens In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. It ...
as a
rule of inference In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...
in every possible world. Note that for axiom D, \Diamond A implicity implies \Diamond\top, which means that for every possible world in the model, there is always at least one possible world accessible from it (which could be itself). This implicit implication \Diamond A \rightarrow \Diamond\top is similar to the implicit implication by existential quantifier on the range of quantification.


Common modal systems


Canonical models

For any normal modal logic, ''L'', a Kripke model (called the canonical model) can be constructed that refutes precisely the non-theorems of ''L'', by an adaptation of the standard technique of using maximal consistent sets as models. Canonical Kripke models play a role similar to the
Lindenbaum–Tarski algebra In mathematical logic, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a logical theory ''T'' consists of the equivalence classes of sentences of the theory (i.e., the quotient, under the equivalence relation ~ defined such that ''p'' ...
construction in algebraic semantics. A set of formulas is ''L''-''consistent'' if no contradiction can be derived from it using the theorems of ''L'', and Modus Ponens. A ''maximal L-consistent set'' (an ''L''-''MCS'' for short) is an ''L''-consistent set that has no proper ''L''-consistent superset. The canonical model of ''L'' is a Kripke model \langle W,R,\Vdash\rangle, where ''W'' is the set of all ''L''-''MCS'', and the relations ''R'' and \Vdash are as follows: : X\;R\;Y if and only if for every formula A, if \Box A\in X then A\in Y, : X\Vdash A if and only if A\in X. The canonical model is a model of ''L'', as every ''L''-''MCS'' contains all theorems of ''L''. By Zorn's lemma, each ''L''-consistent set is contained in an ''L''-''MCS'', in particular every formula unprovable in ''L'' has a counterexample in the canonical model. The main application of canonical models are completeness proofs. Properties of the canonical model of K immediately imply completeness of K with respect to the class of all Kripke frames. This argument does ''not'' work for arbitrary ''L'', because there is no guarantee that the underlying ''frame'' of the canonical model satisfies the frame conditions of ''L''. We say that a formula or a set ''X'' of formulas is canonical with respect to a property ''P'' of Kripke frames, if * ''X'' is valid in every frame that satisfies ''P'', * for any normal modal logic ''L'' that contains ''X'', the underlying frame of the canonical model of ''L'' satisfies ''P''. A union of canonical sets of formulas is itself canonical. It follows from the preceding discussion that any logic axiomatized by a canonical set of formulas is Kripke complete, and
compact Compact as used in politics may refer broadly to a pact or treaty; in more specific cases it may refer to: * Interstate compact * Blood compact, an ancient ritual of the Philippines * Compact government, a type of colonial rule utilized in Briti ...
. The axioms T, 4, D, B, 5, H, G (and thus any combination of them) are canonical. GL and Grz are not canonical, because they are not compact. The axiom M by itself is not canonical (Goldblatt, 1991), but the combined logic S4.1 (in fact, even K4.1) is canonical. In general, it is undecidable whether a given axiom is canonical. We know a nice sufficient condition: Henrik Sahlqvist identified a broad class of formulas (now called Sahlqvist formulas) such that * a Sahlqvist formula is canonical, * the class of frames corresponding to a Sahlqvist formula is first-order definable, * there is an algorithm that computes the corresponding frame condition to a given Sahlqvist formula. This is a powerful criterion: for example, all axioms listed above as canonical are (equivalent to) Sahlqvist formulas.


Finite model property

A logic has the finite model property (FMP) if it is complete with respect to a class of finite frames. An application of this notion is the decidability question: it follows from
Post's theorem In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees. Background The statement of Post's theorem uses several concepts relating to definability and re ...
that a recursively axiomatized modal logic ''L'' which has FMP is decidable, provided it is decidable whether a given finite frame is a model of ''L''. In particular, every finitely axiomatizable logic with FMP is decidable. There are various methods for establishing FMP for a given logic. Refinements and extensions of the canonical model construction often work, using tools such as
filtration Filtration is a physical separation process that separates solid matter and fluid from a mixture using a ''filter medium'' that has a complex structure through which only the fluid can pass. Solid particles that cannot pass through the filter m ...
or unravelling. As another possibility, completeness proofs based on cut-free sequent calculi usually produce finite models directly. Most of the modal systems used in practice (including all listed above) have FMP. In some cases, we can use FMP to prove Kripke completeness of a logic: every normal modal logic is complete with respect to a class of modal algebras, and a ''finite'' modal algebra can be transformed into a Kripke frame. As an example, Robert Bull proved using this method that every normal extension of S4.3 has FMP, and is Kripke complete.


Multimodal logics

Kripke semantics has a straightforward generalization to logics with more than one modality. A Kripke frame for a language with \ as the set of its necessity operators consists of a non-empty set ''W'' equipped with binary relations ''Ri'' for each ''i'' ∈ ''I''. The definition of a satisfaction relation is modified as follows: : w\Vdash\Box_i A if and only if \forall u\,(w\;R_i\;u\Rightarrow u\Vdash A). A simplified semantics, discovered by Tim Carlson, is often used for polymodal
provability logic Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic. Examples ...
s. A Carlson model is a structure \langle W,R,\_,\Vdash\rangle with a single accessibility relation ''R'', and subsets ''Di'' ⊆ ''W'' for each modality. Satisfaction is defined as : w\Vdash\Box_i A if and only if \forall u\in D_i\,(w\;R\;u\Rightarrow u\Vdash A). Carlson models are easier to visualize and to work with than usual polymodal Kripke models; there are, however, Kripke complete polymodal logics which are Carlson incomplete.


Semantics of intuitionistic logic

Kripke semantics for
intuitionistic logic Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
follows the same principles as the semantics of modal logic, but it uses a different definition of satisfaction. An intuitionistic Kripke model is a triple \langle W,\le,\Vdash\rangle, where \langle W,\le\rangle is a
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 ca ...
ed Kripke frame, and \Vdash satisfies the following conditions: * if ''p'' is a propositional variable, w\le u, and w\Vdash p, then u\Vdash p (''persistency'' condition (cf.
monotonicity In mathematics, a monotonic function (or monotone function) is a function between ordered sets that preserves or reverses the given order. This concept first arose in calculus, and was later generalized to the more abstract setting of order ...
)), * w\Vdash A\land B if and only if w\Vdash A and w\Vdash B, * w\Vdash A\lor B if and only if w\Vdash A or w\Vdash B, * w\Vdash A\to B if and only if for all u\ge w, u\Vdash A implies u\Vdash B, * not w\Vdash\bot. The negation of ''A'', ¬''A'', could be defined as an abbreviation for ''A'' → ⊥. If for all ''u'' such that ''w'' ≤ ''u'', not ''u'' ''A'', then ''w'' ''A'' → ⊥ is
vacuously true In mathematics and logic, a vacuous truth is a conditional or universal statement (a universal statement that can be converted to a conditional statement) that is true because the antecedent cannot be satisfied. For example, the statement "sh ...
, so ''w'' ¬''A''. Intuitionistic logic is sound and complete with respect to its Kripke semantics, and it has the finite model property.


Intuitionistic first-order logic

Let ''L'' be a first-order language. A Kripke model of ''L'' is a triple \langle W,\le,\_\rangle, where \langle W,\le\rangle is an intuitionistic Kripke frame, ''Mw'' is a (classical) ''L''-structure for each node ''w'' ∈ ''W'', and the following compatibility conditions hold whenever ''u'' ≤ ''v'': * the domain of ''Mu'' is included in the domain of ''Mv'', * realizations of function symbols in ''Mu'' and ''Mv'' agree on elements of ''Mu'', * for each ''n''-ary predicate ''P'' and elements ''a''1,...,''an'' ∈ ''Mu'': if ''P''(''a''1,...,''an'') holds in ''Mu'', then it holds in ''Mv''. Given an evaluation ''e'' of variables by elements of ''Mw'', we define the satisfaction relation w\Vdash A /math>: * w\Vdash P(t_1,\dots,t_n) /math> if and only if P(t_1 \dots,t_n holds in ''Mw'', * w\Vdash(A\land B) /math> if and only if w\Vdash A /math> and w\Vdash B /math>, * w\Vdash(A\lor B) /math> if and only if w\Vdash A /math> or w\Vdash B /math>, * w\Vdash(A\to B) /math> if and only if for all u\ge w, u\Vdash A /math> implies u\Vdash B /math>, * not w\Vdash\bot /math>, * w\Vdash(\exists x\,A) /math> if and only if there exists an a\in M_w such that w\Vdash A (x\to a)/math>, * w\Vdash(\forall x\,A) /math> if and only if for every u\ge w and every a\in M_u , u\Vdash A (x\to a)/math>. Here ''e''(''x''→''a'') is the evaluation which gives ''x'' the value ''a'', and otherwise agrees with ''e''. See a slightly different formalization in.


Kripke–Joyal semantics

As part of the independent development of
sheaf theory In mathematics, a sheaf is a tool for systematically tracking data (such as sets, abelian groups, rings) attached to the open sets of a topological space and defined locally with regard to them. For example, for each open set, the data could ...
, it was realised around 1965 that Kripke semantics was intimately related to the treatment of
existential quantification In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, whe ...
in
topos theory In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much like the category of sets and possess a notio ...
. That is, the 'local' aspect of existence for sections of a sheaf was a kind of logic of the 'possible'. Though this development was the work of a number of people, the name Kripke–Joyal semantics is often used in this connection.


Model constructions

As in classical
model theory In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the st ...
, there are methods for constructing a new Kripke model from other models. The natural
homomorphism In algebra, a homomorphism is a structure-preserving map between two algebraic structures of the same type (such as two groups, two rings, or two vector spaces). The word ''homomorphism'' comes from the Ancient Greek language: () meaning "same ...
s in Kripke semantics are called p-morphisms (which is short for ''pseudo-epimorphism'', but the latter term is rarely used). A p-morphism of Kripke frames \langle W,R\rangle and \langle W',R'\rangle is a mapping f\colon W\to W' such that * ''f'' preserves the accessibility relation, i.e., ''u R v'' implies ''f''(''u'') ''R’'' ''f''(''v''), * whenever ''f''(''u'') ''R’'' ''v''’, there is a ''v'' ∈ ''W'' such that ''u R v'' and ''f''(''v'') = ''v''’. A p-morphism of Kripke models \langle W,R,\Vdash\rangle and \langle W',R',\Vdash'\rangle is a p-morphism of their underlying frames f\colon W\to W', which satisfies : w\Vdash p if and only if f(w)\Vdash'p, for any propositional variable ''p''. P-morphisms are a special kind of
bisimulation In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa. Intuitively two systems are bisimilar if ...
s. In general, a bisimulation between frames \langle W,R\rangle and \langle W',R'\rangle is a relation ''B ⊆ W × W’'', which satisfies the following “zig-zag” property: * if ''u B u’'' and ''u R v'', there exists ''v’'' ∈ ''W’'' such that ''v B v’'' and ''u’ R’ v’'', * if ''u B u’'' and ''u’ R’ v’'', there exists ''v'' ∈ ''W'' such that ''v B v’'' and ''u R v''. A bisimulation of models is additionally required to preserve forcing of
atomic formula In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformul ...
s: : if ''w B w’'', then w\Vdash p if and only if w'\Vdash'p, for any propositional variable ''p''. The key property which follows from this definition is that bisimulations (hence also p-morphisms) of models preserve the satisfaction of ''all'' formulas, not only propositional variables. We can transform a Kripke model into a
tree In botany, a tree is a perennial plant with an elongated Plant stem, stem, or trunk (botany), trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, including only woody plants with secondar ...
using unravelling. Given a model \langle W,R,\Vdash\rangle and a fixed node ''w''0 ∈ ''W'', we define a model \langle W',R',\Vdash'\rangle, where ''W’'' is the set of all finite sequences s=\langle w_0,w_1,\dots,w_n\rangle such that ''wi R wi+1'' for all ''i'' < ''n'', and s\Vdash p if and only if w_n\Vdash p for a propositional variable ''p''. The definition of the accessibility relation ''R’'' varies; in the simplest case we put :\langle w_0,w_1,\dots,w_n\rangle\;R'\;\langle w_0,w_1,\dots,w_n,w_\rangle, but many applications need the reflexive and/or transitive closure of this relation, or similar modifications. Filtration is a useful construction which uses to prove FMP for many logics. Let ''X'' be a set of formulas closed under taking subformulas. An ''X''-filtration of a model \langle W,R,\Vdash\rangle is a mapping ''f'' from ''W'' to a model \langle W',R',\Vdash'\rangle such that * ''f'' is a
surjection In mathematics, a surjective function (also known as surjection, or onto function) is a function that every element can be mapped from element so that . In other words, every element of the function's codomain is the image of one element of ...
, * ''f'' preserves the accessibility relation, and (in both directions) satisfaction of variables ''p'' ∈ ''X'', * if ''f''(''u'') ''R’'' ''f''(''v'') and u\Vdash\Box A, where \Box A\in X, then v\Vdash A. It follows that ''f'' preserves satisfaction of all formulas from ''X''. In typical applications, we take ''f'' as the projection onto the
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 ...
of ''W'' over the relation : ''u ≡X v'' if and only if for all ''A'' ∈ ''X'', u\Vdash A if and only if v\Vdash A. As in the case of unravelling, the definition of the accessibility relation on the quotient varies.


General frame semantics

The main defect of Kripke semantics is the existence of Kripke incomplete logics, and logics which are complete but not compact. It can be remedied by equipping Kripke frames with extra structure which restricts the set of possible valuations, using ideas from algebraic semantics. This gives rise to the general frame semantics.


Computer science applications

Blackburn et al. (2001) point out that because a relational structure is simply a set together with a collection of relations on that set, it is unsurprising that relational structures are to be found just about everywhere. As an example from
theoretical computer science computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory. It is difficult to circumscribe the ...
, they give labeled transition systems, which model program execution. Blackburn et al. thus claim because of this connection that modal languages are ideally suited in providing "internal, local perspective on relational structures." (p. xii)


History and terminology

Similar work that predated Kripke's revolutionary semantic breakthroughs:preprint
(See the last two paragraphs in Section 3 Quasi-historical Interlude: the Road from Vienna to Los Angeles.) *
Rudolf Carnap Rudolf Carnap (; ; 18 May 1891 – 14 September 1970) was a German-language philosopher who was active in Europe before 1935 and in the United States thereafter. He was a major member of the Vienna Circle and an advocate of logical positivism. ...
seems to have been the first to have the idea that one can give a possible world semantics for the modalities of necessity and possibility by means of giving the valuation function a parameter that ranges over Leibnizian possible worlds. Bayart develops this idea further, but neither gave recursive definitions of satisfaction in the style introduced by Tarski; * J.C.C. McKinsey and
Alfred Tarski Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician a ...
developed an approach to modeling modal logics that is still influential in modern research, namely the algebraic approach, in which Boolean algebras with operators are used as models.
Bjarni Jónsson Bjarni Jónsson (February 15, 1920 – September 30, 2016) was an Icelandic mathematician and logician working in universal algebra, lattice theory, model theory and set theory. He was emeritus distinguished professor of mathematics at Vanderbilt ...
and Tarski established the representability of Boolean algebras with operators in terms of frames. If the two ideas had been put together, the result would have been precisely frame models, which is to say Kripke models, years before Kripke. But no one (not even Tarski) saw the connection at the time. *
Arthur Prior Arthur Norman Prior (4 December 1914 – 6 October 1969), usually cited as A. N. Prior, was a New Zealand–born logician and philosopher. Prior (1957) founded tense logic, now also known as temporal logic, and made important contributions ...
, building on unpublished work of C. A. Meredith, developed a translation of sentential modal logic into classical predicate logic that, if he had combined it with the usual model theory for the latter, would have produced a model theory equivalent to Kripke models for the former. But his approach was resolutely syntactic and anti-model-theoretic. * Stig Kanger gave a rather more complex approach to the interpretation of modal logic, but one that contains many of the key ideas of Kripke's approach. He first noted the relationship between conditions on accessibility relations and
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 Radiohe ...
-style axioms for modal logic. Kanger failed, however, to give a completeness proof for his system; *
Jaakko Hintikka Kaarlo Jaakko Juhani Hintikka (12 January 1929 – 12 August 2015) was a Finnish philosopher and logician. Life and career Hintikka was born in Helsingin maalaiskunta (now Vantaa). In 1953, he received his doctorate from the University of Helsi ...
gave a semantics in his papers introducing epistemic logic that is a simple variation of Kripke's semantics, equivalent to the characterisation of valuations by means of maximal consistent sets. He doesn't give inference rules for epistemic logic, and so cannot give a completeness proof; *
Richard Montague Richard Merritt Montague (September 20, 1930 – March 7, 1971) was an American mathematician and philosopher who made contributions to mathematical logic and the philosophy of language. He is known for proposing Montague grammar to formalize th ...
had many of the key ideas contained in Kripke's work, but he did not regard them as significant, because he had no completeness proof, and so did not publish until after Kripke's papers had created a sensation in the logic community; *
Evert Willem Beth Evert Willem Beth (7 July 1908 – 12 April 1964) was a Dutch philosopher and logician, whose work principally concerned the foundations of mathematics. He was a member of the Significs Group. Biography Beth was born in Almelo, a small to ...
presented a semantics of intuitionistic logic based on trees, which closely resembles Kripke semantics, except for using a more cumbersome definition of satisfaction.


See also

*
Alexandrov topology In topology, an Alexandrov topology is a topology in which the intersection of any family of open sets is open. It is an axiom of topology that the intersection of any ''finite'' family of open sets is open; in Alexandrov topologies the finite restr ...
*
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(A\to B)\to(\Box A\to\Box B) and it is closed under: * Detachment rule (''modus po ...
* Two-dimensionalism * Muddy Children Puzzle


Notes

:aAfter
Andrzej Grzegorczyk Andrzej Grzegorczyk (; 22 August 1922 – 20 March 2014) was a Polish logician, mathematician, philosopher, and ethicist noted for his work in computability, mathematical logic, and the foundations of mathematics. Historical family background ...
.


References

* * * * * * * * *


External links

* * * N.B: Constructive = intuitionistic. * * {{DEFAULTSORT:Kripke Semantics Modal logic Model theory Mathematical logic Philosophical logic Sheaf theory Non-classical logic de:Kripke-Semantik