A fragment of formalized analysis (Q1097881)

The author presents a formalization for a fragment of analysis by restricting functionals to those representable by numerical zero-one functions and using a many-sorted language. The theory T contains Peano arithmetic, predicate logic with equality, a scheme for the existence of universal functions and a restricted reduction scheme \(\exists \alpha^ n\forall x_ 1,...,x_ n\) \((\alpha^ n(x_ 1,...,x_ n)=0\leftrightarrow A(x_ 1,...,x_ n,{\bar \beta})),\) where the parameters in \({\bar \beta}\) are at most n-place. It is shown that the restriction cannot be dropped. A model for T is constructed by means of functions relatively computable in sets \(H_ n\). The same system is a model for the theory \(T_ 1\), obtained by adding reduction axioms for functionals.