Search

Answering a question raised by Shavrukov and Visser (Notre Dame J Form Log 55(4):569–582, 2014), we show that the lattice of $$\exists \Sigma ^\mathsf {b}_1$$ -sentences (in the language of Buss’ weak arithmetical system $$\mathsf {S}^1_2$$ ) over any computable enumerable consistent extension T of $$\mathsf {S}^1_2$$ is uniformly dense (in the sense of Definition 2). We also show that for every $$\mathcal {C} \in \{\Phi _n: n\ge 3\} \cup \{\Theta _n: n \ge 2\}$$ (where $$\Phi $$ and $$\Theta $$ refer to the known hierarchies of arithmetical formulas introduced by Burr for intuitionistic arithmetic) the lattices of $$\mathcal {C}$$ -sentences over any c.e. consistent extension T of the intuitionistic version of Robinson Arithmetic $${{\,\mathrm{\mathsf {R}}\,}}$$ are uniformly dense. As an immediate consequence of the proof, all these lattices are also locally universal (in the sense of Definition 3).

In Chapter 10, we have seen that Peano Arithmetic PA is incomplete. Moreover, if we omit the Induction Schema and replace it by the axiom \(\forall x(x=0\vee\exists y(x=sy))\), stating that every number is either 0 or has a predecessor, then the resulting theory, called Robinson Arithmetic, is also incomplete.

In this paper we study local induction w.r.t. Σ1-formulas over the weak arithmetic PA- The local induction scheme, which was introduced in, says roughly this: for any virtual class X that is progressive, i.e., is closed under zero and successor, and for any non-empty virtual class Y that is definable by a Σ1-formula without parameters, the intersection of X and Y is non-empty. In other words, we have, for all Σ1-sentences S, that S implies SX, whenever X is progressive. Since, in the weak context, we have (at least) two definitions of Σ1, we obtain two minimal theories of local induction w.r.t. Σ1-formulas, which we call Peano Corto and Peano Basso. In the paper we give careful definitions of Peano Corto and Peano Basso. We establish their naturalness both by giving a model theoretic characterization and by providing an equivalent formulation in terms of a sentential reflection scheme. The theories Peano Corto and Peano Basso occupy a salient place among the sequential theories on the boundary between weak and strong theories. They bring together a powerful collection of principles that is locally interpretable in PA- Moreover, they have an important role as examples of various phenomena in the metamathematics of arithmetical (and, more generally, sequential) theories. We illustrate this by studying their behavior w.r.t. interpretability, model interpretability and local interpretability. In many ways the theories are more like Peano arithmetic or Zermelo Fraenkel set theory, than like finitely axiomatized theories as Elementary Arithmetic, |Σ1 and ACA0. On the one hand, Peano Corto and Peano Basso are very weak: they are locally cut-interpretable in PA- On the other hand, they behave as if they were strong: they are not contained in any consistent finitely axiomatized arithmetical theory, however strong. Moreover, they extend IΠ1-, the theory of parameter-free Π1-induction. © 2014 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

The Paradox of the Knower was originally presented by Kaplan and Montague (1960) [26] as a puzzle about the everyday notion of knowledge in the face of self-reference. The paradox shows that any theory extending Robinson arithmetic with a predicate K ( x ) satisfying the factivity axiom K ( A ¯ ) → A as well as a few other epistemically plausible principles is inconsistent. After surveying the background of the paradox, we will focus on a recent debate about the role of epistemic closure principles in the Knower. We will suggest this debate sheds new light on the concept of knowledge which is at issue in the paradox – i.e. is it a “thin” notion divorced from concepts such as evidence or justification, or is it a “thick” notion more closely resembling mathematical provability? We will argue that a number of features of the paradox suggest that the latter option is more plausible. Along the way, we will provide a reconstruction of the paradox using a quantified extension of Artemovʼs (2001) [2] Logic of Proofs, as well as a series of results linking the original formulation of the paradox to reflection principles for formal arithmetic. On this basis, we will argue that while the Knower can be understood to motivate a distinction between levels of knowledge, it does not provide a rationale for recognizing a uniform hierarchy of knowledge predicates in the manner suggested by Anderson (1984) [1] .

