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

前提（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 (集合の合…

記号的には、 [x1:t1, ..., xk:tk | A1, ..., An |- B] 最初はk個の変数型宣言。型理論で言う型環境。 次にn個の前提（仮説）論理式。 1個の結論論理式。 出現するすべての変数は型環境で型付けされている。 自然言語風の記述は： for x1:t1, ..., xk:tk giv…

環境として、論理環境（logical environment）と応用固有環境（application-specific environment）がある。論理環境は、論理定理データベースと論理推論規則データベースからなる。応用固有環境は、応用固有定理データベースと応用固有推論規則データベース…

Natural Deduction Mizar SerND → introduction assume assume + use → elimination – apply ∧ introduction thus concat ∧ elimination – select ∨ introduction – add ∨ elimination per cases cases ∀ introduction let for ∀ elimination – instantiate …

逆像のf-1 を f^* と書く。 // SerND 共通部分の逆像 target f^*(C)∩f^*(D) = f^*(C∩D) proof target f^*(C)∩f^*(D) ⊆ f^*(C∩D) proof assume x∈(f^*(C)∩f^*(D)) ---(ass) expand by (集合の共通部分) x∈f^*(C) ∧ x∈f^*(D) expand $.1, $.2 by (写像の逆像) …

// SerND 集合のド・モルガンの法則target X＼(A∩B) = (X＼A)∪(X＼B) proof target X＼(A∩B) ⊆ (X＼A)∪(X＼B) proof assume x∈X＼(A∩B) ---(ass) expand by (集合の差) x∈X ∧ ¬(x∈A∩B) expand $.2.1 by (集合の共通部分) x∈X ∧ ¬(x∈A ∧ x∈B) rewrite $.2 by …

キーワード 意味 備考 target 目標は…である。 proof end （これから）証明しよう。 set …と置く。 by the way ところで リーフの開始 remark …であることを注意しておく。 concat …との連言を作る。 ∧導入 select …を抜き出すと、 ∧除去 add …との選言を作…

Mizar Isar let fix assume assume set let set def consider ... such that obtain ... where take (no equivalent) per cases ... proof ... qed suppose next assume (no keyword) have thus show hence then show thesis (?thesis) proof ... end proof …

αを名前を表すメタメタ変数として： 項メタ変数 %α 命題メタ変数 _α 式パスメタ変数 @α 自然言語（英語）としての自然さよりは、人工言語としての整合性を重視する。使う前置詞： by with to of from byとwithは区別しない。by/withはどちらでもいいことを示…

次を示す。 f(A)＼f(P) ⊆ f(A＼P) 下に、清書したフォワードプルーフ。作業的にはバックワード探索をしている。使う（一部未使用）定義、論理法則、推論規則： DefSetInc: A⊆B :⇔ ∀x.(x∈A ⇒ x∈B) DefSetDiff: X = A＼B :⇔ ∀x.(x∈X ⇔ (x∈A ∧ ¬(x∈B))) DefSetD…