Not all Kripke models of HA are locally PA

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F22%3A00553323" target="_blank" >RIV/67985840:_____/22:00553323 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/00216208:11320/22:10456572

Výsledek na webu

<a href="https://doi.org/10.1016/j.aim.2021.108126" target="_blank" >https://doi.org/10.1016/j.aim.2021.108126</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.aim.2021.108126" target="_blank" >10.1016/j.aim.2021.108126</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Not all Kripke models of HA are locally PA

Popis výsledku v původním jazyce

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, Mk 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, Mk⊨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⊩HA+ECT0 (ECT0 stands for Extended Church Thesis). The characterization says that for every arithmetical structure M, there exists a rooted Kripke model K⊩HA+ECT0 with the root r such that Mr=M iff M⊨ThΠ(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 Mr⊭IΔ1 and hence K is not even locally 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 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⊩T with the root r such that Mr=M. As applications of this sufficient condition, we construct two new Kripke models. The first one is a Kripke model K⊩HA+¬θ+MP (θ is an instance of ECT0 and MP is Markov's principle) which is not locally IΔ1. The second one is a Kripke model K⊩HA such that K forces exactly the sentences that are provable from HA, but it is not locally IΔ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Δ1.

Název v anglickém jazyce

Not all Kripke models of HA are locally PA

Popis výsledku anglicky

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, Mk 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, Mk⊨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⊩HA+ECT0 (ECT0 stands for Extended Church Thesis). The characterization says that for every arithmetical structure M, there exists a rooted Kripke model K⊩HA+ECT0 with the root r such that Mr=M iff M⊨ThΠ(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 Mr⊭IΔ1 and hence K is not even locally 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 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⊩T with the root r such that Mr=M. As applications of this sufficient condition, we construct two new Kripke models. The first one is a Kripke model K⊩HA+¬θ+MP (θ is an instance of ECT0 and MP is Markov's principle) which is not locally IΔ1. The second one is a Kripke model K⊩HA such that K forces exactly the sentences that are provable from HA, but it is not locally IΔ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Δ1.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

<a href="/cs/project/GX19-27871X" target="_blank" >GX19-27871X: Efektivní aproximační algoritmy a obvodová složitost</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Advances in Mathematics

ISSN

0001-8708

e-ISSN

1090-2082

Svazek periodika

397

Číslo periodika v rámci svazku

March

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

22

Strana od-do

108126

Kód UT WoS článku

000793112500025

EID výsledku v databázi Scopus

2-s2.0-85120862006