We present a number of results on the structure of initial segments of models of Peano arithmetic with the arithmetic operations of addition, subtraction, multiplication, division, exponentiation and logarithm. Each of the binary operations introduced is defined in two dual ways, often with quite different results, and we attempt to systematise the issues and show how various calculations may be carried out. To understand the behaviour of addition and subtraction we introduce a notion of derivative on cuts, analogous to differentiation in the calculus. Multiplication, division and other operations are described by higher order versions of derivative. The work here is presented as important preliminary work related to a nonstandard measure theory of non-definable bounded subsets of a model of Peano arithmetic.

Wos proposed 33 basic research problems for automated reasoning field, one of them is the problem of automated theorem finding. The problem has not been solved until now. The problem implicitly requires some metrics to be used for measuring interestingness of found theorems. We have proposed some metrics to measure interestingness of theorems found by using forward reasoning approach. We have measured interestingness of the theorems of NBG set theory by using those metrics. To confirm the generality of the proposed metrics, we have to apply them in other mathematical fields. This paper presents a case study in Peano’s arithmetic to show the generality of proposed metrics. We evaluate the interestingness of theorems of Peano’s arithmetic obtained by using forward reasoning approach, and confirm the effectiveness of the metrics.

An elementary rheory of concatenation is introduced and used to establish mutual interpretability of Robinson arithmetic, Minimal Predicative Set Theory, the quantifier-free part of Kirby's finitary set theory, and Adjunctive Set Theory, with or without extensionality., Comment: 61 pages

This paper concerns the relationship between transitivity of entailment, omega-inconsistency and nonstandard models of arithmetic. First, it provides a cut-free sequent calculus for non-transitive logic of truth STT based on Robinson Arithmetic and shows that this logic is omega-inconsistent. It then identifies the conditions in McGee (1985) for an omega-inconsistent logic as quantified standard deontic logic, presents a cut-free labelled sequent calculus for quantified standard deontic logic based on Robinson Arithmetic where the deontic modality is treated as a predicate, proves omega-inconsistency and shows thus, pace Cobreros et al.(2013), that the result in McGee (1985) does not rely on transitivity. Finally, it also explains why the omega-inconsistent logics of truth in question do not require nonstandard models of arithmetic.

This paper presents new constructions of models of Hume's Principle and Basic Law V with restricted amounts of comprehension. The techniques used in these constructions are drawn from hyperarithmetic theory and the model theory of fields, and formalizing these techniques within various subsystems of second-order Peano arithmetic allows one to put upper and lower bounds on the interpretability strength of these theories and hence to compare these theories to the canonical subsystems of second-order arithmetic. The main results of this paper are: (i) there is a consistent extension of the hyperarithmetic fragment of Basic Law V which interprets the hyperarithmetic fragment of second-order Peano arithmetic, and (ii) the hyperarithmetic fragment of Hume's Principle does not interpret the hyperarithmetic fragment of second-order Peano arithmetic, so that in this specific sense there is no predicative version of Frege's Theorem.

Shepherdson [14] showed that for a discrete ordered ring I, I is a model of I Open iff I is an integer part of a real closed ordered field. In this paper, we consider integer parts satisfying PA. We show that if a real closed ordered field R has an integer part I that is a nonstandard model of PA (or even IΣ4), then R must be recursively saturated. In particular, the real closure of I, RC (I), is recursively saturated. We also show that if R is a countable recursively saturated real closed ordered field, then there is an integer part I such that R = RC(I) and I is a nonstandard model of PA.

