Proof-theoretic investigations into the Friedman-Sheard theories and other theories of truth
Proof-theoretic investigations into the Friedman-Sheard theories and other theories of truth
复制标题
对弗里德曼-谢尔德理论和其他真理理论的证明理论研究
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Graham Emil Leigh
中科院分区：
文献类型：
--
作者：
Graham Emil Leigh
本文是关于公理真理理论的分析。在[FS 87]中，弗里德曼和谢尔德定义了九种真理理论。每一个理论都通过十二个真值原则的集合的最大相容子集（称为可选公理）来扩展弱基真值理论。九个理论中的两个的证明理论强度已经由Cantini [Can 90]和Halbach [Hal 94]确定。我们确定的证据理论的力量，其余的七个弗里德曼-谢尔德理论，以及他们的许多子理论产生一些可能令人惊讶的结果。这些理论的分析利用无穷证明理论的技术，如削减消除和良序证明。我们证明了这七个理论的范围从PA的保守扩展到依赖选择的强度。此外，我们表明，大多数集的可选公理没有真量词公理形成保守的PA扩展时，添加到基础理论，并突出了特定的作用，一些可选公理在确定证明理论的强度。然后，我们重铸弗里德曼和谢尔德的计划在一个纯粹的直觉设置，定义一个直观的基础理论免除经典逻辑和经典的真理谓词和分类的所有子集的可选公理，无论是一致的或不一致的新的基础理论。作为
This thesis is concerned with the analysis of theories of axiomatic truth. In [FS87], Friedman and Sheard define nine theories of truth. Each theory extends a weak base theory of truth by a maximal consistent subset of a collection of twelve principles of truth (referred to as Optional Axioms). The proof-theoretic strength of two of the nine theories has been determined by Cantini [Can90] and Halbach [Hal94]. We ascertain the proof-theoretic strength of the remaining seven Friedman-Sheard theories as well as many of their sub-theories yielding some possibly surprising results. The analysis of these theories utilises techniques of infinitary proof theory such as cut elimination and well-ordering proofs. We prove that the seven theories range from a conservative extension of PA to the strength of Σ1 dependent choice. Moreover, we show that most sets of Optional Axioms without the truthquantifier axioms form conservative extensions of PA when added to the base theory, and highlight the specific role some Optional Axioms play in determining the proof-theoretic strength. We then recast Friedman and Sheard’s programme in a purely intuitionistic setting, defining an intuitionistic base theory dispensing with both classical logic and a classical truth predicate and classifying all subsets of the Optional Axioms as either consistent or inconsistent over the new base theory. As a