| 可消去性准则 eliminability criterion 合式定义遵循的两准则之一。由波兰莱斯涅夫斯基最早表述。指一个定义出的符号，总是能从该理论的任何公式中消去。例如在形式算术理论中，加法是初始符号，通过它按下列方式定义减法符号是满足可消去性准则的：x-y=z，当且仅当，x=y+z。可以用上式，消去减号的任一出现。如据上式，就能从“如果y≠0，则x-y≠x”中消去“-”，从而得到算术上等值的语句：“如果y≠0，则x≠y+x”。定义出的符号有一特点，就是能被消去，与初始符号恰好相反。该准则可以形式地加以表述：在某一系统中引入一个新符号的一个公式S满足可消去性准则，当且仅当，如果S1是一个新符号出现的公式，就有一个该新符号在其中并不出现的公式S2，使S→(S1↔S2)能从该系统的公理和在先的定义中推得。 |