4.6 Article

Not all Kripke models of HA are locally PA

期刊

ADVANCES IN MATHEMATICS
卷 397, 期 -, 页码 -

出版社

ACADEMIC PRESS INC ELSEVIER SCIENCE
DOI: 10.1016/j.aim.2021.108126

关键词

Heyting Arithmetic; Peano Arithmetic; Kripke models; Local models; PA-normal; Realizability

资金

  1. GACR [19-27871X]
  2. [RVO: 67985840]
  3. [SVV-2020-260589]

向作者/读者索取更多资源

This paper focuses on the local properties of Kripke models of Heyting Arithmetic. By introducing two new Kripke model construction methods, the question of whether every Kripke model is locally PA is answered negatively, and several related results and applications are obtained.
Let K be an arbitrary Kripke model of Heyting Arithmetic, HA. For every node k in K, we can view the classical structure of k, M-k as a model of some classical theory of arithmetic. Let T be a classical theory in the language of arithmetic. We say K is locally T, iff for every k in K, M-k |= T. One of the most important problems in the model theory of HA is the following question: Is every Kripke model of HA locally PA? We answer this question negatively. We introduce two new Kripke model constructions to this end. The first construction actually characterizes the arithmetical structures that can be the root of a Kripke model K IF HA + ECT0 (ECT0 stands for Extended Church Thesis). The characterization says that for every arithmetical structure sic, there exists a rooted Kripke model K IF HA + ECT0 with the root r such that M-r = M M |= Th-Pi 2 (PA). One of the consequences of this characterization is that there is a rooted Kripke model K HA + ECT0 with the root r such that sic(r) |&NOTEQUexpressionL;& nbsp;I delta(1) and hence K is not even locally I delta(1). The second Kripke model construction is an implicit way of doing the first construction which works for any reasonable consistent intuitionistic arithmetical theory T with a recursively enumerable set of axioms that has the existence property. We get a sufficient condition from this construction that describes when for an arithmetical structure M, there exists a rooted Kripke model K ?& nbsp;T with the root r such that M-r = M. As applications of this sufficient condition, we construct two new Kripke models. The first one is a Kripke model K ?HA + theta + MP (theta is an instance of ECT0 & nbsp;and MP is Markov's principle) which is not locally I delta(1). The second one is a Kripke model K ?& nbsp;HA such that K forces exactly the sentences that are provable from HA, but it is not locally I delta(1). Also, we will prove that every countable Kripke model of intuitionistic first-order logic can be transformed into another Kripke model with the full infinite binary tree as the Kripke frame such that both Kripke models force the same sentences. So with the previous result, there is a binary Kripke model K of HA such that K is not locally I delta(1). (C)& nbsp;2021 Elsevier Inc. All rights reserved.

作者

我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。

评论

主要评分

4.6
评分不足

次要评分

新颖性
-
重要性
-
科学严谨性
-
评价这篇论文

推荐

暂无数据
暂无数据