3 HOL basics

　前回お話したtoplevel loopにおいてできることの２つ目は，evaluate expressions，つまり，数や文字列の評価でした．
　「HOL Lightは，これに加えて，数学的陳述や論理的主張を表す「term」と，証明済みの主張を表す「theorem」を評価するツールの集まりです．」
　と，チュートリアルには書かれており，それはその通りなのですが，HOL Lightでのtermは，述語論理のtrem（項）のみならず，formula（論理式）なども含めた考察の対象全てである点に注意が必要です．つまり，前後に`記号のついた中味以外はメタのものであり，termやtheoremは，メタ言語であるOCamelのtypeです．
　なお，theorem（定理式）については，term（のうち論理で言うformula）のうち，HOL Lightの公理と推論規則により証明可能なもののことである点は述語論理と同じです．