Index src

公式

strict provable sort wff;

设置聚合公式的办法，与latex一致

def cbw (A: wff): wff = $ A $;
notation cbw (A: wff): wff = ($\wff{$:max) A ($}$:0);

集合

pure sort set;

类

strict sort class;

类的表示

term cab {x: set} (P: wff x): class;
prefix cab: $\class$ prec max;

集合到类的转换

term cv (x: set): class;
coercion cv: set > class;

设置花括号是聚合类所用，与latex一致

def cbc (x: class): class = $ x $;
notation cbc (x: class): class = (${$:max) x ($}$:0);

否定联结词¬A

term neg (A: wff): wff;
prefix neg: $\neg$ prec 50;

蕴涵联结词A→B

term imp (A B: wff): wff;
infixr imp: $\imp$ prec 20;

合取联结词A∧B

def and (A B: wff): wff = $ \neg (A \imp \neg B) $;
infixl and: $\and$ prec 30;

析取联结词A∨B

def or (A B: wff): wff = $ \neg A \imp B $;
infixl or: $\or$ prec 30;

等价联结词A↔B

def iff (A B: wff): wff = $ (A \imp B) \and (B \imp A) $;
infixr iff: $\iff$ prec 10;

等于谓词x=y

term eq (x y: class): wff;
infixl eq: $=$ prec 60;

属于谓词x∈y

term in (x y: class): wff;
infixl in: $\in$ prec 60;

包括谓词x∋y

def cont (x y: class): wff = $ y \in x $;
infixl cont: $\cont$ prec 60;

不等于谓词x/=y

def ne (x y: class): wff = $ \neg x = y $;
infixl ne: $\ne$ prec 60;

不属于谓词x/∈y

def nin (x y: class): wff = $ \neg x \in y $;
infixl nin: $\nin$ prec 60;

不包括谓词x/∋y

def ncont (x y: class): wff = $ \neg x \cont y $;
infixl ncont: $\ncont$ prec 60;

任意量词∀x

term fo {x: set} (P: wff x): wff;
prefix fo: $\fo$ prec 50;

存在量词∃x

def ex {x: set} (P: wff x): wff = $ \neg \fo x \neg P $;
prefix ex: $\ex$ prec 50;

不存在量词∄x

def nex {x: set} (P: wff x): wff = $ \neg \ex x P $;
prefix nex: $\nex$ prec 50;

最多一个量词∃*x

def mo {x: set} (P: wff x): wff = $ \ex y \fo x (P \imp x = y) $;
prefix mo: $\mo$ prec 50;

存在唯一量词∃!x

def eu {x: set} (P: wff x): wff = $ \ex y \fo x (P \iff x = y) $;
prefix eu: $\eu$ prec 50;

限域任意量词(∀x∈y)

def foin {x: set} (y: class) (P: wff x): wff = $ \fo x (x \in y \imp P) $;
prefix foin: $\foin$ prec 50;

限域存在量词(∃x∈y)

def exin {x: set} (y: class) (P: wff x): wff = $ \ex x (x \in y \and P) $;
prefix exin: $\exin$ prec 50;

限域不存在量词(∄x∈y)

def nexin {x: set} (y: class) (P: wff x): wff = $ \nex x (x \in y \and P) $;
prefix nexin: $\nexin$ prec 50;

限域做多一个量词(∃*x∈y)

def moin {x: set} (y: class) (P: wff x): wff = $ \mo x (x \in y \and P) $;
prefix moin: $\moin$ prec 50;

限域存在唯一量词(∃!x∈y)

def euin {x: set} (y: class) (P: wff x): wff = $ \eu x (x \in y \and P) $;
prefix euin: $\euin$ prec 50;

真值⊤

def true: wff = $ \fo x x = x \imp \fo x x = x $;
prefix true: $\true$ prec max;

假值⊥

def false: wff = $ \neg \true $;
prefix false: $\false$ prec max;

无关Ⅎx

def nf {x: set} (A: wff x): wff = $ \ex x A \imp \fo x A $;
prefix nf: $\nf$ prec 50;

替换[y/x]

def sb (y: set) {x: set} (P: wff x): wff = $ \fo t (t = y \imp \fo x (x = t \imp P)) $;
prefix sb: $\sb$ prec 50;

上一步骤后件标识符hold

term hold: wff;
prefix hold: $\_$ prec max;

分离规则mp

axiom ax_mp (A B: wff): $ A \imp B $ > $ A $ > $ B $;

公理1

axiom ax_1 (A B: wff): $ A \imp B \imp A $;

公理2

axiom ax_2 (A B C: wff): $ (A \imp B \imp C) \imp (A \imp B) \imp A \imp C $;

公理3

axiom ax_3 (A B: wff): $ (\neg A \imp \neg B) \imp B \imp A $;

全称化规则gen

axiom ax_gen {x: set} (A: wff x): $ A $ > $ \fo x A $;

公理4

axiom ax_4 {x: set} (A B: wff x): $ \fo x (A \imp B) \imp \fo x A \imp \fo x B $;

公理5

axiom ax_5 (A: wff) {x: set}: $ A \imp \fo x A $;

公理6

axiom ax_6 {x: set} (y: set): $ \ex x x = y $;

公理7

axiom ax_7 (x y z: set): $ x = y \imp x = z \imp y = z $;

公理8

axiom ax_8 (x y z: set): $ x = y \imp x \in z \imp y \in z $;

公理9

axiom ax_9 (x y z: set): $ x = y \imp z \in x \imp z \in y $;

公理10

axiom ax_10 {x: set} (P: wff x): $ \neg \fo x P \imp \fo x \neg \fo x P $;

公理11

axiom ax_11 {x y: set} (P: wff x y): $ \fo x \fo y P \imp \fo y \fo x P $;

公理12

axiom ax_12 {x: set} (y: set) (P: wff x): $ x = y \imp P \imp \fo x (x = y \imp P) $;

公理13

axiom ax_13 {x: set} (y z: set): $ \neg x = y \imp y = z \imp \fo x y = z $;

外延公理

axiom ax_ext {z: set} (x y: set): $ \fo z (z \in x \iff z \in y) \imp x = y $;

替换公理

axiom ax_rep {w x y z: set} (P: wff w x y z): $ \fo x \ex y \fo z (\fo y P \imp z = y) \imp \ex y \fo z (z \in y \iff \ex w (w \in x \and \fo y P)) $;

幂集公理

axiom ax_pow {w y z: set} (x: set): $ \ex y \fo z (\fo w (w \in z \imp w \in x) \imp z \in y) $;

并集公理

axiom ax_un {w y z: set} (x: set): $ \ex y \fo z (\ex w (z \in w \and w \in x) \imp z \in y) $;

