公理集合

FC 系统共 6 条公理，其中 $A_1$—$A_3$ 为 PC 的公理。

$$ \begin{aligned} A_1&:A\to(B\to A) \\ A_2&:(A\to(B\to C))\to((A\to B)\to(A\to C)) \\ A_3&:(\neg A\to\neg B)\to(B\to A) \\ A_4&:\forall vA\to A_t^v\qquad t\text{ 对 }v\text{ 可代入} \\ A_5&:\forall v(A\to B)\to(\forall vA\to\forall vB) \\ A_6&:A\to\forall vA\qquad v\text{ 在 }A\text{ 中无自由出现} \end{aligned} $$

推理规则

分离规则

$$ r_{mp}: \frac{A, A\to B}{B} $$

基本定理

下述定理的名字仅为本人为方便记忆所取，并非来自可信来源。

定理 1：任取消除

前件的 $\forall$ 可以直接消除。

$$ \vdash_{FC}\forall vA\to A $$

定理 2：存在引入

可以在后件直接引入 $\exist$。

$$ \vdash_{FC}A\to\exist vA $$

定理 3：定理 1 + 定理 2

$$ \vdash_{FC}\forall vA\to\exist vA $$

定理 4：全称推广（1）

对在 FC 中的任何公式 $A$，

$$ \text{if }\vdash A, \text{then}\vdash\forall vA $$