kripke语义(也叫做关系语义或框架语义，并经常混淆于可能世界语义)是模态逻辑系统的形式语义，于1950年代晚期和1960年代早期由saulkripke建立。它后来为另一个非经典逻辑，最重要的直觉逻辑所接受。kripke语义的发现是非经典逻辑开发中重大突破，因为这种逻辑的模型论在kripke之前实际上是不存在的。
模态逻辑的语义
对于我们的目的，模态逻辑的语言由命题变量，读者喜欢的布尔连结词的完备集合(比如{→,¬}或{∨,∧,¬})，和模态算子<math>\box</math>(“必然性”)构成。对偶的模态算子<math>\diamond</math>(“可能性”)定义为一个简写:<math>\diamonda:=\neg\box\nega</math>。更多背景请参见模态逻辑。
基本定义
kripke框架或模态框架是<w,r>对，这里的w是非空集合，r是在w上的二元关系。w的元素叫做节点或世界，而r叫做可及关系。
kripke模型是<w,r,<math>\vdash</math>>三元组，这里的<w,r>是kripke框架，而<math>\vdash</math>是在w的节点和模态公式之间的如下关系:
<math>w\vdash\nega</math>当且仅当<math>w\not\vdasha</math>，
<math>w\vdasha\tob</math>当且仅当<math>w\not\vdasha</math>或<math>w\vdashb</math>，
<math>w\vdash\boxa</math>当且仅当<math>\forallu\,(w\;r\;u\rightarrowu\vdasha)</math>。
我们把w<math>\vdash</math>a读做“w满足a”，“a满足于w”，或“w力迫a”。关系<math>\vdash</math>叫做“满足关系”、“求值关系”或“力迫关系”。注意满足关系由它在命题变量上的值唯一确定。
公式a在下列之中是有效的:
模型<w,r,<math>\vdash</math>>，如果对于所有w∈w有w<math>\vdash</math>a，
框架<w,r>，如果对于<math>\vdash</math>的所有可能的选择，它在<w,r,<math>\vdash</math>>中是有效的，
框架或模型的类c，如果它在c的每个成员中都是有效的。
我们定义thm(c)为在c中有效的所有公式的集合。反过来说，如果x是公式的集合，则设mod(x)是使来自x的所有公式有效的所有框架的类。
一个模态逻辑(就是说一个公式的集合)l关于框架的类c是可靠的，如果l⊆thm(c)。l关于c是完备的，如果l⊇thm(c)。
对应性和完备性
语义对于逻辑(就是推理系统)研究是有用的，条件是在语义蕴涵关系忠实的反映语法对应物--推论关系(可推导性)。所以知道哪个模态逻辑关于哪类kripke框架是可靠的和完备的，并为它们确定这种类是关键性的。
对于kripke框架的任何类c，thm(c)是正规模态逻辑；特别是，最小化正规模态逻辑k的定理，在所有kripke模型中都是有效的。不幸的是，逆命题不是一般性成立的:有kripke不完备的正规模态逻辑。事实上这不是问题，因为实际中研究的多数模态系统关于由简单条件所描述的框架类是完备的。
正规模态逻辑l对应于框架类c，条件是c=mod(l)。换句话说，c是l关于c是可靠的最大的框架类；随后l是kripke完备的当且仅当它关于它所对应的类是完备的。
作为一个例子，考虑模式t:<math>\box</math>a→a。t在任何自反的框架<w,r>中是有效的:如果w<math>\vdash\box</math>a，则w<math>\vdash</math>a，因为wrw。在另一方面，使t有效的框架必须是自反的:固定w∈w，并定义命题变量p的满足为如下:u<math>\vdash</math>p当且仅当wru。那么w<math>\vdash\box</math>p，所以w<math>\vdash</math>p于t，这意味着wrw使用了<math>\vdash</math>的定义。我们见到t对应于自反的kripke框架的类。
特征化l的对应类经常比证明它的完备性要容易许多，所以对应性充当完备性证明的指导。对应性还用于证实模态逻辑的不完备性:假定l1⊆l2是对应于同一个框架类的正规模态逻辑，l1不证明l2的所有定理。那么l1是kripke不完备的。例如，模式<math>\box(a\equiv\boxa)\to\boxa</math>生成一个不完备的逻辑，因为它对应于同gl一样的框架类(viz.传递性和逆良基的框架)，但是它不证明<math>\boxa\to\box\boxa</math>。
规范模型
对于任何正规模态逻辑l，我们可以构造一个kripke模型(称为规范模型)，它且只有它使l的定理有效，通过接纳使用极大一致集合作为模型的标准技术。规范kripke模型扮演的角色类似于在代数语义中的lindenbaum╟tarski代数构造。
公式集合l是一致的，如果从它们、l的公理和肯定前件中不能推导出矛盾。极大l一致的集合(简写为l-mcs)是没有真l一致的超集的l一致的集合。
l的规范模型是kripke模型<w,r,<math>\vdash</math>>，这里的w是所有l-mcs，而关系r和<math>\vdash</math>为如下:
<math>x\;r\;y</math>当且仅当对所有的公式<math>a</math>，如果<math>\boxa\inx</math>则<math>a\iny</math>，
<math>x\vdasha</math>当且仅当<math>a\inx</math>。
规范模型是l的模型，因为所有的l-mcs包含l的所有定理。通过zorn引理，每个l一致的集合都包含在一个l-mcs中，特别是在l中不可证明的所有公式都在规范模型中有一个反例。
规范模型的主要应用是完备性证明。例如，k的规范模型的性质直接蕴含k关于所有kripke框架类的完备性。这个论证不适合任意的l，因为没有对规范模型的底层框架满足l的框架条件的担保。
我们说一个公式或公式的集合x关于kripke的一个性质p是规范的，如果
x在满足p的所有框架中是有效的，
对于包含x的任何正规模态逻辑l，l的规范模型底层框架满足p。
明显的，公式的规范集合的并集自身是规范的。服从前面的讨论，由公式的规范集合公理化的任何逻辑是kripke完备的和紧凑的。
公理t、4、d、b、5、h、g(和它们的任意组合)都是规范的。gl和grz不是规范的，因为他们不是紧凑的。公理m自身不是规范的(goldblatt,1991)，但是组合的逻辑s4.1(事实上甚至k4.1)是规范的。
一般的，给定的公理是否是规范的是不可判定的。不过我们知道一个好的充分条件:h。sahlqvist识别了如下广泛的一类公式(现在叫做sahlqvist公式)
sahlqvist公式是规范的，
对应于sahlqvist公式的框架类是一阶可定义的，
有计算对一个给定的sahlqvist公式的对应框架条件的算法。
这是一个非常强力的准则；例如，上面列出的规范的所有公理是实际上的(等价于)sahlqvist公式。
有限模型性质
逻辑拥有有限模型性质(fmp)，如果它关于有限框架的类是完备的。这个概念的主要应用之一是可判定性问题:它服从post定理，有fmp的递归公理化的模态逻辑l是可判定的，倘若给定的有限框架是否是l的模型是可判定的。特别是，有fmp的所有的有限可公理化的逻辑都是可判定的。
有各种方法为给定的逻辑建立fmp。精练并扩展规范模型构造通常就行了，使用工具如过滤或拆分。还有一种可能性，给予免切的相继式演算的完备性证明通常直接产生有限模型。
多数实际上使用的模态系统(包括所有上面列出的)都有fmp。
在某些情况下，我们可以使用fmp来证明逻辑的kripke完备性:所有正规模态逻辑关于模态代数的类都是完备的，而有限的模态代数可以变换成kripke框架。作为例子，robertbull使用这个方法证明了s4.3的所有普通扩展都有fmp，并且是kripke完备的。
多模态逻辑
kripke语义对有多于一个模态的逻辑有直接的推广。带有<math>\{\box_i;\,i\ini\}</math>作为必然性算子的集合的语言的kripke框架，由对每个i∈i装备上二元关系ri一个非空集合w构成。满足关系的定义修改为如下:
<math>w\vdash\box_ia</math>当且仅当<math>\forallu\,(w\;r_i\;u\rightarrowu\vdasha)</math>。
由timcarlson发现的简化的语义，经常用于多模态可证明性逻辑。carlson模型是结构<w,r,i∈i,⊩>，带有一个单一的可及关系r，和给每个模态的子集di⊆w。满足性定义为
<math>w\vdash\box_ia</math>当且仅当<math>\forallu\ind_i\,(w\;r\;u\rightarrowu\vdasha)</math>。
carlson模型比通常的多模态kripke模型易于形象化和使用；但是，kripke完备的多模态逻辑是carlson不完备的。
直觉逻辑的语义
直觉逻辑的kripke语义服从和模态逻辑的语义同样的原理，但是它使用了满足的不同的定义。
直觉kripke模型是一个三元组<w,≤,<math>\vdash</math>>，这里的<w,≤>是传递的和自反的kripke框架(就是说可及关系是预序)，而<math>\vdash</math>满足下列条件:
如果p是命题变量，w≤u，而且w<math>\vdash</math>p，则u<math>\vdash</math>p(坚持条件)，
w<math>\vdash</math>a∧b当且仅当w<math>\vdash</math>a并且w<math>\vdash</math>b，
w<math>\vdash</math>a∨b当且仅当w<math>\vdash</math>a或者w<math>\vdash</math>b，
w<math>\vdash</math>a→b当且仅当对于所有u≥w，u<math>\vdash</math>a蕴含u<math>\vdash</math>b，
无w<math>\vdash</math>⊥。
直觉逻辑关于它的kripke语义是可靠的和完备的，并且它有fmp。
直觉一阶逻辑
设l是一阶语言。l的kripke模型是三元组<w,≤,w∈w>，这里的<w,≤>是直觉kripke框架，mw是每个节点w∈w的(经典)l-结构，而下列相容性条件只要在u≤v时都是成立的:
mu的域包含在mv的域中，
mu和mv中的函数符号实现一致于mu的元素，
对于每个n元谓词p和元素a1,...,an∈mu:如果p(a1,...,an)成立于mu，则它成立于mv。
给出经由mw的元素的变量求值e，我们定义满足关系w<math>\vdash</math>a[e]:
w<math>\vdash</math>p(t1,...,tn)[e]当且仅当'p(t1[e],...,tn[e])成立于mw，
w<math>\vdash</math>(a∧b)[e]当且仅当w<math>\vdash</math>a[e]并且w<math>\vdash</math>b[e]，
w<math>\vdash</math>(a∨b)[e]当且仅当w<math>\vdash</math>a[e]或者w<math>\vdash</math>b[e]，
w<math>\vdash</math>(a→b)[e]当且仅当对于所有的u≥w，u<math>\vdash</math>a[e]蕴含u<math>\vdash</math>b[e]，
无w<math>\vdash</math>⊥[e]，
w<math>\vdash</math>(∃xa)[e]当且仅当存在一个a∈mw，使得w<math>\vdash</math>a[e(x→a)]，
w<math>\vdash</math>(∀xa)[e]当且仅当对于所有的u≥w和所有的a∈mu，u<math>\vdash</math>a[e(x→a)]。
这里的e(x→a)是给予x值a的求值，在其他方面一致于e。
kripke-joyal语义
作为独立开发的层论的一部分，在1965年左右认识到kripke语义密切相关于在topos论中对存在量化的处理。就是对一个层的截面的存在性的'局部'示象是一种'可能性'的逻辑。因为这种开发是很多人的工作，比之于理论更合于概念上洞察的天性，归与荣誉不是很容易的。kripke-joyal语义这个名称经常用做这种联系。
模型构造
同在经典的模型论中一样，有从其他模型构造一个新的kripke模型的方法。
在kripke语义中天然的同态叫做p-态射(它是伪满射的简写，但这个术语很少用)。kripke框架<w,r>和<w’,r’>的p-态射是一个映射f:w→w’满足
f保留可及关系，就是说urv蕴涵f(u)r’f(v)，
在f(u)r’v’的时候，有一个v∈w使得f(v)=v’。
kripke模型<w,r,<math>\vdash</math>>和<w’,r’,<math>\vdash</math>’>的p-态射是它们的底层框架的p-态射f:w→w’，它满足
对于任何命题变量p，w<math>\vdash</math>p当且仅当f(w)<math>\vdash</math>’p。
p-态射是特殊种类的双仿(bisimulation)。一般的说，在框架<w,r>和<w’,r’>之间的双仿是关系b⊆w×w’，它满足下列“zig-zag”性质:
如果ubu’并且urv，则存在v’∈w’使得vbv’，
如果ubu’并且u’r’v’，则存在v∈w使得vbv’。
模型的双仿是对保持原子公式的力迫的补充要求:
对于任何命题变量p，如果wbw’，则w<math>\vdash</math>p当且仅当w’<math>\vdash</math>’p。
从这个定义我们得到的关键性质是模型的双仿(所以也是p-态射)保持所有公式的满足性，而不只是命题变量。
我可以使用拆分(unravelling)把kripke模型变换成树。给出一个模型<w,r,<math>\vdash</math>>和固定的节点w0∈w，我们定义一个模型<w’,r’,<math>\vdash</math>’>，这里的w’是所有有限序列s=<w0,w1,...,wn>的集合，使得对于所有i<n和s<math>\vdash</math>p，wirwi+1当且仅当对于所有变量p，wn<math>\vdash</math>p。定义可及关系r’变化；在最简单的情况下我们置
<w0,w1,...,wn>r’<w0,w1,...,wn,wn+1>,
但是很多应用需要这个关系的自反与/或传递闭包，或类似的变更。
过滤是p-态射的一个变种。设x是在采纳子公式(subformulas)下闭合的公式的集合。模型<w,r,<math>\vdash</math>>的x-过滤是从w到模型<w’,r’,<math>\vdash</math>’>的映射f，使得
f是满射，
f保持可及关系，和(在两个方向上)变量p∈x的满足性，
如果f(u)r’f(v)并且u<math>\vdash\box</math>a，这里的<math>\box</math>a∈x，则v<math>\vdash</math>a。
得到了f保持来自x的所有公式的满足性。在典型的应用中，我们把f采纳为在w在下列关系上对份额的投影
u≡xv当且仅当对于所有a∈x，u<math>\vdash</math>a当且仅当v<math>\vdash</math>a。
同在拆分的情况下一样，定义可及关系在份额变化上。
历史和术语
kripke语义不是kripke首创的，以上述方式给出的基于使求值相对于节点的语义早于kripke的工作许久:
carnap好像是首先有了这种想法，通过给予求值函数以莱布尼兹的可能世界为范围的一个参数的方式，对必然性和可能性的模态给出一种可能世界语义。bayart进一步发展了这种想法，但是他们都没能给出tarski介入的这种风格的满足的递归定义；
jónsson和tarski给出了仍然影响着当代模态逻辑研究的表达语义的方式，就是代数方法，这包含了kripke语义的很多关键想法。他们把这个想法应用于直觉逻辑的语义研究，但没有见到与模态逻辑的联系；
kanger对模态逻辑的释义给出了更加复杂的方式，但是包含了kripke方式的很多关键想法。他首先注意到在关于可及关系的条件和lewis-风格的模态逻辑公理之间的联系。但是kanger没能给出对他的系统的完备性证明；
jaakkohintikka在他的论文中介入了是kripke语义的简单变体的认识逻辑，等同于通过最大化一致集合的方式构造求值的塑造。他没能为认识逻辑给出推理规则，所以没能给出完备性证明；
richardmontague有了包含在kripke工作中的很多关键想法，但是他没有把它们当作是重要的，所以一直没有发表直到kripke的论文出版在逻辑学社区中造成了轰动之后；
evertw.beth为直觉逻辑提出了一种基于树的语义，它极其类似于kripke语义，除了使用了更加麻烦的满足定义之外。
尽管kripke语义的根本思想在kripke首次发表之前就广为流传了，saulkripke关于模态逻辑的工作仍可恰当的当作是开拓性的。最重要的是，kripke是第一个为模态逻辑证明了完备性定理的人，并且kripke识别了最弱的正规模态逻辑。
尽管kripke的工作有开创性贡献，很多模态逻辑学家反对术语kripke语义，因为这是对先驱们做的重要贡献的失礼。反对另一个最广泛使用的术语可能世界语义的理由是它不适合应用于不是可能性和必然性的模态，比如在认识或道义逻辑中。他们喜欢术语关系语义或框架语义。