>>240
> >>237
> これって225へのレスじゃないよね？

237とは別人だが横レスすると、操作的意味論も数理論理学的には証明論という事になる。
λ計算でのreduction theoryだから構文的対象とその関係に対する推論規則の体系だからね。
無論、手続き的プログラミング言語に対する公理的意味論も数理論理学的には証明論的な体系の一つ。

> それから、ここの｢操作的意味論｣は｢公理的意味論｣の間違い？
> それから、操作的意味論を意味論などと呼ぶから話がおかしくなるのでは？

君の上の主張は歴史を無視した非常に視野の狭い主張。
「意味論(semantics)」という概念は数理論理学の成立以前から
言語学や個々の語学（英語学やフランス語学など個々の自然言語に対するもの）の中で確立されていた概念。
自然言語の意味論にも様々なアプローチがあって、数理論理学的に見てモデル論的でない意味論は山ほどある。
そしてプログラミング言語の意味論は自然言語の意味論と同じ意味での「意味論」。
だから、操作的意味論も公理的意味論も、表示的意味論と同じく、プログラミング言語に対する意味論として有意。

例えば、「プログラミング言語のモデル論」と呼ぶのならば、表示的意味論以外のアプローチはおかしいと主張しても正当だが。
何故ならば、「モデル論」という言葉や概念は数理論理学によって確立されたものだから、数理論理学的な意味でのモデル論以外はNGだと
主張するのは妥当だが、「意味論」は言語学で既に成立していた言葉を、数理論理学の中では勝手に非常に狭い意味に限定して使うように
しただけ。

従って、数理論理学に属さない分野で「意味論」という言葉を数理論理学の用法から外れた使い方をしてもNGとは言えない。
そしてプログラミング言語は少なくとも当初は数理論理学には属さずに発展してきた。
1960年代のプログラミング言語は数理論理学には縛られずに発展して来た。
そしてプログラミング言語の意味を形式的に捉える最初のアプローチである操作的意味論（PlotkinのSOSとは随分と違うアプローチだが）は
その1960年代前半に考え出された。
プログラミング言語が数理論理学を強く意識し、数理論理学屋がプログラミング言語の理論に大量に入り込むようになったのは型理論ブームからだよ。