正则公理

axiom ax_reg {y z: set} (x: set): $ \ex y y \in x \imp \ex y (y \in x \and \fo z (z \in y \imp \neg z \in x)) $;

无穷公理

axiom ax_inf {w y z: set} (x: set): $ \ex y (x \in y \and \fo z (z \in y \imp \ex w (z \in w \and w \in y))) $;

选择公理

axiom ax_ac {t u v w y z: set} (x: set):
  $ \ex y \fo z \fo w (z \in w \and w \in x \imp \ex v \fo u (\ex t (u \in w \and w \in t \and (u \in t \and t \in y)) \iff u = v)) $;

类定义公理

axiom df_clab {x y: set} (P: wff x y): $ x \in \class y P \iff \sb x y P $;

类等式公理

axiom df_cleq (A B: class) {u v x: set} (y z t: set):
  $ y = z \iff \fo u (u \in y \iff u \in z) $ >
  $ t = t \iff \fo v (v \in t \iff v \in t) $ >
  $ A = B \iff \fo x (x \in A \iff x \in B) $;

类属于公理

axiom df_clel (A B: class) {u v x: set} (y z t: set):
  $ y \in z \iff \ex u (u = y \and u \in z) $ >
  $ t \in t \iff \ex v (v = t \and v \in t) $ >
  $ A \in B \iff \ex x (x = A \and x \in B) $;

左引入\imp

theorem introl_imp (A B: wff): $ A \imp B \imp A $;

\imp左插入

theorem imp_imp_insl (A B C: wff): $ (A \imp B \imp C) \imp (A \imp B) \imp A \imp C $;

同一律

theorem imp_refl (A: wff): $ A \imp A $;

\imp左引入\imp

theorem imp_introl_imp (A B C: wff): $ (B \imp C) \imp (A \imp B) \imp A \imp C $;

\imp\imp左交换

theorem imp_imp_swapl (A B C: wff): $ (A \imp B \imp C) \imp B \imp A \imp C $;

MP公式

theorem mp_thm (A B: wff): $ (A \imp B) \imp A \imp B $;

MP公式调换形式

theorem mp_hswap_thm (A B: wff): $ A \imp (A \imp B) \imp B $;

带前件的MP公式

theorem mp_with_ant_thm (A B C: wff): $ (A \imp B \imp C) \imp (A \imp B) \imp A \imp C $;

\imp左引入右侧

theorem imp_introrsl_imp (A B C: wff): $ (A \imp B) \imp A \imp C \imp B $;

\imp右侧左消除

theorem imp_imp_elimrsl (A B C: wff): $ (A \imp B \imp C) \imp B \imp A \imp C $;

\imp对\imp右逆引入

theorem imp_introrevr_imp (A B C: wff): $ (A \imp B) \imp (B \imp C) \imp A \imp C $;

\imp传递

theorem imp_tran (A B C: wff): $ (A \imp B) \imp (B \imp C) \imp A \imp C $;

\imp继位

theorem imp_replast (A B C D: wff): $ (A \imp B \imp C) \imp (C \imp D) \imp A \imp B \imp D $;

\imp替换第二位

theorem imp_repsecond (A B C D: wff): $ (A \imp B \imp C) \imp (D \imp B) \imp A \imp D \imp C $;

\imp左提取

theorem imp_imp_extl (A B C: wff): $ ((A \imp B) \imp A \imp C) \imp A \imp B \imp C $;

\imp右插入

theorem imp_imp_insr (A B C: wff): $ ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C $;

\imp左同化

theorem imp_imp_assiml (A B: wff): $ (A \imp A \imp B) \imp A \imp B $;

\imp正结合

theorem imp_assocfwd (A B C: wff): $ ((A \imp B) \imp C) \imp A \imp B \imp C $;

\neg\imp逆消除

theorem neg_imp_elimrev (A B: wff): $ (\neg A \imp \neg B) \imp B \imp A $;

\neg消除右引入\imp

theorem neg_elimintror_imp (A B: wff): $ \neg A \imp A \imp B $;

右引入\neg\imp

theorem intror_neg_imp (A B: wff): $ A \imp \neg A \imp B $;

\neg\neg消除

theorem negneg_elim (A: wff): $ \neg \neg A \imp A $;

\neg\neg引出

theorem negneg_intro (A: wff): $ A \imp \neg \neg A $;

\neg\imp交换

theorem neg_imp_swap (A B: wff): $ (\neg A \imp B) \imp \neg B \imp A $;

\imp\neg交换

theorem imp_neg_swap (A B: wff): $ (A \imp \neg B) \imp B \imp \neg A $;

\imp逆引入\neg

theorem imp_introrev_neg (A B: wff): $ (A \imp B) \imp \neg B \imp \neg A $;

\neg\imp左拆分

theorem negimp_splitl (A B: wff): $ \neg (A \imp B) \imp A $;

\neg\imp右拆分\neg

theorem negimp_splitr_neg (A B: wff): $ \neg (A \imp B) \imp \neg B $;

\neg\imp合成

theorem negimp_comp (A B: wff): $ A \imp \neg B \imp \neg (A \imp B) $;

\neg\imp推出同一

theorem neg_imp_tosame (A: wff): $ (\neg A \imp A) \imp A $;

\imp\neg推出同一\neg

theorem imp_neg_tosame_neg (A: wff): $ (A \imp \neg A) \imp \neg A $;

\imp左合并\neg\imp

