HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
, second-order arithmetic is a collection of
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
atic systems that formalize the
natural number In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called '' cardinal ...
s and their subsets. It is an alternative to
axiomatic set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concern ...
as a foundation for much, but not all, of mathematics. A precursor to second-order arithmetic that involves third-order parameters was introduced by
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many ...
and
Paul Bernays Paul Isaac Bernays (17 October 1888 – 18 September 1977) was a Swiss mathematician who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant and close collaborator of ...
in their book '' Grundlagen der Mathematik''. The standard axiomatization of second-order arithmetic is denoted by Z2. Second-order arithmetic includes, but is significantly stronger than, its
first-order In mathematics and other formal sciences, first-order or first order most often means either: * "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of hig ...
counterpart
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
. Unlike Peano arithmetic, second-order arithmetic allows quantification over sets of natural numbers as well as numbers themselves. Because
real number In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every ...
s can be represented as ( infinite) sets of natural numbers in well-known ways, and because second-order arithmetic allows quantification over such sets, it is possible to formalize the
real number In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every ...
s in second-order arithmetic. For this reason, second-order arithmetic is sometimes called "
analysis Analysis ( : analyses) is the process of breaking a complex topic or substance into smaller parts in order to gain a better understanding of it. The technique has been applied in the study of mathematics and logic since before Aristotle (3 ...
" (Sieg 2013, p. 291). Second-order arithmetic can also be seen as a weak version of
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concern ...
in which every element is either a natural number or a set of natural numbers. Although it is much weaker than
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such ...
, second-order arithmetic can prove essentially all of the results of
classical mathematics In the foundations of mathematics, classical mathematics refers generally to the mainstream approach to mathematics, which is based on classical logic and ZFC set theory. It stands in contrast to other types of mathematics such as constructive ...
expressible in its language. A subsystem of second-order arithmetic is a
theory A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may ...
in the language of second-order arithmetic each axiom of which is a theorem of full second-order arithmetic (Z2). Such subsystems are essential to reverse mathematics, a research program investigating how much of classical mathematics can be derived in certain weak subsystems of varying strength. Much of core mathematics can be formalized in these weak subsystems, some of which are defined below. Reverse mathematics also clarifies the extent and manner in which classical mathematics is nonconstructive.


Definition


Syntax

The language of second-order arithmetic is two-sorted. The first sort of terms and in particular variables, usually denoted by lower case letters, consists of
individual An individual is that which exists as a distinct entity. Individuality (or self-hood) is the state or quality of being an individual; particularly (in the case of humans) of being a person unique from other people and possessing one's own need ...
s, whose intended interpretation is as natural numbers. The other sort of variables, variously called "set variables", "class variables", or even "predicates" are usually denoted by upper-case letters. They refer to classes/predicates/properties of individuals, and so can be thought of as sets of natural numbers. Both individuals and set variables can be quantified universally or existentially. A formula with no bound set variables (that is, no quantifiers over set variables) is called arithmetical. An arithmetical formula may have free set variables and bound individual variables. Individual terms are formed from the constant 0, the unary function ''S'' (the ''
successor function In mathematics, the successor function or successor operation sends a natural number to the next one. The successor function is denoted by ''S'', so ''S''(''n'') = ''n'' +1. For example, ''S''(1) = 2 and ''S''(2) = 3. The successor functio ...
''), and the binary operations + and \cdot (addition and multiplication). The successor function adds 1 to its input. The relations = (equality) and < (comparison of natural numbers) relate two individuals, whereas the relation ∈ (membership) relates an individual and a set (or class). Thus in notation the language of second-order arithmetic is given by the signature \mathcal=\. For example, \forall n (n\in X \rightarrow Sn \in X), is a
well-formed formula In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can ...
of second-order arithmetic that is arithmetical, has one free set variable ''X'' and one bound individual variable ''n'' (but no bound set variables, as is required of an arithmetical formula)—whereas \exists X \forall n(n\in X \leftrightarrow n < SSSSSS0\cdot SSSSSSS0) is a well-formed formula that is not arithmetical, having one bound set variable ''X'' and one bound individual variable ''n''.


Semantics

Several different interpretations of the quantifiers are possible. If second-order arithmetic is studied using the full semantics of second-order logic then the set quantifiers range over all subsets of the range of the number variables. If second-order arithmetic is formalized using the semantics of
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
(Henkin semantics) then any model includes a domain for the set variables to range over, and this domain may be a proper subset of the full powerset of the domain of number variables (Shapiro 1991, pp. 74–75).


Axioms


Basic

The following axioms are known as the ''basic axioms'', or sometimes the ''Robinson axioms.'' The resulting
first-order theory First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quan ...
, known as
Robinson arithmetic In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q i ...
, is essentially
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
without induction. The
domain of discourse In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range. Overview The doma ...
for the quantified variables is the
natural number In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called '' cardinal ...
s, collectively denoted by N, and including the distinguished member 0, called "
zero 0 (zero) is a number representing an empty quantity. In place-value notation such as the Hindu–Arabic numeral system, 0 also serves as a placeholder numerical digit, which works by Multiplication, multiplying digits to the left of 0 by th ...
." The primitive functions are the unary
successor function In mathematics, the successor function or successor operation sends a natural number to the next one. The successor function is denoted by ''S'', so ''S''(''n'') = ''n'' +1. For example, ''S''(1) = 2 and ''S''(2) = 3. The successor functio ...
, denoted by
prefix A prefix is an affix which is placed before the stem of a word. Adding it to the beginning of one word changes it into another word. For example, when the prefix ''un-'' is added to the word ''happy'', it creates the word ''unhappy''. Particul ...
S, and two
binary operation In mathematics, a binary operation or dyadic operation is a rule for combining two elements (called operands) to produce another element. More formally, a binary operation is an operation of arity two. More specifically, an internal binary op ...
s,
addition Addition (usually signified by the plus symbol ) is one of the four basic operations of arithmetic, the other three being subtraction, multiplication and division. The addition of two whole numbers results in the total amount or '' sum'' ...
and
multiplication Multiplication (often denoted by the Multiplication sign, cross symbol , by the mid-line #Notation and terminology, dot operator , by juxtaposition, or, on computers, by an asterisk ) is one of the four Elementary arithmetic, elementary Op ...
, denoted by
infix An infix is an affix inserted inside a word stem (an existing word or the core of a family of words). It contrasts with '' adfix,'' a rare term for an affix attached to the outside of a stem, such as a prefix or suffix. When marking text for i ...
"+" and " \cdot", respectively. There is also a primitive
binary relation In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over sets and is a new set of ordered pairs consisting of elements in and in ...
called
order Order, ORDER or Orders may refer to: * Categorization, the process in which ideas and objects are recognized, differentiated, and understood * Heterarchy, a system of organization wherein the elements have the potential to be ranked a number of ...
, denoted by infix "<". Axioms governing the
successor function In mathematics, the successor function or successor operation sends a natural number to the next one. The successor function is denoted by ''S'', so ''S''(''n'') = ''n'' +1. For example, ''S''(1) = 2 and ''S''(2) = 3. The successor functio ...
and
zero 0 (zero) is a number representing an empty quantity. In place-value notation such as the Hindu–Arabic numeral system, 0 also serves as a placeholder numerical digit, which works by Multiplication, multiplying digits to the left of 0 by th ...
: :1. \forall m m=0 \rightarrow \bot ("the successor of a natural number is never zero") :2. \forall m \forall n m=Sn \rightarrow m=n ("the successor function is
injective In mathematics, an injective function (also known as injection, or one-to-one function) is a function that maps distinct elements of its domain to distinct elements; that is, implies . (Equivalently, implies in the equivalent contrapositi ...
") :3. \forall n =n_\lor_\exists_m_[Sm=n.html" ;"title="m=n.html" ;"title="=n \lor \exists m [Sm=n">=n \lor \exists m [Sm=n">m=n.html" ;"title="=n \lor \exists m [Sm=n">=n \lor \exists m [Sm=n ("every natural number is zero or a successor") Addition defined recursion, recursively: :4. \forall m [m+0=m]. :5. \forall m \forall n [m+Sn = S(m+n)]. Multiplication defined recursively: :6. \forall m [m\cdot 0 = 0]. :7. \forall m \forall n \cdot Sn = (m\cdot n)+m Axioms governing the order relation "<": :8. \forall m <0 \rightarrow \bot ("no natural number is smaller than zero") :9. \forall n \forall m :10. \forall n =n \lor 0 ("every natural number is zero or bigger than zero") :11. \forall m \forall n Sm These axioms are all first-order statements. That is, all variables range over the
natural number In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called '' cardinal ...
s and not sets thereof, a fact even stronger than their being arithmetical. Moreover, there is but one existential quantifier, in Axiom 3. Axioms 1 and 2, together with an axiom schema of induction make up the usual Peano–Dedekind definition of N. Adding to these axioms any sort of axiom schema of induction makes redundant the axioms 3, 10, and 11.


Induction and comprehension schema

If ''φ''(''n'') is a formula of second-order arithmetic with a free number variable ''n'' and possibly other free number or set variables (written ''m'' and ''X''), the induction axiom for ''φ'' is the axiom: :\forall m \forall X ((\varphi(0) \land \forall n (\varphi(n) \rightarrow \varphi(Sn))) \rightarrow \forall n \varphi(n)) The (full) second-order induction scheme consists of all instances of this axiom, over all second-order formulas. One particularly important instance of the induction scheme is when ''φ'' is the formula "n \in X" expressing the fact that ''n'' is a member of ''X'' (''X'' being a free set variable): in this case, the induction axiom for ''φ'' is :\forall X ((0\in X \land \forall n (n\in X \rightarrow Sn\in X)) \rightarrow \forall n (n\in X)) This sentence is called the second-order induction axiom. If ''φ''(''n'') is a formula with a free variable ''n'' and possibly other free variables, but not the variable ''Z'', the comprehension axiom for ''φ'' is the formula :\exists Z \forall n (n\in Z \leftrightarrow \varphi(n)) This axiom makes it possible to form the set Z = \ of natural numbers satisfying ''φ''(''n''). There is a technical restriction that the formula ''φ'' may not contain the variable ''Z'', for otherwise the formula n \not \in Z would lead to the comprehension axiom :\exists Z \forall n ( n \in Z \leftrightarrow n \not \in Z), which is inconsistent. This convention is assumed in the remainder of this article.


The full system

The formal theory of second-order arithmetic (in the language of second-order arithmetic) consists of the basic axioms, the comprehension axiom for every formula ''φ'' (arithmetic or otherwise), and the second-order induction axiom. This theory is sometimes called ''full second-order arithmetic'' to distinguish it from its subsystems, defined below. Because full second-order semantics imply that every possible set exists, the comprehension axioms may be taken to be part of the deductive system when these semantics are employed (Shapiro 1991, p. 66).


Models

This section describes second-order arithmetic with first-order semantics. Thus a model \mathcal of the language of second-order arithmetic consists of a set ''M'' (which forms the range of individual variables) together with a constant 0 (an element of ''M''), a function ''S'' from ''M'' to ''M'', two binary operations + and · on ''M'', a binary relation < on ''M'', and a collection ''D'' of subsets of ''M'', which is the range of the set variables. Omitting ''D'' produces a model of the language of first-order arithmetic. When ''D'' is the full powerset of ''M'', the model \mathcal is called a full model. The use of full second-order semantics is equivalent to limiting the models of second-order arithmetic to the full models. In fact, the axioms of second-order arithmetic have only one full model. This follows from the fact that the
Peano axioms In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
with the second-order induction axiom have only one model under second-order semantics.


Definable functions

The first-order functions that are provably total in second-order arithmetic are precisely the same as those representable in
system F System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorph ...
(Girard and Taylor 1987, pp. 122–123). Almost equivalently, system F is the theory of functionals corresponding to second-order arithmetic in a manner parallel to how Gödel's system T corresponds to first-order arithmetic in the Dialectica interpretation.


More types of models

When a model of the language of second-order arithmetic has certain properties, it can also be called these other names: *When ''M'' is the usual set of natural numbers with its usual operations, \mathcal is called an ω-model. In this case, the model may be identified with ''D'', its collection of sets of naturals, because this set is enough to completely determine an ω-model. The unique full \omega-model, which is the usual set of natural numbers with its usual structure and all its subsets, is called the intended or standard model of second-order arithmetic. *A model M of the language of second-order arithmetic is called a β-model if M\prec_1^1\mathcal P(\omega), i.e. the Σ11-statements with parameters from M that are satisfied by M are the same as those satisfied by the full model.W. Marek
Stable sets, a characterization of β2-models of full second-order arithmetic and some related facts
(1973, pp.176-177). Accessed 2021 November 4.
Some notions that are absolute with respect to β-models include "A\subseteq\omega\times\omega encodes a well-order" and "A\subseteq\omega\times\omega is a tree". *The above result has been extended to the concept of a β''n''-model for n\in\mathbb N, which has the same definition as the above except \prec_1^1 is replaced by \prec_n^1, i.e. \Sigma_1^1 is replaced by \Sigma_n^1. Using this definition β0-models are the same as ω-models.


Subsystems

There are many named subsystems of second-order arithmetic. A subscript 0 in the name of a subsystem indicates that it includes only a restricted portion of the full second-order induction scheme (Friedman 1976). Such a restriction lowers the
proof-theoretic strength In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has ...
of the system significantly. For example, the system ACA0 described below is equiconsistent with
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
. The corresponding theory ACA, consisting of ACA0 plus the full second-order induction scheme, is stronger than Peano arithmetic.


Arithmetical comprehension

Many of the well-studied subsystems are related to closure properties of models. For example, it can be shown that every ω-model of full second-order arithmetic is closed under Turing jump, but not every ω-model closed under Turing jump is a model of full second-order arithmetic. The subsystem ACA0 includes just enough axioms to capture the notion of closure under Turing jump. ACA0 is defined as the theory consisting of the basic axioms, the arithmetical comprehension axiom scheme (in other words the comprehension axiom for every ''arithmetical'' formula ''φ'') and the ordinary second-order induction axiom. It would be equivalent to include the entire arithmetical induction axiom scheme, in other words to include the induction axiom for every arithmetical formula ''φ''. It can be shown that a collection ''S'' of subsets of ω determines an ω-model of ACA0 if and only if ''S'' is closed under Turing jump, Turing reducibility, and Turing join (Simpson 2009, pp. 311–313). The subscript 0 in ACA0 indicates that not every instance of the induction axiom scheme is included this subsystem. This makes no difference for ω-models, which automatically satisfy every instance of the induction axiom. It is of importance, however, in the study of non-ω-models. The system consisting of ACA0 plus induction for all formulas is sometimes called ACA with no subscript. The system ACA0 is a conservative extension of first-order arithmetic (or first-order Peano axioms), defined as the basic axioms, plus the first-order induction axiom scheme (for all formulas ''φ'' involving no class variables at all, bound or otherwise), in the language of first-order arithmetic (which does not permit class variables at all). In particular it has the same proof-theoretic ordinal ε0 as first-order arithmetic, owing to the limited induction schema.


The arithmetical hierarchy for formulas

A formula is called ''bounded arithmetical'', or Δ00, when all its quantifiers are of the form ∀''n''<''t'' or ∃''n''<''t'' (where ''n'' is the individual variable being quantified and ''t'' is an individual term), where :\forall n stands for :\forall n(n and :\exists n stands for :\exists n(n. A formula is called Σ01 (or sometimes Σ1), respectively Π01 (or sometimes Π1) when it of the form ∃''m''(''φ''), respectively ∀''m''(''φ'') where ''φ'' is a bounded arithmetical formula and ''m'' is an individual variable (that is free in ''φ''). More generally, a formula is called Σ0''n'', respectively Π0''n'' when it is obtained by adding existential, respectively universal, individual quantifiers to a Π0''n''−1, respectively Σ0''n''−1 formula (and Σ00 and Π00 are all equivalent to Δ00). By construction, all these formulas are arithmetical (no class variables are ever bound) and, in fact, by putting the formula in Skolem prenex form one can see that every arithmetical formula is equivalent to a Σ0''n'' or Π0''n'' formula for all large enough ''n''.


Recursive comprehension

The subsystem RCA0 is a weaker system than ACA0 and is often used as the base system in reverse mathematics. It consists of: the basic axioms, the Σ01 induction scheme, and the Δ01 comprehension scheme. The former term is clear: the Σ01 induction scheme is the induction axiom for every Σ01 formula ''φ''. The term "Δ01 comprehension" is more complex, because there is no such thing as a Δ01 formula. The Δ01 comprehension scheme instead asserts the comprehension axiom for every Σ01 formula which is equivalent to a Π01 formula. This scheme includes, for every Σ01 formula ''φ'' and every Π01 formula ψ, the axiom: :\forall m \forall X ((\forall n (\varphi(n) \leftrightarrow \psi(n))) \rightarrow \exists Z \forall n (n\in Z \leftrightarrow \varphi(n))) The set of first-order consequences of RCA0 is the same as those of the subsystem IΣ1 of Peano arithmetic in which induction is restricted to Σ01 formulas. In turn, IΣ1 is conservative over
primitive recursive arithmetic Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician , reprinted in translation in as a formalization of his finitist conception of the foundations of ...
(PRA) for \Pi^0_2 sentences. Moreover, the proof-theoretic ordinal of \mathrm_0 is ωω, the same as that of PRA. It can be seen that a collection ''S'' of subsets of ω determines an ω-model of RCA0 if and only if ''S ''is closed under Turing reducibility and Turing join. In particular, the collection of all computable subsets of ω gives an ω-model of RCA0. This is the motivation behind the name of this system—if a set can be proved to exist using RCA0, then the set is recursive (i.e. computable).


Weaker systems

Sometimes an even weaker system than RCA0 is desired. One such system is defined as follows: one must first augment the language of arithmetic with an exponential function (in stronger systems the exponential can be defined in terms of addition and multiplication by the usual trick, but when the system becomes too weak this is no longer possible) and the basic axioms by the obvious axioms defining exponentiation inductively from multiplication; then the system consists of the (enriched) basic axioms, plus Δ01 comprehension, plus Δ00 induction.


Stronger systems

Over ACA0, each formula of second-order arithmetic is equivalent to a Σ1''n'' or Π1''n'' formula for all large enough ''n''. The system Π11-comprehension is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every ( boldfaceP. D. Welch
"Weak Systems of Determinacy and Arithmetical Quasi-Inductive Definitions"
(2010 draft ver., p. 3). Accessed 31 July 2022.
) Π11 formula ''φ''. This is equivalent to Σ11-comprehension (on the other hand, Δ11-comprehension, defined analogously to Δ01-comprehension, is weaker).


Projective determinacy

Projective determinacy In mathematical logic, projective determinacy is the special case of the axiom of determinacy applying only to projective sets. The axiom of projective determinacy, abbreviated PD, states that for any two-player infinite game of perfect informatio ...
is the assertion that every two-player perfect information game with moves being integers, game length ω and projective payoff set is determined, that is one of the players has a winning strategy. (The first player wins the game if the play belongs to the payoff set; otherwise, the second player wins.) A set is projective iff (as a predicate) it is expressible by a formula in the language of second-order arithmetic, allowing real numbers as parameters, so projective determinacy is expressible as a schema in the language of Z2. Many natural propositions expressible in the language of second-order arithmetic are independent of Z2 and even ZFC but are provable from projective determinacy. Examples include coanalytic perfect subset property, measurability and the property of Baire for \Sigma^1_2 sets, \Pi^1_3 uniformization, etc. Over a weak base theory (such as RCA0), projective determinacy implies comprehension and provides an essentially complete theory of second-order arithmetic — natural statements in the language of Z2 that are independent of Z2 with projective determinacy are hard to find (Woodin 2001). ZFC + is conservative over Z2 with projective determinacy, that is a statement in the language of second-order arithmetic is provable in Z2 with projective determinacy iff its translation into the language of set theory is provable in ZFC + .


Coding mathematics

Second-order arithmetic directly formalizes natural numbers and sets of natural numbers. However, it is able to formalize other mathematical objects indirectly via coding techniques, a fact which was first noticed by
Weyl Hermann Klaus Hugo Weyl, (; 9 November 1885 – 8 December 1955) was a German mathematician, theoretical physicist and philosopher. Although much of his working life was spent in Zürich, Switzerland, and then Princeton, New Jersey, he is assoc ...
(Simpson 2009, p. 16). The integers, rational numbers, and real numbers can all be formalized in the subsystem RCA0, along with
complete Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...
separable
metric space In mathematics, a metric space is a set together with a notion of '' distance'' between its elements, usually called points. The distance is measured by a function called a metric or distance function. Metric spaces are the most general setti ...
s and continuous functions between them (Simpson 2009, Chapter II). The research program of reverse mathematics uses these formalizations of mathematics in second-order arithmetic to study the set-existence axioms required to prove mathematical theorems (Simpson 2009, p. 32). For example, the
intermediate value theorem In mathematical analysis, the intermediate value theorem states that if f is a continuous function whose domain contains the interval , then it takes on any given value between f(a) and f(b) at some point within the interval. This has two impor ...
for functions from the reals to the reals is provable in RCA0 (Simpson 2009, p. 87), while the Bolzano–Weierstrass theorem is equivalent to ACA0 over RCA0 (Simpson 2009, p. 34). The aforementioned coding works well for continuous and total functions, as shown in (Kohlenbach 2002, Section 4), assuming a higher-order base theory plus weak Kőnig's lemma. As perhaps expected, in the case of
topology In mathematics, topology (from the Greek words , and ) is concerned with the properties of a geometric object that are preserved under continuous deformations, such as stretching, twisting, crumpling, and bending; that is, without closing ...
or
measure theory In mathematics, the concept of a measure is a generalization and formalization of geometrical measures (length, area, volume) and other common notions, such as mass and probability of events. These seemingly distinct concepts have many simila ...
, coding is not without problems, as explored in e.g. (Hunter, 2008) or (Normann and Sanders, 2019). However, even coding Riemann integrable functions leads to problems: as shown in (Normann and Sanders, 2020), the minimal (comprehension) axioms needed to prove Arzelà's convergence theorem for the Riemann integral are ''very'' different depending on whether one uses second-order codes or third-order functions.


See also

*
Paris–Harrington theorem In mathematical logic, the Paris–Harrington theorem states that a certain combinatorial principle in Ramsey theory, namely the strengthened finite Ramsey theorem, is true, but not provable in Peano arithmetic. This has been described by some (su ...
*
Presburger arithmetic Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omit ...
*
True arithmetic In mathematical logic, true arithmetic is the set of all true first-order statements about the arithmetic of natural numbers. This is the theory associated with the standard model of the Peano axioms in the language of the first-order Peano a ...


References

* Burgess, J. P. (2005),
Fixing Frege
', Princeton University Press. * Buss, S. R. (1998), ''Handbook of proof theory'', Elsevier. * Friedman, H. (1976), "Systems of second order arithmetic with restricted induction," I, II (Abstracts). ''
Journal of Symbolic Logic The '' Journal of Symbolic Logic'' is a peer-reviewed mathematics journal published quarterly by Association for Symbolic Logic. It was established in 1936 and covers mathematical logic. The journal is indexed by ''Mathematical Reviews'', Zentralb ...
'', v. 41, pp. 557– 559
JStor
* Girard, J.-Y. and Taylor (1987),
Proofs and Types
', Cambridge University Press. * Hilbert, D. and Bernays, P. (1934), ''Grundlagen der Mathematik'', Springer-Verlag. * Hunter, James, ''Higher order Reverse Topology'', Dissertation, University of Madison-Wisconsin

'. * Ulrich Kohlenbach, Kohlenbach, U., ''Foundational and mathematical uses of higher types'', Reflections on the foundations of mathematics, Lect. Notes Log., vol. 15, ASL, 2002, pp. 92–116. * Dag Normann and Sam Sanders, ''Representations in measure theory'', arXiv
1902.02756
(2019). * Dag Normann and Sam Sanders, ''On the uncountability of \mathbb'', arxiv

(2020), pp. 37. * Wilfried Sieg, Sieg, W. (2013),
Hilbert's Programs and Beyond
', Oxford University Press. * Shapiro, S. (1991), ''Foundations without foundationalism'', Oxford University Press. * Simpson, S. G. (2009),
Subsystems of second order arithmetic
', 2nd edition, Perspectives in Logic, Cambridge University Press. * Takeuti, G. (1975) ''Proof theory'' {{isbn, 0-444-10492-5 * Woodin, W. H. (2001), "The Continuum Hypothesis, Part I", ''
Notices of the American Mathematical Society ''Notices of the American Mathematical Society'' is the membership journal of the American Mathematical Society (AMS), published monthly except for the combined June/July issue. The first volume appeared in 1953. Each issue of the magazine sinc ...
'', v. 48 n. 6. Formal theories of arithmetic