The provability logics of recursively enumerable theories extending peano arithmetic at arbitrary theories extending peano arithmetic

1984 ◽  
Vol 13 (1) ◽  
pp. 97-113 ◽  
Author(s):  
Albert Visser
Keyword(s):  
Peano Arithmetic ◽  
Recursively Enumerable

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

Π10 classes and Boolean combinations of recursively enumerable sets

1974 ◽  
Vol 39 (1) ◽  
pp. 95-96 ◽  
Author(s):  
Carl G. Jockusch
Keyword(s):  
Turing Machine ◽  
Peano Arithmetic ◽  
Binary Sequences ◽  
First Order ◽  
Recursive Tree ◽  
Recursively Enumerable ◽  
Private Correspondence ◽  
Recursively Enumerable Sets ◽  
Binary Input

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

Arithmetic Without the Exponential

1992 ◽  
Author(s):  
Raymond M. Smullyan
Keyword(s):  
Recursive Function ◽  
Function Theory ◽  
Axiom System ◽  
Peano Arithmetic ◽  
Recursively Enumerable

§1. By an arithmetic term or formula, we mean a term or formula in which the exponential symbol E does not appear, and by an arithmetic relation (or set), we mean a relation (set) expressible by an arithmetic formula. By the axiom system P.A. (Peano Arithmetic), we mean the system P.E. with axiom schemes N10 and N11 deleted, and in the remaining axiom schemes, terms and formulas are understood to be arithmetic terms and formulas. The system P.A. is the more usual object of modern study (indeed, the system P.E. is rarely considered in the literature). We chose to give the incompleteness proof for P.E. first since it is the simpler. In this chapter, we will prove the incompleteness of P.A. and establish several other results that will be needed in later chapters. The incompleteness of P.A. will easily follow from the incompleteness of P.E., once we show that the relation xy = z is not only Arithmetic but arithmetic (definable from plus and times alone). We will first have to show that certain other relations are arithmetic, and as we are at it, we will show stronger results about these relations that will be needed, not for the incompleteness proof of this chapter, but for several chapters that follow—we will sooner or later need to show that certain key relations are not only arithmetic, but belong to a much narrower class of relations, the Σ1-relations, which we will shortly define. These relations are the same as those known as recursively enumerable. Before defining the Σ1-relations, we turn to a still narrower class, the Σ0-relations, that will play a key role in our later development of recursive function theory. §2. We now define the classes of Σ0-formulas and Σ0-relations and then the Σ1-formulas and relations. By an atomic Σ0-formula, we shall mean a formula of one of the four forms c1 + c2 = c3, c1 · c2 =c3, c1 = c2 or c1 ≤ c2, where each of c1, c2 or c3 is either a variable or a numeral (but some may be variables and others numerals).

Some properties of the syntactic p-recursion categories generated by consistent, recursively enumerable extensions of Peano arithmetic.

1991 ◽  
Vol 56 (2) ◽  
pp. 643-660 ◽  
Author(s):  
Robert A. Di Paola ◽  
Franco Montagna
Keyword(s):  
Peano Arithmetic ◽  
Incompleteness Theorem ◽  
Easy Consequence ◽  
Recursively Enumerable ◽  
Bona Fide ◽  
Precise Relationship

The dominical categories were introduced by Di Paola and Heller, as a first step toward a category-theoretic treatment of the generalized first Godel incompleteness theorem [1]. In his Ph.D. dissertation [7], Rosolini subsequently defined the closely related p-categories, which should prove pertinent to category-theoretic representations of incompleteness for intuitionistic systems. The precise relationship between these two concepts is as follows: every dominical category is a pointed p-category, but there are p-categories, indeed pointed p-isotypes (all pairs of objects being isomorphic) with a Turing morphism that are not dominical. The first of these assertions is an easy consequence of the fact that in a dominical category C by definition the near product functor when restricted to the subcategory Ct, of total morphisms of C (as “total” is defined in [1]) constitutes a bona fide product such that the derived associativity and commutativity isomorphisms are natural on C × C × C and C × C, respectively, as noted in [7]. As to the second, p-recursion categories (that is, pointed p-isotypes having a Turing morphism) that are not dominical were defined and studied by Montagna in [6], the syntactic p-categories ST and S′T associated with consistent, recursively enumerable extensions of Peano arithmetic, PA. These merit detailed investigation on several counts.

scholarly journals Inconsistent Models for Relevant Arithmetics

2021 ◽  
Vol 18 (5) ◽  
pp. 380-400
Author(s):  
Robert Meyer ◽  
Chris Mortensen
Keyword(s):  
Classical Logic ◽  
Relevant Logic ◽  
Peano Arithmetic ◽  
Incompleteness Theorem ◽  
Intrinsic Interest ◽  
Recursively Enumerable ◽  
Classical Quantum ◽  
The Absolute ◽  
Quantum Arithmetic ◽  
Inconsistent Theories

