PROVABILITY LOGICS RELATIVE TO A FIXED EXTENSION OF PEANO ARITHMETIC

2018 ◽  
Vol 83 (3) ◽  
pp. 1229-1246
Author(s):  
TAISHI KURAHASHI
Keyword(s):  
Peano Arithmetic ◽  
Provability Logic ◽  
Consistent Extension ◽  
Image Position ◽  
Computably Enumerable

AbstractLet T and U be any consistent theories of arithmetic. If T is computably enumerable, then the provability predicate $P{r_\tau }\left( x \right)$ of T is naturally obtained from each ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of T. The provability logic $P{L_\tau }\left( U \right)$ of τ relative to U is the set of all modal formulas which are provable in U under all arithmetical interpretations where □ is interpreted by $P{r_\tau }\left( x \right)$. It was proved by Beklemishev based on the previous studies by Artemov, Visser, and Japaridze that every $P{L_\tau }\left( U \right)$ coincides with one of the logics $G{L_\alpha }$, ${D_\beta }$, ${S_\beta }$, and $GL_\beta ^ -$, where α and β are subsets of ω and β is cofinite.We prove that if U is a computably enumerable consistent extension of Peano Arithmetic and L is one of $G{L_\alpha }$, ${D_\beta }$, ${S_\beta }$, and $GL_\beta ^ -$, where α is computably enumerable and β is cofinite, then there exists a ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of some extension of $I{{\rm{\Sigma }}_1}$ such that $P{L_\tau }\left( U \right)$ is exactly L.

Polynomially and superexponentially shorter proofs in fragments of arithmetic

1992 ◽  
Vol 57 (3) ◽  
pp. 844-863 ◽  
Author(s):  
Franco Montagna
Keyword(s):  
Fixed Points ◽  
Recursive Function ◽  
Peano Arithmetic ◽  
Modal Language ◽  
Primitive Recursive Function ◽  
Consistent Extension ◽  
Image Position ◽  
Primitive Recursive ◽  
Increasing Function

In Parikh [71] it is shown that, if T is an r.e. consistent extension of Peano arithmetic PA, then, for each primitive recursive function g, there is a formula φ of PA such that(In the following, Proof T(z, φ) and Prov T(φ) denote the metalinguistic assertions that z codes a proof of φ in T and that φ is provable in T respectively, where ProofT(z, ┌φ┐) and ProvT(┌φ┐) are the formalizations of Proof T(z,φ) and ProvT(φ) respectively in the language of PA, ┌φ┐ denotes the Gödel number of φ and ┌φ┐ denotes the corresponding numeral. Also, for typographical reasons, subscripts will not be made boldface.) If g is a rapidly increasing function, we express (1) by saying that ProvT(┌φ┐) has a much shorter proof modulo g than φ. Parikh's result is based on the fact that a suitable formula A(x), roughly asserting that (1) holds with x in place of φ, has only provable fixed points. In de Jongh and Montagna [89], this situation is generalized and investigated in a modal context. There, a characterization is given of arithmetical formulas arising from modal formulas of a suitable modal language which have only provable fixed points, and Parikh's result is obtained as a particular case.

Automorphism groups of arithmetically saturated models

2006 ◽  
Vol 71 (1) ◽  
pp. 203-216 ◽  
Author(s):  
Ermek S. Nurkhaidarov
Keyword(s):  
Automorphism Group ◽  
Automorphism Groups ◽  
Open Subgroup ◽  
Peano Arithmetic ◽  
Standard System ◽  
Permutation Groups ◽  
Saturated Model ◽  
Saturated Models ◽  
Homogeneous Set ◽  
Image Position

In this paper we study the automorphism groups of countable arithmetically saturated models of Peano Arithmetic. The automorphism groups of such structures form a rich class of permutation groups. When studying the automorphism group of a model, one is interested to what extent a model is recoverable from its automorphism group. Kossak-Schmerl [12] show that if M is a countable, arithmetically saturated model of Peano Arithmetic, then Aut(M) codes SSy(M). Using that result they prove:Let M1. M2 be countable arithmetically saturated models of Peano Arithmetic such that Aut(M1) ≅ Aut(M2). Then SSy(M1) = SSy(M2).We show that if M is a countable arithmetically saturated of Peano Arithmetic, then Aut(M) can recognize if some maximal open subgroup is a stabilizer of a nonstandard element, which is smaller than any nonstandard definable element. That fact is used to show the main theorem:Let M1, M2be countable arithmetically saturated models of Peano Arithmetic such that Aut(M1) ≅ Aut(M2). Then for every n < ωHere RT2n is Infinite Ramsey's Theorem stating that every 2-coloring of [ω]n has an infinite homogeneous set. Theorem 0.2 shows that for models of a false arithmetic the converse of Kossak-Schmerl Theorem 0.1 is not true. Using the results of Reverse Mathematics we obtain the following corollary:There exist four countable arithmetically saturated models of Peano Arithmetic such that they have the same standard system but their automorphism groups are pairwise non-isomorphic.

Solution of a problem of Tarski

