Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Kripke semantics
Summary
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é Joyal. It was first conceived for modal logics, and later adapted to intuitionistic logic and other non-classical systems. The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the model theory of such logics was almost non-existent before Kripke (algebraic semantics existed, but were considered 'syntax in disguise').
Modal logic
The language of propositional modal logic consists of a countably infinite set of propositional variables, a set of truth-functional connectives (in this article and ), and the modal operator ("necessarily"). The modal operator ("possibly") is (classically) the dual of and may be defined in terms of necessity like so: ("possibly A" is defined as equivalent to "not necessarily not A").
A Kripke frame or modal frame is a pair , where W is a (possibly empty) set, and R is a binary relation on W. Elements
of W are called nodes or worlds, and R is known as the accessibility relation.
A Kripke model is a triple , where
is a Kripke frame, and is a relation between nodes of W and modal formulas, such that for all w ∈ W and modal formulas A and B:
if and only if ,
if and only if or ,
if and only if for all such that .
We read as “w satisfies
A”, “A is satisfied in w”, or
“w forces A”. The relation 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 , if for all w ∈ W,
a frame , if it is valid in for all possible choices of ,
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.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Ontological neighbourhood
Related courses (2)
MATH-381: Mathematical logic
Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.
CS-550: Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
Related lectures (11)
Relational Semantics of Loops
Explores the relational semantics of loops in programs and the mathematical interpretation of loop structures.
Automating First-Order Logic Proofs Using Resolution
Covers first-order logic syntax, semantics, Skolemization, resolution, and normal form transformations.
Variables & Operators
Covers the basics of C programming, including variables, operators, and system-oriented programming, emphasizing differences from Java.
Related publications (34)
Related people (7)
Related units (1)
Related concepts (23)
Interpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics. The most commonly studied formal logics are propositional logic, predicate logic and their modal analogs, and for these there are standard ways of presenting an interpretation.
Completeness (logic)
In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula having the property can be derived using that system, i.e. is one of its theorems; otherwise the system is said to be incomplete. The term "complete" is also used without qualification, with differing meanings depending on the context, mostly referring to the property of semantical validity. Intuitively, a system is called complete in this particular sense, if it can derive every formula that is true.
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. There are a number of provability logics, some of which are covered in the literature mentioned in . The basic system is generally referred to as GL (for Gödel–Löb) or L or K4W (W stands for well-foundedness). It can be obtained by adding the modal version of Löb's theorem to the logic K (or K4).