模型从公理集合中导出定理集称之为理论，有了理论我们要解释它的语义必须借助某个模型(model)。因为形式系统只是符号抽象，借助模型我们可为每个常量、函数、谓词符号找到真理性的解释。即定义每个论域，并表明域上成员和常量公理之间的关系。公理的谓词符号必须派定为域中对象的性质，函数派定为对域中对象的操作。公理集合一般情况下只是定义的部分（偏）函数和谓词，是问题域的一个侧面。所以能满足该理论的模型往往不止一个
• 模型 从公理集合中导出定理集称之为理论， 有了理 论我们要解释它的语义必须借助某个模型(model)。 因为形式系统只是符号抽象，借助模型我们可为每 个常量、函数、谓词符号找到真理性的解释。 即定 义每个论域， 并表明域上成员和常量公理之间的关 系。 公理的谓词符号必须派定为域中对象的性质， 函数派定为对域中对象的操作。 公理集合一般情况下只是定义的部分(偏)函数 和谓词， 是问题域的一个侧面。 所以能满足该理论 的模型往往不止一个
例一个最简单的理论公理集：vXinterval(X)notinterval(X+l)(al)(a2)vXnot interval (X+1)interval(X)2=1+1(a3)从间隔数公理可导出定理：(t1)vXinterval (X)interval (X+2)(t2)VXinterval (X+2) → interval(X)谓词interval(间隔数）在整数域上有两个子域odd、even都能够满足间隔数理论不能证明interval(3),也不能证明notinterval(3)为真命题这就是Milbert讨论过的可判定（decidability）问题.1936年Church和Turing证实谓词演算可判定性问题是没有解的一旦我们断言interval(3）或interval(2)是真命题，我们立刻可通过演绎证明按这个理论写出的每一个谓词为真.这就是Godel和Herbrand1930年证实的谓词演算具备的完整性（completeness）
例 一个最简单的理论 公理集: Xinterval(X)→not interval (X+1) (a1) Xnot interval (X+1)→interval(X) (a2) 2=1+1 (a3) 从间隔数公理可导出定理: Xinterval (X)→interval (X+2) (t1) Xinterval (X+2) → interval(X) (t2) 谓词interval(间隔数)在整数域上有两个子域odd、even都能够满足 间隔数理论不能证明interval(3),也不能证明not interval(3)为真命题 这就是Milbert讨论过的可判定(decidability)问题.1936年Church和 Turing证实谓词演算可判定性问题是没有解的 一旦我们断言interval(3)或interval(2)是真命题,我们立刻可通过 演绎证明按这个理论写出的每一个谓词为真.这就是Godel和 Herbrand1930年证实的谓词演算具备的完整性(completeness)
证明技术从谓词演算具有完整性，理论上可证明按公理集合建立的任何理论关键是效率。如果我们从公理出发做出每一个步骤，在新的步骤上仍然要查找每一个公理，找出可能的推理。如此下去就形成一个庞大的树行公理集，每层的结点表示一个公理的语句，其深度和宽度随问题和最初给出的公理而定，一层一步骤，N层的树就是N步推理对于自动定理证明程序，只有穷举每条可能的证明步骤才能说它是完全的。穷举完所有路径马上遇到组合爆炸问题，无论是深度优先还是广度优先，百步演绎可能的路径数都是天文数字
• 证明技术 从谓词演算具有完整性， 理论上可证明按公理 集合建立的任何理论。 关键是效率。 如果我们从公理出发做出每一个 步骤， 在新的步骤上仍然要查找每一个公理，找出 可能的推理。如此下去就形成一个庞大的树行公理 集， 每层的结点表示一个公理的语句， 其深度和宽 度随问题和最初给出的公理而定， 一层一步骤， N 层的树就是N步推理。 对于自动定理证明程序， 只有穷举每条可能的证 明步骤才能说它是完全的。 穷举完所有路径马上遇 到组合爆炸问题，无论是深度优先还是广度优先， 百步演绎可能的路径数都是天文数字