MESON

　次の定理の証明を考えて見て下さい．

関数ｆ，ｇに対して，ｆ（ｇ（ｘ））＝ｘをみたすｘが唯一つ存在するならば，ｇ（ｆ（ｙ））＝ｙをみたすｙが唯一つ存在する

　特に難しい訳ではないにせよ，ｙ＝ｇ（ｘ），そしてｙが異なればｆ（ｙ）も異なることに気付くにはそれなりの経験が必要でしょう．
　ところが，HOL LightのMESON関数は，model eliminationと呼ばれる証明の構成方法により

MESON[] `(?!x. f(g(x)) = x) ==> (?!y. g(f(y)) = y)` ;;
Warning: inventing type variables
0..0..1..solved at 4
0..0..1..2..6..12..25..46..82..142..238..390..solved at 431
val it : thm = |- (?!x. f (g x) = x) ==> (?!y. g (f y) = y)

のように証明可能であると直ちに答えてくれます．
　ここで記号の約束です．HOL Lightでは，数理論理の

項，論理式などをterm，tmと呼び，前後に`が付いたもの，
定理式をtheorem，thmと呼び，前に|-が付いたもの

で表します．更に

一意的特称量化子　?!
特称量化子　?
全称量化子　!

であり，束縛変数の列の最後にはピリオド，束縛変数間の区切りに一つ以上のスペース，連続する同じ量化子は

!x y z. ?s t.

のように省略でき，

==>　<=>　/\　\/　~　T　F

などは標準的な用法で右結合，関数の括弧は付けても付けなくても構いません．

　上のMESONは，第１引数としてtheoremのリスト（空リストは[ ]，区切りの記号は;），第２引数としてtermをとり，そのリストのthmを仮定として，HOL Lightにおいて，入力されたtmが証明可能であるとき，それをtheoremとして出力する関数です．入出力は，引数なしで呼ぶと

MESON;;
val it : thm list -> term -> thm =

のように答えてくれます．sedなどがインストールされた環境なら

help "MESON" ;;

でヘルプが表示されますが
http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.html
の方が便利かも知れません．