scholarly journals AXIOMATIZATION OF PROVABLE n-PROVABILITY

2019 ◽  
Vol 84 (02) ◽  
pp. 849-869 ◽  
Author(s):  
EVGENY KOLMAKOV ◽  
LEV BEKLEMISHEV
Keyword(s):  
Peano Arithmetic ◽  
Additional Information ◽  
Recursively Enumerable ◽  
Speed Up ◽  
Reflection Principles ◽  
Image Position

AbstractA formula φ is called n-provable in a formal arithmetical theory S if φ is provable in S together with all true arithmetical ${{\rm{\Pi }}_n}$-sentences taken as additional axioms. While in general the set of all n-provable formulas, for a fixed $n > 0$, is not recursively enumerable, the set of formulas φ whose n-provability is provable in a given r.e. metatheory T is r.e. This set is deductively closed and will be, in general, an extension of S. We prove that these theories can be naturally axiomatized in terms of progressions of iterated local reflection principles. In particular, the set of provably 1-provable sentences of Peano arithmetic $PA$ can be axiomatized by ${\varepsilon _0}$ times iterated local reflection schema over $PA$. Our characterizations yield additional information on the proof-theoretic strength of these theories (w.r.t. various measures of it) and on their axiomatizability. We also study the question of speed-up of proofs and show that in some cases a proof of n-provability of a sentence can be much shorter than its proof from iterated reflection principles.

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.

scholarly journals TRUTH AND FEASIBLE REDUCIBILITY

2019 ◽  
Vol 85 (1) ◽  
pp. 367-421
Author(s):  
ALI ENAYAT ◽  
MATEUSZ ŁEŁYK ◽  
BARTOSZ WCISŁO
Keyword(s):  
Polynomial Time ◽  
Computable Function ◽  
Peano Arithmetic ◽  
Base Theory ◽  
Speed Up ◽  
Image Position

AbstractLet ${\cal T}$ be any of the three canonical truth theories CT− (compositional truth without extra induction), FS− (Friedman–Sheard truth without extra induction), or KF− (Kripke–Feferman truth without extra induction), where the base theory of ${\cal T}$ is PA (Peano arithmetic). We establish the following theorem, which implies that ${\cal T}$ has no more than polynomial speed-up over PA.Theorem.${\cal T}$is feasibly reducible to PA, in the sense that there is a polynomial time computable function f such that for every${\cal T}$-proof π of an arithmetical sentence ϕ, f (π) is a PA-proof of ϕ.

MARGINALIA ON A THEOREM OF WOODIN

2017 ◽  
Vol 82 (1) ◽  
pp. 359-374
Author(s):  
RASMUS BLANCK ◽  
ALI ENAYAT
Keyword(s):  
Fixed Point ◽  
Peano Arithmetic ◽  
Countable Model ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Finite Set ◽  
Image Position

AbstractLet $\left\langle {{W_n}:n \in \omega } \right\rangle$ be a canonical enumeration of recursively enumerable sets, and suppose T is a recursively enumerable extension of PA (Peano Arithmetic) in the same language. Woodin (2011) showed that there exists an index $e \in \omega$ (that depends on T) with the property that if${\cal M}$ is a countable model of T and for some${\cal M}$-finite set s, ${\cal M}$ satisfies ${W_e} \subseteq s$, then${\cal M}$ has an end extension${\cal N}$ that satisfies T + We = s.Here we generalize Woodin’s theorem to all recursively enumerable extensions T of the fragment ${{\rm{I}\rm{\Sigma }}_1}$ of PA, and remove the countability restriction on ${\cal M}$ when T extends PA. We also derive model-theoretic consequences of a classic fixed-point construction of Kripke (1962) and compare them with Woodin’s theorem.

scholarly journals Interpretability over peano arithmetic

1999 ◽  
Vol 64 (4) ◽  
pp. 1407-1425
Author(s):  
Claes Strannegård
Keyword(s):  
Modal Logic ◽  
Completeness Theorem ◽  
Peano Arithmetic ◽  
Embedding Theorem ◽  
Compactness Theorem ◽  
Partial Answer ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Interpretability Logic

