Elementary formal systems
Raymond M. Smullyan · Journal of the Mathematical Society of Japan · 1961
\S 1. Introduction.Like the canonical languages of Post [2], [3], elementary formal systems (as they are to be defined) provide a direct characteriza- tion of recursive enumerability for sets (and relations) of formal $\exp\dot{r}essions$ , without recourse to G\"odel numbering.3)In this paper we develop just enough of the theory of these systems to construct a " universal " system and to prove its recursive unsolvability.This proof is of $unlJsual$ brevity; no number theory is employed, and the Post normal form theorem for canonical systems is circumvented.\S 2. Elementary formal systems.For any finite alphabet $K$ we define an elementary formal system (E) over $K$ as a collection of the following items: (i) the alphabet $K$ ; (ii) A new alphabet of symbols called variables; (iii) another alphabet of symbols called predicates, each of which is assigned a unique posi- tive integer called itsdegree; (iv) two more $symbols\rightarrow and$ , ; (v) A finite set $A_{1},$ $\cdots,$ $A_{z}$ of expressions which are (well formed) formulas, according to the definition given below; these strings are called the axioms of the system (E).By a term of (E) we mean any string composed of symbols of $K$ and vari- ables (or either one alone).By an atomic formula of (E) we mean an expres- sion of the form $Pt_{1},$ $\cdots,$ $t_{n}$ , where $t_{1},$ $\cdots,$ $t_{n}$ are terms and $P$ is a predicate of degree $n$ .By a (well formed) formula of (E) we mean either an atomic formula