oupoの日記

体系CLwで遊んだ

logic

最近現代数理論理学序説を読み始めました。今日は体系CLwで遊びました。Lazy Kを触ったことがあったので、この体系にはどういう意図があるのかはなんとなくわかった上で進められました。
本に載っていない命題で、次のようなものを見つけて証明しました

$\frac{M \triangleright N}{MR \triangleright NR}$ は許容推論である
$x$ はw-正規形
$MN$ がw-正規形なら $M$ と $N$ はともにw-正規形
$Mx \triangleright __1 T$ が公理となるような項 $T$ が存在せず、 $M$ がw-正規形ならば $Mx$ はw-正規形
$M$ がw-正規形ならば $xM$ はw-正規形
$Mx_1 \ldots x_n$ がw-正規形で $N_1, \ldots, N_n$ がw-正規形なら $MN_1 \ldots N_n$ はw-正規形
$M$ がw-正規形で $M \triangleright __w T$ ならば $M \equiv T$
(Church-Rosserの定理を前提として) $M$ のw-正規形が存在するとき、 $M$ のw-正規形は一意である

筆者: oupo (連絡先: oupo.nejiki@gmail.com)