A new domain S of symbolic expressions is introduced and its structure is studied formally. To study S formally an intuitionistic first order theory, SA, is introduced. SA is a theory adequate for developing elementary metamathematics within it. Gödels second incompleteness theorem is proved formally within SA to show the adequacy. A modified version of Post-Smullyan's formal system is used to define basic concepts in SA. The close relation between formal systems and the logic programming language Qute is also pointed out.
Cite this article
Masahiko Sato, Theory of Symbolic Expressions, II. Publ. Res. Inst. Math. Sci. 21 (1985), no. 3, pp. 455–540DOI 10.2977/PRIMS/1195179055