高阶逻辑, 此條目没有列出任何参考或来源, 2022年10月9日, 維基百科所有的內容都應該可供查證, 请协助補充可靠来源以改善这篇条目, 无法查证的內容可能會因為異議提出而移除, 在数学中, 在很多方面有别于一阶逻辑, 其一是变量类型出现在量化中, 粗略的说, 一阶逻辑中禁止量化谓词, 允许这么做的系统请参见二阶逻辑, 区别于一阶逻辑的其他方式是在构造中允许下层的类型论, 高阶谓词是接受其他谓词作为参数的谓词, 一般的, 阶为n的高阶谓词接受一个或多个, 阶的谓词作为参数, 这里的n, 对高阶函数类似的评述也成立. 此條目没有列出任何参考或来源 2022年10月9日 維基百科所有的內容都應該可供查證 请协助補充可靠来源以改善这篇条目 无法查证的內容可能會因為異議提出而移除 在数学中 高阶逻辑在很多方面有别于一阶逻辑 其一是变量类型出现在量化中 粗略的说 一阶逻辑中禁止量化谓词 允许这么做的系统请参见二阶逻辑 高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型论 高阶谓词是接受其他谓词作为参数的谓词 一般的 阶为n的高阶谓词接受一个或多个 n 1 阶的谓词作为参数 这里的n gt 1 对高阶函数类似的评述也成立 高阶逻辑更加富有表达力 但是它们的性质 特别是有关模型论的 使它们对很多应用不能表现良好 作为哥德尔的结论 经典高阶逻辑不容许 递归的公理化的 可靠的和完备的证明演算 这个缺陷可以通过使用Henkin模型来修补 高阶逻辑的一个实例是构造演算 参见 编辑高阶文法 有类型lambda演算 直觉类型论延伸阅读 编辑Alonzo Church A Formulation of the Simple Theory of Types Journal of Symbolic Logic Vol 5 1940 56 68 Leon Henkin Completeness in the theory of types Journal of Symbolic Logic Vol 15 1950 81 91 Peter B Andrews An Introduction to Mathematical Logic and Type Theory To Truth Through Proof 2nd edition Academic Press 2002 J Lambek P J Scott Introduction to Higher Order Categorical Logic Cambridge University Press 1986 外部链接 编辑A short article from the Encyclopedia of Artificial Intelligence 这是一篇與逻辑学相關的小作品 你可以通过编辑或修订扩充其内容 查论编 取自 https zh wikipedia org w index php title 高阶逻辑 amp oldid 74016721, 维基百科，wiki，书籍，书籍，图书馆，
