⋀ 在 Isabelle 中是什么意思？答案

【问题标题】：What does ⋀ mean in Isabelle?⋀ 在 Isabelle 中是什么意思？
【发布时间】：2016-07-21 14:52:49
【问题描述】：

（这几乎是一个逻辑问题。） ⋀ 如⋀y . Py 似乎是一种占位符。它发生在使用apply (rule allI) 或apply (erule exE 之后。起初我认为这就像一个假装的∀，因为allI 是(!!x. Px) => ∀x. Px 的规则（我相信!! 在我得到这个的地方用来代表⋀）。但在某些似乎符合此规则的情况下，我似乎无法应用allI。 ⋀ 的真正含义是什么？我想知道⋀ 在不同情况下是否有不同的含义。

【问题讨论】：

标签： logic isabelle quantifiers

【解决方案1】：

⋀ 是一个通用量词，是的，但它是一个元逻辑。 IE。你用来描述你工作的逻辑的那个，包括∀。类似地，? 是元蕴涵运算符。这是伊莎贝尔元逻辑仅有的两个原语；没有否定，所以它比经典逻辑弱得多。请参阅http://isabelle.in.tum.de/coursematerial/PSV2009-1/session2/document.pdf 或https://www.cl.cam.ac.uk/teaching/1011/L21/5%20-%20Logic.pdf 了解更多信息。

【讨论】：