Theory of symbolic expressions. II (Q1075757)

The paper continues a formal treatment of the theory of symbolic expressions which was introduced by the author in Theor. Comput. Sci. 22, 19-55 (1983; Zbl 0535.68013). The author slightly modified his original formalism based on Lisp-like structures into a system which is substantially influenced also by Prolog. Within this framework several formal systems are defined, formalizing first order theories and symbolic arithmetic. To show adequacy of the theory, a formal proof of Gödel's second incompleteness theorem is shown within this system. The theory of symbolic expressions provides a natural means of encoding metamathematical entities such as proofs or programs. Formal systems closely correspond to logic programs in the programming language Qute, which presents a framework for a theorem prover for the formal systems.