Abstract

理论体系不仅需要承担证明任务，还必须承担证明之外的构件管理、版本比较和整体组织等辅助角色。然而，这些角色既不能独立成为证明任务，也不能混入主式或附式之中。本文以理论体系运转过程中必然出现的非证明角色为对象，通过约束递推、最小结构证明和整体闭合证明，论证证明推进必然产生内部构件，版本演化必然产生比较任务，体系扩展必然产生组织任务，三类角色分别对应式件层、比较元式和统摄形式三个正式层位。进一步证明三层位具有必要性、独立退化性、不可合并性和整体闭合性，并与证明层共同构成完整的理论角色分工体系。本文同时指出，三层位的建立不是文体安排，而是理论可审查性、版本可维护性和体系可组织性的必要条件，为大型形式理论提供统一的层位结构。