Кері математика: Теоремалардан аксиомаларға қарай зерттеулер

Branch of mathematical logic

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the axiom of choice and Zorn's lemma are equivalent over ZF set theory. The goal of reverse mathematics, however, is to study possible axioms of ordinary theorems of mathematics rather than possible axioms for set theory. Reverse mathematics is usually carried out using subsystems of second order arithmetic, where many of its definitions and methods are inspired by previous work in constructive analysis and proof theory. The use of second order arithmetic also allows many techniques from recursion theory to be employed; many results in reverse mathematics have corresponding results in computable analysis. In higher order reverse mathematics, the focus is on subsystems of higher order arithmetic, and the associated richer language. The program was founded by and brought forward by Steve Simpson. A standard reference for the subject is , while an introduction for non specialists is An introduction to higher order reverse mathematics, and also the founding paper, is .

In reverse mathematics, one starts with a framework language and a base theory—a core axiom system—that is too weak to prove most of the theorems one might be interested in, but still powerful enough to develop the definitions necessary to state these theorems. For example, to study the theorem “Every bounded sequence of real numbers has a supremum” it is necessary to use a base system that can speak of real numbers and sequences of real numbers. For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem. To show that a system S is required to prove a theorem T, two proofs are required. The first proof shows T is provable from S; this is an ordinary mathematical proof along with a justification that it can be carried out in the system S. The second proof, known as a reversal, shows that T itself implies S; this proof is carried out in the base system. For instance, the base theory of higher order reverse mathematics, called , proves the same sentences as RCA0, up to language. As noted in the previous paragraph, second order comprehension axioms easily generalize to the higher order framework. However, theorems expressing the compactness of basic spaces behave quite differently in second and higher order arithmetic: on one hand, when restricted to countable covers/the language of second order arithmetic, the compactness of the unit interval is provable in WKL0 from the next section. On the other hand, given uncountable covers/the language of higher order arithmetic, the compactness of the unit interval is only provable from (full) second order arithmetic. Other covering lemmas (e. g. due to Lindelöf, Vitali, Besicovitch, etc.) exhibit the same behavior, and many basic properties of the gauge integral are equivalent to the compactness of the underlying space.

Second order arithmetic is a formal theory of the natural numbers and sets of natural numbers. Many mathematical objects, such as countable rings, groups, and fields, as well as points in effective Polish spaces, can be represented as sets of natural numbers, and modulo this representation can be studied in second order arithmetic. Reverse mathematics makes use of several subsystems of second order arithmetic. A typical reverse mathematics theorem shows that a particular mathematical theorem T is equivalent to a particular subsystem S of second order arithmetic over a weaker subsystem B. This weaker system B is known as the base system for the result; in order for the reverse mathematics result to have
meaning, this system must not itself be able to prove the mathematical theorem T.

describes five particular subsystems of second order arithmetic, which he calls the Big Five, that occur frequently in reverse mathematics. In order of increasing strength, these systems are named by the initialisms RCA0, WKL0, ACA0, ATR0, and Π CA0. The following table summarizes the "big five" systems and lists the counterpart systems in higher order arithmetic. p.40
Any partial function can be extended to a total function. Various theorems in combinatorics, such as certain forms of Ramsey's theorem.

The ω in ω model stands for the set of non negative integers (or finite ordinals). An ω model is a model for a fragment of second order arithmetic whose first order part is the standard model of Peano arithmetic, but whose second order part may be non standard. More precisely, an ω model is given by a choice of subsets of The first order variables are interpreted in the usual way as elements of , and , have their usual meanings, while second order variables are interpreted as elements of There is a standard ω model where one just takes to consist of all subsets of the integers. However, there are also other ω models; for example, RCA0 has a minimal ω model where consists of the recursive subsets of
A β model is an ω model that agrees with the standard ω model on truth of and sentences (with parameters). Non ω models are also useful, especially in the proofs of conservation theorems.