PC 中的公理也是 FC 中的定理。
FC 中的定理，证明以及演绎，演绎结果的定义与 PC 中是一样的！
$$ \begin{align*} 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) \end{align*} $$
$v$相关
$$ \begin{align*} A_4:&&&\forall vA\to A^v_t,t对A的变元v可代入\\ A_5:&&&\forall v(A\to B)\to(\forall vA\to \forall vB) \\ A_6:&&& A\to \forall vA, \bold {v在A中无自由出现} \end{align*} $$
$$ \begin{align*} T_1:&&& \vdash \forall vA\to A \\ T_2:&&& \vdash A\to \exist vA \\ T_3:&&& \vdash \forall vA \to \exist vA \\ T_4:&&& \text{if} \vdash A, \text{then} \vdash \forall vA \\ T_5:&&& \text{if} \ \Gamma \vdash A,\text{then} \ \Gamma\vdash \forall vA \quad \bold{v在\Gamma中无自由出现} \\ &&& T_4 \& T_5: \textcolor{blue}{全称推广定理} \\ T_8:&&& \text{if} \ \Gamma\cup \{A\} 是不一致的, 那么 \Gamma \vdash \neg A \quad 反证法 \\ T_{10}:&&&\text{if}\ \Gamma \vdash \exist vA \ \text{and} \ \Gamma ;A\vdash B, \text{then} \ \Gamma\vdash B \quad \bold{v在\Gamma和B中无自由出现} \end{align*} $$
语义或者说结构是解释「某个命题具体在什么『定义域』上讨论什么问题」，一个语义包含论域 $D$ 和解释 $I$。
例如：对于公式 $\exist xG(x, y)$，一个可能的语义是：
这样 $\exist xG$ 就有了明确的意义：$\exist x, x<y$。
解释通常用「使谓词为 1 的个体变元的集合」表示，如 $\bar{P}=\{(0,0),(0,1)\}$ 表示对于二元谓词 $P(x, y)$ 当且仅当 $(x, y)=(0,0)$ 或 $(0,1)$ 时为真。