repülő szőnyeg

Kripke szemantikája

november 12, 2009 at 9:15 am (metafizika)
Tags: kripke, logika, modális logika, ruzsa

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, beginning when he was a teenager. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems. The discovery of Kripke semantics was a breakthrough in the theory of non-classical logics, because the model theory of such logics was nonexistent before Kripke.

The language of propositional modal logic consists of a countably infinite set of propositional variables, a set of truth-functional connectives (in this article $\to$ and $\neg$ ), and the modal operator $\Box$ (“necessarily”). The dual modal operator $\Diamond$ (“possibly”) of $\Box$ is defined as $\Diamond A=_{df}\neg\Box\neg A$ . See the page on modal logic for more background.

[edit] Basic definitions

A Kripke frame or modal frame is a pair $\langle W,R\rangle$ , where W is a non-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 $\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:

$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 $\forall u\,(w\; R\; u \to u\Vdash A)$ .

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 with respect to a class of frames C, if L ⊆ Thm(C). L is complete wrt C if L ⊇ Thm(C).

[edit] Correspondence and completeness

Semantics is useful for investigating a logic (i.e. a derivation system) only if the semantical entailment relation reflects its syntactical counterpart, the 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 particular, theorems of the minimal normal modal logic, K, are valid in every Kripke model). However, the converse does not hold in general. There are Kripke incomplete normal modal logics, which is not a problem, because most of the modal systems studied are complete of classes of frames described by simple conditions.

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₁ ⊆ L₂ are normal modal logics that correspond to the same class of frames, but L₁ does not prove all theorems of L₂. Then L₁ is Kripke incomplete. For example, the schema $\Box(A\equiv\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$ .

The table below is a list of common modal axioms together with their corresponding classes. The naming of the axioms often varies.

kripke szemantika

Here is a list of several common modal systems. Frame conditions for some of them were simplified: the logics are complete with respect to the frame classes given in the table, but they may correspond to a larger class of frames.

kripke szemnatika2

Canonical models

For any normal modal logic L, a Kripke model (called the canonical model) can be constructed, which validates precisely the 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 construction in algebraic semantics.

A set of formulas is L-consistent if no contradiction can be derived from them using the axioms of L, and Modus Ponens. A maximal L-consistent set (an L-MCS for short) is an L-consistent set which 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 which satisfies P,
for any normal modal logic L which 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.

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: H. 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 which 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.

[edit] 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 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 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 wrt 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.

[edit] Multimodal logics

[edit] Semantics of intuitionistic logic

Kripke semantics for the intuitionistic logic 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 partially ordered 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),
$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$ .

Intuitionistic logic is sound and complete with respect to its Kripke semantics, and it has FMP.

[edit] Intuitionistic first-order logic

Let L be a first-order language. A Kripke model of L is a triple $\langle W,\le,\{M_w\}_{w\in W}\rangle$ , where $\langle W,\le\rangle$ is an intuitionistic Kripke frame, M_w is a (classical) L-structure for each node w ∈ W, and the following compatibility conditions hold whenever u ≤ v:

the domain of M_u is included in the domain of M_v,
realizations of function symbols in M_u and M_v agree on elements of M_u,
for each n-ary predicate P and elements a₁,…,a_n ∈ M_u: if P(a₁,…,a_n) holds in M_u, then it holds in M_v.

Given an evaluation e of variables by elements of M_w, we define the satisfaction relation $w\Vdash A[e]$ :

$w\Vdash P(t_1,\dots,t_n)[e]$ if and only if $P(t_1[e],\dots,t_n[e])$ holds in M_w,
$w\Vdash(A\land B)[e]$ if and only if $w\Vdash A[e]$ and $w\Vdash B[e]$ ,
$w\Vdash(A\lor B)[e]$ if and only if $w\Vdash A[e]$ or $w\Vdash B[e]$ ,
$w\Vdash(A\to B)[e]$ if and only if for all $u\ge w$ , $u\Vdash A[e]$ implies $u\Vdash B[e]$ ,
not $w\Vdash\bot[e]$ ,
$w\Vdash(\exists x\,A)[e]$ if and only if there exists an $a\in M_w$ such that $w\Vdash A[e(x\to a)]$ ,
$w\Vdash(\forall x\,A)[e]$ if and only if for every $u\ge w$ and every $a\in M_u$ , $u\Vdash A[e(x\to a)]$ .

