¬φが閉論理式ならφも閉論理式

FVar(φ) = ∅ のとき、φを閉論理式と呼ぶ

¬φが閉論理式であるとは

FVar(¬φ) = ∅ であること

証明

FVar(¬φ) = FVar(φ) である

FVar(¬φ) = ∅ であるので、 FVar(φ) = FVar(¬φ) = ∅ となる

証明終了

¬, ∧, ∨, →あたりは似た感じになりそう

∀, ∃は違う感じになりそう

∀xφが閉論理式ならφも閉論理式