1956 ◽  
Vol 21 (1) ◽  
pp. 49-51 ◽  
Author(s):  
John Myhill
Keyword(s):  
Unary Operation ◽  
Negative Answer ◽  
Operation Symbol ◽  
Counter Example ◽  
Recursively Enumerable ◽  
Consistent Extension ◽  
Axiomatizable Theory ◽  
Definition Of ◽  
Image Position ◽  
The Given

We presuppose the terminology of [1], and we give a negative answer to the following problem ([1], p. 19): Does every essentially undecidable axiomatizable theory have an essentially undecidable finitely axiomatizable subtheory?We use the following theorem of Kleene ([2], p. 311). There exist two recursively enumerable sets α and β such that (1) α and β are disjoint (2) there is no recursive set η for which α ⊂ η, β ⊂ η′. By the definition of recursive enumerability, there are recursive predicates Φ and Ψ for whichWe now specify a theory T which will afford a counter-example to the given problem of Tarski. The only non-logical constants of T are two binary predicates P and Q, one unary operation symbol S, and one individual constant 0. As in ([1], p. 52) we defineThe only non-logical axioms of T are the formulae P(Δm, Δn) for all pairs of integers m, n satisfying Δ(m, n); the formulae Q(Δm, Δn) for all pairs of integers m, n satisfying Ψ(m, n); and the formulaT is consistent, since it has a model. It remains to show that (1) every consistent extension of T is undecidable (2) if T1 is a finitely axiomatizable subtheory of T, there exists a consistent and decidable extension of T1 which has the same constants as T1.

scholarly journals ENAYAT MODELS OF PEANO ARITHMETIC

2018 ◽  
Vol 83 (04) ◽  
pp. 1501-1511 ◽  
Author(s):  
ATHAR ABDUL-QUADER
Keyword(s):  
Linear Order ◽  
Peano Arithmetic ◽  
Countable Model ◽  
Natural Question ◽  
Conservative Extension ◽  
Image Position ◽  
Definable Elements

AbstractSimpson [6] showed that every countable model ${\cal M} \models PA$ has an expansion $\left( {{\cal M},X} \right) \models P{A^{\rm{*}}}$ that is pointwise definable. A natural question is whether, in general, one can obtain expansions of a nonprime model in which the definable elements coincide with those of the underlying model. Enayat [1] showed that this is impossible by proving that there is ${\cal M} \models PA$ such that for each undefinable class X of ${\cal M}$, the expansion $\left( {{\cal M},X} \right)$ is pointwise definable. We call models with this property Enayat models. In this article, we study Enayat models and show that a model of $PA$ is Enayat if it is countable, has no proper cofinal submodels and is a conservative extension of all of its elementary cuts. We then show that, for any countable linear order γ, if there is a model ${\cal M}$ such that $Lt\left( {\cal M} \right) \cong \gamma$, then there is an Enayat model ${\cal M}$ such that $Lt\left( {\cal M} \right) \cong \gamma$.

Signal Recovery Beyond Linear Estimates

2019 ◽  
pp. 386-446
Author(s):  
John Stillwell
Keyword(s):  
Peano Arithmetic ◽  
Computable Analysis ◽  
Signal Recovery ◽  
Church’S Thesis ◽  
Equivalent Definition ◽  
Computably Enumerable Sets ◽  
Natural Concept ◽  
Definition Of ◽  
Computably Enumerable

This chapter explains why Σ‎0 1 formulas of Peano arithmetic (PA) capture all computably enumerable sets, as claimed by Alonzo Church's thesis from the previous chapter. This allows us to capture “computable analysis” in the language of PA, since computable sets and functions are definable in terms of computable enumerability. To justify the claim that Σ‎0 1 = “computably enumerable,” this chapter makes a thorough analysis of the concept of computation. It takes a precise, but intuitively natural, concept of computation and translates it into the language of PA. The chapter demonstrates that the translation is indeed Σ‎0 1, but with a slightly different (though equivalent) definition of Σ‎0 1.

Iterated reflection principles and the ω-rule

1982 ◽  
Vol 47 (4) ◽  
pp. 721-733 ◽  
Author(s):  
Ulf R. Schmerl
Keyword(s):  
Reflection Principle ◽  
Peano Arithmetic ◽  
Equivalent System ◽  
Formal Similarity ◽  
Sound System ◽  
Formal Systems ◽  
Ordinal Notations ◽  
Axiomatizable Theory ◽  
Reflection Principles ◽  
Image Position

