isabelle - 如何在 Isabelle/FOL 中定义“最多”？

Question

我正在尝试增加FOL.thy量词MOST，我打算将其定义为简单多数，即

(MOST x. P(x)) ==> card P(x) > card ~P(x).

我不确定如何修改FOL.thy文件。在下axiomatization，我想补充：

Most :: "('a => o) => o"  (binder "MOST " 10)

并且，在该where条款下：

specM: "(ALL x. P(x)) ==> (MOST x. P(x))" and
mostI: "(MOST x. P(x)) ==> ..."

其中“...”是表达上述约束的正确方式，即P(x)和的基数~P(x)。（同样，我不确定这里有一个好名字，欢迎提出建议。）

我想在“符号”部分添加一个条目，并且由于缺乏更好的想法，选择使用 delta：

Most (binder "∆" 10)

同样在该notation部分中。

1）如何正确表达基数约束？

2）我还需要修改哪些其他内容？

对于后一个问题，指出最终我想评估一些不同的结论是否是必要的、可能的或不可能的可能会有所帮助，假设前提将包括使用“大多数”和“全部”的量化断言（以及连词、析取等）。

Answer 1

除非有特殊原因，否则通常最好将 Isabelle/HOL 作为您想到的任何应用程序的起点。

FOL 或 HOL 是否更强的论点取决于额外的公理化。Isabelle/ZF 在 FOL 之上提供了完整的 Zermelo-Fraenkel 集合论，因此它比普通的 HOL 更具表现力，但它的工具和库几乎落后了 20 年。

与其从底部开始，不如从HOL.thy顶部进入理论Main，可能还有一些进一步的理论$ISABELLE_HOME/src/HOL/Library。

你的草图Most让我想起了$ISABELLE_HOME/src/HOL/Library/Infite_Set虽然那是关于更有趣的无限集。关于 HOL 中的序数和基数还有更多的理论有待发现。这取决于您的最终应用程序是什么。