In mathematical logic, secondorder arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precursor to secondorder arithmetic that involves thirdorder parameters was introduced by David Hilbert and Paul Bernays in their book Grundlagen der Mathematik.^{[1]} The standard axiomatization of secondorder arithmetic is denoted by Z_{2}.
Secondorder arithmetic includes, but is significantly stronger than, its firstorder counterpart Peano arithmetic. Unlike Peano arithmetic, secondorder arithmetic allows quantification over sets of natural numbers as well as numbers themselves. Because real numbers can be represented as (infinite) sets of natural numbers in wellknown ways, and because secondorder arithmetic allows quantification over such sets, it is possible to formalize the real numbers in secondorder arithmetic. For this reason, secondorder arithmetic is sometimes called "analysis".^{[2]}
Secondorder arithmetic can also be seen as a weak version of set theory 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, secondorder arithmetic can prove essentially all of the results of classical mathematics expressible in its language.
A subsystem of secondorder arithmetic is a theory in the language of secondorder arithmetic each axiom of which is a theorem of full secondorder arithmetic (Z_{2}). 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.
YouTube Encyclopedic

1/5Views:42 948737 5931 179 002154 705641 214

How to Solve a Second Order Linear Homogeneous Recurrence Relation(Distinct Real Roots Case)

Second Order Linear Differential Equations

2nd order linear homogeneous differential equations 1  Khan Academy

Undetermined Coefficients: Solving nonhomogeneous ODEs

