33证明系统 ·公理和推理规则 T,x:o ·M=N: (5 T 入x:G.M=入x:gN:o→T TM1=M2:O→TT■ N=N2:O (y) T MIN=M2N2:t T 入x:o.M=入y:gyx]M:o→T, ,其中ye FVM闪 (c) T (Ax:O.M)N=NIx M t (B) T 入x:o.(Mx)=M:o→ 其中xEFV(M) (7
3.3 证明系统 • 公理和推理规则 () () x.M = y.[y/x]M : →, 其中y FV(M) () (x.M)N =[N/x]M : () x.(Mx) =M : →, 其中x FV(M) () , x: M = N : x:.M = x:.N : → M1 = M2 : → N1 = N2 : M1 N1 = M2 N2 :
33证明系统 ·引理3.6如果TM=N:o并且T⌒T包含M和 N中所有的自由变量，那么T'M=N:o 基调Σ的类型化)理论 Σ项之间的包含上述公理的一组良类型的等式， 并且封闭于上述推理规则 ETM=N:o表示：等式I M=N:o是从 公理和E的等式可证 E的理论TE)是指：从公理和E的等式可证的等 式集合
3.3 证明系统 • 引理3.6 如果 M = N :并且包含M和 N中所有的自由变量，那么 M = N: • 基调的类型化理论 – 项之间的包含上述公理的一组良类型的等式， 并且封闭于上述推理规则 – E M = N: 表示：等式 M = N:是从 公理和E的等式可证 – E的理论Th(E)是指：从公理和E的等式可证的等 式集合
33证明系统 ,代数和简单类型化演算之间的联系 在类型化入→上可以增加代数公理，任何代数等式 可以看成入等式 - 任何一个代数证明可以在)中执行 代数证明规则(subs)不在入→中，但可以证明它是 入的导出规则 M=N [T,x:s]P=0 [T] P,Q∈Ters(∑，T [PIx]M=[O]N [T]
3.3 证明系统 • 代数和简单类型化演算之间的联系 – 在类型化→上可以增加代数公理，任何代数等式 可以看成→等式 – 任何一个代数证明可以在→中执行 – 代数证明规则(subst)不在→中，但可以证明它是 →的导出规则 P, Q Termss (, ) M = N , x : s P =Q P/xM = Q/xN
3.3证明系统 命题3.8 令E是代数基调Σ上代数项之间的一组等式，令E 是单个这样的等式。若在代数证明系统中有EE, 则把E的等式和E都看成是基调Σ上入项之间的等 式，在入证明系统中也有E E 命题3.9（守恒性） 令E是代数基调Σ上代数项之间的等式集合，并令E 是单个这样的等式。当把E的等式和E都看成是基 调Σ上入项之间的等式时，若在入证明系统中有 E E,则在该代数证明系统中也有E
3.3 证明系统 • 命题3.8 令E 是代数基调上代数项之间的一组等式，令E 是单个这样的等式。若在代数证明系统中有E E， 则把E的等式和E都看成是基调→上→项之间的等 式，在→证明系统中也有E E • 命题3.9（守恒性） 令E是代数基调上代数项之间的等式集合，并令E 是单个这样的等式。当把E的等式和E都看成是基 调→上→项之间的等式时，若在→证明系统中有 E E，则在该代数证明系统中也有E E
3.3证明系统 命题3.10 存在有类型化入演算理论E及没有·x自由出现的 项M和N,使得 E T,x:o M=N:T 但是E T M=N:t 表明等式中变量情况会影响可证明性
3.3 证明系统 • 命题3.10 存在有类型化演算理论E及没有x自由出现的 项M和N，使得 E , x: M = N : 但是E M = N : – 表明等式中变量情况会影响可证明性