This paper develops in certain directions the work of Meyer in [3], [4], [5] and [6] (see also Routley [10] and Asenjo [11]). In those works, Peano’s axioms for arithmetic were formulated with a logical base of the relevant logic R, and it was proved finitistically that the resulting arithmetic, called R♯, was absolutely consistent. It was pointed out that such a result escapes incau- tious formulations of Goedel’s second incompleteness theorem, and provides a basis for a revived Hilbert programme. The absolute consistency result used as a model arithmetic modulo two. Modulo arithmetics are not or- dinarily thought of as an extension of Peano arithmetic, since some of the propositions of the latter, such as that zero is the successor of no number, fail in the former. Consequently a logical base which, unlike classical logic, tolerates contradictory theories was used for the model. The logical base for the model was the three-valued logic RM3 (see e.g. [1] or [8]), which has the advantage that while it is an extension of R, it is finite valued and so easier to handle. The resulting model-theoretic structure (called in this paper RM32) is interesting in its own right in that the set of sentences true therein consti- tutes a negation inconsistent but absolutely consistent arithmetic which is an extension of R♯. In fact, in the light of the result of [6], it is an extension of Peano arithmetic with a base of a classical logic, P♯. A generalisation of the structure is to modulo arithmetics with the same logical base RM3, but with varying moduli (called RM3i here). We first study the properties of these arithmetics in this paper. The study is then generalised by vary- ing the logical base, to give the arithmetics RMni, of logical base RMn and modulus i. Not all of these exist, however, as arithmetical properties and logical properties interact, as we will show. The arithmetics RMni give rise, on intersection, to an inconsistent arithmetic RMω which is not of modulo i for any i. We also study its properties, and, among other results, we show by finitistic means that the more natural relevant arithmetics R♯ and R♯♯ are incomplete (whether or not consistent and recursively enumerable). In the rest of the paper we apply these techniques to several topics, particularly relevant quantum arithmetic in which we are able to show (unlike classical quantum arithmetic) that the law of distribution remains unprovable. Aside from its intrinsic interest, we regard the present exercise as a demonstration that inconsistent theories and models are of mathematical worth and interest.

A minimal pair of Π10 classes

1971 ◽  
Vol 36 (1) ◽  
pp. 66-78 ◽  
Author(s):  
Carl G. Jockusch ◽  
Robert I. Soare
Keyword(s):  
Peano Arithmetic ◽  
Minimal Degree ◽  
Minimal Pair ◽  
Turing Degrees ◽  
Complete Extension ◽  
Recursively Enumerable

A pair of sets (A0, A1) forms a minimal pair if A0 and A1 are nonrecursive, and if whenever a set B is recursive both in A0 and in A1 then B is recursive. C. E. M. Yates [8] and independently A. H. Lachlan [4] proved the existence of a minima] pair of recursively enumerable (r.e.) sets thereby establishing a conjecture of G. E. Sacks [6]. We simplify Lachlan's construction, and then generalize this result by constructing two disjoint pairs of r.e. sets (A0, B0) and (A1B1) such that if C0 separates (A0, A1 and C1 separates (B0, B1), then C0 and C1 form a minimal pair. (We say that C separates (A0, A1) if A0 ⊂ C and C ∩ = ∅.) The question arose in our study of (Turing) degrees of members of certain classes, where we proved the weaker result [2, Theorem 4.1] that the above pairs may be chosen so that C0 and C2 are merely Turing incomparable. (There we used a variation of the weaker result to improve a result of Scott and Tennenbaum that no complete extension of Peano arithmetic has minimal degree.)

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.

Pseudo-complements and ordinal logics based on consistency statements

1966 ◽  
Vol 31 (3) ◽  
pp. 359-364 ◽  
Author(s):  
Robert A. Di Paola
Keyword(s):  
Recursive Function ◽  
Peano Arithmetic ◽  
Additional Property ◽  
Primitive Recursive Function ◽  
Recursively Enumerable ◽  
Primitive Recursive

Following [1] we write {n} for the nth recursively enumerable (re) set; that is, {n} = {x|VyT(n, x, y)}. By a “pair (T, α)” we mean a consistent re extension T of Peano arithmetic P and an RE-formula α which numerates the non-logical axioms of T in P [4]. Given a pair (T, α) and a particular formula which binumerates the Kleene T predicate in P, there can be defined a primitive recursive function Nα such that and which has the additional property that {Nα(Nα(n))} = ø for all n.

Torre models in the isols

1994 ◽  
Vol 59 (1) ◽  
pp. 140-150 ◽  
Author(s):  
Joseph Barback
Keyword(s):  
Number Theory ◽  
Structural Property ◽  
Recursive Function ◽  
Peano Arithmetic ◽  
The Other ◽  
Close Connection ◽  
New Variety ◽  
Nonstandard Model ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets

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

Sign in / Sign up

Export Citation Format

Share Document