slide 13: 量词的自然演绎

关于 的一些规定

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

关于 的一些规定

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