αを名前を表すメタメタ変数として： 項メタ変数 %α 命題メタ変数 _α 式パスメタ変数 @α 自然言語（英語）としての自然さよりは、人工言語としての整合性を重視する。使う前置詞： 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…