Syntactic aspects of modal incompleteness theorems

Syntactic aspects of modal incompleteness theorems
复制标题

模态不完备性定理的句法方面

DOI:
10.1111/j.1755-2567.1979.tb00794.x
复制
发表时间:
2008
期刊:
影响因子:
--
通讯作者:
J. Benthem
J. Benthem
中科院分区:
--
文献类型:
--
作者:
J. Benthem

文献摘要

被引文献

相似文献

本文讨论命题模态逻辑。当需要时,将解释符号约定。模态公式使用命题字母(p,q,r,...)构建,布尔运算符(7:不,+:如果...那么... A:and,v:or,c*:if and only if)和一元模态运算符0(必然),0(可能)。实际上,将7、+和0作为原语就足够了,使用其他运算符的众所周知的可定义性。最小模态逻辑K有一组关于分离(肯定前件)和替换规则的命题公理(对于命题逻辑)。此外,它有模态公理U(p+ q)+(Op-+ Oq),以及模态规则“必然性”(从cp推断Ocp)。(请注意,K经常不使用替换规则而使用公理图式来公理化。)K中的扣除量可以定义如下。Z kKcp如果存在一个有限的模态公式序列,其末端为cp,使得序列中的每个公式或者属于C,或者是K的公理,或者通过应用某种推理规则从先前的公式中得出。一个框架是一个有序偶(W,R),它由一个集合W(所谓的“世界”)和W上的二元关系R(“可达性”)组成。帧将由8(=(W,R))表示。框架中模态公式的真值可以通过框架8上的赋值V来定义,该框架8将W的子集分配给命题字母。使用著名的Kripke真值定义,V可以以规范的方式提升到所有模态公式的集合。现在cp在8中为真(“$ k cp”),如果对于8上的所有估值V,V(cp)= W。下面的模态推论的概念
THIS PAPER is concerned with propositional modal logic. Notational conventions will be explained as the need for them arises. Modal formulas are constructed using proposition letters (p, q, r,...), Boolean operators (7: not,+: if... then..., A: and, v: or, c*: if and only if) and unary modal operators 0 (necessarily), 0 (possibly). It actually suffices to take 7,+ and 0 as primitives, using the well-known definability of the other operators. The minimal modal logic K has a set of propositional axioms complete (for propositional logic) with respect to the rules of detachment (modus ponens) and substitution. Moreover, it has the modal axiom U (p+ q)+(Op-+ Oq), as well as the modal rule of “necessitation”(to infer Ocp from cp).(Notice that, very often, K is axiomatized without using the rule of substitution, but with axiom schemata.) Deducibility in K may then be defined as follows. Z kKcp if a finite sequence of modal formulas exists with cp at its end, such that each formula in the sequence either belongs to C, or is an axiom of K, or follows from previous formulas by an application of some rule of inference.This notion of deducibility admits of a semantic characterization through the following concepts. A frame is an ordered couple (W, R) consisting of a set W (of so-called “worlds”) with a binary relation R on W (“accessibility”). Frames will be denoted by 8 (=(W, R)). Truth of modal formulas in frames is definable by the intermediary of a valuation V on such a frame 8 which assigns subsets of W to proposition letters. Using the well-known Kripke truth definition, V may be lifted to the set of all modal formulas in a canonical fashion. Now cp is true in 8 (“$ k cp”) if V (cp)= W for all valuations V on 8. The following notion of modal consequence then