Method of Undetermined Coefficients  Nonhomogeneous 2nd Order Differential Equations
Transcription
Definition
Syntax
The language of secondorder arithmetic is twosorted. The first sort of terms and in particular variables, usually denoted by lower case letters, consists of individuals, 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 uppercase 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), and the binary operations + and (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 secondorder arithmetic is given by the signature .
For example, , is a wellformed formula of secondorder 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 is a wellformed 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 secondorder arithmetic is studied using the full semantics of secondorder logic then the set quantifiers range over all subsets of the range of the individual variables. If secondorder arithmetic is formalized using the semantics of firstorder logic (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 individual variables.^{[3]}
Axioms
Basic
The following axioms are known as the basic axioms, or sometimes the Robinson axioms. The resulting firstorder theory, known as Robinson arithmetic, is essentially Peano arithmetic without induction. The domain of discourse for the quantified variables is the natural numbers, collectively denoted by N, and including the distinguished member , called "zero."
The primitive functions are the unary successor function, denoted by prefix , and two binary operations, addition and multiplication, denoted by the infix operator "+" and "", respectively. There is also a primitive binary relation called order, denoted by the infix operator "<".
Axioms governing the successor function and zero:
 1. ("the successor of a natural number is never zero")
 2. ("the successor function is injective")
 3. ("every natural number is zero or a successor")
Addition defined recursively:
 4.
 5.
Multiplication defined recursively:
 6.
 7.
Axioms governing the order relation "<":
 8. ("no natural number is smaller than zero")
 9.
 10. ("every natural number is zero or bigger than zero")
 11.
These axioms are all firstorder statements. That is, all variables range over the natural numbers 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 secondorder arithmetic with a free individual variable n and possibly other free individual or set variables (written m_{1},...,m_{k} and X_{1},...,X_{l}), the induction axiom for φ is the axiom:
The (full) secondorder induction scheme consists of all instances of this axiom, over all secondorder formulas.
One particularly important instance of the induction scheme is when φ is the formula "" expressing the fact that n is a member of X (X being a free set variable): in this case, the induction axiom for φ is
This sentence is called the secondorder 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
This axiom makes it possible to form the set of natural numbers satisfying φ(n). There is a technical restriction that the formula φ may not contain the variable Z, for otherwise the formula would lead to the comprehension axiom
 ,
which is inconsistent. This convention is assumed in the remainder of this article.
The full system
The formal theory of secondorder arithmetic (in the language of secondorder arithmetic) consists of the basic axioms, the comprehension axiom for every formula φ (arithmetic or otherwise), and the secondorder induction axiom. This theory is sometimes called full secondorder arithmetic to distinguish it from its subsystems, defined below. Because full secondorder semantics imply that every possible set exists, the comprehension axioms may be taken to be part of the deductive system when full secondorder semantics is employed.^{[3]}
Models
This section describes secondorder arithmetic with firstorder semantics. Thus a model of the language of secondorder 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 firstorder arithmetic.
When D is the full powerset of M, the model is called a full model. The use of full secondorder semantics is equivalent to limiting the models of secondorder arithmetic to the full models. In fact, the axioms of secondorder arithmetic have only one full model. This follows from the fact that the Peano axioms with the secondorder induction axiom have only one model under secondorder semantics.
Definable functions
The firstorder functions that are provably total in secondorder arithmetic are precisely the same as those representable in system F.^{[4]} Almost equivalently, system F is the theory of functionals corresponding to secondorder arithmetic in a manner parallel to how Gödel's system T corresponds to firstorder arithmetic in the Dialectica interpretation.
More types of models
When a model of the language of secondorder 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, 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 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 secondorder arithmetic.^{[5]}
 A model of the language of secondorder arithmetic is called a βmodel if , i.e. the Σ^{1}_{1}statements with parameters from that are satisfied by are the same as those satisfied by the full model.^{[6]} Some notions that are absolute with respect to βmodels include " encodes a wellorder"^{[7]} and " is a tree".^{[6]}
 The above result has been extended to the concept of a β_{n}model for , which has the same definition as the above except is replaced by , i.e. is replaced by .^{[6]} Using this definition β_{0}models are the same as ωmodels.^{[8]}
Subsystems
There are many named subsystems of secondorder arithmetic.
A subscript 0 in the name of a subsystem indicates that it includes only a restricted portion of the full secondorder induction scheme.^{[9]} Such a restriction lowers the prooftheoretic strength of the system significantly. For example, the system ACA_{0} described below is equiconsistent with Peano arithmetic. The corresponding theory ACA, consisting of ACA_{0} plus the full secondorder induction scheme, is stronger than Peano arithmetic.
Arithmetical comprehension
Many of the wellstudied subsystems are related to closure properties of models. For example, it can be shown that every ωmodel of full secondorder arithmetic is closed under Turing jump, but not every ωmodel closed under Turing jump is a model of full secondorder arithmetic. The subsystem ACA_{0} includes just enough axioms to capture the notion of closure under Turing jump.
ACA_{0} 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 secondorder induction axiom. It would be equivalent to also 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 ACA_{0} if and only if S is closed under Turing jump, Turing reducibility, and Turing join.^{[10]}
The subscript 0 in ACA_{0} 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 ACA_{0} plus induction for all formulas is sometimes called ACA with no subscript.
The system ACA_{0} is a conservative extension of firstorder arithmetic (or firstorder Peano axioms), defined as the basic axioms, plus the firstorder induction axiom scheme (for all formulas φ involving no class variables at all, bound or otherwise), in the language of firstorder arithmetic (which does not permit class variables at all). In particular it has the same prooftheoretic ordinal ε_{0} as firstorder arithmetic, owing to the limited induction schema.
The arithmetical hierarchy for formulas
A formula is called bounded arithmetical, or Δ^{0}_{0}, 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
stands for
and
stands for
 .
A formula is called Σ^{0}_{1} (or sometimes Σ_{1}), respectively Π^{0}_{1} (or sometimes Π_{1}) when it is 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 Σ^{0}_{0} and Π^{0}_{0} are both equal to Δ^{0}_{0}). 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 logically equivalent to a Σ^{0}_{n} or Π^{0}_{n} formula for all large enough n.
Recursive comprehension
The subsystem RCA_{0} is a weaker system than ACA_{0} and is often used as the base system in reverse mathematics. It consists of: the basic axioms, the Σ^{0}_{1} induction scheme, and the Δ^{0}_{1} comprehension scheme. The former term is clear: the Σ^{0}_{1} induction scheme is the induction axiom for every Σ^{0}_{1} formula φ. The term "Δ^{0}_{1} comprehension" is more complex, because there is no such thing as a Δ^{0}_{1} formula. The Δ^{0}_{1} comprehension scheme instead asserts the comprehension axiom for every Σ^{0}_{1} formula that is logically equivalent to a Π^{0}_{1} formula. This scheme includes, for every Σ^{0}_{1} formula φ and every Π^{0}_{1} formula ψ, the axiom:
The set of firstorder consequences of RCA_{0} is the same as those of the subsystem IΣ_{1} of Peano arithmetic in which induction is restricted to Σ^{0}_{1} formulas. In turn, IΣ_{1} is conservative over primitive recursive arithmetic (PRA) for sentences. Moreover, the prooftheoretic ordinal of is ω^{ω}, the same as that of PRA.
It can be seen that a collection S of subsets of ω determines an ωmodel of RCA_{0} 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 RCA_{0}. This is the motivation behind the name of this system—if a set can be proved to exist using RCA_{0}, then the set is recursive (i.e. computable).
Weaker systems
Sometimes an even weaker system than RCA_{0} is desired. One such system is defined as follows: one must first augment the language of arithmetic with an exponential function symbol (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 Δ^{0}_{1} comprehension, plus Δ^{0}_{0} induction.
Stronger systems
Over ACA_{0}, each formula of secondorder arithmetic is equivalent to a Σ^{1}_{n} or Π^{1}_{n} formula for all large enough n. The system Π^{1}_{1}comprehension is the system consisting of the basic axioms, plus the ordinary secondorder induction axiom and the comprehension axiom for every (boldface^{[11]}) Π^{1}_{1} formula φ. This is equivalent to Σ^{1}_{1}comprehension (on the other hand, Δ^{1}_{1}comprehension, defined analogously to Δ^{0}_{1}comprehension, is weaker).
Projective determinacy
Projective determinacy is the assertion that every twoplayer perfect information game with moves being natural numbers, 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 if and only if (as a predicate) it is expressible by a formula in the language of secondorder arithmetic, allowing real numbers as parameters, so projective determinacy is expressible as a schema in the language of Z_{2}.
Many natural propositions expressible in the language of secondorder arithmetic are independent of Z_{2} and even ZFC but are provable from projective determinacy. Examples include coanalytic perfect subset property, measurability and the property of Baire for sets, uniformization, etc. Over a weak base theory (such as RCA_{0}), projective determinacy implies comprehension and provides an essentially complete theory of secondorder arithmetic — natural statements in the language of Z_{2} that are independent of Z_{2} with projective determinacy are hard to find.^{[12]}
ZFC + {there are n Woodin cardinals: n is a natural number} is conservative over Z_{2} with projective determinacy^{[citation needed]}, that is a statement in the language of secondorder arithmetic is provable in Z_{2} with projective determinacy if and only if its translation into the language of set theory is provable in ZFC + {there are n Woodin cardinals: n∈N}.
Coding mathematics
Secondorder 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 that was first noticed by Weyl.^{[13]} The integers, rational numbers, and real numbers can all be formalized in the subsystem RCA_{0}, along with complete separable metric spaces and continuous functions between them.^{[14]}
The research program of reverse mathematics uses these formalizations of mathematics in secondorder arithmetic to study the setexistence axioms required to prove mathematical theorems.^{[15]} For example, the intermediate value theorem for functions from the reals to the reals is provable in RCA_{0},^{[16]} while the Bolzano–Weierstrass theorem is equivalent to ACA_{0} over RCA_{0}.^{[17]}
The aforementioned coding works well for continuous and total functions, assuming a higherorder base theory plus weak Kőnig's lemma.^{[18]} As perhaps expected, in the case of topology, coding is not without problems.^{[19]}
See also
References
 ^ Hilbert, D.; Bernays, P. (1934). Grundlagen der Mathematik. SpringerVerlag. MR 0237246.
 ^ Sieg, W. (2013). Hilbert's Programs and Beyond. Oxford University Press. p. 291. ISBN 9780199707157.
 ^ ^{a} ^{b} Shapiro, Stewart (1991). Foundations Without Foundationalism: A Case for SecondOrder Logic. Oxford Logic Guides. Vol. 17. The Clarendon Press, Oxford University Press, New York. pp. 66, 74–75. ISBN 0198533918. MR 1143781.
 ^ Girard, JeanYves (1987). Proofs and Types. Translated by Taylor, Paul. Cambridge University Press. pp. 122–123. ISBN 0521371813.
 ^ Simpson, S. G. (2009). Subsystems of Second Order Arithmetic. Perspectives in Logic (2nd ed.). Cambridge University Press. pp. 3–4. ISBN 9780521884396. MR 2517689.
 ^ ^{a} ^{b} ^{c} Marek, W. (1974–1975). "Stable sets, a characterization of β_{2}models of full second order arithmetic and some related facts". Fundamenta Mathematicae. 82: 175–189. doi:10.4064/fm822175189. MR 0373897.
 ^ Marek, W. (1978). "ωmodels of second order arithmetic and admissible sets". Fundamenta Mathematicae. 98 (2): 103–120. doi:10.4064/fm982103120. MR 0476490.
 ^ Marek, W. (1973). "Observations concerning elementary extensions of ωmodels. II". The Journal of Symbolic Logic. 38: 227–231. doi:10.2307/2272059. JSTOR 2272059. MR 0337612.
 ^ Friedman, H. (1976). "Systems of second order arithmetic with restricted induction, I, II". Meeting of the Association for Symbolic Logic. Journal of Symbolic Logic (Abstracts). 41: 557–559. JSTOR 2272259.
 ^ Simpson 2009, pp. 311–313.
 ^ Welch, P. D. (2011). "Weak systems of determinacy and arithmetical quasiinductive definitions" (PDF). The Journal of Symbolic Logic. 76 (2): 418–436. doi:10.2178/jsl/1305810756. MR 2830409.
 ^ Woodin, W. H. (2001). "The Continuum Hypothesis, Part I". Notices of the American Mathematical Society. 48 (6).
 ^ Simpson 2009, p. 16.
 ^ Simpson 2009, Chapter II.
 ^ Simpson 2009, p. 32.
 ^ Simpson 2009, p. 87.
 ^ Simpson 2009, p. 34.
 ^ Kohlenbach, Ulrich (2002). "Foundational and mathematical uses of higher types". Reflections on the Foundations of Mathematics: Essays in honor of Solomon Feferman, Papers from the symposium held at Stanford University, Stanford, CA, December 11–13, 1998. Lecture Notes in Logic. Vol. 15. Urbana, Illinois: Association for Symbolic Logic. pp. 92–116. ISBN 1568811691. MR 1943304.
 ^ Hunter, James (2008). Higher order Reverse Topology (PDF) (Doctoral dissertation). University of MadisonWisconsin.
Further reading
 Burgess, J. P. (2005). Fixing Frege. Princeton University Press.
 Buss, S. R. (1998). Handbook of Proof Theory. Elsevier. ISBN 0444898409.
 Takeuti, G. (1975). Proof Theory. ISBN 0444104925.