In this chapter we establish some basic facts about Σ1-relations and functions that will be needed for the rest of this study. We also introduce the notion of fixed-points of formulas and prove a fundamental fact about them which is crucial for Gödel’s second incompleteness theorem and related results of the next chapter. A formula F(v1,...,vn) is said to define a relation R(x1,..., xn) in a system S if for all numbers a1,...,an, the two following conditions hold. (1) R(a1,... ,an) ⇒ F(ā1,... , ā n) is provable in S. (2) R̃(a1,...,an) ⇒ F(ā1,... , ā n) is refutable in S. We say that F(v1,...,vn) completely represents R(x1, . . . ,xn ) in S iff F represents R and ~ F represents the complement R of R in S—in other words, if (1) and (2) above hold with “⇒” replaced by “↔”. If F defines R in S and S is consistent, then F completely represents R in S. Proof. Assume hypothesis. We must show that the converses of (1) and (2) above must hold. Suppose F(ā1,... , ān) is provable in S. Then F(ā1,..., ān) is not refutable in S (by the assumption of consistency). Therefore by (2), R̃ (a1,...,an) cannot hold. Hence R(a1,...,an) holds. Similarly, if F(ā1,..., ān) is refutable, then it is not provable. Hence by (1), R(a1,..., an) cannot hold and hence R̃ (a1,...,an). By a recursive set or relation, we mean one such that it and its complement are both Σ1. [There are many different, but equivalent, definitions in the literature of recursive relations. We will consider some others in the sequel to this volume.] It is obvious that a formula F defines a relation R in S iff F separates R from R̃ in S. Suppose now S is a Rosser system and that R is a recursive relation. Then R and R̃ are both Σ1. Hence R is separable from R̃ in S, which means that R is definable in S. And so we have: 1. If S is a Rosser system, then all recursive relations are definable in S. 2. If S is a consistent Rosser system, then all recursive relations are completely representable in S.