The paper undertakes three interdisciplinary tasks. The first one consists in constructing a formal model of the basic arithmetic competence, that is, the competence sufficient for solving simple arithmetic story-tasks which do not require any mathematical mastery knowledge about laws, definitions and theorems. The second task is to present a generalized arithmetic theory, called the arithmetic of indexed numbers (INA). All models of the development of counting abilities presuppose the common assumption that our simple, folk arithmetic encoded linguistically in the mind is based on the linear number representation. This classical conception is rejected and a competitive hypothesis is formulated according to which the basic mature representational system of cognitive arithmetic is a structure composed of many numerical axes which possess a common constituent, namely, the numeral zero. Arithmetic of indexed numbers is just a formal tool for modelling the basic mature arithmetic competence. The third task is to develop a standpoint called temporal pluralism, which is motivated by neo-Kantian philosophy of arithmetic.

Bounded lattices (that is lattices that are both lower bounded and upper bounded) form a large class of lattices that include all distributive lattices, many nondistributive finite lattices such as the pentagon lattice N5. and all lattices in any variety generated by a finite bounded lattice. Extending a theorem of Paris for distributive lattices, we prove that if L is an ℵ0-algebraic bounded lattice, then every countable nonstandard model of Peano Arithmetic has a cofinal elementary extension such that the interstructure lattice Lt(/) is isomorphic to L.

We present a functional interpretation of Peano arithmetic that uses Godel’s computable functionals and which systematically injects uniformities into the statements of finite-type arithmetic. As a consequence, some uniform boundedness principles (not necessarily set-theoretically true) are interpreted while maintaining unmoved the Π 2 0 -sentences of arithmetic. We explain why this interpretation is tailored to yield conservation results.

We give alternative proofs of results due to Paris and Wilkie concerning the existence of end extensions of countable models of $B\Sigma_{1}$ , that is, the theory of $\Sigma_{1}$ collection.

A Turing degree d is homogeneous bounding if every complete decidable (CD) theory has a d-decidable homogeneous model , i.e., the elementary diagram De () has degree d. It follows from results of Macintyre and Marker that every PA degree (i.e., every degree of a complete extension of Peano Arithmetic) is homogeneous bounding. We prove that in fact a degree is homogeneous bounding if and only if it is a PA degree. We do this by showing that there is a single CD theory T such that every homogeneous model of T has a PA degree.

ionism has enjoyed some preliminary success with Hume’s Principle, which says that the number of F s is identical to the number of Gs just in case the F s and the Gs can be one-to-one correlated. This abstraction principle can be formalized as (HP) #F = #G ↔ F ≈ G where #F denotes the number of F s and F ≈ G abbreviates the second-order claim that there is a relation that one-to-one correlates F s and the Gs. Burgess describes (with unsurpassed attention to historical detail) how Hume’s Principle has been found to have two very desirable properties. Let Frege Arithmetic (or FA for short) be the second-order theory whose sole nonlogical axiom is (HP). Then firstly, FA is consistent. And secondly, Frege’s own definitions and derivations show how FA gives rise to all the axioms of ordinary Peano arithmetic—a result known as Frege’s theorem. The previous section alluded to the question how strong concept comprehension axioms are needed for Frege’s theorem to go through. Linnebo, 2004 proves that, given Frege’s own definitions of the primitive signs of arithmetic, predicative comprehension is insufficient to prove that every number has a successor. In Section 2.3 Burgess cleverly bypasses this limitative result by adopting an alternative, non-Fregean definition of natural number predicate, which allows him to interpret Robinson arithmetic Q (which of course says that every number has a successor) in FA with only predicative comprehension. If one imposes no requirements (beyond the obvious technical ones) on one’s definitions of the primitive signs of arithmetic, then Burgess’s result will dispel any worries caused by Linnebo, 2004. If, on the other hand, one requires that these definitions should correspond to our ordinary arithmetical thought and practice, and if one thinks that Frege’s definitions are implicit in such thought and practice, then the result will be of no immediate philosophical significance.10 Setting aside all questions about impredicative comprehension, it is clear that any viable abstractionism must be able to delineate a much wider class of acceptable abstraction principles than just Hume’s Principle. Burgess summarizes some of the efforts towards this goal Heck, gives a different predicative proof of Frege’s theorem, using Frege’s own definitions transposed to the un-Fregean setting of ramified second-order logic.

