論理／メタ論理の記法をどうするか - 檜山正幸のキマイラ飼育記 (はてなBlog)

最近割と、論理／メタ論理の話をする機会があるのですが、そのとき、どんな書き方をすればいいか悩みます。

内容：

キーワード方式とターンスタイル方式
正しさを分類する
書き方の変種や修飾
意味的帰結の書き方

キーワード方式とターンスタイル方式

For x∈R, y∈R.
For x ≧0, y ≧0.
  IsCorrect x + y ≧ 0

少し前までは、次のような書き方をしてました。これ(↓)は、誰か（誰だか忘れた）の真似をしたものです。

Given x∈R, y∈R.
Given x ≧0, y ≧0.
  Holds x + y ≧ 0

キーワードの差（ForとGiven、IsCorrectとHolds）以外何の違いもありません。IsCorrectとHoldsは、ターンスタイル記号'|-'と同じ意味です。論理／メタ論理における標準的記法はターンスタイル記号です。

ターンスタイル記号より、上に紹介した書き方がいい点は：

英単語由来のキーワードのほうが、見慣れない記号'|-'より幾分か親しみやすい。
文脈（前提）を、何行かに分けてグルーピングして書ける。

「幾分か親しみやすい」は気分的なもので、たいした理由ではないです。「何行かに分けて書ける」もターンスタイル記法でもやれば出来ます。文脈をグルーピングしたいなら、区切り記号（例えばスラッシュ）を導入すればいいでしょう。

x∈R, y∈R / x ≧0, y ≧0 |- x + y ≧ 0

どう書こうが同じだろ、ってのが僕の感想ですが、“気分的な差”とか“視覚的な（見た目の）差”とかが実にバカにできなくて、「どう書くべきか」の判断は難しくなります。

正しさを分類する

前節のキーワード 'IsCorrect', 'Holds' は、「正しい」「成立する」という意味です。それ以上の説明は要らないように思えますが、そうではありません。メタ論理（モデル論や証明論）のモットーは、正しさや成立することを厳密に分析することです。

少なくとも、'|-'（ターンスタイル記号）と'|='（ダブルターンスタイル記号）はシッカリと区別する必要があります。ターンスタイル記号は“構文的に正しい”、ダブルターンスタイル記号は“意味的に正しい”という主張（に使う記号）です。今日は、内容的説明をする気はなくて、記法の話ですから、“構文的に正しい”と“意味的に正しい”がどう違うかは説明しません。

'|-' と '|=' をキーワードにするなら何がいいのだろう？ 'IsProvable'と'IsValid'かな。

IsProvable x + y ≧ 0
IsValid x + y ≧ 0

'|-' と '|=' は、形は似てますが、使い方がだいぶ違います。'|-'の左側には証明の前提を書きます。

x ≧0, y ≧0 |- x + y ≧ 0

キーワードで書くなら（ピリオド打つのはやめた）、

For x ≧0, y ≧0
IsProvable  x + y ≧ 0

あるいは、

Given x ≧0, y ≧0
IsProvable  x + y ≧ 0

なんかGivenのほうがいいような気がしてきた。まったくの気分だが。

'|='の左側には、右側の命題を成立させるモデルを書きます。モデルとは、命題を解釈するための構造です。例えば、自然数の変数・定数・演算・関係を使うモデルをN-model、実数の変数・定数・演算・関係を使うモデルをR-modelとしたとき：

N-model |= ∀x, y.(x + y ≧ 0)
R-model |=/ ∀x, y.(x + y ≧ 0)

'|=/'は「正しくない」の意味です。全称限量子を付けないで、自由変数が残っていると妥当性〈validity〉の判断はできません。

R-model |= x + y ≧ 0 （なんともいえない）

変数への具体的な値の割り当てを、変数の状態〈state〉、束縛〈binding〉、付値〈valuation〉などと呼びます。状態まで付ければ妥当性が判断できます。

