Theory of symbolic expressions. I (Q791311)

The paper describes a basic framework of the theory of symbolic expressions. A domain of symbolic expressions (sexps) is introduced consisting of infinite leaf-free binary trees with nodes marked by 0 or 1. Marking of the nodes of a sexp can be defined using LISP-like terms built from 0, 1, car, cdr, cons and snoc, defining markings of finite components of the infinite binary tree. For more convenient work with sexps, a special reference language enabling natural work with them is introduced, with the meaning of language expressions defined as appropriate markings of the nodes of sexps. Formal systems are defined as sexps containing axioms coded in a special way. Paricularly, the formal system talking about sexps is also a sexp and this allows to prove, e.g., the existence of a recursively enumerable but nonrecursive set without the use of Gödel numbering, because all necessary codings are provided using sexps only. Using the introduced notions, a particular formal system is defined in which the basic concepts of computability theory are described, and in terms of this system the semantics of the programming language Hyperlisp is given. The paper presents a clear and interesting introduction into a rather original framework for the study of finite mathematics.