Developing continuity theory in a formal predicative set theory

We present correct and natural development of continuity theory in a predicative set theory called PZFU. This is done by using a delicate and careful choice of those Dedekind cuts that are taken as real numbers. PZFU is based on ancestral logic rather than on first-order logic. Its key feature is that it is definitional in the sense that every object that is shown in it to exist is defined by some closed term of the theory. This allows for a very concrete, computationally oriented model of it. The development of analysis in PZFU does not involve coding, and the definitions it provides for the basic notions are the natural ones.