除6.1公理系统的符号外，引入
表示有限个公式的集合。
表示
间的推理关系，
为形式前提，
为形式结论，或说使用推理规则可由得。（2）形成规则
同6.1公理系统形成规则和定义。
（3）变形规则
①
② 如果
则
③ 如果
且
则
④
且
⑤
⑥ 如果
，则
⑦
且
⑧
⑨ 如果
，则
⑩
⑾ 如果
；
则
⑿
⒀ 如果
（a不在中出现）则
⒁
如果（a不在B中出现）则
⒂
是由
把其中a的某些出现替换为x而得）