引入律 若厂Fa(x/t) 且t对x在a中自由, (+) 则厂上彐ca 直观含义: 若「能保证当Q中的x”取值”为的时候成立, 则『一定能保证有一个x使Q成立 (是使得彐a成立的”证据”) 注意条件”对x在a中自由”不可少。∃ Γ ` α(x/t), t x α ✕✖✜ Γ ` ∃xα (∃+) ✔ Γ ✣α x” ” t ✢, Γ✶✶ x α ✢. (t ∃xα ✢” ”.) : ”t x α ✕✖” ✥ 7