JournalsprimsVol. 21 , No. 3DOI 10.2977/prims/1195179055

Theory of Symbolic Expressions, II

  • Masahiko Sato

    University of Tokyo, Japan
Theory of Symbolic Expressions, II cover


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.