scholarly journals Interpretability over peano arithmetic

1999 ◽  
Vol 64 (4) ◽  
pp. 1407-1425
Author(s):  
Claes Strannegård

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).

1974 ◽  
Vol 39 (1) ◽  
pp. 95-96 ◽  
Author(s):  
Carl G. Jockusch

Let be the collection of all sets which are finite Boolean combinations of recursively enumerable (r.e.) sets of numbers. Dale Myers asked [private correspondence] whether there exists a nonempty class of sets containing no member of . In this note we construct such a class. The motivation for Myers' question was his observation (reported in [1]) that the existence of such a class is equivalent to the assertion that there is a finite consistent set of tiles which has no m-trial tiling of the plane for any m (obeying the “origin constraint”). (For explanations of these terms and further results on tilings of the plane, cf. [1] and [5].) In addition to the application to tilings, the proof of our results gives some information on bi-immune sets and on complete extensions of first-order Peano arithmetic.A class of sets may be roughly described as the class of infinite binary input tapes for which a fixed Turing machine fails to halt, or alternatively as the class of infinite branches of a recursive tree of finite binary sequences. (In these definitions, sets of numbers are identified with the corresponding binary sequences.) Precise definitions, as well as many results concerning such classes, may be found in [3] and [4].


1990 ◽  
Vol 55 (3) ◽  
pp. 1059-1089 ◽  
Author(s):  
Alessandro Berarducci

AbstractPA is Peano arithmetic. The formula InterpPA(α, β) is a formalization of the assertion that the theory PA + α interprets the theory PA + β (the variables α and β are intended to range over codes of sentences of PA). We extend Solovay's modal analysis of the formalized provability predicate of PA, PrPA(x), to the case of the formalized interpretability relation InterpPA(x, y). The relevant modal logic, in addition to the usual provability operator ‘□’, has a binary operator ‘⊳’ to be interpreted as the formalized interpretability relation. We give an axiomatization and a decision procedure for the class of those modal formulas that express valid interpretability principles (for every assignment of the atomic modal formulas to sentences of PA). Our results continue to hold if we replace the base theory PA with Zermelo-Fraenkel set theory, but not with Gödel-Bernays set theory. This sensitivity to the base theory shows that the language is quite expressive. Our proof uses in an essential way earlier work done by A. Visser, D. de Jongh, and F. Veltman on this problem.


2012 ◽  
Vol 6 (1) ◽  
pp. 129-146 ◽  
Author(s):  
TAISHI KURAHASHI

AbstractSolovay proved the arithmetical completeness theorem for the system GL of propositional modal logic of provability. Montagna proved that this completeness does not hold for a natural extension QGL of GL to the predicate modal logic. Let Th(QGL) be the set of all theorems of QGL, Fr(QGL) be the set of all formulas valid in all transitive and conversely well-founded Kripke frames, and let PL(T) be the set of all predicate modal formulas provable in Tfor any arithmetical interpretation. Montagna’s results are described as Th(QGL) ⊊ (Fr(QGL), PL(PA) ⊈ Fr(QGL), and Th(QGL) ⊊ PL(PA).In this paper, we prove the following three theorems: (1) Fr(QGL) ⊈ PL(T) for any Σ1-sound recursively enumerable extension T of I Σ1, (2) PL(T) ⊈ Fr(QGL) for any recursively enumerable A-theory T extending I Σ1, and (3) Th(QGL) ⊊ Fr(QGL) ∩ PL(T) for any recursively enumerable A-theory T extending I Σ2.To prove these theorems, we use iterated consistency assertions and nonstandard models of arithmetic, and we improve Artemov’s lemma which is used to prove Vardanyan’s theorem on the Π02-completeness of PL(T).


1994 ◽  
Vol 59 (1) ◽  
pp. 140-150 ◽  
Author(s):  
Joseph Barback

AbstractIn [14] J. Hirschfeld established the close connection of models of the true AE sentences of Peano Arithmetic and homomorphic images of the semiring of recursive functions. This fragment of Arithmetic includes most of the familiar results of classical number theory. There are two nice ways that such models appear in the isols. One way was introduced by A. Nerode in [20] and is referred to in the literature as Nerode Semirings. The other way is called a tame model. It is very similar to a Nerode Semiring and was introduced in [6]. The model theoretic properties of Nerode Semirings and tame models have been widely studied by T. G. McLaughlin ([16], [17], and [18]).In this paper we introduce a new variety of tame model called a torre model. It has as a generator an infinite regressive isol with a nice structural property relative to recursively enumerable sets and their extensions to the isols. What is then obtained is a nonstandard model in the isols of the fragment of Peano Arithmetic with the following property: Let T be a torre model. Let f be any recursive function, and let fΛ be its extension to the isols. If there is an isol A with fΛ(A) ϵ T, then there is also an isol B ϵ T with fΛ(B) = fΛ(A).


2017 ◽  
Vol 82 (1) ◽  
pp. 359-374
Author(s):  
RASMUS BLANCK ◽  
ALI ENAYAT

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.


Author(s):  
Artiom Alhazov ◽  
Rudolf Freund ◽  
Sergiu Ivanov

AbstractCatalytic P systems are among the first variants of membrane systems ever considered in this area. This variant of systems also features some prominent computational complexity questions, and in particular the problem of using only one catalyst in the whole system: is one catalyst enough to allow for generating all recursively enumerable sets of multisets? Several additional ingredients have been shown to be sufficient for obtaining computational completeness even with only one catalyst. In this paper, we show that one catalyst is sufficient for obtaining computational completeness if either catalytic rules have weak priority over non-catalytic rules or else instead of the standard maximally parallel derivation mode, we use the derivation mode maxobjects, i.e., we only take those multisets of rules which affect the maximal number of objects in the underlying configuration.


1963 ◽  
Vol 28 (1) ◽  
pp. 43-50 ◽  
Author(s):  
L. P. Belluce ◽  
C. C. Chang

This paper contains some results concerning the completeness of a first-order system of infinite valued logicThere are under consideration two distinct notions of completeness corresponding to the two notions of validity (see Definition 3) and strong validity (see Definition 4). Both notions of validity, whether based on the unit interval [0, 1] or based on linearly ordered MV-algebras, use the element 1 as the designated truth value. Originally, it was thought by many investigators in the field that one should be able to prove that the set of valid sentences is recursively enumerable. It was first proved by Rutledge in [9] that the set of valid sentences in the monadic first-order infinite valued logic is recursively enumerable.


Sign in / Sign up

Export Citation Format

Share Document