問題集8の解答と解説： 当たり前であることを証明する (A15R8-1)
※この記事は「記事15 解答8-1」
問題集8とは、次の記事（の問題部分）のことです：
「シーケントとスコット・ブラケット (A10P8) // 組み込み推論を表すシーケント」の解答例＋解説。
シーケント (x, y∈R), x2 = -3, x ≧ 0 → 1 + 1 = 3 を、日本語風に読み下してみます。
実数 x, y に対して、
x2 = -3, x ≧ 0 だとする。
これらから、
1 + 1 = 3
が出る。
「何を言ってるんだ？ これは」と思うかも知れませんが、このシーケントの“正しさの度合い”はスコット・ブラケットを計算すれば分かります。日本語で考えるのは現実世界での話で、形式化された世界（モデルの世界、演繹システムの世界）での形式化された主張（＝シーケント）の正しさは、スコット・ブラケットと呼ばれる関数の関数値で測るのでした。
〚(x, y∈R), x2 = -3, x ≧ 0 → 1 + 1 = 3〛
= 〚x, y∈R| x2 = -3, x ≧ 0〛c ∪ 〚x, y∈R| 1 + 1 = 3〛左辺のスコット・ブラケットと右辺のスコット・ブラケットを別々に計算する：
〚x, y∈R| x2 = -3, x ≧ 0〛
= 〚x, y∈R| x2 = -3〛∩〚x, y∈R| x ≧ 0〛
= 0∩{(x, y)∈R2| x ≧ 0}
= 0〚x, y∈R| 1 + 1 = 3〛
= 0もとの計算に戻って：
= 〚x, y∈R| x2 = -3, x ≧ 0〛c ∪ 〚x, y∈R| 1 + 1 = 3〛
= 0c ∪ 0
= R2∪ 0
= R2
このシーケントのコンテキストは、(x, y∈R) = (x∈R, y∈R) で、コンテキスト領域はR2、したがって、
- 〚(x, y∈R), x2 = -3, x ≧ 0 → 1 + 1 = 3〛 = Dom((x∈R, y∈R)) = R2
スコット・ブラケットの値がコンテキスト領域と一致するシーケントは正しい（そう定義している）から、
- シーケント (x, y∈R), x2 = -3, x ≧ 0 → 1 + 1 = 3 は正しい。
ここで出てきた「正しい」は完全にテクニカルタームであり、既に定義済みです。「関数が連続である」とか「ベクトル空間は有限次元である」とかと同様に「シーケントは正しい」はテクニカルな主張です。
解析学で「この関数は連続なんじゃないの？ 5,6個の点つないだグラフを見ると、そんな感じ」「いやぁ、どことなく不連続な雰囲気があるなぁ」とかの議論がナンセンスであると同様に、「このシーケントは正しいんじゃないの？ 日本語にしてみると、そんな感じ」とか「いやぁ、どことなく正しくない雰囲気があるなぁ」とかの議論はナンセンスです。定義があるんだから、定義にしたがって「正しい」（あるいは「正しくない」）を示す、それしかありません。
次に、シーケント (), 1 + 1 = 2 → 1 + 1 = 2 を考えましょう。ここで、() は空なコンテキストであり、その領域は Dom(()) = 1 です。
日本語風読み下しは：
1 + 1 = 2 だとする。
これにより、
1 + 1 = 2
が出る。
スコット・ブラケットを計算してみると：
〚(), 1 + 1 = 2 → 1 + 1 = 2〛
= 〚| 1 + 1 = 2〛c ∪ 〚| 1 + 1 = 2〛
= 1c ∪ 1
= 0 ∪ 1
= 1
したがって、
- シーケント (), 1 + 1 = 2 → 1 + 1 = 2 は正しい。
シーケント (), 1 + 1 = 3 → 1 + 1 = 3 はどうでしょう？ 四の五の言わずにスコット・ブラケットを計算：
〚(), 1 + 1 = 3 → 1 + 1 = 3〛
= 〚| 1 + 1 = 3〛c ∪ 〚| 1 + 1 = 3〛
= 0c ∪ 0
= 1 ∪ 0
= 1
より一般に、αをコンテキスト、Aを論理式として、α, A → A という形をしたシーケントはすべて正しいと思われますよね。
α に対して、
A だとする。
これにより、
A
が出る。
これは当たり前に聞こえます。もちろん、日本語読み下しなんて当てにはならないですけど。当てになるのは、スコット・ブラケットの定義にしたがった証明（通常の証明、現実世界の数学的行為としての証明）です。やってみます。
Dom(α) = X とすると、〚α| A → A〛 は Pow(X) に値を取る。
- 〚α| A → A〛 = 〚α|A〛c ∪ 〚α|A〛
どんな部分集合 S ⊆ Pow(X) に対しても、
- Sc ∪ S = X
は成立するから、
- 〚α| A → A〛 = 〚α|A〛c ∪ 〚α|A〛 = X
したがって、
- 〚α| A → A〛 = Dom(α)
よって、シーケント α A → A は、コンテキストα、論理式Aによらずに常に正しい。
α, A → A だけでなく、α, A → T や α, A∧B → A もいかにも当たり前です。しかし、「日本語読み下しにしてみたら、当たり前に聞こえたから」なんてのは何の根拠にもなりません。そんなことではくて、通常の数学の証明として当たり前さを確認しましょう。「通常の」ですから形式化する必要はありません。自然言語で普通に証明を書けばいいのです。形式化された証明（近々定義する）は、我々人間同士のコミュニケーションに使うものではなくて、演繹システムの内部データ／内部処理のことです。
我々が、人工的な構築物である演繹システムの内部で遂行される形式化された証明を調べようとしているのは確かです。だからといって、現実世界での通常の数学的行為を捨てたり変えたりする必要はまったくありません。いつもどおり、今までどおり、普通の／通常の証明（＝メタ証明）をすればいいのです。
何度も同じことを繰り返しますが：
- 論理の数学的モデルは人工的なシステムであり、天然に存在しないし、神様やサンタさんがプレゼントしてもくれない。
- したがって、論理の数学的モデルは、人間がゼロから細部に渡って構築（定義）しなくてはならない。“数学的”モデルなのだから、構築の方法は完全に数学的であり、雰囲気的な曖昧な議論は許されない。
- 以上のことを我々生きている人間が現実世界で行うにあたり、今までの考え方／やり方を変える必要はない。現実世界で使っている素朴集合論と、現実世界で使っている古典論理は今まで同様に普通に使う。
