slide 13: 量词的自然演绎

关于 $\forall$ 的一些规定

• 引入：对于 $\forall_I$，变量 $x$ 必须是一个新的变量，且在子证明（sub-proof）当中是 local 的
• 消除：对于 $\forall_E$，变量 $x$ 必须是任意一个在当前证明作用域的变量

关于 $\exists$ 的一些规定

• 引入：对于 $\exists_I$，变量 $x$ 必须是任意一个在当前证明作用域的变量
• 消除：对于 $\exists_E$，变量 $x$ 必须是一个新的变量，且在子证明（sub-proof）当中是 local 的