theorem imp_mergel_neg_imp (A B C: wff): $ (A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C $;

\neg\imp与\imp左合并\imp

theorem neg_imp_with_imp_mergel_imp (A B C: wff): $ (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp C $;

\imp左矛盾消去

theorem imp2_elimcontradl (A B: wff): $ (A \imp B) \imp (\neg A \imp B) \imp B $;

矛盾律

theorem contradiction (A: wff): $ \neg (A \and \neg A) $;

\and合成

theorem and_comp (A B: wff): $ A \imp B \imp A \and B $;

\and左拆分

theorem and_splitl (A B: wff): $ A \and B \imp A $;

\and右拆分

theorem and_splitr (A B: wff): $ A \and B \imp B $;

\imp左左\and引入

theorem imp_introlsl_and (A B C: wff): $ (B \imp C) \imp A \and B \imp C $;

\imp左右\and引入

theorem imp_introlsr_and (A B C: wff): $ (A \imp C) \imp A \and B \imp C $;

\imp左引入\and

theorem imp_introl_and (A B C: wff): $ (A \imp B) \imp C \and A \imp C \and B $;

\imp右引入\and

theorem imp_intror_and (A B C: wff): $ (A \imp B) \imp A \and C \imp B \and C $;

\and左更新

theorem and_updl (A B C: wff): $ A \and B \imp (A \imp C) \imp C \and B $;

\and右更新

theorem and_updr (A B C: wff): $ A \and B \imp (B \imp C) \imp A \and C $;

嵌套前件聚合\and

theorem imp_nested_assemb_and (A B C: wff): $ (A \imp B \imp C) \imp A \and B \imp C $;

前件\and拆解嵌套\imp

theorem and_imp_break_nested (A B C: wff): $ (A \and B \imp C) \imp A \imp B \imp C $;

\imp对\and左提取

theorem imp_and_extl (A B C: wff): $ (A \imp B) \and (A \imp C) \imp A \imp B \and C $;

\imp右聚集\and

theorem imp_collectr_and (A B C: wff): $ (A \imp B) \imp (A \imp C) \imp A \imp B \and C $;

\imp\and右提取

theorem imp_and_extr (A B C: wff): $ (A \imp C) \and (B \imp C) \imp A \and B \imp C $;

\imp左聚集\and

theorem imp_collectl_and (A B C: wff): $ (A \imp C) \imp (B \imp C) \imp A \and B \imp C $;

\imp\and左插入

theorem imp_and_insl (A B C: wff): $ (A \imp B \and C) \imp (A \imp B) \and (A \imp C) $;

\imp\and右侧右拆分

theorem imp_and_splitrsl (A B C: wff): $ (A \imp B \and C) \imp A \imp B $;

\imp\and右侧左拆分

theorem imp_and_splitrsr (A B C: wff): $ (A \imp B \and C) \imp A \imp C $;

假设为空时引入假设（不可直接引用）

theorem _hyp_null_intro (G: wff): $ G \imp G $;

假设不为空时引入假设（不可直接引用）

theorem _hyp_intro (A G: wff): $ G \and A \imp A $;

假设为空时补全假设（不可直接引用）

theorem _hyp_null_complete (A G: wff): $ A $ > $ G \imp A $;

假设不为空时补全假设（不可直接引用）

theorem _hyp_complete (A G_1 G_2: wff): $ G_1 \imp A $ > $ G_1 \and G_2 \imp A $;

带假设的mp规则（不可直接引用）

theorem _hyp_mp (A B G: wff): $ G \imp A \imp B $ > $ G \imp A $ > $ G \imp B $;

假设移出（不可直接引用）

theorem _hyp_rm (A G_1 G_2: wff): $ G_1 \and G_2 \imp A $ > $ G_1 \imp G_2 \imp A $;

假设为空时对移出的假设进行收集（不可直接引用）

theorem _hyp_null_collect (A G_1 G_2: wff): $ G_1 \imp G_2 \imp A $ > $ G_1 \and G_2 \imp A $;

假设不为空时对移出的假设进行收集（不可直接引用）

theorem _hyp_collect (A G_1 G_2 G_3: wff): $ G_1 \imp G_2 \imp G_3 \imp A $ > $ G_1 \imp G_2 \and G_3 \imp A $;

排中律

theorem excluded_middle (A: wff): $ A \or \neg A $;

\or左引入

theorem introl_or (A B: wff): $ B \imp A \or B $;

\or右引入

theorem intror_or (A B: wff): $ A \imp A \or B $;

\and蕴涵\or

theorem and_to_or (A B: wff): $ A \and B \imp A \or B $;

\or对\imp左引入

theorem imp_introl_or (A B C: wff): $ (A \imp B) \imp C \or A \imp C \or B $;

\or对\imp右引入

theorem imp_intror_or (A B C: wff): $ (A \imp B) \imp A \or C \imp B \or C $;

\or左更新

theorem or_updl (A B C: wff): $ A \or B \imp (A \imp C) \imp C \or B $;

\or右更新

theorem or_updr (A B C: wff): $ A \or B \imp (B \imp C) \imp A \or C $;

\or左消除

theorem or_eliml (A B: wff): $ A \or B \imp \neg A \imp B $;

\or右消除

theorem or_elimr (A B: wff): $ A \or B \imp \neg B \imp A $;

\imp\or左插入

theorem imp_or_insl (A B C: wff): $ (A \imp B \or C) \imp (A \imp B) \or (A \imp C) $;

\imp\or左提取

theorem imp_or_extl (A B C: wff): $ (A \imp B) \or (A \imp C) \imp A \imp B \or C $;

\imp\or右插入

theorem or_imp_insr (A B C: wff): $ (A \or B \imp C) \imp (A \imp C) \or (B \imp C) $;

\imp\and左插入\or

theorem imp_and_insl_or (A B C: wff): $ (A \imp B \and C) \imp (A \imp B) \or (A \imp C) $;

\imp\and左提取\or

theorem imp_and_extl_or (A B C: wff): $ (A \imp B) \and (A \imp C) \imp A \imp B \or C $;

\imp\and右插入\or

theorem and_imp_insr_or (A B C: wff): $ (A \and B \imp C) \imp (A \imp C) \or (B \imp C) $;

\imp\and右提取\or

theorem imp_and_extr_or (A B C: wff): $ (A \imp C) \and (B \imp C) \imp A \or B \imp C $;

\imp左聚集\or

theorem imp_collectl_or (A B C: wff): $ (A \imp C) \imp (B \imp C) \imp A \or B \imp C $;

\or\imp右插入\and

theorem or_imp_insr_and (A B C: wff): $ (A \or B \imp C) \imp (A \imp C) \and (B \imp C) $;

\or\imp左侧左拆分

theorem or_imp_splitlsl (A B C: wff): $ (A \or B \imp C) \imp A \imp C $;

\or\imp左侧右拆分

theorem or_imp_splitlsr (A B C: wff): $ (A \or B \imp C) \imp B \imp C $;

\imp\or右提取\and

theorem imp_or_extr_and (A B C: wff): $ (A \imp C) \or (B \imp C) \imp A \and B \imp C $;

\iff合成

theorem iff_comp (A B: wff): $ (A \imp B) \imp (B \imp A) \imp (A \iff B) $;

\iff正分解

theorem iff_decomp (A B: wff): $ (A \iff B) \imp A \imp B $;

\iff逆分解

theorem iff_decompbwd (A B: wff): $ (A \iff B) \imp B \imp A $;

\iff正消除

theorem iff_eliml (A B: wff): $ (A \iff B) \imp A \imp B $;

\iff逆消除

theorem iff_elimr (A B: wff): $ (A \iff B) \imp B \imp A $;

\iff自反

theorem iff_refl (A: wff): $ A \iff A $;

\and定义式

theorem and_def (A B: wff): $ A \and B \iff \neg (A \imp \neg B) $;

\or定义式

theorem or_def (A B: wff): $ A \or B \iff \neg A \imp B $;

\iff对称

theorem iff_symm (A B: wff): $ (A \iff B) \imp (B \iff A) $;

\iff交换

theorem iff_comm (A B: wff): $ (A \iff B) \iff B \iff A $;

\imp对\imp左置换

theorem imp_imp_perml (A B C: wff): $ A \imp B \imp C \iff B \imp A \imp C $;

\imp对\imp左折叠

theorem imp_imp_foldl (A B: wff): $ A \imp A \imp B \iff A \imp B $;

\imp逆指配\neg

theorem imp_allocrev_neg (A B: wff): $ A \imp B \iff \neg B \imp \neg A $;

\neg\imp置换

theorem neg_imp_perm (A B: wff): $ \neg A \imp B \iff \neg B \imp A $;

\imp\neg置换

theorem imp_neg_perm (A B: wff): $ A \imp \neg B \iff B \imp \neg A $;

\neg\neg等价

theorem negneg_alloc (A: wff): $ A \iff \neg \neg A $;

嵌套前件收集\and

theorem imp_nested_gatherl_and (A B C: wff): $ A \imp B \imp C \iff A \and B \imp C $;

\imp\imp左分配

theorem imp_imp_distl (A B C: wff): $ A \imp B \imp C \iff (A \imp B) \imp A \imp C $;

\imp\and左分配

theorem imp_and_distl (A B C: wff): $ A \imp B \and C \iff (A \imp B) \and (A \imp C) $;

\imp\or左分配

theorem imp_or_distl (A B C: wff): $ A \imp B \or C \iff (A \imp B) \or (A \imp C) $;

\and\imp右分配\or

theorem and_imp_distr_or (A B C: wff): $ A \and B \imp C \iff (A \imp C) \or (B \imp C) $;

\or\imp右分配\and

theorem or_imp_distr_and (A B C: wff): $ A \or B \imp C \iff (A \imp C) \and (B \imp C) $;

\imp\iff左插入

theorem imp_iff_insl (A B C: wff): $ (A \imp (B \iff C)) \imp (A \imp B \iff A \imp C) $;

\imp\iff左提取

theorem imp_iff_extl (A B C: wff): $ (A \imp B \iff A \imp C) \imp A \imp (B \iff C) $;

\imp\iff左分配

theorem imp_iff_distl (A B C: wff): $ A \imp (B \iff C) \iff A \imp B \iff A \imp C $;

\iff左引入\imp

theorem iff_introl_imp (A B C: wff): $ (B \iff C) \imp (A \imp B \iff A \imp C) $;

\iff右引入\imp

theorem iff_intror_imp (A B C: wff): $ (A \iff B) \imp (A \imp C \iff B \imp C) $;

\iff\imp左插入

theorem iff_imp_insl (A B C: wff): $ (A \iff B \imp C) \imp (A \iff B) \imp (A \iff C) $;

\imp\iff右插入

theorem imp_iff_insr (A B C: wff): $ (A \imp B \iff C) \imp (A \iff C) \imp (B \iff C) $;

\iff传递

theorem iff_tran (A B C: wff): $ (A \iff B) \imp (B \iff C) \imp (A \iff C) $;

\iff\imp传递至\imp

theorem iff_imp_tran_imp (A B C: wff): $ (A \iff B) \imp (B \imp C) \imp A \imp C $;

\imp\iff传递至\imp

theorem imp_iff_tran_imp (A B C: wff): $ (A \imp B) \imp (B \iff C) \imp A \imp C $;

\iff引入\neg

theorem iff_intro_neg (A B: wff): $ (A \iff B) \imp (\neg A \iff \neg B) $;

\neg\iff消除

theorem neg_iff_elim (A B: wff): $ (\neg A \iff \neg B) \imp (A \iff B) $;

\iff指配\neg

theorem iff_alloc_neg (A B: wff): $ (A \iff B) \iff \neg A \iff \neg B $;

\iff同时引入\imp

theorem iff_simintro_imp (A B C D: wff): $ (A \iff B) \imp (C \iff D) \imp (A \imp C \iff B \imp D) $;

\iff同时引入\or

theorem iff_simintro_or (A B C D: wff): $ (A \iff B) \imp (C \iff D) \imp (A \or C \iff B \or D) $;

\iff左引入\or

theorem iff_introl_or (A B C: wff): $ (B \iff C) \imp (A \or B \iff A \or C) $;

\iff右引入\or

theorem iff_intror_or (A B C: wff): $ (A \iff B) \imp (A \or C \iff B \or C) $;

\iff同时引入\and

theorem iff_simintro_and (A B C D: wff): $ (A \iff B) \imp (C \iff D) \imp (A \and C \iff B \and D) $;

\iff左引入\and

theorem iff_introl_and (A B C: wff): $ (B \iff C) \imp (A \and B \iff A \and C) $;

\iff右引入\and

theorem iff_intror_and (A B C: wff): $ (A \iff B) \imp (A \and C \iff B \and C) $;

\iff同时引入\iff

theorem iff_simintro_iff (A B C D: wff): $ (A \iff B) \imp (C \iff D) \imp ((A \iff C) \iff B \iff D) $;

\iff左引入\iff

theorem iff_introl_iff (A B C: wff): $ (B \iff C) \imp ((A \iff B) \iff A \iff C) $;

\iff右引入\iff

theorem iff_intror_iff (A B C: wff): $ (A \iff B) \imp ((A \iff C) \iff B \iff C) $;

\neg\iff置换

theorem neg_iff_perm (A B: wff): $ (\neg A \iff B) \iff \neg B \iff A $;

\iff\neg置换

theorem iff_neg_perm (A B: wff): $ (A \iff \neg B) \iff B \iff \neg A $;

\imp布尔等价式

theorem imp_boole_def (A B: wff): $ A \imp B \iff \neg A \or B $;

\neg\imp布尔等价式

theorem negimp_boole_def (A B: wff): $ \neg (A \imp B) \iff A \and \neg B $;

\iff布尔等价式

theorem iff_boole_def (A B: wff): $ (A \iff B) \iff \neg A \or B \and (\neg B \or A) $;

\neg\iff布尔等价式

theorem negiff_boole_def (A B: wff): $ \neg (A \iff B) \iff A \and \neg B \or (B \and \neg A) $;

\or归一

theorem or_unify (A: wff): $ A \or A \iff A $;

\and归一

theorem and_unify (A: wff): $ A \and A \iff A $;

\or交换

theorem or_comm (A B: wff): $ A \or B \iff B \or A $;

\and交换

theorem and_comm (A B: wff): $ A \and B \iff B \and A $;

\or结合

theorem or_assoc (A B C: wff): $ A \or B \or C \iff A \or (B \or C) $;

\and结合

theorem and_assoc (A B C: wff): $ A \and B \and C \iff A \and (B \and C) $;

\and\or左分配

theorem and_or_distl (A B C: wff): $ A \and (B \or C) \iff A \and B \or (A \and C) $;

\or\and右分配

theorem or_and_distr (A B C: wff): $ A \or B \and C \iff A \and C \or (B \and C) $;

\or\and左分配

theorem or_and_distl (A B C: wff): $ A \or (B \and C) \iff A \or B \and (A \or C) $;

\and\or右分配

theorem and_or_distr (A B C: wff): $ A \and B \or C \iff A \or C \and (B \or C) $;

\and\or左吸收

theorem and_or_absorbl (A B: wff): $ A \and (A \or B) \iff A $;

\or\and左吸收

theorem or_and_absorbl (A B: wff): $ A \or (A \and B) \iff A $;

\neg\or分配\and

theorem neg_or_dist_and (A B: wff): $ \neg (A \or B) \iff \neg A \and \neg B $;

\neg\and分配\or

theorem neg_and_dist_or (A B: wff): $ \neg (A \and B) \iff \neg A \or \neg B $;

二值遍历式之单个变量

theorem binary1 (A: wff): $ A \or \neg A $;

\true证明

theorem true_proof: $ \true $;

\neg\false证明

theorem negfalse_proof: $ \neg \false $;

爆炸原理

theorem explosion (A: wff): $ \false \imp A $;

\true\imp等价自身

theorem trueimp_eqv_self (A: wff): $ \true \imp A \iff A $;

\imp\false等价\neg自身

theorem impfalse_eqv_negself (A: wff): $ A \imp \false \iff \neg A $;

定理与\true等价

theorem prov_iff_true (A: wff): $ A \imp (A \iff \true) $;

否定的定理与\false等价

theorem provneg_iff_false (A: wff): $ \neg A \imp (A \iff \false) $;

真值合成

theorem true_comp (A: wff): $ A \imp \true $;

假值合成

theorem false_comp (A: wff): $ A \imp \neg A \imp \false $;

赋值为真

theorem assgin_true (A: wff): $ A \iff A \iff \true $;

赋值为假

theorem assign_false (A: wff): $ \neg A \iff A \iff \false $;

反证法

theorem proof_by_contrad (A: wff): $ (\neg A \imp \false) \imp A $;

归谬法

theorem proof_by_absurd (A: wff): $ (A \imp \false) \imp \neg A $;

排中律tf形式

theorem excluded_middle_tf (A: wff): $ (A \iff \true) \or (A \iff \false) $;

矛盾律tf形式

theorem contradiction_tf (A: wff): $ \neg ((A \iff \true) \and (A \iff \false)) $;

\neg真值表：\neg \true \iff \false

theorem neg_true_iff_false: $ \neg \true \iff \false $;

\neg真值表：\neg \false \iff \true

theorem neg_false_iff_true: $ \neg \false \iff \true $;

\imp真值表：\true \imp \true \iff \true

theorem true_imp_true_iff_true: $ \true \imp \true \iff \true $;

\imp真值表：\true \imp \false \iff \false

theorem true_imp_false_iff_false: $ \true \imp \false \iff \false $;

\imp真值表：\false \imp \true \iff \true

theorem false_imp_true_iff_true: $ \false \imp \true \iff \true $;

\imp真值表：\false \imp \false \iff \true

theorem false_imp_false_iff_true: $ \false \imp \false \iff \true $;

\imp真值表：wff \imp \true \iff \true

theorem wff_imp_true_iff_true (A: wff): $ A \imp \true \iff \true $;

\imp真值表：wff \imp \false \iff \neg wff

theorem wff_imp_false_iff_neg_wff (A: wff): $ A \imp \false \iff \neg A $;

\imp真值表：\true \imp wff \iff wff

theorem true_imp_wff_iff_wff (A: wff): $ \true \imp A \iff A $;

\imp真值表：\false \imp wff \iff \true

theorem false_imp_wff_iff_true (A: wff): $ \false \imp A \iff \true $;

\and真值表：\true \and \true \iff \true

theorem true_and_true_iff_true: $ \true \and \true \iff \true $;

\and真值表：\true \and \false \iff \false

theorem true_and_false_iff_false: $ \true \and \false \iff \false $;

\and真值表：\false \and \true \iff \false

theorem false_and_true_iff_false: $ \false \and \true \iff \false $;

\and真值表：\false \and \false \iff \false

theorem false_and_false_iff_false: $ \false \and \false \iff \false $;

\and真值表：A \and \true \iff A

theorem wff_and_true_iff_self (A: wff): $ A \and \true \iff A $;

\and真值表：wff \and \false \iff \false

theorem wff_and_false_iff_false (A: wff): $ A \and \false \iff \false $;

\and真值表：\true \and A \iff A

theorem true_and_wff_iff_self (A: wff): $ \true \and A \iff A $;

\and真值表：\false \and A \iff \false

theorem false_and_wff_iff_false (A: wff): $ \false \and A \iff \false $;

\or真值表：\true \or \true \iff \true

theorem true_or_true_iff_true: $ \true \or \true \iff \true $;

\or真值表：\true \or \false \iff \true

theorem true_or_false_iff_true: $ \true \or \false \iff \true $;

\or真值表：\false \or \true \iff \true

theorem false_or_true_iff_true: $ \false \or \true \iff \true $;

\or真值表：\false \or \false \iff \false

theorem false_or_false_iff_false: $ \false \or \false \iff \false $;

\or真值表：wff \or \true \iff \true

theorem wff_or_true_iff_true (A: wff): $ A \or \true \iff \true $;

\or真值表：wff \or \false \iff wff

theorem wff_or_false_iff_wff (A: wff): $ A \or \false \iff A $;

\or真值表：\true \or wff \iff \true

theorem true_or_wff_iff_true (A: wff): $ \true \or A \iff \true $;

\or真值表：\false \or wff \iff wff

theorem false_or_wff_iff_wff (A: wff): $ \false \or A \iff A $;

\iff真值表：(\true \iff \true) \iff \true

theorem true_iff_true_iff_true: $ (\true \iff \true) \iff \true $;

\iff真值表：(\true \iff \false) \iff \false

theorem true_iff_false_iff_false: $ (\true \iff \false) \iff \false $;

\iff真值表：(\false \iff \true) \iff \false

theorem false_iff_true_iff_false: $ (\false \iff \true) \iff \false $;

\iff真值表：(\false \iff \false) \iff \true

theorem false_iff_false_iff_true: $ (\false \iff \false) \iff \true $;

\iff真值表：(A \iff \true) \iff A

theorem wff_iff_true_iff_self (A: wff): $ (A \iff \true) \iff A $;

\iff真值表：(A \iff \false) \iff \neg A

theorem wff_iff_false_iff_negself (A: wff): $ (A \iff \false) \iff \neg A $;

\iff真值表：(\true \iff A) \iff A

theorem true_iff_wff_iff_wff (A: wff): $ (\true \iff A) \iff A $;

\iff真值表：(\false \iff A) \iff \neg

theorem false_iff_wff_iff_negself (A: wff): $ (\false \iff A) \iff \neg A $;

\fo对\imp插入

theorem fo_imp_ins {x: set} (A B: wff x): $ \fo x (A \imp B) \imp \fo x A \imp \fo x B $;

\fo引入

theorem intro_fo {x: set} (A: wff x): $ A $ > $ \fo x A $;

$\fo$ 的MP规则

theorem fomp (B: wff) {x: set} (A: wff x): $ \fo x A \imp B $ > $ A $ > $ B $;

\fo对\imp引入

theorem imp_intro_fo {x: set} (A B: wff x): $ A \imp B $ > $ \fo x A \imp \fo x B $;

\fo对\iff插入

theorem fo_iff_ins {x: set} (A B: wff x): $ \fo x (A \iff B) \imp (\fo x A \iff \fo x B) $;

\fo对\iff引入

theorem iff_intro_fo {x: set} (A B: wff x): $ A \iff B $ > $ \fo x A \iff \fo x B $;

\fo交换

theorem fo_swap {x y: set} (A: wff x y): $ \fo x \fo y A \imp \fo y \fo x A $;

\fo置换

theorem fo_perm {x y: set} (A: wff x y): $ \fo x \fo y A \iff \fo y \fo x A $;

\fo\and分配

theorem fo_and_dist {x: set} (A B: wff x): $ \fo x (A \and B) \iff \fo x A \and \fo x B $;

\ex等价\neg\fo\neg

theorem ex_eqv_negfoneg {x: set} (A: wff x): $ \ex x A \iff \neg \fo x \neg A $;

\fo等价\neg\ex\neg

theorem fo_eqv_negexneg {x: set} (A: wff x): $ \fo x A \iff \neg \ex x \neg A $;

\fo\neg等价\neg\ex

theorem foneg_eqv_negex {x: set} (A: wff x): $ \fo x \neg A \iff \neg \ex x A $;

\ex\neg等价\neg\fo

theorem exneg_eqv_negfo {x: set} (A: wff x): $ \ex x \neg A \iff \neg \fo x A $;

\ex置换

theorem ex_perm {x y: set} (A: wff x y): $ \ex x \ex y A \iff \ex y \ex x A $;

\ex交换

theorem ex_swap {x y: set} (A: wff x y): $ \ex x \ex y A \imp \ex y \ex x A $;

\fo\imp插入成\ex

theorem fo_imp_insto_ex {x: set} (A B: wff x): $ \fo x (A \imp B) \imp \ex x A \imp \ex x B $;

\imp引入\ex

theorem imp_intro_ex {x: set} (A B: wff x): $ A \imp B $ > $ \ex x A \imp \ex x B $;

\fo\iff插入\ex

theorem fo_iff_insto_ex {x: set} (A B: wff x): $ \fo x (A \iff B) \imp (\ex x A \iff \ex x B) $;

\iff引入\ex

theorem iff_intro_ex {x: set} (A B: wff x): $ A \iff B $ > $ \ex x A \iff \ex x B $;

\ex\imp分配成\fo\ex

theorem ex_imp_distto_fo_ex {x: set} (A B: wff x): $ \ex x (A \imp B) \iff \fo x A \imp \ex x B $;

\ex\and插入

theorem ex_and_ins {x: set} (A B: wff x): $ \ex x (A \and B) \imp \ex x A \and \ex x B $;

\ex\imp\fo提取成\fo

theorem ex_imp_fo_extto_fo {x: set} (A B: wff x): $ (\ex x A \imp \fo x B) \imp \fo x (A \imp B) $;

\fo\and\ex提取成\ex

theorem fo_and_ex_extto_ex {x: set} (A B: wff x): $ \fo x A \and \ex x B \imp \ex x (A \and B) $;

\ex\and\fo提取成\ex

theorem ex_and_fo_extto_ex {x: set} (A B: wff x): $ \ex x A \and \fo x B \imp \ex x (A \and B) $;

\fo\or插入成\ex

theorem fo_or_insto_fo_ex {x: set} (A B: wff x): $ \fo x (A \or B) \imp \fo x A \or \ex x B $;

\fo\or提取

theorem fo_or_ext {x: set} (A B: wff x): $ \fo x A \or \fo x B \imp \fo x (A \or B) $;

\ex\or分配

theorem ex_or_dist {x: set} (A B: wff x): $ \ex x (A \or B) \iff \ex x A \or \ex x B $;

\fo\or插入成\ex\fo

theorem fo_or_insto_ex_fo {x: set} (A B: wff x): $ \fo x (A \or B) \imp \ex x A \or \fo x B $;

\fo无关引入

theorem fo_intro_abs (A: wff) {x: set}: $ A \imp \fo x A $;

存在性公理

theorem existene {x: set} (y: set): $ \ex x x = y $;

等式公理

theorem equality (x y z: set): $ x = y \imp x = z \imp y = z $;

替换公理

theorem substitution {x: set} (y: set) (P: wff x): $ x = y \imp P \imp \fo x (x = y \imp P) $;

\fo\imp插入右侧(左侧不出现)

theorem fo_imp_insrs_absls (A: wff) {x: set} (B: wff x): $ \fo x (A \imp B) \imp A \imp \fo x B $;

\ex消除(不出现)

theorem ex_elim_abs (A: wff) {x: set}: $ \ex x A \imp A $;

\fo\imp引入左侧成\ex(右侧不出现)

theorem fo_imp_inslsto_ex_absrs (B: wff) {x: set} (A: wff x): $ \fo x (A \imp B) \imp \ex x A \imp B $;

集合等号自反性

theorem eqs_refl (x: set): $ x = x $;

集合等号对称性

theorem eqs_sym (x y: set): $ x = y \imp y = x $;

集合等号传递性

theorem eqs_tran (x y z: set): $ x = y \imp y = z \imp x = z $;

集合等号左替换性

theorem eqs_repl (x y z: set): $ x = y \imp (x = z \iff y = z) $;

集合等号右替换性

theorem eqs_repr (x y z: set): $ x = y \imp (z = x \iff z = y) $;

\ex引入

theorem ex_intro {x: set} (A: wff x): $ A \imp \ex x A $;

\fo消除

theorem fo_elim {x: set} (A: wff x): $ \fo x A \imp A $;

\fo变成\ex

theorem fo_to_ex {x: set} (A: wff x): $ \fo x A \imp \ex x A $;

\fo指配(不出现)

theorem fo_alloc_abs (A: wff) {x: set}: $ A \iff \fo x A $;

\ex指配(不出现)

theorem ex_alloc_abs (A: wff) {x: set}: $ A \iff \ex x A $;

\fo指配(可证)

theorem fo_alloc_prov {x: set} (A: wff x): $ A $ > $ A \iff \fo x A $;

\imp左侧引入\fo

theorem imp_introls_fo {x: set} (A B: wff x): $ (A \imp B) \imp \fo x A \imp B $;

\imp左侧消除\ex

theorem imp_elimls_ex {x: set} (A B: wff x): $ (\ex x A \imp B) \imp A \imp B $;

\fo对\neg\fo引入

theorem negfo_intro_fo {x: set} (A: wff x): $ \neg \fo x A \imp \fo x \neg \fo x A $;

\ex引入\fo

theorem ex_intro_fo {x: set} (A: wff x): $ \ex x A \imp \fo x \ex x A $;

\ex\fo消除为\fo

theorem exfo_elim_fo {x: set} (A: wff x): $ \ex x \fo x A \imp \fo x A $;

\nf不出现（不可引用）

theorem _nf_abs (A: wff) {x: set}: $ \nf x A $;

\nf拆解（不可引用）

theorem _nf_decomp {x: set} (A: wff x): $ \nf x A $ > $ A \imp \fo x A $;

\nf合成（不可引用）

theorem _nf_comp {x: set} (A: wff x): $ A \imp \fo x A $ > $ \nf x A $;

\iff引入\nf（不可引用）

theorem iff_intro_nf {x: set} (A B: wff x): $ A \iff B $ > $ \nf x A \iff \nf x B $;

\nf闭包\neg（不可引用）

theorem _nf_clos_neg {x: set} (A: wff x): $ \nf x A $ > $ \nf x \neg A $;

\nf闭包\imp（不可引用）

theorem _nf_clos_imp {x: set} (A B: wff x): $ \nf x A $ > $ \nf x B $ > $ \nf x (A \imp B) $;

\nf闭包\and（不可引用）

theorem _nf_clos_and {x: set} (A B: wff x): $ \nf x A $ > $ \nf x B $ > $ \nf x (A \and B) $;

\nf闭包\or（不可引用）

theorem _nf_clos_or {x: set} (A B: wff x): $ \nf x A $ > $ \nf x B $ > $ \nf x (A \or B) $;

\nf闭包\iff（不可引用）

theorem _nf_clos_iff {x: set} (A B: wff x): $ \nf x A $ > $ \nf x B $ > $ \nf x (A \iff B) $;

\nf闭包\fo不同变元（不可引用）

theorem _nf_clos_fo_difvar {x y: set} (A: wff x y): $ \nf x A $ > $ \nf x \fo y A $;

\nf闭包\ex不同变元（不可引用）

theorem _nf_clos_ex_difvar {x y: set} (A: wff x y): $ \nf x A $ > $ \nf x \ex y A $;

\nf闭包\nf不同变元（不可引用）

theorem _nf_clos_nf_difvar {x y: set} (A: wff x y): $ \nf x A $ > $ \nf x \nf y A $;

同变元\nf\ex（不可引用）

theorem _nf_ex_same {x: set} (A: wff x): $ \nf x \ex x A $;

同变元\nf\fo（不可引用）

theorem _nf_fo_same {x: set} (A: wff x): $ \nf x \fo x A $;

同变元\nf\nf（不可引用）

theorem _nf_nf_same {x: set} (A: wff x): $ \nf x \nf x A $;

\nf定理（不可引用）

theorem _nf_prov {x: set} (A: wff x): $ A $ > $ \nf x A $;

\nf\true（不可引用）

theorem _nf_true {x: set}: $ \nf x \true $;

\nf\false（不可引用）

theorem _nf_false {x: set}: $ \nf x \false $;

\fo引入(无关)

theorem fo_intro_nf {x: set} (A: wff x): $ \nf x A $ > $ A \imp \fo x A $;

\ex消除(无关)

theorem ex_elim_nf {x: set} (A: wff x): $ \nf x A $ > $ \ex x A \imp A $;

\fo指配(无关)

theorem fo_alloc_nf {x: set} (A: wff x): $ \nf x A $ > $ A \iff \fo x A $;

\ex指配(无关)

theorem ex_alloc_nf {x: set} (A: wff x): $ \nf x A $ > $ A \iff \ex x A $;

\imp右侧引入\fo(左侧无关)

theorem imp_intrors_fo_nfls {x: set} (A B: wff x): $ \nf x A $ > $ A \imp B $ > $ A \imp \fo x B $;

\imp左侧引入\ex(右侧无关)

theorem imp_introls_ex_nfrs {x: set} (A B: wff x): $ \nf x B $ > $ A \imp B $ > $ \ex x A \imp B $;

带\ex的MP规则(无关)

theorem mpex_nfrs {x: set} (A B: wff x): $ \nf x B $ > $ A \imp B $ > $ \ex x A $ > $ B $;

\ex\fo交换

theorem ex_fo_swap {x y: set} (A: wff x y): $ \ex x \fo y A \imp \fo y \ex x A $;

\fo\imp分配左侧\ex(右侧无关)

theorem fo_imp_distls_ex_nfrs {x: set} (A B: wff x): $ \nf x B $ > $ \fo x (A \imp B) \iff \ex x A \imp B $;

\fo\imp分配右侧(左侧无关)

theorem fo_imp_distrs_nfls {x: set} (A B: wff x): $ \nf x A $ > $ \fo x (A \imp B) \iff A \imp \fo x B $;

\ex\imp分配左侧\fo(右侧无关)

theorem ex_imp_distls_fo_nfrs {x: set} (A B: wff x): $ \nf x B $ > $ \ex x (A \imp B) \iff \fo x A \imp B $;

\ex\imp分配右侧(左侧无关)

theorem ex_imp_distrs_nfls {x: set} (A B: wff x): $ \nf x A $ > $ \ex x (A \imp B) \iff A \imp \ex x B $;

\fo\and分配左侧(右侧不出现)

theorem fo_and_distls_nfrs {x: set} (A B: wff x): $ \nf x B $ > $ \fo x (A \and B) \iff \fo x A \and B $;

\fo\and分配右侧(左侧不出现)

theorem fo_and_distrs_nfls {x: set} (A B: wff x): $ \nf x A $ > $ \fo x (A \and B) \iff A \and \fo x B $;

\ex\and分配左侧(右侧不出现)

theorem ex_and_distls_nfrs {x: set} (A B: wff x): $ \nf x B $ > $ \ex x (A \and B) \iff \ex x A \and B $;

\ex\and分配右侧(左侧不出现)

theorem ex_and_distrs_nfls {x: set} (A B: wff x): $ \nf x A $ > $ \ex x (A \and B) \iff A \and \ex x B $;

\fo\or分配左侧(右侧不出现)

theorem fo_or_distls_nfrs {x: set} (A B: wff x): $ \nf x B $ > $ \fo x (A \or B) \iff \fo x A \or B $;

\fo\or分配右侧(左侧不出现)

theorem fo_or_distrs_nfls {x: set} (A B: wff x): $ \nf x A $ > $ \fo x (A \or B) \iff A \or \fo x B $;

\ex\or分配左侧(右侧不出现)

theorem ex_or_distls_nfrs {x: set} (A B: wff x): $ \nf x B $ > $ \ex x (A \or B) \iff \ex x A \or B $;

\ex\or分配右侧(左侧不出现)

theorem ex_or_distrs_nfls {x: set} (A B: wff x): $ \nf x A $ > $ \ex x (A \or B) \iff A \or \ex x B $;

intro_fo的假设无关形式（不可引用）

theorem _hyp_intro_fo {x: set} (G A: wff x): $ \nf x G $ > $ G \imp A $ > $ G \imp \fo x A $;

fomp的假设无关形式（不可引用）

theorem _hyp_fomp {x: set} (G A B: wff x): $ \nf x G $ > $ G \imp \fo x A \imp B $ > $ G \imp A $ > $ G \imp B $;

imp_intro_fo的假设无关形式（不可引用）

theorem _hyp_imp_intro_fo {x: set} (G A B: wff x): $ \nf x G $ > $ G \imp A \imp B $ > $ G \imp \fo x A \imp \fo x B $;

iff_intro_fo的假设无关形式（不可引用）

theorem _hyp_iff_intro_fo {x: set} (G A B: wff x): $ \nf x G $ > $ G \imp (A \iff B) $ > $ G \imp (\fo x A \iff \fo x B) $;

imp_intro_ex的假设无关形式（不可引用）

theorem _hyp_imp_intro_ex {x: set} (G A B: wff x): $ \nf x G $ > $ G \imp A \imp B $ > $ G \imp \ex x A \imp \ex x B $;

iff_intro_ex的假设无关形式（不可引用）

theorem _hyp_iff_intro_ex {x: set} (G A B: wff x): $ \nf x G $ > $ G \imp (A \iff B) $ > $ G \imp (\ex x A \iff \ex x B) $;

fo_alloc_prov的假设无关形式（不可引用）

theorem _hyp_fo_alloc_prov {x: set} (G A: wff x): $ \nf x G $ > $ G \imp A $ > $ G \imp (A \iff \fo x A) $;

imp_intrors_fo_nfls的假设和公式无关形式（不可引用）

theorem _hyp_imp_intrors_fo_nfls {x: set} (G A B: wff x): $ \nf x G $ > $ \nf x A $ > $ G \imp A \imp B $ > $ G \imp A \imp \fo x B $;

imp_introls_ex_nfrs的假设和公式无关形式（不可引用）

theorem _hyp_imp_introls_ex_nfrs {x: set} (G A B: wff x): $ \nf x G $ > $ \nf x B $ > $ G \imp A \imp B $ > $ G \imp \ex x A \imp B $;

mpex_nfrs的假设和公式无关形式（不可引用）

theorem _hyp_mpex_nfrs {x: set} (G A B: wff x): $ \nf x G $ > $ \nf x B $ > $ G \imp A \imp B $ > $ G \imp \ex x A $ > $ G \imp B $;

对不同变量的$ \sb y x A $的定义方式。

theorem sb_def_dif {x: set} (y: set) (A: wff x): $ \sb y x A \iff \fo x (x = y \imp A) $;

全称量词可以通过代入实例消去。

theorem fo_elim_sb {x: set} (y: set) (A: wff x): $ \fo x A \imp \sb y x A $;

如果有一个集合实例满足该公式，则存在一个集合满足该公式。

theorem sb_to_ex {x: set} (y: set) (A: wff x): $ \sb y x A \imp \ex x A $;

如果A与x无关，则A与[t/x]A等价。

theorem sb_alloc_nf {x: set} (y: set) (A: wff x): $ \nf x A $ > $ A \iff \sb y x A $;

如果A可证，则A中任意变量替换后也可证。

theorem intro_sb {x: set} (y: set) (A: wff x): $ A $ > $ \sb y x A $;

intro_sb的假设无关形式。

theorem _hyp_intro_sb {x: set} (y: set) (G A: wff x): $ \nf x G $ > $ G \imp A $ > $ G \imp \sb y x A $;

替换操作对蕴涵的插入律。

theorem sb_imp_ins {x: set} (y: set) (A B: wff x): $ \sb y x (A \imp B) \imp \sb y x A \imp \sb y x B $;

替换操作对蕴涵的引入律

theorem imp_intro_sb {x: set} (y: set) (A B: wff x): $ A \imp B $ > $ \sb y x A \imp \sb y x B $;

imp_intro_sb的假设无关形式。

theorem _hyp_imp_intro_sb (G: wff) {x: set} (y: set) (A B: wff x): $ \nf x G $ > $ G \imp A \imp B $ > $ G \imp \sb y x A \imp \sb y x B $;

替换操作对等价的插入律

theorem sb_iff_ins {x: set} (y: set) (A B: wff x): $ \sb y x (A \iff B) \imp (\sb y x A \iff \sb y x B) $;

替换操作对等价的引入律

theorem iff_intro_sb {x: set} (y: set) (A B: wff x): $ A \iff B $ > $ \sb y x A \iff \sb y x B $;

iff_intro_sb的假设无关形式（不可引用）

theorem _hyp_iff_intro_sb {x: set} (y: set) (G A B: wff x): $ \nf x G $ > $ G \imp (A \iff B) $ > $ G \imp (\sb y x A \iff \sb y x B) $;

对公式A和集合变元x,y，若x=y，则将公式A中的z替换为x得到的公式与将公式A中的z替换为y得到的公式等价。

theorem eqs_to_sb_same_iff {z: set} (x y: set) (A: wff z): $ x = y \imp (\sb x z A \iff \sb y z A) $;