一种真正无类型的认知者悖论解决方案
A genuinely untyped solution to the knower paradoxes
AI总结：
本文提出一个一致的真正无类型一阶知识理论，通过知识谓词与真谓词形式化真实性原则以解决认知者悖论，并借助自指和Löb定理支持公共知识推理。
摘要：
Kaplan和Montague已经表明，对于将知识形式化为谓词的一阶知识理论而言，某些直观公理放在一起是不一致的。他们的论证依赖于自指公式。我提出了一个一致的一阶理论来解决这些认知者悖论，其主要特征如下：\n- 它通过同时使用知识谓词和真谓词，对真实性原则（即知识要求真）给出忠实的形式化，从而解决认知者悖论。\n- 它是真正无类型的。也就是说，它的无类型不仅意味着使用一个适用于语言中所有句子（包括出现该谓词的句子）的单一知识谓词，还意味着其公理对语言中的所有句子进行量化，从而支持关于无类型知识归属的全面推理。\n- 公共知识谓词可以在该系统中利用自指来定义。这一事实，连同该系统真正无类型的性质以及一种基于Löb定理的技术，使其能够支持关于无类型公共知识归属的全面推理（而无需任何直接处理公共知识的公理）。
英文摘要：
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öb's theorem, enables it to support comprehensive reasoning with untyped common knowledge ascriptions (without having any axiom directly addressing common knowledge).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
