Marginalia to a Theorem of Jacopini

Abstract

In 1975, G. Jacopini proved the existence of an easy term, i.e., a term which can be consistently (with beta conversion) identified with any other term. In 1980, A. Visser generalized Jacopini's result to R.E. theories; namely, easy terms for consistent (with beta conversion) R.E. theories exist. Of course, no such generalization for non-R.E. theories exists. For example, it is easy to see that there is no easy term for Barendregt's theory H. In this note we shall generalize Jacopini's result to non-R.E. theories as follows. Say that an equation M=N is easy if for any consistent (with beta conversion) extension T we have that T∪{M=N} is consistent. We shall prove that easy equations exist.