论文标题
并非所有$ \ sf ha $的kripke型号都是本地$ \ sf pa $
Not all Kripke models of $\sf HA$ are locally $\sf PA$
论文作者
论文摘要
令$ {\ bf k} $为hyting算术的任意kripke模型，$ {\ sf ha} $。对于$ {\ bf k} $中的每个节点$ k $，我们可以将$ k $，$ {\ mathfrak m} _k $的经典结构视为某种算术理论的模型。让$ {\ sf t} $成为算术语言的经典理论。我们说$ {\ bf k} $是本地$ {\ sf t} $，iff in $ {\ bf k} $中的每个$ k $，$ {\ mathfrak m} _k \ models {\ sf t} $。 $ {\ sf ha} $的模型理论中最重要的问题之一是以下问题：{\是$ {\ sf ha} $的每个kripke模型本地$ {\ sf pa} $？}我们对此问题负面回答。我们将两个新的Kripke模型构造引入了这一目标。第一个结构实际上表征了算术结构，这些结构可能是kripke模型$ {\ bf k} \ vdash {\ sf ha}+{\ sf ect_0} $（$ {\ sf ect_0} $ for Extended Churchsisss）。表征表明，对于每个算术结构$ {\ Mathfrak m} $，存在一个生根的kripke型号$ {\ bf k} \ vdash {\ sf ha}+{\ sf ha}+{\ sf ect_0} $，带有$ r $ m} \ models {\ bf th} _ {π_2}（{\ sf pa}）$。这种表征的后果之一是，有一个生根的kripke $ {\ bf k} \ vdash {\ sf ha}+{\ sf iect_0} $带有root $ r $本地$ {\ bf i}Δ_1$。第二个Kripke模型构建是进行第一个构造的隐含方式，该构造适用于任何合理的一致直觉算术理论$ {\ sf t} $，并具有一组具有存在属性的公理集。我们从这种结构中获得了足够的条件，该结构描述了何时为算术结构$ {\ mathfrak m} $，存在一个生根的kripke型号$ {\ bf k} \ vdash {\ vdash {\ sf t} $ at loot $ r $
Let ${\bf K}$ be an arbitrary Kripke model of Heyting Arithmetic, ${\sf HA}$. For every node $k$ in ${\bf K}$, we can view the classical structure of $k$, ${\mathfrak M}_k$ as a model of some classical theory of arithmetic. Let ${\sf T}$ be a classical theory in the language of arithmetic. We say ${\bf K}$ is locally ${\sf T}$, iff for every $k$ in ${\bf K}$, ${\mathfrak M}_k\models{\sf T}$. One of the most important problems in the model theory of ${\sf HA}$ is the following question: {\it Is every Kripke model of ${\sf HA}$ locally ${\sf 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 ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ (${\sf ECT_0}$ stands for Extended Church Thesis). The characterization says that for every arithmetical structure ${\mathfrak M}$, there exists a rooted Kripke model ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ with the root $r$ such that ${\mathfrak M}_r={\mathfrak M}$ iff ${\mathfrak M}\models{\bf Th}_{Π_2}({\sf PA})$. One of the consequences of this characterization is that there is a rooted Kripke model ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ with the root $r$ such that ${\mathfrak M}_r\not\models{\bf I}Δ_1$ and hence ${\bf K}$ is not even locally ${\bf I}Δ_1$. The second Kripke model construction is an implicit way of doing the first construction which works for any reasonable consistent intuitionistic arithmetical theory ${\sf 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 ${\mathfrak M}$, there exists a rooted Kripke model ${\bf K}\Vdash {\sf T}$ with the root $r$ such that ${\mathfrak M}_r={\mathfrak M}$.
