Theory of Symbolic Expressions, II
Masahiko Sato · Publications of the Research Institute for Mathematical Sciences · 1985
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.