We establish the following model theoretic characterization of the fragment I¢0+Exp+B§1 of Peano arithmetic in terms of fixed points of automorphisms of models of bounded arithmetic (the fragment I¢0 of Peano arithmetic with induction limited to ¢0-formulae).

We study the arithmetical schema asserting that every eventually decreasing elementary recursive function has a limit. Some other related principles are also formulated. We establish their relationship with restricted parameter-free induction schemata. We also prove that the same principle, formulated as an inference rule, provides an axiomatization of the Σ 2 -consequences of I Σ 1 . Using these results we show that ILM is the logic of Π 1 -conservativity of any reasonable extension of parameter-free Π 1 -induction schema. This result, however, cannot be much improved: by adapting a theorem of D. Zambella and G. Mints we show that the logic of Π 1 -conservativity of primitive recursive arithmetic properly extends ILM . In the third part of the paper we give an ordinal classification of Σ n 0 -consequences of the standard fragments of Peano arithmetic in terms of reflection principles. This is interesting in view of the general program of ordinal analysis of theories, which in the most standard cases classifies Π -classes of sentences (usually Π 1 1 or Π 2 0 ).

Girard’s maxim, that Peano Arithmetic is (best viewed as) a theory of one inductive definition, is re-examined in the light of a weak theory EA(I;O) formalising basic principles of Nelson’s predicative Arithmetic.

This paper is a study of reflection principles in fragments of formal Peano arithmetic and their applications to the comparison and classification of arithmetical theories.

Let M be a model of first order Peano arithmetic (PA) and I an initial segment of M that is closed under multiplication. LetM0 be the {0, 1,+}-reduct ofM. We show that there is another model N of PA that is also an expansion of M0 such that a · Ma = a · Na if and only if a ∈ I for all a ∈ M.

Geometric theories are presented as contraction- and cut-free systems of sequent calculi with mathematical rules following a prescribed rule-scheme that extends the scheme given in Negri and von Plato (1998). Examples include cut-free calculi for Robinson arithmetic and real closed fields. As an immediate consequence of cut elimination, it is shown that if a geometric implication is classically derivable from a geometric theory then it is intuitionistically derivable.

We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates, IΔ1. We show that IΔ1 is independent from the set of all true arithmetical Π2-sentences. Moreover, we establish the connections between this theory and some classes of oracle computable functions with restrictions on the allowed number of queries. We also obtain some conservation and independence results for parameter free and inference rule forms of Δ1-induction.An open problem formulated by J. Paris (see [4, 5]) is whether IΔ1 proves the corresponding least element principle for decidable predicates, LΔ1 (or, equivalently, the Σ1-collection principle BΣ1). We reduce this question to a purely computation-theoretic one.

The shortest definition of a number by a first order formula with one free variable, where the notion of a formula defining a number extends a notion used by Boolos in a proof of the Incompleteness Theorem, is shown to be non computable. This is followed by an examination of the complexity of sets associated with this function.

Let us recall that Raphael Robinson's Arithmetic Q is an axiom system that differs from Peano Arithmetic essentially by containing no Induction axioms [13], [18]. We will generalize the semantic-tableaux version of the Second Incompleteness Theorem almost to the level of System Q. We will prove that there exists a single rather long Π1 sentence, valid in the standard model of the Natural Numbers and denoted as V. such that if α is any finite consistent extension of Q + V then α will be unable to prove its Semantic Tableaux consistency. The same result will also apply to axiom systems α with infinite cardinality when these infinite-sized axiom systems satisfy a minor additional constraint, called the Conventional Encoding Property.Our formalism will also imply that the semantic-tableaux version of the Second Incompleteness Theorem generalizes for the axiom system IΣ0, as well as for all its natural extensions. (This answers an open question raised twenty years ago by Paris and Wilkie [15].)

