一阶谓词逻辑演算形式系统的定理(量词第二部分)
假设无关前件 $\forall$ 引入
定理1（假设无关前件 $\forall$ 引入#E）： $\Gamma \vdash (A \imp B) \imp (\forall x A \imp B)$ （$x$ 在 $\Gamma$ 中无自由出现）
〔证明定理1〕
〔定理1证毕〕
$$\begin{aligned}
\ind{1}\b \Gamma &&(前提集)\\
\ind{2}\b\b A \imp B &&(\text{假设})\\
\ind{3}\b\b \forall x (A \imp B) &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{4}\b\b \forall x A \imp \forall x B &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329050339CST}{\text{\text{$\forall$}对\text{$\imp$}下沉\#R}})\\
\ind{5}\b\b \forall x B \imp B \forall 消除 \#E&&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250326012718CST}{\text{\text{$\forall$}消除\#E}})\\
\ind{6}\b\b \forall x A \imp B &&(4,5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250413085601CST}{\text{\text{$\imp$}传递\#1}})\\
\ind{7}\b (A \imp B) \imp (\forall x A \imp B) &&(2\-6\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})
\end{aligned}$$
规则1（假设无关前件 $\forall$ 引入#R）： $\Gamma \Vdash A \imp B \vdash \forall x A \imp B$ （$x$ 在 $\Gamma$ 中无自由出现）
假设无关前后件 $\forall$ 引入
定理2（假设无关前后件 $\forall$ 引入#E）： $\Gamma \vdash (A \imp B) \imp (\forall x A \imp \forall x B)$ （$x$ 在 $\Gamma$ 中无自由出现）
〔证明定理2〕
〔定理2证毕〕
$$\begin{aligned}
\ind{1}\b \Gamma &&(前提集)\\
\ind{2}\b\b A \imp B &&(\text{假设})\\
\ind{3}\b\b \forall x (A \imp B) &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{4}\b\b \forall x A \imp \forall x B &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329050339CST}{\text{\text{$\forall$}对\text{$\imp$}下沉\#R}})\\
\ind{7}\b (A \imp B) \imp (\forall x A \imp \forall x B) &&(2\-4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})
\end{aligned}$$
规则2（假设无关前后件 $\forall$ 引入#R）： $\Gamma \vdash (A \imp B) \imp (\forall x A \imp \forall x B)$ （$x$ 在 $\Gamma$ 中无自由出现）
假设无关分隔前件 $\exists$ 引入
定理3（假设无关分隔前件 $\exists$ 引入#E）： $\Gamma \vdash (A \imp B) \imp (\exists x A \imp B)$ （$\Gamma \vdash A \imp B$ 且 $x$ 在 $\Gamma$ 和 $B$ 中无自由出现）
〔证明定理3〕
〔定理3证毕〕
$$\begin{aligned}
\ind{1} \b \Gamma &&(前提集)\\
\ind{2} \b A \imp B &&(已知结论)\\
\ind{3} \b \neg B \imp \neg A &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250326093342CST}{\text{逆\text{$\neg$}引出\#1}})\\
\ind{4} \b \forall x (\neg B \imp \neg A) &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{5} \b \forall x \neg B \imp \forall x \neg A &&(4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329050339CST}{\text{\text{$\forall$}对\text{$\imp$}下沉\#R}})\\
\ind{6} \b \neg B \imp \forall x \neg B &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250417145419CST}{\text{无关\text{$\forall$}引入\#R}})\\
\ind{7} \b \neg B \imp \forall x \neg A &&(6,5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250413085601CST}{\text{\text{$\imp$}传递\#1}})\\
\ind{8} \b \neg \forall x \neg A \imp B &&(7\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250326093237CST}{\text{左\text{$\neg$}交换\#1}})\\
\ind{9} \b \exists x A \imp B &&(8\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/compositions_of_fc/#20250325213235CST}{\text{特称量词\text{$\exists$}}})
\end{aligned}$$
规则3（分隔前件 $\exists$ 引入#R）： $\Gamma \Vdash A \imp B \vdash \exists x A \imp B$ （$\Gamma \vdash A \imp B$ 且 $x$ 在 $\Gamma$ 和 $B$ 中无自由出现）
结论无关假设 $\exists$ 引入
原理1（结论无关假设 $\exists$ 引入）：若 $\Gamma \cup \set{A} \vdash B$ 且 $x$ 在 $\Gamma$ 和 $B$ 中无自由出现，则 $\Gamma \vdash \exists x A \imp B$ 。
〔证明原理1〕由演绎定理#1可得 $\Gamma \vdash A \imp B$ 。则由分隔前件 $\exists$ 引入#R可得 $\Gamma \vdash \exists x A \imp B$ 。〔原理1证毕〕
假设无关前后件 $\exists$ 引入
定理4（假设无关前后件 $\exists$ 引入#E）： $\Gamma \vdash (A \imp B) \imp (\exists x A \imp \exists x B)$ （$x$ 在 $\Gamma$ 中无自由出现）
〔证明定理4〕
〔定理4证毕〕
$$\begin{aligned}
\ind{1}\b \Gamma &&(前提集)\\
\ind{2}\b A \imp B &&(已知结论)\\
\ind{3}\b \neg B \imp \neg A &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250326093342CST}{\text{逆\text{$\neg$}引出\#1}})\\
\ind{4}\b \forall x (\neg B \imp \neg A) &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{5}\b \forall x \neg B \imp \forall x \neg A &&(4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329050339CST}{\text{\text{$\forall$}对\text{$\imp$}下沉\#R}})\\
\ind{6}\b \neg \forall x \neg A \imp \neg \forall x \neg B &&(5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250326093342CST}{\text{逆\text{$\neg$}引出\#1}})\\
\ind{7}\b \exists x A \imp \exists x B &&(6\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/compositions_of_fc/#20250325213235CST}{\text{特称量词\text{$\exists$}}})
\end{aligned}$$
规则4（假设无关前后件 $\exists$ 引入#R）： $\Gamma \vdash (A \imp B) \imp (\exists x A \imp \exists x B)$ （$x$ 在 $\Gamma$ 中无自由出现）
否定前件 $\forall$ 后件 $\exists$ 合并至 $\exists$
定理5（否定前件 $\forall$ 后件 $\exists$ 合并至 $\exists$ #E）： $\vdash (\forall x \neg A \imp \exists x B) \imp \exists x (\neg A \imp B)$
〔证明定理5〕
〔定理5证毕〕
$$\begin{aligned}
\ind{1}\b \forall x \neg A \imp \exists x B &&(\text{假设})\\
\ind{2}\b\b \forall x \neg (\neg A \imp B) &&(\text{假设})\\
\ind{3}\b\b \neg(\neg A \imp B) &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250416234555CST}{\text{\text{$\forall$}消除\#R}})\\
\ind{4}\b\b A \imp (\neg A \imp B) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250326092957CST}{\text{\text{$\neg\imp$}引出\#1}})\\
\ind{5}\b\b \neg (\neg A \imp B) \imp \neg A &&(4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250326093342CST}{\text{逆\text{$\neg$}引出\#1}})\\
\ind{6}\b\b \neg A &&(3,5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{7}\b\b \forall x \neg A &&(6\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{8}\b\b \exists x B &&(7,1\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{9}\b\b \neg \forall x \neg B &&(8\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/compositions_of_fc/#20250325213235CST}{\text{特称量词\text{$\exists$}}})\\
\ind{10}\b\b B \imp (\neg A \imp B) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325214136CST}{\text{\text{$\imp$}左引入\#1}})\\
\ind{11}\b\b \neg (\neg A \imp B) \imp \neg B &&(10\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250326093342CST}{\text{逆\text{$\neg$}引出\#1}})\\
\ind{12}\b\b \neg B &&(3,11\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{13}\b\b \forall x \neg B &&(12\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250418223903CST}{\text{可推式假设无关\text{$\forall$}引入\#E}})\\
\ind{14}\b\b \perp &&( ext{13,9矛盾})\\
\ind{15}\b \neg \forall x \neg (\neg A \imp B) &&(2\-14\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250410105419CST}{\text{归谬论}})\\
\ind{16}\b \exists x (\neg A \imp B) &&(15\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/compositions_of_fc/#20250325213235CST}{\text{特称量词\text{$\exists$}}})\\
\ind{17} (\forall x \neg A \imp \exists x B) \imp \exists x (\neg A \imp B) &&(1\-16\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})
\end{aligned}$$
规则5（否定前件 $\forall$ 后件 $\exists$ 合并至 $\exists$ #R）： $\forall x \neg A \imp \exists x B \vdash \exists x (\neg A \imp B)$
分隔前件 $\forall$ 变 $\exists$ 等价提前
定理6（分隔前件 $\forall$ 变 $\exists$ 等价提前#E）： $\vdash (\forall x A \imp B) \iff \exists x (A \imp B)$ （$x$ 在 $B$ 中无自由出现）
〔证明定理6〕
〔定理6证毕〕
$$\begin{aligned}
\ind{1} \b \forall x \neg (A \imp B) &&(\text{假设})\\
\ind{2} \b \neg(A \imp B) &&(1\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250416234555CST}{\text{\text{$\forall$}消除\#R}})\\
\ind{3} \b A \and \neg B &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250420224507CST}{\text{否定\text{$\imp$}等价式\#E}})\\
\ind{4} \b A &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_conjunction_and_disjunction/#20250409164133CST}{\text{\text{$\and$}拆分\#1}})\\
\ind{5} \b \neg B &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_conjunction_and_disjunction/#20250409164148CST}{\text{\text{$\and$}拆分\#2}})\\
\ind{6} \b \forall x A &&(4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{7} \b \forall x A \and \neg B &&(6,5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_conjunction_and_disjunction/#20250409175237CST}{\text{\text{$\and$}合成\#1}})\\
\ind{8} \b \neg (\forall x A \imp B) &&(7\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250420224507CST}{\text{否定\text{$\imp$}等价式\#E}})\\
\ind{9} \forall x \neg (A \imp B) \imp \neg (\forall x A \imp B) &&(1\-8\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{10} (\forall x A \imp B) \imp \neg \forall x \neg (A \imp B) &&(9\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250326093334CST}{\text{右\text{$\neg$}交换\#1}})\\
\ind{11} (\forall x A \imp B) \imp \exists x (A \imp B) &&(10\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/compositions_of_fc/#20250325213235CST}{\text{特称量词\text{$\exists$}}})\\
\ind{12} \b A \imp B &&(\text{假设})\\
\ind{13} \b\b \forall x A &&(\text{假设})\\
\ind{14} \b\b A &&(13\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250416234555CST}{\text{\text{$\forall$}消除\#R}})\\
\ind{15} \b\b B &&(14,12\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{16} \b \forall x A \imp B &&(13\-15\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{17} \exists x (A \imp B) \imp (\forall x A \imp B) &&(12\-16\href{#20250421193739CST}{\text{结论无关假设\text{$\exists$}引入}})\\
\ind{18} (\forall x A \imp B) \iff \exists x (A \imp B) &&(11,17\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250401065123CST}{\text{\text{$\iff$}合成\#1}})
\end{aligned}$$
规则6（分隔前件 $\forall$ 变 $\exists$ 等价提前#R）： $\forall x A \imp B \vdashv \exists x (A \imp B)$ （$x$ 在 $B$ 中无自由出现）
分隔前件 $\exists$ 变 $\forall$ 等价提前
定理7（分隔前件 $\exists$ 变 $\forall$ 等价提前#E）： $\vdash (\exists x A \imp B) \iff \forall x (A \imp B)$ （$x$ 在 $B$ 中无自由出现）
〔证明定理7〕
〔定理7证毕〕
$$\begin{aligned}
\ind{1} \b \exists x A \imp B &&(\text{假设})\\
\ind{2} \b\b A &&(\text{假设})\\
\ind{3} \b\b \exists x A &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250417224153CST}{\text{\text{$\exists$}引入\#R}})\\
\ind{4} \b\b B &&(3,1\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{5} \b A \imp B &&(2\-4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{6} \b \forall x (A \imp B) &&(5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{7} (\exists x A \imp B) \imp \forall x (A \imp B) &&(1\-6\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{8} \b \forall x (A \imp B) &&(\text{假设})\\
\ind{9} \b A \imp B &&(8\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250416234555CST}{\text{\text{$\forall$}消除\#R}})\\
\ind{10} \b\b A &&(\text{假设})\\
\ind{11} \b\b B &&(10，9\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{12} \b \exists x A \imp B &&(10,11\href{#20250421193739CST}{\text{结论无关假设\text{$\exists$}引入}})\\
\ind{13} \forall x (A \imp B) \imp (\exists x A \imp B) &&(8\-12\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{14} (\exists x A \imp B) \iff \forall x (A \imp B) &&(7,13\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250401065123CST}{\text{\text{$\iff$}合成\#1}})
\end{aligned}$$
规则7（分隔前件 $\exists$ 变 $\forall$ 等价提前#R）： $\exists x A \imp B \vdashv \forall x (A \imp B)$ （$x$ 在 $B$ 中无自由出现）
分隔后件 $\forall$ 等价提前
定理8（分隔后件 $\forall$ 等价提前#E）： $\vdash (A \imp \forall x B) \iff \forall x (A \imp B)$ （$x$ 在 $A$ 中无自由出现）
〔证明定理8〕
〔定理8证毕〕
$$\begin{aligned}
\ind{1} \b A \imp \forall x B &&(\text{假设})\\
\ind{2} \b\b A &&(\text{假设})\\
\ind{3} \b\b \forall x B &&(2,1\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{4} \b\b B &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250416234555CST}{\text{\text{$\forall$}消除\#R}})\\
\ind{5} \b A \imp B &&(2\-4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{6} \b \forall x (A \imp B) &&(5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{7} (A \imp \forall x B) \imp \forall x (A \imp B) &&(1\-6\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{8} \forall x (A \imp B) \imp (\forall x A \imp \forall x B) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250415135143CST}{\text{\text{$\forall$}对\text{$\imp$}下沉\#E}})\\
\ind{9} A \imp \forall x A &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250417110850CST}{\text{无关\text{$\forall$}引入\#E}})\\
\ind{10} (\forall x A \imp \forall x B) \imp (A \imp \forall x B) &&(9\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250326092937CST}{\text{\text{$\imp$}对\text{$\imp$}右逆插入\#1}})\\
\ind{11} \forall x (A \imp B) \imp (A \imp \forall x B) &&(8,10\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250413085601CST}{\text{\text{$\imp$}传递\#1}})\\
\ind{12} (A \imp \forall x B) \iff \forall x (A \imp B) &&(7,11\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250401065123CST}{\text{\text{$\iff$}合成\#1}})
\end{aligned}$$
规则8（分隔后件 $\forall$ 等价提前#R）： $A \imp \forall x B \vdashv \forall x (A \imp B)$ （$x$ 在 $A$ 中无自由出现）
分隔后件 $\exists$ 等价提前
定理9（分隔后件 $\exists$ 等价提前#E）： $\vdash (A \imp \exists x B) \iff \exists x (A \imp B)$ （$x$ 在 $A$ 中无自由出现）
〔证明定理9〕
〔定理9证毕〕
$$\begin{aligned}
\ind{1} \b A \imp \exists x B &&(\text{假设})\\
\ind{2} \b\b \neg \exists x (A \imp B) &&(\text{假设})\\
\ind{3} \b\b \forall x \neg (A \imp B) &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250418125702CST}{\text{\text{$\neg\exists$}等价\text{$\forall\neg$}\#R}})\\
\ind{4} \b\b \neg (A \imp B) &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250416234555CST}{\text{\text{$\forall$}消除\#R}})\\
\ind{5} \b\b A \and \neg B &&(4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250420224507CST}{\text{否定\text{$\imp$}等价式\#E}})\\
\ind{6} \b\b A &&(5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_conjunction_and_disjunction/#20250409164133CST}{\text{\text{$\and$}拆分\#1}})\\
\ind{7} \b\b \neg B &&(5\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_conjunction_and_disjunction/#20250409164148CST}{\text{\text{$\and$}拆分\#2}})\\
\ind{8} \b\b \forall x \neg B &&(7\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250329032623CST}{\text{可推式假设无关\text{$\forall$}引入\#R}})\\
\ind{9} \b\b \exists x B &&(6,1\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{10} \b\b \neg \forall x \neg B &&(9\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/compositions_of_fc/#20250325213235CST}{\text{特称量词\text{$\exists$}}})\\
\ind{11} \b\b \perp &&( ext{8,10矛盾})\\
\ind{12} \b \exists x (A \imp B) &&(2\-11\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_negation/#20250410105319CST}{\text{反证法}})\\
\ind{13} (A \imp \exists x B) \imp \exists x (A \imp B) &&(1\-12\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{14} \b A \imp B &&(\text{假设})\\
\ind{15} \b\b A &&(\text{假设})\\
\ind{16} \b\b B &&(15,14\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250325215058CST}{\text{\text{$\imp$}消除\#1}})\\
\ind{17} \b\b \exists x B &&(16\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250417224153CST}{\text{\text{$\exists$}引入\#R}})\\
\ind{18} \b A \imp \exists x B &&(15\-17\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_implication/#20250417105942CST}{\text{假设\text{$\imp$}引入\#1}})\\
\ind{19} \exists x (A \imp B) \imp (A \imp \exists x B) &&(14\-18\href{#20250421193739CST}{\text{结论无关假设\text{$\exists$}引入}})\\
\ind{20} (A \imp \exists x B) \iff \exists x (A \imp B) &&(13,19\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250401065123CST}{\text{\text{$\iff$}合成\#1}})
\end{aligned}$$
规则9（分隔后件 $\exists$ 等价提前#R）： $(A \imp \exists x B) \vdashv \exists x (A \imp B)$ （$x$ 在 $A$ 中无自由出现）
分隔左 $\forall$ 对 $\or$ 等价提前
定理10（分隔左 $\forall$ 对 $\or$ 等价提前#E）： $\vdash (\forall x A \or B) \iff \forall x (A \or B)$ （$x$ 在 $B$ 中无自由出现）
〔证明定理10〕
〔定理10证毕〕
$$\begin{aligned}
\ind{1} (\exists x \neg A \imp B) \iff \forall x (\neg A \imp B) &&(\href{#20250421094712CST}{\text{分隔前件\text{$\exists$}变\text{$\forall$}等价提前\#E}})\\
\ind{2} \neg \forall x A \iff \exists x \neg A &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250418123107CST}{\text{\text{$\neg\forall$}等价\text{$\exists\neg$}\#E}})\\
\ind{3} (\neg \forall x A \imp B) \iff (\exists x \neg A \imp B) &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250411190926CST}{\text{\text{$\imp$}对\text{$\iff$}右插入\#E}})\\
\ind{4} (\neg \forall x A \imp B) \iff \forall x (\neg A \imp B) &&(3,1\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250411123252CST}{\text{\text{$\iff$}传递\#1}})\\
\ind{5} (\forall x A \or B) \iff \forall x (A \or B) &&(4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/compositions_of_fc/#20250325213146CST}{\text{析取联结词\text{$\or$}}})
\end{aligned}$$
规则10（分隔左 $\forall$ 对 $\or$ 等价提前#R）： $\forall x A \or B \vdashv \forall x (A \or B)$ （$x$ 在 $B$ 中无自由出现）
分隔左 $\exists$ 对 $\or$ 等价提前
定理11（分隔左 $\exists$ 对 $\or$ 等价提前#E）： $\vdash (\exists x A \or B) \iff \exists x (A \or B)$ （$x$ 在 $B$ 中无自由出现）
〔证明定理11〕
〔定理11证毕〕
$$\begin{aligned}
\ind{1} (\forall x \neg A \imp B) \iff \exists x (\neg A \imp B) &&(\href{#20250419094709CST}{\text{分隔前件\text{$\forall$}变\text{$\exists$}等价提前\#E}})\\
\ind{2} \neg \exists x A \iff \forall x \neg A &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250418125109CST}{\text{\text{$\neg\exists$}等价\text{$\forall\neg$}\#E}})\\
\ind{3} (\neg \exists x A \imp B) \iff (\forall x \neg A \imp B) &&(2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250411190926CST}{\text{\text{$\imp$}对\text{$\iff$}右插入\#E}})\\
\ind{4} (\neg \exists x A \imp B) \iff \exists x (\neg A \imp B) &&(3,1\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250411123252CST}{\text{\text{$\iff$}传递\#1}})\\
\ind{5} (\exists x A \or B) \iff \exists x (A \or B) &&(4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/compositions_of_fc/#20250325213146CST}{\text{析取联结词\text{$\or$}}})
\end{aligned}$$
规则11（分隔左 $\exists$ 对 $\or$ 等价提前#R）： $\exists x A \or B \vdashv \exists x (A \or B)$ （$x$ 在 $B$ 中无自由出现）
分隔右 $\forall$ 对 $\or$ 等价提前
定理12（分隔右 $\forall$ 对 $\or$ 等价提前#E）： $\vdash (A \or \forall x B) \iff \forall x (A \or B)$ （$x$ 在 $A$ 中无自由出现）
〔证明定理12〕
〔定理12证毕〕
$$\begin{aligned}
\ind{1} (A \or \forall x B) \iff (\forall x B \or A) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_boolean_algebra/#20250410151100CST}{\text{\text{$\or$}交换律\#R1}})\\
\ind{2} (\forall x B \or A) \iff \forall x (B \or A) &&(\href{#20250422001417CST}{\text{分隔左\text{$\forall$}对\text{$\or$}等价提前\#E}})\\
\ind{3} B \or A \iff A \or B &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_boolean_algebra/#20250410151100CST}{\text{\text{$\or$}交换律\#R1}})\\
\ind{4} \forall x (B \or A) \iff \forall x (A \or B) &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250415122439CST}{\text{\text{$\iff$}同时\text{$\forall$}\#R}})\\
\ind{5} (A \or \forall x B) \iff \forall x (A \or B) &&(1,2,4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250413163210CST}{\text{\text{$\iff$}传递\#2}})
\end{aligned}$$
规则12（分隔右 $\forall$ 对 $\or$ 等价提前#R）： $(A \or \forall x B) \vdashv \forall x (A \or B)$ （$x$ 在 $A$ 中无自由出现）
分隔右 $\exists$ 对 $\or$ 等价提前
定理13（分隔右 $\exists$ 对 $\or$ 等价提前#E）： $\vdash (A \or \exists x B) \iff \exists x (A \or B)$ （$x$ 在 $A$ 中无自由出现）
〔证明定理13〕
〔定理13证毕〕
$$\begin{aligned}
\ind{1} (A \or \exists x B) \iff (\exists x B \or A) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_boolean_algebra/#20250410151100CST}{\text{\text{$\or$}交换律\#R1}})\\
\ind{2} (\exists x B \or A) \iff \exists x (B \or A) &&(\href{#20250422095243CST}{\text{分隔左\text{$\exists$}对\text{$\or$}等价提前\#E}})\\
\ind{3} B \or A \iff A \or B &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_boolean_algebra/#20250410151100CST}{\text{\text{$\or$}交换律\#R1}})\\
\ind{4} \exists x (B \or A) \iff \exists x (A \or B) &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250419122738CST}{\text{\text{$\iff$}同时\text{$\exists$}\#E}})\\
\ind{5} (A \or \exists x B) \iff \exists x (A \or B) &&(1,2,4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250413163210CST}{\text{\text{$\iff$}传递\#2}})
\end{aligned}$$
规则13（分隔右 $\forall$ 对 $\or$ 等价提前#R）： $A \or \forall x B \vdashv \forall x (A \or B)$ （$x$ 在 $A$ 中无自由出现）
分隔左 $\forall$ 对 $\and$ 等价提前
定理14（分隔左 $\forall$ 对 $\and$ 等价提前#E）： $\vdash (\forall x A \and B) \iff \forall x (A \and B)$ （$x$ 在 $B$ 中无自由出现）
〔证明〕
〔证毕〕
$$\begin{aligned}
\ind{1} \neg (\forall x A \imp \neg B) \iff \neg \exists x (A \imp \neg B) &&(\href{#20250419094709CST}{\text{分隔前件\text{$\forall$}变\text{$\exists$}等价提前\#E}})\\
\ind{2} \neg \exists x (A \imp \neg B) \iff \forall x \neg (A \imp \neg B) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250418125109CST}{\text{\text{$\neg\exists$}等价\text{$\forall\neg$}\#E}})\\
\ind{3} \neg (\forall x A \imp \neg B) \iff \forall x \neg (A \imp \neg B) &&(1,2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250411123252CST}{\text{\text{$\iff$}传递\#1}})
\end{aligned}$$
规则14（分隔左 $\forall$ 对 $\and$ 等价提前#R）： $\forall x A \and B \vdashv \forall x (A \and B)$ （$x$ 在 $B$ 中无自由出现）
分隔左 $\exists$ 对 $\and$ 等价提前
定理15（分隔左 $\exists$ 对 $\and$ 等价提前#E）： $\vdash (\exists x A \and B) \iff \exists x (A \and B)$ （$x$ 在 $B$ 中无自由出现）
〔证明定理15〕
〔定理15证毕〕
$$\begin{aligned}
\ind{1} \neg (\exists x A \imp \neg B) \iff \neg \forall x (A \imp \neg B) &&(\href{#20250421094712CST}{\text{分隔前件\text{$\exists$}变\text{$\forall$}等价提前\#E}})\\
\ind{2} \neg \forall x (A \imp \neg B) \iff \exists x \neg (A \imp \neg B) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250418123107CST}{\text{\text{$\neg\forall$}等价\text{$\exists\neg$}\#E}})\\
\ind{3} \neg (\exists x A \imp \neg B) \iff \exists x \neg (A \imp \neg B) &&(1,2\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250411123252CST}{\text{\text{$\iff$}传递\#1}})
\end{aligned}$$
规则15（分隔左 $\exists$ 对 $\and$ 等价提前#R）： $\exists x A \and B \vdashv \exists x (A \and B)$ （$x$ 在 $B$ 中无自由出现）
分隔右 $\forall$ 对 $\and$ 等价提前
定理16（分隔右 $\forall$ 对 $\and$ 等价提前#E）： $\vdash (A \and \forall x B) \iff \forall x (A \and B)$ （$x$ 在 $A$ 中无自由出现）
〔证明定理16〕
〔定理16证毕〕
$$\begin{aligned}
\ind{1} (A \and \forall x B) \iff (\forall x B \and A) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_boolean_algebra/#20250410151153CST}{\text{\text{$\and$}交换律\#E1}})\\
\ind{2} (\forall x B \and A) \iff \forall x (B \and A) &&(\href{#20250422130150CST}{\text{分隔左\text{$\forall$}对\text{$\and$}等价提前\#E}})\\
\ind{3} B \and A \iff A \and B &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_boolean_algebra/#20250410151153CST}{\text{\text{$\and$}交换律\#E1}})\\
\ind{4} \forall x (B \and A) \iff \forall x (A \and B) &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250415122439CST}{\text{\text{$\iff$}同时\text{$\forall$}\#R}})\\
\ind{5} (A \and \forall x B) \iff \forall x (A \and B) &&(1,2,4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250413163210CST}{\text{\text{$\iff$}传递\#2}})
\end{aligned}$$
规则16（分隔右 $\forall$ 对 $\and$ 等价提前#R）： $A \and \forall x B \vdashv \forall x (A \and B)$ （$x$ 在 $A$ 中无自由出现）
分隔右 $\exists$ 对 $\and$ 等价提前
定理17（分隔右 $\exists$ 对 $\and$ 等价提前#E）： $\vdash (A \and \exists x B) \iff \exists x (A \and B)$ （$x$ 在 $A$ 中无自由出现）
〔证明定理17〕
〔定理17证毕〕
$$\begin{aligned}
\ind{1} (A \and \exists x B) \iff (\exists x B \and A) &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_boolean_algebra/#20250410151153CST}{\text{\text{$\and$}交换律\#E1}})\\
\ind{2} (\exists x B \and A) \iff \exists x (B \and A) &&(\href{#20250422130944CST}{\text{分隔左\text{$\exists$}对\text{$\and$}等价提前\#E}})\\
\ind{3} B \and A \iff A \and B &&(\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_boolean_algebra/#20250410151153CST}{\text{\text{$\and$}交换律\#E1}})\\
\ind{4} \exists x (B \and A) \iff \exists x (A \and B) &&(3\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_first-order_predicate_calculus/theorems_about_qualifiers_in_fc_part_1/#20250419122742CST}{\text{\text{$\iff$}同时\text{$\exists$}\#R}})\\
\ind{5} (A \and \exists x B) \iff \exists x (A \and B) &&(1,2,4\href{/posts/science/mathematics/metamathematics/naive_mathematical_logic/formal_system_of_propositional_calculus/theorems_in_pc_equivalence/#20250413163210CST}{\text{\text{$\iff$}传递\#2}})
\end{aligned}$$
规则17（分隔右 $\exists$ 对 $\and$ 等价提前#R）： $A \and \exists x B \vdashv \exists x (A \and B)$ （$x$ 在 $A$ 中无自由出现）