形式化
运用形式语言构造形式系统的方法和程序。 目的在于使演绎系统更为严格。形式化包括四个步骤： 第一，列出初始符号。初始符号是些本身不具有任何意义的符号。在所构造的形式系统中，只出现这些符号，不出现其他符号。 第二，给出形成规则。形成规则规定，在初始符号构成的任意的符号串中，那些是系统内的合式公式(简称公式)，哪些不是。 第三，给出公理集。公理是系统内不经推导就加以断定的公式。 公理集如果是空集，相应的形式系统就称为自然推理系统。 第四，给出推导规则。 推导规则规定，系统内公式的推导，哪些是允许的，哪些是不允许的。 依据公理和推导规则断定公式的过程，称为证明。 经证明的公式，称为系统内的定理。 严格性和抽象性是形式化的两个重要特点。 一个形式系统能够在有穷步骤内断定：一个符号是否为一初始符号；一个符号序列是否为一公式；一个公式是否为一公理；一个有穷长的公式序列是否为一证明。 除此以外，形式系统不承认任何别的东西，哪怕它们在直观上多么天经地义。 形式系统的抽象性表现在它自身仅仅是个符号系统，除了表示符号间的关系外，不表示任何别的意义。但是通过解释，找到模型，它可以刻画具体的对象世界，更有意义的是，同一个形式系统，可以作出不同的解释，建立不同的模型，从而可以刻画即使表面上多么迥然不同的对象世界。 |