Let T 0?T 1 denote that each computable function, which is provable total in the first order theory T 0, is also provable total in the first order theory T 1. Te relation ? induces a degree structure on the sound finite Π2 extensions of EA (Elementary Arithmetic). This paper is devoted to the study of this structure. However we do not study the structure directly. Rather we define an isomorphic subrecursive degree structure , and then we study by ubrecursive and computability-theoretic means. Furthermore, we introduce and investigate some operators on the degrees of . These operators corresponds to inferencerules in formal arithmetic. One operator corresponds to the Σ1 collection rule. Another operator corresponds to the Σ1 induction rule.

In this paper, the sequential variants of the multiplicative arithmetic with the below-defined formsAIO,I+, andI− of the induction axiom are investigated, and some relations between the classes of theorems in these systems are determined. In addition, the multiplicative systems with these induction axioms, for which the classes of derivable formulas are equivalent, are presented.

We generalize a result on True Arithmetic (ℐA) by Lachlan and Soare to certain other completions of Peano Arithmetic (PA). If ℐ is a completion of PA, then Rep(ℐ) denotes the family of sets X ⊆ ω for which there exists a formula φ(x) such that for all n ∈ ω, if n ∈ X, then ℐ ⊢ φ(S(n) (0)) and if n ∉ X, then ℐ ⊢ ┐φ(S(n)(O)). We show that if S, J ⊆ P(ω) such that S is a Scott set, J is a jump ideal, S ⊂ J and for all X ∈ J, there exists C ∈ S such that C is a “coding” set for the family of subtrees of 2 computable in X, and if ℐ is a completion of PA Such that Rep(ℐ) = S, then there exists a model A of ℐ such that J is the Scott set of A and no enumeration of Rep(ℐ) is computable in A. The model A of ℐ is obtained via a new notion of forcing.Before proving our main result, we demonstrate the existence of uncountably many different pairs (S, J) satisfying the conditions of our theorem. This involves a new characterization of 1-generic sets as coding sets for the computable subtrees of 2. In particular, C C ⊆ ω is a coding set for the family of subtrees of 2 computable in X if and only if for all trees T ⊆ 2 computable in X, if χc is a path through T, then there exists σ ∈ T such that σ ⊂ χc and every extension of σ is in T. Jockusch noted a connection between 1-generic sets and coding sets for computable subtrees of 2. We show they are identical.

This chapter introduces Peano Arithmetic and discusses two respects in which it is incomplete.

Within a weak subsystem of second-order arithmetic WKL0, we develop basic part of non-standard analysis up to the Peano existence theorem.

Data exchange is the problem of transforming data structured under a source schema into data structured under a target schema, taking into account structural relationships between the two schemas, which are described by a schema mapping. Existing schema-mapping languages lack the ability to express arithmetic operations, such as addition and multiplication, which naturally arise in data warehousing, ETL applications, and applications involving scientific data. We initiate the study of data exchange for arithmetic schema mappings, that is, schema mappings specified by source-to-target dependencies and target dependencies that may include arithmetic formulas interpreted over the algebraic real numbers (we restrict attention to algebraic real numbers to maintain finite presentability).We show that, for arithmetic schema mappings without target dependencies, the existence-of-solutions problem can be solved in polynomial time, and, if a solution exists, then a universal solution (suitably defined) exists and can be computed in polynomial time. In the case of arithmetic schema mappings with a weakly acyclic set of target dependencies, a universal solution may not exist, but a finite universal basis exists (if a solution exists) and can be computed in polynomial space. The existence-of-solutions problem turns out to be NP-hard, and solvable in PSpace. In fact, we show it is ∃R-complete, which means that it has the same complexity as the decision problem for the existential theory of the real numbers, or, equivalently, the problem of deciding whether or not a quantifier-free arithmetic formula has a solution over the real numbers. If we allow only linear arithmetic formulas in the schema mapping and in the query, interpreted over the rational numbers, then the existence-of-solutions problem is NP-complete. We obtain analogous complexity results for the data complexity of computing the certain answers of arithmetic conjunctive queries and linear arithmetic conjunctive queries.

