Formal mathematical analysis

An axiomatic theory aimed at formalizing (cf. Formalization method) mathematical analysis. The aim is to construct a formal axiomatic theory with minimum possible deductive and expressive strength, but still sufficient for formalizing all the traditional material of mathematical analysis.

The most extensively developed version of formal mathematical analysis, due to D. Hilbert and P. Bernays (see [1]), can be described as follows. To the language of classical formal arithmetic (cf. Arithmetic, formal) one adds a new kind of variables $X,Y,Z,\dots,$ which are regarded as running over sets of natural numbers. One adds a new kind of atomic formulas: $(t\in X)$ ("belonging to the set X"). The logical axioms of formal arithmetic and the axiom scheme of induction are naturally strengthened in such a way as to include the formulas of the extended language. Finally, one adds a single new axiom scheme — the axiom scheme of comprehension:

$$\exists X\forall y(y\in X\equiv A(y)),$$

where $A(y)$ is a formula of the language in question not containing $X$ freely and $y$ is a variable for a natural number.

This theory (the so-called Hilbert–Bernays theory; in it one speaks of natural numbers and sets of natural numbers) is sufficient for a natural formalization of mathematical analysis. It is an interesting problem to provide a foundation for the consistency of the Hilbert–Bernays theory by methods that are constructive to a sufficient degree. According to the Gödel incompleteness theorem, this cannot be done without using means that go beyond the limits of formal mathematical analysis. C. Spector (see [3]) succeeded in proving the consistency of this theory by means of a modification of the Gödel interpretation for intuitionistic arithmetic (see Gödel interpretation of intuitionistic arithmetic), which is a certain far-reaching extension of the requirements of intuitionism. The fundamental difficulties in attempts to prove the consistency of the Hilbert–Bernays theory are connected with a special feature of the comprehension axiom of that theory, i.e. that in the formula $A(y)$ occurring in the axiom scheme of comprehension one is allowed to make free use of quantifiers over sets. Thus, in clarifying whether a number $y$ belongs to a set $X$ being defined in the axiom, it is necessary to use the availability of all sets of natural numbers, among which is the set $X$ that is being defined. One could say that the comprehension axiom of formal analysis expresses to a certain degree the necessity for all sets actually to exist simultaneously.

This special feature (it is encountered in several set-theoretic formal theories) is called non-predicativity of a theory. Hilbert–Bernays formal analysis is a non-predicative analysis.

In order to remove the non-predicativity, various formal axiomatic theories of predicative (or ramified) analysis have been proposed. For example, in one of the most widely used formulations, going back to H. Weyl, one considers variables of the form $X^m,Y^k,\dots,$ with natural numbers as the superscripts. The variables are regarded as running over sets of natural numbers. The axiom scheme of comprehension in this theory has the form

$$\exists X^m\forall y(y\in X^m\equiv A(y)),$$

where the bound set variables in $A(y)$ have index $<m$, and the free set variables have index $\leq m$. Thus, sets of natural numbers in predicative analysis, essentially speaking, split (are "ramified") into layers, with sets in a higher layer being defined only in terms of sets in lower layers (and sets in the given layer that have already been defined). It is comparatively easy to prove the consistency of ramified analysis by constructive methods, but the simplicity of this theory is achieved at a high price: ramified analysis is less well-suited to formalization, and the analogue of a theorem of formal mathematical analysis always assumes an unnatural form in predicative analysis. E.g., the least upper bound of a bounded set of real numbers is defined in an essentially non-predicative way.

There is an equivalent formulation of non-predicative Hilbert–Bernays analysis in which functions mapping natural numbers to natural numbers figure along with sets of natural numbers. Namely, for functions of this kind one adjoins to formal arithmetic the variables $\alpha,\beta,\gamma,\dots,$ and a new kind of terms: $\alpha(t)$ ("the result of applying a to t"); the logical axioms and the axiom scheme of induction are naturally extended to the formulas of the new language, and, finally, one adds a single new axiom, the so-called axiom of choice in analysis:

$$\forall x\exists yA(x,y)\supset\exists\alpha\forall xA(x,\alpha(x)),$$

which asserts that if for all $x$ there is a $y$ satisfying the condition $A(x,y)$, then there is a function $\alpha$ that, for any $x$, picks a corresponding $y$. The merit of this formulation is that, after excluding the law of the excluded middle from the logical axioms, the system one obtains is convenient for the formalization of intuitionistic or constructive formal mathematical analysis. Intuitionistic (respectively, constructive) formal mathematical analysis is a reworking of traditional mathematics according to the demands of the program of intuitionism (respectively, constructive mathematics). In formalizing these disciplines one admits the possibility of treating the variables $\alpha,\beta,\gamma,\dots,$ as only running over functions that are "effective" in some sense or other, for example, intuitionistic choice sequences. In this interpretation the axiom of choice in analysis is a true assertion. To develop substantial areas of analysis one supplements this theory with new axioms expressing specific intuitionistic or constructive principles such as bar induction or the constructive selection principle of A.A. Markov.

References[edit]

Comments[edit]

The formal axiomatic theory called above "formal mathematical analysis" is also known as second-order arithmetic or second-order Peano arithmetic.