4 Propositional logic

　HOL Lightの命題論理は一般的なものであり，命題定数は

F　(Falsity)
T　(Truth)

論理記号は

~　　(Not)

さらに結合の強い順に

/\　 (And)
\/　 (Or)
==>　(Implies)<=>　(Iff)

で，同じ結合記号どうしは右結合，formula，および，truth valuesの設定もごく普通のものです．
　前回のARITH_RULEのみでも，例えば

ARITH_RULE `x

のような証明が得られます．
　HOL Lightの全ての中置き演算子の結合の強さ（数値が大きい程強い）と向きは

infixes();;
val it : (string * (int * string)) list =
[("<=>", (2, "right")); ("==>", (4, "right")); ("\\/", (6, "right"));
("/\\", (8, "right")); ("==", (10, "right")); ("===", (10, "right"));
("treal_eq", (10, "right")); ("IN", (11, "right")); ("<", (12, "right"));
("<<", (12, "right")); ("<<<", (12, "right")); ("<<=", (12, "right"));
("<=", (12, "right")); ("<=_c", (12, "right")); ("<_c", (12, "right")); ("=", (12, "right")); ("=_c", (12, "right")); (">", (12, "right"));
(">=", (12, "right")); (">=_c", (12, "right")); (">_c", (12, "right"));
("HAS_SIZE", (12, "right")); ("PSUBSET", (12, "right"));
("SUBSET", (12, "right")); ("divides", (12, "right"));
("treal_le", (12, "right")); (",", (14, "right")); ("..", (15, "right"));
("+", (16, "right")); ("++", (16, "right")); ("UNION", (16, "right"));
("treal_add", (16, "right")); ("-", (18, "left")); ("DIFF", (18, "left"));
("*", (20, "right")); ("**", (20, "right")); ("INTER", (20, "right"));
("treal_mul", (20, "right")); ("INSERT", (21, "right"));
("DELETE", (21, "left")); ("CROSS", (22, "right")); ("/", (22, "left"));
("DIV", (22, "left")); ("MOD", (22, "left")); ("div", (22, "left"));
("rem", (22, "left")); ("EXP", (24, "left")); ("pow", (24, "left"));
("$", (25, "left")); ("o", (26, "right"))]

のように得ることができます．OCaml（HOL Light）でのリストの書式は

[ e1 ; ... ; en ]

です（各要素は同じtype，詳しくは
http://www.i.kyushu-u.ac.jp/~bannai/ocaml-intro/basics.html
などを参照のこと）．一つの演算子の情報を得るだけなら，演算子名をstringとして指定して

get_infix_status "==>";;
val it : int * string = (4, "right")

とします．もし，この設定を変更したり，新たな結合子に強さと向きを与えたいなら

parse_as_infix("+",(1,"left"));;
val it : unit = ()

とすればよいのですが，これでは < のほうが強いので ( x < x ) + 1 となり叱られます．

`x < x + 1`;;
Exception: Failure "unify: types cannot be unified".

　なお，複数の結合子については

`x

のように駄目ですが

`(p ==> q)==>r`;;
val it : term = `(p ==> q) ==> r`
`p ==> (q==>r)`;;
val it : term = `p ==> q ==> r`

のように大丈夫なものもあります（上記の通り右結合）．