In Kripke’s theory of truth,the largest intrinsic fixed point—like the least fixed point—is of special theoretical interest among all fixed points.However,for intrinsic yet ungrounded sentences(i.e.,those belonging...In Kripke’s theory of truth,the largest intrinsic fixed point—like the least fixed point—is of special theoretical interest among all fixed points.However,for intrinsic yet ungrounded sentences(i.e.,those belonging to the largest intrinsic fixed points but not to the least fixed point),only sporadic examples have been provided so far,and a universal criterion for deciding such sentences remains unknown.This paper aims to establish a general criterion for determining intrinsic truth in Boolean systems of self-referential sentences under Kleene’s strong valuation scheme.To achieve this,we first present a known result about the definability of three-valued functions within Kleene’s strong logic.Then,by reducing the problem of determining the fixed points to a calculation problem in propositional logic,we demonstrate a truth-functional characteristic for the intrinsic truths in Boolean systems.We thus find an effective method for constructing intrinsic truths in a first-order language for Peano arithmetic.We also discuss the applicability of our findings to Kleene’s weak valuation scheme.展开更多
According to Kripke, traditional approaches to presupposition and anaphora do not work in some compound sentences because traditionally, they have been thought to assign presuppositions to each clause in isolation. I ...According to Kripke, traditional approaches to presupposition and anaphora do not work in some compound sentences because traditionally, they have been thought to assign presuppositions to each clause in isolation. I agree with this criticism, but also think that context is required in order to determine the presupposition included in a complex sentence. To show the context role in fixing the utterance truth-conditions in those cases, this paper introduces the Kripkean anaphoric account on presuppositions （section 2）, and then criticizes this approach because it is very restrictive （section 3）. The paper concludes that to solve those difficulties, one should appeal to a two-dimensional framework, including a new parameter that focuses on the sentence according to the concrete features of the context： the speaker＇s point of view （section 4）.展开更多
This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of s...This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of state explosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Kripke structure, and a 3 valued fair CTL(Computation Tree Logic) semantics correspondingly. It defines a fair preorder between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a pertinent theorem is also given, which indicates the relationship between the partial state spaces and the more complete one by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae.展开更多
The aim of this paper is to defend Searle＇s view on the semantic role that descriptions associated with proper names play in real contexts. Through an analysis of Kripke＇s critique of Searle＇s views, I reach the co...The aim of this paper is to defend Searle＇s view on the semantic role that descriptions associated with proper names play in real contexts. Through an analysis of Kripke＇s critique of Searle＇s views, I reach the conclusion that Kripke;s criticism is based upon a misinterpretation of Searle＇s ideas. Searle tried to answer the question ＂what is the object named as such？＂ That is different from the question that Kripke attributed to the descriptivists, i.e. ＂what are the necessary criteria to identify the referent of a name in every possible world？＂ I think Searle＇s question is also a question that Kripke＇s Causal Theory of Names has to answer, i.e. how a name transmits through a linguistic community.展开更多
This paper aims to examine the general issue of how reference is possible in philosophy of language through a case analysis of the ＂double reference＂ semantic-syntactic structure of ideographic hexagram （guaxiang ...This paper aims to examine the general issue of how reference is possible in philosophy of language through a case analysis of the ＂double reference＂ semantic-syntactic structure of ideographic hexagram （guaxiang 卦象） names in the Yijing text. I regard the case of the ＂hexagram＂ names as being quite representative of the ＂double-reference＂ semantic-syntactic structure of referring names. I thus explore how the general morals drawn from this account of ＂hexagram＂ names can engage two representative approaches, the Fregean and Kripkean ones, and contribute to our understanding and treatment of the issue of reference.展开更多
This article extends the foundational work of Wang and Wang on modal logic over lattices.Building upon their framework using polyadic modal logic with binary modalities<sup>and<inf>under standard Kripke se...This article extends the foundational work of Wang and Wang on modal logic over lattices.Building upon their framework using polyadic modal logic with binary modalities<sup>and<inf>under standard Kripke semantics to axiomatize lattice structures,we focus on the modal characterization of bounded lattices and their extensions relevant to logical systems.By introducing nullary modalities 1(maximum element)and 0(minimum element),we first establish a modal axiomatic system for bounded lattices.Subsequently,we provide pure formula characterizations of complementation and orthocomplementation relations in lattices,along with corresponding completeness results.As key applications,we present modal characterizations of fundamental logical algebraic structures:Boolean algebras,orthomodular lattices,and Heyting algebras.The last section develops novel axiomatization results for atomic lattices and atomless lattices.Throughout this work,all axiomatic systems are shown to be strongly complete via pureformula extensions,demonstrating how hybrid modal languages with nullary operators can uniformly capture boundary elements,complementation properties,and latticetheoretic operations central to both classical and nonclassical logics.展开更多
模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状...模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(State/Event Linear Temporal Logic,SE-LTL)给出了一种简洁和直接的方式表达包含状态和事件的系统属性.在SE-LTL中,状态和事件都可以作为原子命题.基于自动机理论的线性时序逻辑(Linear Temporal Logic,LTL)模型检验可以被用来对SE-LTL属性进行验证.然而SE-LTL属性在经典的stutter等价(stutter-equivalent)下无法保持,所以最有效的并发程序状态约简技术:偏序约简技术(Partial Order Reduction,POR)不能直接应用于SE-LTL的验证.该文提出一种新的方法利用已有的偏序约简技术对SE-LTL验证过程的状态空间进行约简.该方法分为两个部分:第一个部分是针对SE-LTL不带NEXT算子的约简方法;第二部分则是带NEXT算子的约简方法.第一部分的主要思想是从一个Büchi自动机(Automata,BA)中抽取出“状态部分”.“状态部分”的含义是该部分只与系统的状态相关.基于“状态部分”,给出关于BA和标签Kripke结构(Labeled Kripke Structure)的同步乘,并在同步乘的构造过程中嵌入偏序约简技术,从而约简同步乘的状态空间,即该文的约简技术是on-the-fly的.嵌入的偏序约简在已有的偏序约简基础上,面向SE-LTL公式中的事件引入新的可见操作的识别方法.为了能够将偏序约简技术应用到所有的SE-LTL公式,该文同时给出验证SE-LTL带NEXT算子的偏序约简算法.NEXT算子是偏序约简的另一个主要障碍.该部分是文中的第二部分工作.该部分的技术依然是on-the-fly的,并且需要与状态部分的识别相结合.通过将该文技术实现到SPIN模型检验器中对已有的模型进行验证.Spin是针对LTL的并发程序模型检验器.实现部分包括SE-LTL到BA的转化,以及on-the-fly的模型验证过程.实验的过程主要针对三个模型集:生产消费者模型,哲学家就餐问题以及公共对象请求代理体系结构中的GIOP协议.验证结果表明,对比完全基于状态的模型检验和不带偏序约简的状态事件模型检验,该文的方法具有更好的效率,并且能够被应用于状态事件系统,特别是安全有关嵌入式系统的验证.展开更多
基金supported by National Social Science Foundation of China,“A Truth-theoretical Study on Limits of Artificial Intelligence”(No.24AZX018)Major Interdisciplinary Cultivation Project of Philosophy and Social Sciences at South China Normal University,“Research on Frontier Issues in Epistemic Logic in Analytic Philosophy.”。
文摘In Kripke’s theory of truth,the largest intrinsic fixed point—like the least fixed point—is of special theoretical interest among all fixed points.However,for intrinsic yet ungrounded sentences(i.e.,those belonging to the largest intrinsic fixed points but not to the least fixed point),only sporadic examples have been provided so far,and a universal criterion for deciding such sentences remains unknown.This paper aims to establish a general criterion for determining intrinsic truth in Boolean systems of self-referential sentences under Kleene’s strong valuation scheme.To achieve this,we first present a known result about the definability of three-valued functions within Kleene’s strong logic.Then,by reducing the problem of determining the fixed points to a calculation problem in propositional logic,we demonstrate a truth-functional characteristic for the intrinsic truths in Boolean systems.We thus find an effective method for constructing intrinsic truths in a first-order language for Peano arithmetic.We also discuss the applicability of our findings to Kleene’s weak valuation scheme.
文摘According to Kripke, traditional approaches to presupposition and anaphora do not work in some compound sentences because traditionally, they have been thought to assign presuppositions to each clause in isolation. I agree with this criticism, but also think that context is required in order to determine the presupposition included in a complex sentence. To show the context role in fixing the utterance truth-conditions in those cases, this paper introduces the Kripkean anaphoric account on presuppositions （section 2）, and then criticizes this approach because it is very restrictive （section 3）. The paper concludes that to solve those difficulties, one should appeal to a two-dimensional framework, including a new parameter that focuses on the sentence according to the concrete features of the context： the speaker＇s point of view （section 4）.
基金National Natural Science Foundation of China( No.60 173 10 3 )
文摘This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of state explosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Kripke structure, and a 3 valued fair CTL(Computation Tree Logic) semantics correspondingly. It defines a fair preorder between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a pertinent theorem is also given, which indicates the relationship between the partial state spaces and the more complete one by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae.
文摘The aim of this paper is to defend Searle＇s view on the semantic role that descriptions associated with proper names play in real contexts. Through an analysis of Kripke＇s critique of Searle＇s views, I reach the conclusion that Kripke;s criticism is based upon a misinterpretation of Searle＇s ideas. Searle tried to answer the question ＂what is the object named as such？＂ That is different from the question that Kripke attributed to the descriptivists, i.e. ＂what are the necessary criteria to identify the referent of a name in every possible world？＂ I think Searle＇s question is also a question that Kripke＇s Causal Theory of Names has to answer, i.e. how a name transmits through a linguistic community.
文摘This paper aims to examine the general issue of how reference is possible in philosophy of language through a case analysis of the ＂double reference＂ semantic-syntactic structure of ideographic hexagram （guaxiang 卦象） names in the Yijing text. I regard the case of the ＂hexagram＂ names as being quite representative of the ＂double-reference＂ semantic-syntactic structure of referring names. I thus explore how the general morals drawn from this account of ＂hexagram＂ names can engage two representative approaches, the Fregean and Kripkean ones, and contribute to our understanding and treatment of the issue of reference.
基金supported by China Postdoctoral Science Foundation(2024M750225).
文摘This article extends the foundational work of Wang and Wang on modal logic over lattices.Building upon their framework using polyadic modal logic with binary modalities<sup>and<inf>under standard Kripke semantics to axiomatize lattice structures,we focus on the modal characterization of bounded lattices and their extensions relevant to logical systems.By introducing nullary modalities 1(maximum element)and 0(minimum element),we first establish a modal axiomatic system for bounded lattices.Subsequently,we provide pure formula characterizations of complementation and orthocomplementation relations in lattices,along with corresponding completeness results.As key applications,we present modal characterizations of fundamental logical algebraic structures:Boolean algebras,orthomodular lattices,and Heyting algebras.The last section develops novel axiomatization results for atomic lattices and atomless lattices.Throughout this work,all axiomatic systems are shown to be strongly complete via pureformula extensions,demonstrating how hybrid modal languages with nullary operators can uniformly capture boundary elements,complementation properties,and latticetheoretic operations central to both classical and nonclassical logics.
文摘模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(State/Event Linear Temporal Logic,SE-LTL)给出了一种简洁和直接的方式表达包含状态和事件的系统属性.在SE-LTL中,状态和事件都可以作为原子命题.基于自动机理论的线性时序逻辑(Linear Temporal Logic,LTL)模型检验可以被用来对SE-LTL属性进行验证.然而SE-LTL属性在经典的stutter等价(stutter-equivalent)下无法保持,所以最有效的并发程序状态约简技术:偏序约简技术(Partial Order Reduction,POR)不能直接应用于SE-LTL的验证.该文提出一种新的方法利用已有的偏序约简技术对SE-LTL验证过程的状态空间进行约简.该方法分为两个部分:第一个部分是针对SE-LTL不带NEXT算子的约简方法;第二部分则是带NEXT算子的约简方法.第一部分的主要思想是从一个Büchi自动机(Automata,BA)中抽取出“状态部分”.“状态部分”的含义是该部分只与系统的状态相关.基于“状态部分”,给出关于BA和标签Kripke结构(Labeled Kripke Structure)的同步乘,并在同步乘的构造过程中嵌入偏序约简技术,从而约简同步乘的状态空间,即该文的约简技术是on-the-fly的.嵌入的偏序约简在已有的偏序约简基础上,面向SE-LTL公式中的事件引入新的可见操作的识别方法.为了能够将偏序约简技术应用到所有的SE-LTL公式,该文同时给出验证SE-LTL带NEXT算子的偏序约简算法.NEXT算子是偏序约简的另一个主要障碍.该部分是文中的第二部分工作.该部分的技术依然是on-the-fly的,并且需要与状态部分的识别相结合.通过将该文技术实现到SPIN模型检验器中对已有的模型进行验证.Spin是针对LTL的并发程序模型检验器.实现部分包括SE-LTL到BA的转化,以及on-the-fly的模型验证过程.实验的过程主要针对三个模型集:生产消费者模型,哲学家就餐问题以及公共对象请求代理体系结构中的GIOP协议.验证结果表明,对比完全基于状态的模型检验和不带偏序约简的状态事件模型检验,该文的方法具有更好的效率,并且能够被应用于状态事件系统,特别是安全有关嵌入式系统的验证.