AbstractWe investigate the modal logic of interpretability over Peano arithmetic. Our main result is a compactness theorem that extends the arithmetical completeness theorem for the interpretability logic ILMω. This extension concerns recursively enumerable sets of formulas of interpretability logic (rather than single formulas). As corollaries we obtain a uniform arithmetical completeness theorem for the interpretability logic ILM and a partial answer to a question of Orey from 1961. After some simplifications, we also obtain Shavrukov's embedding theorem for Magari algebras (a.k.a. diagonalizable algebras).

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.

Register machine proof of the theorem on exponential diophantine representation of enumerable sets

1984 ◽  
Vol 49 (3) ◽  
pp. 818-829 ◽  
Author(s):  
J. P. Jones ◽  
Y. V. Matijasevič
Keyword(s):  
Natural Number ◽  
Polynomial Time ◽  
Simple Proof ◽  
Diophantine Equations ◽  
Polynomial Equation ◽  
Exponential Diophantine Equations ◽  
Recursively Enumerable ◽  
Image Position ◽  
The Right ◽  
Exponential Relation

The purpose of the present paper is to give a new, simple proof of the theorem of M. Davis, H. Putnam and J. Robinson [1961], which states that every recursively enumerable relation A(a1, …, an) is exponential diophantine, i.e. can be represented in the formwhere a1 …, an, x1, …, xm range over natural numbers and R and S are functions built up from these variables and natural number constants by the operations of addition, A + B, multiplication, AB, and exponentiation, AB. We refer to the variables a1,…,an as parameters and the variables x1 …, xm as unknowns.Historically, the Davis, Putnam and Robinson theorem was one of the important steps in the eventual solution of Hilbert's tenth problem by the second author [1970], who proved that the exponential relation, a = bc, is diophantine, and hence that the right side of (1) can be replaced by a polynomial equation. But this part will not be reproved here. Readers wishing to read about the proof of that are directed to the papers of Y. Matijasevič [1971a], M. Davis [1973], Y. Matijasevič and J. Robinson [1975] or C. Smoryński [1972]. We concern ourselves here for the most part only with exponential diophantine equations until §5 where we mention a few consequences for the class NP of sets computable in nondeterministic polynomial time.

Reductions of Hilbert's tenth problem

1958 ◽  
Vol 23 (2) ◽  
pp. 183-187 ◽  
Author(s):  
Martin Davis ◽  
Hilary Putnam
Keyword(s):  
Diophantine Equation ◽  
Hilbert's Tenth Problem ◽  
Recursively Enumerable ◽  
Hilbert’S Tenth Problem ◽  
Essential Change ◽  
Recursive Predicate ◽  
Image Position ◽  
Positive Integers

Hilbert's tenth problem is to find an algorithm for determining whether or not a diophantine equation possesses solutions. A diophantine predicate (of positive integers) is defined to be one of the formwhere P is a polynomial with integral coefficients (positive, negative, or zero). Previous work has considered the variables as ranging over nonnegative integers; but we shall find it more useful here to restrict the range to positive integers, no essential change being thereby introduced. It is clear that the recursive unsolvability of Hilbert's tenth problem would follow if one could show that some non-recursive predicate were diophantine. In particular, it would suffice to show that every recursively enumerable predicate is diophantine. Actually, it would suffice to prove far less.

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.

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.

Applications of Strict Π11 predicates to infinitary logic

1969 ◽  
Vol 34 (3) ◽  
pp. 409-423 ◽  
Author(s):  
Jon Barwise
Keyword(s):  
Normal Form ◽  
Infinitary Logic ◽  
Natural Numbers ◽  
Recursively Enumerable ◽  
Image Position

Consider the predicate of natural numbers defined by: where R is recursive. If, as usual, the variable ƒ ranges over ωω (the set of functions from natural numbers to natural numbers) then this is just the usual normal form for Π11 sets. If, however, ƒ ranges over 2ω (the set of functions from ω into {0, 1}) then every such predicate is recursively enumerable.3 Thus the second type of formula is generally ignored. However, the reduction just mentioned requires proof, and the proof uses some form of the Brower-König Infinity Lemma.

Sign in / Sign up

Export Citation Format

Share Document