是否有高阶逻辑的参考定义，如 HOL、Isabelle 等？答案

【问题标题】：Is there a reference definition of higher-order logic as in HOL, Isabelle, etc?是否有高阶逻辑的参考定义，如 HOL、Isabelle 等？
【发布时间】：2015-03-10 13:49:51
【问题描述】：

我正在阅读"Concrete semantics with Isabelle/HOL"，我对高阶逻辑非常感兴趣。我知道普通的一阶逻辑和一些模态逻辑，但我以前接触过高阶逻辑及其元理论的情况很少，所以我想填补空白。我读到 HOL 本质上是 Church 的简单类型理论，而 Pure 是前者的直觉主义变体。问题是“本质上”这个词：Isabelle/HOL 和 Isabelle/Pure 理论与Andrews' textbook 有何不同？是否有关于 Isabelle/HOL 和 Isabelle/Pure 中使用的高阶逻辑的教科书介绍，并讨论了它们的元理论特性？

【问题讨论】：

标签： logic isabelle

【解决方案1】：

关于 HOL 及其许多变体和方言可以说很多。这是Isabelle 和其他HOL 系统的邮件列表中经常出现的主题。例如，这是 2013 年 1 月/2 月在 isabelle-users:Where to learn about HOL vs FOL? 上的一个相关帖子，其中还引用了一些相关文献。

Isabelle/Isar Implementation 手册，2 Primitive logic部分也有一点关于 Isabelle/Pure（最小 HOL）的逻辑。。 p>

【讨论】：