Here e(x→a) is the evaluation which gives x the value a, and otherwise agrees with e.

See a slightly different formalization in ^[1].

[edit] Kripke–Joyal semantics

As part of the quite independent development of sheaf theory, it was realised around 1965 that Kripke semantics was intimately related to the treatment of existential quantification in topos theory. That is, the ‘local’ aspect of existence for sections of a sheaf was a kind of logic of the ‘possible’. Since this development was the work of a number of people, and was more in the nature of a conceptual insight than a theorem, it is not so easy to attribute credit. The name Kripke–Joyal semantics is often used in this connection.

[edit] Model constructions

As in the classical model theory, there are methods for constructing a new Kripke model from other models.

The natural homomorphisms 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 bisimulations. 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 formulas:

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 using unravelling. Given a model $\langle W,R,\Vdash\rangle$ and a fixed node w₀ ∈ 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 w_i R w_i+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_{n+1}\rangle$ ,

but many applications need the reflexive and/or transitive closure of this relation, or similar modifications.

Filtration is a variant of a p-morphism. 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,
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 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.

„	Úgy tűnik, az ókori időkben Szaúd-Arábia és Afrika voltak a legnagyobb tömjénellátó területek, míg ma a gumikereskedelem központja Aden és Omán. Ősi egyiptomi rituális szövegekből tudjuk, hogy a tömjént a Nílus felső vidékére szállították a kereskedők, ám erre talán a leglátványosabb bizonyítékot szolgáltatnak a thébai templomban látható i. e. 1500-ból származó freskók, amelyek egy, az egyiptomi királynő parancsára a punok földjére induló hajóhadat ábrázolnak. Ezeken a reliefeken öt, kincsekkel roskadásig megrakott hajót láthatunk, egyiken harmincegy kis becserepezett tömjénfát szállítanak.	”

„	Az Arábiával és Indiával folytatott tömjén- és fűszerkereskedelem egyre fontosabbá vált, és a görögök első ízben kezdtek közvetlenül Indiával kereskedni. A tengeri útvonal felfedezése, vagy inkább újrafelfedezése egy bizonyos Cyzicusi Eudoxus nevéhez köthető, akit VIII. Ptolemaiosz Euergetész uralkodása idején bíztak meg ezzel a feladattal. Eudoxos kétszer utazott Indiába, azonban összekülönbözött a Ptolemaioszokkal, végül azon az úton halt meg, amit egy, a ptolemaioszi befolyástól mentes indiai tengeri útvonal megtalálása céljából kezdett el Afrika körülhajózásával. Az Egyiptom és India közötti közvetlen kapcsolat létrejöttében talán szerepet játszhatott az ez időben megfigyelhető arab hatalom gyengülése is. Lényegesen nőtt a fahéj, és egyéb keleti fűszerek, mint a bors egyiptomi importja, bár az Indiai óceánon folio szállítás egyelőre ritka volt, évente legfeljebb húsz egyiptomi hajó vágott neki a Vörös Tengeren kívül eső útnak.	”

