Kaplan and Montague have showed that certain intuitive axioms for a first-order theory of knowledge, formalized as a predicate, are jointly inconsistent. Their arguments rely on self-referential formulas. I offer a consistent first-order theory solving these knower paradoxes, with the following main features: - It solves the knower paradoxes by providing a faithful formalization of the principle of veracity (that knowledge requires truth), using both a knowledge and a truth predicate. - It is genuinely untyped. I.e. it is untyped not only in the sense that it uses a single knowledge predicate applying to all sentences in the language (including sentences in which this predicate occurs), but in the sense that its axioms quantify over all sentences in the language, thus supporting comprehensive reasoning with untyped knowledge ascriptions. - Common knowledge predicates can be defined in the system using self-reference. This fact, together with the genuinely untyped nature of the system and a technique based on L\"ob's theorem, enables it to support comprehensive reasoning with untyped common knowledge ascriptions (without having any axiom directly addressing common knowledge).
翻译:一个完全无类型的解决知者悖论的方案
翻译后的摘要:
Kaplan和Montague已经展示了一个一阶知识理论的某些直观公理是相互不一致的。其论据依赖于自指公式。作者提供了一个一致的一阶理论来解决这些知者悖论,其主要特点如下:- 它通过提供一个忠实的真实性原则的形式化证明来解决知者悖论(即,知识需要真实性),使用了知识和真理谓词。- 它是完全无类型的,不仅在使用单个适用于语言中所有句子(包括这个谓词出现的句子)的知识谓词的意义上,而且在其公理中量化了语言中的所有句子,从而支持涵盖了无类型知识归属的全面推理。- 通用的知识谓词可以使用自引用在系统中进行定义。这一事实,加上系统的完全无类型性和一个基于Löb定理的技巧,使得它能够支持对无类型共知归属的全面推理(而不必有任何明确涉及共知的公理)。