Arithmetic and the theory of types

1984 ◽  
Vol 49 (2) ◽  
pp. 621-624 ◽  
Author(s):  
M. Boffa

A hundred years ago, Frege proposed a logical definition of the natural numbers based on the following idea:He replaced this circular definition by the following one:He tried afterwards to found his theory over a notion of class satisfying a general comprehension principle:Russell quickly derived a contradiction from this principle (the famous Russell's paradox) but saved Frege's arithmetic with his theory of types based on the following comprehension principle:In 1979, talking at the Claude Bernard University in Lyon, I remarked that 3 types suffice to provide Frege's arithmetic, showing in fact that PA2 (second order Peano arithmetic) holds in TT3 + AI (theory of types 0, 1, 2 plus a suitable axiom of infinity). I asked whether TT3 + AI was a conservative extension of PA2. Pabion [3] gave a positive answer by a subtle use of the Fraenkel-Moskowski method. This result will be improved in the present paper, with a view to getting models of NF3 + AI in which Frege's arithmetic forms a model isomorphic to a given countable model of PA2.

2018 ◽  
Vol 83 (04) ◽  
pp. 1501-1511 ◽  
Author(s):  
ATHAR ABDUL-QUADER

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


1977 ◽  
Vol 42 (2) ◽  
pp. 238-240 ◽  
Author(s):  
D. van Dalen

The comprehension principle of second order arithmetic asserts the existence of certain species (sets) corresponding to properties of natural numbers. In the intuitionistic theory of sequences of natural numbers there is an analoguous principle, implicit in Brouwer's writing and explicitly stated by Kripke, which asserts the existence of certain sequences corresponding to statements. The justification of this principle, Kripke's Schema, makes use of the concept of the so-called creative subject. For more information the reader is referred to Troelstra [5].Kripke's Schema readsThere is a weaker versionThe idea to reduce species to sequences via Kripke's schema occurred several years ago (cf. [2, p. 128], [5, p. 104]). In [1] the reduction technique was applied in the construction of a model for HAS.On second thought, however, I realized that there is a straightforward, simpler way to exploit Kripke's schema, avoiding models altogether. The idea to present this material separately was forced on the author by C. Smorynski.Consider a second order arithmetic with both species and sequence variables. By KS we have(for convenience we restrict ourselves in KS to 0-1-sequences). An application of AC-NF givesOf course ξ is not uniquely determined. This is the key to the reduction of full second order arithmetic, or HAS, to a theory of sequences.We now introduce a translation τ to eliminate species variables. It is no restriction to suppose that the formulae contain only the sequence variables ξ1, ξ3, ξ5, …Note that by virtue of the definition of τ the axiom of extensionality is automatically verified after translation. The translation τ eliminates the species variables and leaves formulae without species variables invariant.


2001 ◽  
Vol 66 (3) ◽  
pp. 1353-1358 ◽  
Author(s):  
Christopher S. Hardin ◽  
Daniel J. Velleman

This paper is a contribution to the project of determining which set existence axioms are needed to prove various theorems of analysis. For more on this project and its history we refer the reader to [1] and [2].We work in a weak subsystem of second order arithmetic. The language of second order arithmetic includes the symbols 0, 1, =, <, +, ·, and ∈, together with number variables x, y, z, … (which are intended to stand for natural numbers), set variables X, Y, Z, … (which are intended to stand for sets of natural numbers), and the usual quantifiers (which can be applied to both kinds of variables) and logical connectives. We write ∀x < t φ and ∃x < t φ as abbreviations for ∀x(x < t → φ) and ∃x{x < t ∧ φ) respectively; these are called bounded quantifiers. A formula is said to be if it has no quantifiers applied to set variables, and all quantifiers applied to number variables are bounded. It is if it has the form ∃xθ and it is if it has the form ∀xθ, where in both cases θ is .The theory RCA0 has as axioms the usual Peano axioms, with the induction scheme restricted to formulas, and in addition the comprehension scheme, which consists of all formulas of the formwhere φ is , ψ is , and X does not occur free in φ(n). (“RCA” stands for “Recursive Comprehension Axiom.” The reason for the name is that the comprehension scheme is only strong enough to prove the existence of recursive sets.) It is known that this theory is strong enough to allow the development of many of the basic properties of the real numbers, but that certain theorems of elementary analysis are not provable in this theory. Most relevant for our purposes is the fact that it is impossible to prove in RCA0 that every continuous function on the closed interval [0, 1] attains maximum and minimum values (see [1]).Since the most common proof of the Mean Value Theorem makes use of this theorem, it might be thought that the Mean Value Theorem would also not be provable in RCA0. However, we show in this paper that the Mean Value Theorem can be proven in RCA0. All theorems stated in this paper are theorems of RCA0, and all of our reasoning will take place in RCA0.


1939 ◽  
Vol 4 (2) ◽  
pp. 77-79 ◽  
Author(s):  
C. H. Langford

It is known that the usual definition of a dense series without extreme elements is complete with respect to first-order functions, in the sense that any first-order function on the base of a set of postulates defining such a series either is implied by the postulates or is inconsistent with them. It is here understood, in accordance with the usual convention, that when we speak of a function on the base , the function shall be such as to place restrictions only upon elements belonging to the class determined by f; or, more exactly, every variable with a universal prefix shall occur under the hypothesis that its values satisfy f, while every variable with an existential prefix shall have this condition categorically imposed upon it.Consider a set of postulates defining a dense series without extreme elements, and add to this set the condition of Dedekind section, to be formulated as follows. Let the conjunction of the three functions,be written H(ϕ), where the free variables f and g, being parameters throughout, are suppressed. This is the hypothesis of Dedekind's condition, and the conclusion iswhich may be written C(ϕ).


2016 ◽  
Vol 13 (5) ◽  
Author(s):  
Farida Kachapova

This paper describes axiomatic theories SA and SAR, which are versions of second order arithmetic with countably many sorts for sets of natural numbers. The theories are intended to be applied in reverse mathematics because their multi-sorted language allows to express some mathematical statements in more natural form than in the standard second order arithmetic. We study metamathematical properties of the theories SA, SAR and their fragments. We show that SA is mutually interpretable with the theory of arithmetical truth PATr obtained from the Peano arithmetic by adding infinitely many truth predicates. Corresponding fragments of SA and PATr are also mutually interpretable. We compare the proof-theoretical strengths of the fragments; in particular, we show that each fragment SAs with sorts <=s is weaker than next fragment SAs+1.


2013 ◽  
Vol 35 (4) ◽  
pp. 1208-1228 ◽  
Author(s):  
PAUL GLENDINNING ◽  
NIKITA SIDOROV

AbstractLet $0\lt a\lt b\lt 1$ and let $T$ be the doubling map. Set $ \mathcal{J} (a, b): = \{ x\in [0, 1] : {T}^{n} x\not\in (a, b), n\geq 0\} $. In this paper we completely characterize the holes $(a, b)$ for which any of the following scenarios hold: (i) $ \mathcal{J} (a, b)$ contains a point $x\in (0, 1)$; (ii) $ \mathcal{J} (a, b)\cap [\delta , 1- \delta ] $ is infinite for any fixed $\delta \gt 0$; (iii) $ \mathcal{J} (a, b)$ is uncountable of zero Hausdorff dimension; (iv) $ \mathcal{J} (a, b)$ is of positive Hausdorff dimension. In particular, we show that (iv) is always the case if $$\begin{eqnarray*}b- a\lt \frac{1}{4} { \mathop{\prod }\nolimits}_{n= 1}^{\infty } (1- {2}^{- {2}^{n} } )\approx 0. 175\hspace{0.167em} 092\end{eqnarray*}$$ and that this bound is sharp. As a corollary, we give a full description of first- and second-order critical holes introduced by N. Sidorov [Supercritical holes for the doubling map. Preprint, see http://arxiv.org/abs/1204.1920] for the doubling map. Furthermore, we show that our model yields a continuum of ‘routes to chaos’ via arbitrary sequences of products of natural numbers, thus generalizing the standard route to chaos via period doubling.


2016 ◽  
Vol 10 (1) ◽  
pp. 80-91
Author(s):  
GRAHAM LEACH-KROUSE

AbstractIt’s well known that it’s possible to extract, from Frege’s Grudgesetze, an interpretation of second-order Peano Arithmetic in the theory $H{P^2}$, whose sole axiom is Hume’s principle. What’s less well known is that, in Die Grundlagen Der Arithmetic §82–83 Boolos (2011), George Boolos provided a converse interpretation of $H{P^2}$ in $P{A^2}$. Boolos’ interpretation can be used to show that the Frege’s construction allows for any model of $P{A^2}$ to be recovered from some model of $H{P^2}$. So the space of possible arithmetical universes is precisely characterized by Hume’s principle.In this paper, I show that a large class of second-order theories admit characterization by an abstraction principle in this sense. The proof makes use of structural abstraction principles, a class of abstraction principles of considerable intrinsic interest, and categories of interpretations in the sense of Visser (2003).


2009 ◽  
Vol 2 (4) ◽  
pp. 799-815 ◽  
Author(s):  
MARTIN FISCHER

In this paper we will investigate different axiomatic theories of truth that are minimal in some sense. One criterion for minimality will be conservativity over Peano Arithmetic. We will then give a more fine-grained characterization by investigating some interpretability relations. We will show that disquotational theories of truth, as well as compositional theories of truth with restricted induction are relatively interpretable in Peano Arithmetic. Furthermore, we will give an example of a theory of truth that is a conservative extension of Peano Arithmetic but not interpretable in it. We will then use stricter versions of interpretations to compare weak theories of truth to subsystems of second-order arithmetic.


2018 ◽  
Vol 12 (1) ◽  
pp. 97-143 ◽  
Author(s):  
MARCO PANZA ◽  
ANDREA SERENI

AbstractRecent discussions on Fregean and neo-Fregean foundations for arithmetic and real analysis pay much attention to what is called either ‘Application Constraint’ ($AC$) or ‘Frege Constraint’ ($FC$), the requirement that a mathematical theory be so outlined that it immediately allows explaining for its applicability. We distinguish between two constraints, which we, respectively, denote by the latter of these two names, by showing how$AC$generalizes Frege’s views while$FC$comes closer to his original conceptions. Different authors diverge on the interpretation of$FC$and on whether it applies to definitions of both natural and real numbers. Our aim is to trace the origins of$FC$and to explore how different understandings of it can be faithful to Frege’s views about such definitions and to his foundational program. After rehearsing the essential elements of the relevant debate (§1), we appropriately distinguish$AC$from$FC$(§2). We discuss six rationales which may motivate the adoption of different instances of$AC$and$FC$(§3). We turn to the possible interpretations of$FC$(§4), and advance a Semantic$FC$(§4.1), arguing that while it suits Frege’s definition of natural numbers (4.1.1), it cannot reasonably be imposed on definitions of real numbers (§4.1.2), for reasons only partly similar to those offered by Crispin Wright (§4.1.3). We then rehearse a recent exchange between Bob Hale and Vadim Batitzky to shed light on Frege’s conception of real numbers and magnitudes (§4.2). We argue that an Architectonic version of$FC$is indeed faithful to Frege’s definition of real numbers, and compatible with his views on natural ones. Finally, we consider how attributing different instances of$FC$to Frege and appreciating the role of the Architectonic$FC$can provide a more perspicuous understanding of his foundational program, by questioning common pictures of his logicism (§5).


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.


Sign in / Sign up

Export Citation Format

Share Document