証明は、複合証明 proof ... qed か、自動証明 by ... のどちらか。 自動証明の根拠と複合証明のヘッダ部には証明メソッドが書かれる。 複合証明の本体（ボディ）部は、文（ステートメント）の列。 文（ステートメント）は次の種類： fix文 自由変数の宣言 a…

論理式（formula）は極性（ポラリティ polarity, 符号 sign）を持つとする、正負号（positive sign）と負符号（negative sign）。正負号は省略してもよい。（書き方は後で）正（極性が正）の論理式の集まりを論理資産（logical asset(s)）、負の論理式の集ま…

2018年封切り予定の映画『Proud Mary』 http://www.imdb.com/title/tt6421110/ はアクション映画。アクションが主体かどうかは分からないが、アクション要素はあるはず。ヒロインを演じるのはタラジ・P・ヘンソン（Taraji Penda Henson）、1970年9月11日生ま…

前提（premise; プレミス）は次のもの達の総称する。 公理（axiom） 定理（theorem） 仮説（hypothesis, 複数形 -ses） 仮定（assumption） 公理と定理はどちらも論理式またはシーケントで、表現形式上の差はなくて（Mizarでは公理と定理の区別はない）、定…

集合のド・モルガンの法則の証明（順証明、フォワード証明）http://d.hatena.ne.jp/m-hiyama-memo/20170810/1502363526 の最後のほうは、 // SerND (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B) contract $.1, $.2 by (集合の差) (x∈X＼A) ∨ (x∈X＼B) contract by (集合の合…