The ω-rule,with the meaning “if the formula A(n) is provable for all n, then the formula ∀xA(x) is provable”, has a certain formal similarity with a uniform reflection principle saying “if A(n) is provable for all n, then ∀xA(x) is true”. There are indeed some hints in the literature that uniform reflection has sometimes been understood as a “formalized ω-rule” (cf. for example S. Feferman [1], G. Kreisel [3], G. H. Müller [7]). This similarity has even another aspect: replacing the induction rule or scheme in Peano arithmetic PA by the ω-rule leads to a complete and sound system PA∞, where each true arithmetical statement is provable. In [2] Feferman showed that an equivalent system can be obtained by erecting on PA a transfinite progression of formal systems PAα based on iterations of the uniform reflection principle according to the following scheme:Then T = (∪dЄ, PAd, being Kleene's system of ordinal notations, is equivalent to PA∞. Of course, T cannot be an axiomatizable theory.

A HIERARCHY OF COMPUTABLY ENUMERABLE DEGREES

2018 ◽  
Vol 24 (1) ◽  
pp. 53-89 ◽  
Author(s):  
ROD DOWNEY ◽  
NOAM GREENBERG
Keyword(s):  
Computability Theory ◽  
Ordinal Notations ◽  
Image Position ◽  
Computably Enumerable

AbstractWe introduce a new hierarchy of computably enumerable degrees. This hierarchy is based on computable ordinal notations measuring complexity of approximation of${\rm{\Delta }}_2^0$functions. The hierarchy unifies and classifies the combinatorics of a number of diverse constructions in computability theory. It does so along the lines of the high degrees (Martin) and the array noncomputable degrees (Downey, Jockusch, and Stob). The hierarchy also gives a number of natural definability results in the c.e. degrees, including a definable antichain.

UNIVERSAL COMPUTABLY ENUMERABLE EQUIVALENCE RELATIONS

2014 ◽  
Vol 79 (01) ◽  
pp. 60-88 ◽  
Author(s):  
URI ANDREWS ◽  
STEFFEN LEMPP ◽  
JOSEPH S. MILLER ◽  
KENG MENG NG ◽  
LUCA SAN MAURO ◽  
...  
Keyword(s):  
Computable Function ◽  
Order Theory ◽  
Equivalence Relations ◽  
Index Set ◽  
First Order ◽  
First Order Theory ◽  
Bounded Poset ◽  
Image Position ◽  
Open Question ◽  
Computably Enumerable

Abstract We study computably enumerable equivalence relations (ceers), under the reducibility $R \le S$ if there exists a computable function f such that $x\,R\,y$ if and only if $f\left( x \right)\,\,S\,f\left( y \right)$ , for every $x,y$ . We show that the degrees of ceers under the equivalence relation generated by $\le$ form a bounded poset that is neither a lower semilattice, nor an upper semilattice, and its first-order theory is undecidable. We then study the universal ceers. We show that 1) the uniformly effectively inseparable ceers are universal, but there are effectively inseparable ceers that are not universal; 2) a ceer R is universal if and only if $R\prime \le R$ , where $R\prime$ denotes the halting jump operator introduced by Gao and Gerdes (answering an open question of Gao and Gerdes); and 3) both the index set of the universal ceers and the index set of the uniformly effectively inseparable ceers are ${\rm{\Sigma }}_3^0$ -complete (the former answering an open question of Gao and Gerdes).

Flipping properties in arithmetic

1982 ◽  
Vol 47 (2) ◽  
pp. 416-422 ◽  
Author(s):  
L. A. S. Kirby
Keyword(s):  
Standard Model ◽  
Set Theory ◽  
Initial Segment ◽  
Peano Arithmetic ◽  
Combinatorial Properties ◽  
Nonstandard Model ◽  
Standard Part ◽  
The Standard Model ◽  
Nonstandard Models ◽  
Image Position

Flipping properties were introduced in set theory by Abramson, Harrington, Kleinberg and Zwicker [1]. Here we consider them in the context of arithmetic and link them with combinatorial properties of initial segments of nonstandard models studied in [3]. As a corollary we obtain independence resutls involving flipping properties.We follow the notation of the author and Paris in [3] and [2], and assume some knowledge of [3]. M will denote a countable nonstandard model of P (Peano arithmetic) and I will be a proper initial segment of M. We denote by N the standard model or the standard part of M. X ↑ I will mean that X is unbounded in I. If X ⊆ M is coded in M and M ≺ K, let X(K) be the subset of K coded in K by the element which codes X in M. So X(K) ⋂ M = X.Recall that M ≺IK (K is an I-extension of M) if M ≺ K and for some c∈K,In [3] regular and strong initial segments are defined, and among other things it is shown that I is regular if and only if there exists an I-extension of M.

On strong provability predicates and the associated modal logics

1993 ◽  
Vol 58 (1) ◽  
pp. 249-290 ◽  
Author(s):  
Konstantin N. Ignatiev
Keyword(s):  
Fixed Point ◽  
Peano Arithmetic ◽  
Modal Logics ◽  
Fixed Point Property ◽  
Provability Logic ◽  
Point Property ◽  
Craig Interpolation ◽  
Modal Properties ◽  
Craig Interpolation Lemma

AbstractPA is Peano Arithmetic. Pr(x) is the usual Σ1,-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ1. An example: Q is ω-provable if PA + ¬Q is ω-inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω-provability and obtained its arithmetical completeness.In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point property and the Craig interpolation lemma. We also consider other examples of the strong provability predicates and their applications.

Sign in / Sign up

Export Citation Format

Share Document