In the last chapter, we considered the theory IΔ 0 built in the language L A , whose axioms are those of Q, plus (the universal closures of) all instances of the Induction Schema for Δ 0 predicates. Now we lift that restriction on induction, and allow any L A predicate to appear in instances of the Schema. The result is (first-order) Peano Arithmetic. Being generous with induction (a) Given what we said in Section 9.1(a) about the motivation for the induction principle, any instance of the Induction Schema will be intuitively acceptable as an axiom, so long as we replace φ in the Schema by a suitable open wff which expresses a genuine property/relation. We argued at the beginning of the last chapter that Δ 0 wffs are eminently suitable, and we considered the theory you get by adding to Q the instances of the Induction Schema involving such wffs. But why should we be so very restrictive? Take any open wff φ of L A at all. This will be built from no more than the constant term ‘0’, the familiar successor, addition and multiplication functions, plus identity and other logical apparatus. Therefore – you might very well suppose – it ought also to express a perfectly determinate arithmetical property or relation. So why not be generous and allow any open L A wff to be substituted for φ in the Induction Schema? The result of adding to Q (the universal closures of) every instance of the Schema is PA – First-order Peano Arithmetic . (b) …

Sentient Arithmetic is defined as an extension of Elementary Arithmetic with three more derivation rules and the Incompleteness Theorems are derived within it without using any metalanguage. It is shown that Consistency cannot be chosen as an axiom

We prove that a necessary and sufficient condition for a countable set of sets of integers to be equal to the algebra of all sets of integers definable in a nonstandard elementary extension of ω by a formula of the PA language which may include the standardness predicate but does not contain nonstandard parameters, is as follows: is closed under arithmetical definability and contains 0(ω) the set of all (Gödel numbers of) true arithmetical sentences.Some results related to definability of sets of integers in elementary extensions of ω are included.

As is well-known, the formal system in which Frege works in his Grundgesetze der Arithmetik is formally inconsistent, Russell’s Paradox being derivable in it.This system is, except for minor differences, full second-order logic, augmented by a single non-logical axiom, Frege’s Axiom V. It has been known for some time now that the first-order fragment of the theory is consistent. The present paper establishes that both the simple and the ramified predicative second-order fragments are consistent, and that Robinson arithmetic, Q, is relatively interpretable in the simple predicative fragment. The philosophical significance of the result is discussed

We study elementary second order extensions of the theoryID1 of non-iterated inductive definitions and the theoryPAΩ of Peano arithmetic with ordinals. We determine the exact proof-theoretic strength of those extensions and their natural subsystems, and we relate them to subsystems of analysis with arithmetic comprehension plusΠ11 comprehension and bar induction without set parameters.

A new method of “minimal” readability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)—functions f such that HA ⊢ ∀x∃!yA(x, y) ⇒ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of ℒ(HA) with only x,y free—are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the < ε0-recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be < ε0-recursive. The method is extended to intuitionistic finite-type arithmetic, , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived.

The relative strengths of first-order theories axiomatized by transfinite induction, for ordinals less-than e0, and formulas restricted in quantifier complexity, is determined. This is done, in part, by describing the provably recursive functions of such theories. Upper bounds for the provably recursive functions are obtained using model-theoretic techniques. A variety of additional results that come as an application of such techniques are mentioned.

In this paper we study applicative theories of operations and numbers with (and without) the non-constructive minimum operator in the context of a total application operation. We determine the proof-theoretic strength of such theories by relating them to well-known systems like Peano Arithmetic PA and the system (Π∞0-CA)

We prove that in IST, Nelson's internal set theory, the Uniqueness and Collection principles, hold for all (including external) formulas. A corollary of the Collection theorem shows that in IST there are no definable mappings of a set X onto a set Y of greater (not equal) cardinality unless both sets are finite and #(Y) ≤ n #(X) for some standard n. Proofs are based on a rather general technique which may be applied to other nonstandard structures. In particular we prove that in a nonstandard model of PA, Peano arithmetic, every hyperinteger uniquely definable by a formula of the PA language extended by the predicate of standardness, can be defined also by a pure PA formula.