„	A harmadik század jelentős időszak volt az arábiai tömjénkereskedelem történetében. A század politikai és gazdasági válsága miatt a kereskedelem jellege drámaian megváltozott. Azelőtt a Dél-Arábiából induló Tömjénút folyamatosan működni látszott. A harmadik század szűkös gazdasági feltételei miatt az itt folyó kereskedelem nagy része megtorpant, bár sok minden megváltozott a Tetrarchia idején, amikor a gazdasági élet ismét fellendült. Ebben az időszakban a két fő használatban lévő útvonal egyike a Wadi Sirhan, amely korábban Palmürát is érintette, a másik pedig az Aila, amelyen India és Arábia felől érkeztek azok az árucikkek, amelyeket korábban a Vörös-tenger egyiptomi kikötőiben rakodtak ki.	”

	gyongyosicsillanelli on modern héber 2. – 2oo7. …
	gyongyosicsillanelli on modern héber 2. – 2oo7. …
	gyongyosicsillanelli on modern héber 2. – 2oo7. …
	a Vera (akinek fala … on modern héber 2. – 2oo7. …
	Hoffman Barbara on barbinak

november 2009
F	S	S	M	T	W	T
« Sep
		1	2	3	4	5
6	7	8	9	10	11	12
13	14	15	16	17	18	19
20	21	22	23	24	25	26
27	28	29	30

[edit] Basic definitions

[edit] Correspondence and completeness

Canonical models

[edit] Finite model property

[edit] Multimodal logics

[edit] Semantics of intuitionistic logic

[edit] Intuitionistic first-order logic

[edit] Kripke–Joyal semantics

[edit] Model constructions

zakāt: vallási adó

zawāǧir: Isten tiltó szava

yaqīn: bizonyosság

yatima: árva

wa-ġayruhu min ahl al- ḥadīṯ: a többi hagyományozó

wāǧib: az iszlámjog követelménye

waḥdāniyya: Isten egyedülisége

walī: gyám

walīma: lakoma

wāriṯ: örökös

wasīṭa: közvetítő

waṣiyya: végrendelet

Umm al-kitāb: Őskönyv, a Korán eszméje

umma: közösség

uns: intim kapcsolat Istennel

tacarruf: feltárulkozás

tacāzir: önkényes megítélésen alapuló jogszabály

tacrīf: megismertetés

taǧrīd: lecsupaszítás

talāq: válás

tartīlan: jól érthető

taṣawwuf: szúfizmus (iszlám misztika)

tašbīh: hasonlítás

tašhīr: nyilvánosság elé vinni a bűnöst; eretnekség

tawakkul: rábízza magát Istenre

tawfīq: segítség

sālik aṭ-ṭarīq: úton járó

samāc: meghallgatás

sarīra: a szív legmélye

sirr: a szív legmélye

siyāsa: politika

sūq: heti piac

ra’y: vélemény

raḥba: nagymecset udvara

ramaḍān: szent hónap, böjt

rasūl Allāh: Isten Küldötte

rubc: negyed

ruǧūc: visszatérés

rusūm: formák

qabīla: törzs

qāḍī l-quḍāt: főbíró

qadīm: ősi

qawm: klán

qibla: imairány

qiyās: analógia

qurb: Isten közelsége

nafara: kivonul

nāfila: többlet-cselekedet

nasab: genealógia

nash: érvénytelenítés

nash: nem töröltetik el

naṣṣ: szöveg

naṣṣan: szöveg szerint

nikāḥ: házasság

macrifa: megismerés

madāhib al-fiqh: ortodox iskolák

madhab: ḥanbalita jogi iskola

madrasa: iskola

māhiyya: lényeg

mahlūqāt: teremtmények

mahr: jegyajándék

mālikiták:

mawāli: kliens

maẓālim: törvénytelenségek

micrāǧ: égi utazás

mīrāt: örökösödés

miṯlu: ugyanolyan

muḥtasib: piacfelügyelő

murīd: akaró (tanítvány)

murtadd: hűtlen az iszlámhoz

mutafarrid: elkülönülés

ta^carruf: feltárulkozás

ta^cāzir: önkényes megítélésen alapuló jogszabály

ta^crīf: megismertetés

samā^c: meghallgatás

rub^c: negyed

ruǧū^c: visszatérés

ma^crifa: megismerés

mi^crāǧ: égi utazás

i^ctibār: példázat

iǧmā^c: közmegegyezés