ヤッパリなんかオカシイ

オカシイ、オカシイ。

除去規則（elim rule）がIsar satement formatだとobtainsで書かれる。これはオカシくはない、つうかまっとうなんだが、逆に通常の除去規則の書き方はいったいなんなんだ？ ということになる。

disjEの例だと：

• ?P ∨ ?Q ==> (?P ==> ?R) ==> (?Q ==> ?R) ==> ?R

これが生のPureルールシェマ（ルールスキーム）。シーケント風に解釈すると：

• P ∨ Q, (P ==> R), (Q ==> R) |- R

どうやって解釈したかと言うと：

1. 一番右に出現する ==> は |- と解釈する。
2. トップレベルの含意はカンマによる併置と解釈する。
3. 残った==>はそのままにして、自然演繹による証明図の部分図と考える。

Isar satement formatだと、

fixes P :: "bool"
  and Q :: "bool"
assumes "P ∨ Q"
obtains "P" | "Q"

P∨Q を仮定した（assumes）状態で、

• (P ==> R), (Q ==> R) |- R

が言える。これをもって、PまたはQが得られる（記号「|」は外側構文）と言う。Isar statement formatのほうがマトモだが、マトモでないdisjEから、どうやってIsar satementを作り出すのだろう？

もとのPureの論理式を普通に解釈してIsar statementが出てくるとは信じがたい。なんかトリックがあるはずだ。