On the relation between classical and construetive analysis

M. G. Gelfond

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part V, Tome 32 (1972), pp. 5-11

Résumé

The relation of the classical and constructive variants of development of differential and integral calculus is investigated in this paper. A formal language $\Omega$ for this calculus and a class $K$ of $Q$-sentences are described such that the provability of a formula $F$ from $K$ in certain classical calculus $A$ implies the constructive validity of a natural constructive interpretation of $F$. The language $\Omega$ contains in particular the variables for real numbers and real functions which under constructive interpretation became variables for recursive real numbers and uniformly continuous recursive real functions. The well-known examples show that $K$ cannot include all normal (that is $\exists,V$-free) sentences of $\Omega$. Main restrictions are of the type: if $F\in K$, then for every negative occurence of a formula $\forall x B(x)(x\operatorname{real})$ in $F$ the statement $\ll$ the set $\{x:B(x)\}$ is closed $\gg$ is provable in the calculus $A$. The class $K$ proved to be rasher broad; it contains a considerable number of theorems (for example differential and integral inequalitiesi uniqueness theorems and so on) whose conventional classical proofs are essentially non-constructive.