(R-model, {x←1, y←1}) |= x + y ≧ 0
(R-model, {x←0, y←(-1)}) |=/ x + y ≧ 0

状態の記述に'←'を使ったのは臨時の記法です（特に正式な記法はないと思います）*1。

書き方の変種や修飾

'|-'で示す証明可能性は、証明を行う仕掛けである演繹系〈deduction system | 証明系〉が決まらないと定義できません。演繹系をSとして、「Sにより証明可能」は '|-_S' を使えばいいでしょう。

x ≧0, y ≧0 |-_S x + y ≧ 0

キーワード方式だと：

Given x ≧0, y ≧0
IsProvableBy S  x + y ≧ 0

By S はお尻のほうがいいか。

Given x ≧0, y ≧0
IsProvable x + y ≧ 0 By S

キーワードを使うと、“気分”と“見た目”が気になりだす。やはり、自然言語には言霊が宿るせいか？

'|='では、基本的には左側にモデルを書くのですが、何も書かないときがあります。

|= ∀x, y.(x + y ≧ 0)

実は、左が空白のときの解釈が場合により違うんですよ。ヤダナー。

モデルをひとつに固定しているので、あえてモデルは書かない。
複数のモデルを想定するが、左側空白は、どのモデルに対しても成立することを意味する。

モデルがひとつであってもチャンと書くことにして、複数のモデルのどれでも成立するならワイルドカードの'*'を付けるとかすれば混乱は少ないでしょう。

N-model |= ∀x, y.(x + y ≧ 0)
* |= ∀x, y.(x + y ≧ 0)

モデルの集まりをMとして、左側にはモデルの集まりを書く約束なら：

{N-model} |= ∀x, y.(x + y ≧ 0)
M |= ∀x, y.(x + y ≧ 0)

左側にモデルの集まりを書く習慣はたぶんないと思うけど、「何も書かないで省略する」はたいていトラブルを招くんだよなー。

意味的帰結の書き方

ダブルターンスタイル'|='の左側にはモデルを書くので、論理式を書くことはできません。しかし、意味的判断で左側に論理式を書きたいことがあります。標準的記号がないので、僕は'|⇒'を使っています。

x ≧0, y ≧0 |⇒ x + y ≧ 0

これは、次の意味です。

いま考えているどんなモデルMと状態ρに対しても、 (M, ρ) |= x ≧0 かつ (M, ρ) |= y ≧0 ならば、(M, ρ) |= x + y ≧ 0 である。

論理式 A₁, ..., A_n, B のあいだの関係 A₁, ..., A_n |⇒ B は、通常は論理的帰結〈logical consequence〉と呼びます。しかし、これは意味的判断なので、意味的帰結〈semantic consequence〉と呼んだほうが適切でしょう。意味的帰結を伴意〈entailment〉ともいいます。次の記事を参照してください。

意味的帰結〈伴意〉を'|⇒'で表すと、左側に論理式を書けるようになりますが、今度は判断の根拠であるモデルの集まりが書けなくなります。右下添字かな。

x ≧0, y ≧0 |⇒_M x + y ≧ 0

Mは、モデル（と状態）の集まりで、この意味的帰結を主張するときの根拠となったものです。こう約束すると、次の2つの書き方は同じ意味になります。

M |= x + y ≧ 0
|⇒_M x + y ≧ 0

'|-' と '|=' は似てませんが、'|-' と '|⇒' は似た使い方ができます。左側に前提となる命題の並び、右下添字に判断の根拠となる仕掛けや集まりを書くことになります。'|=' は、'|⇒' を定義するための補助的なものと捉えたほうがいいような気がします。

関係しそうな過去記事：

*1:「型推論に関わる論理の概念と用語その6：substitutionの記法」で色々な記法があることを書きました。状態〈束縛 | 付値〉と置換〈substitution | 代入〉は似てますが違う概念です。