$`\newcommand{\mrm}[1]{\mathrm{#1}}\newcommand{\mbf}[1]{\mathbf{#1}}`$ $`A`$ を導出系として、構文ソートとして、formula, true-formula, false-formula を持つとする。次は最外メタレベルで意味を持つ命題： $`x \in \mrm{Term}^\infty(A)_{\text{form…